Stream: Coq users

Topic: Formalization of Actuarial Mathematics in Coq


view this post on Zulip Yosuke Ito (Feb 14 2021 at 05:32):

My name is Yosuke Ito, working as an actuary at a life insurance company in Japan.
Now I am pleased to announce that I have formalized the basic part of actuarial mathematics using Coq.
https://github.com/Yosuke-Ito-345/Actuary

This package offers some basic actuarial notations and well-known formulas of annuities, life tables, premiums and reserves of life insurance.
The proofs are based on the Coq standard library, MathComp and Coquelicot.
The main result at this stage is that the prospective reserve and the retrospective reserve of an endowment life insurance coincide:

Examples.v
Theorem res_eq_pros_retro : forall (t x n : nat), x+t < ω -> t <= n -> n > 0 ->
  \V_{t & x:n} = \P_{x:n} * \s''_{x:t} - \A_{x`1:t} / \A_{x:t`1}.

This package is still at an early stage, so there is plenty of room for further development.
Notice that future updates may not be backward compatible.

Since I am new to Coq, any comment or advice is appreciated.

view this post on Zulip Guillaume Melquiond (Feb 14 2021 at 06:55):

Just a small remark. It seems you are using Rgt and Rge a lot. I would advise against it, especially for the latter. Indeed, (a >= b)%R and (b <= a)%R are not convertible, for some unfortunate historical reasons. So, in the long run, it is better to stick to the one with the more theorems, i.e., Rle. (For Rgt, the situation is less dire, since you can still use theorems about Rlt.)

view this post on Zulip Yosuke Ito (Feb 14 2021 at 07:36):

Thank you for your reply. As you point out, I used both Rgt and Rge, and often had to apply Rle_ge to convert each other. I'll stick to Rle from now on.

view this post on Zulip Yosuke Ito (Jul 24 2021 at 06:58):

I am pleased to announce that the package of formalized actuarial mathematics is updated from version 1.0 to version 2.0.
https://github.com/Yosuke-Ito-345/Actuary

In this update, the continuous payment case of insurance is formalized under the assumption that the survival function is continuously differentiable.
For more information, visit the author's GitHub website.

Be aware that some notations or lemmas are modified from version 1.0 to 2.0.
Please kindly note that future updates may not be backward compatible.

Any comment or advice is welcome.

view this post on Zulip Yosuke Ito (Nov 24 2021 at 12:13):

The other day, I delivered a presentation on the Actuary package at The 17th Theorem Proving and Provers meeting (TPP 2021) in Kitami, Japan. Now the slide is on the web, written in English. If anyone has interest, question, or comment on this project, please let me know.
https://t6s.github.io/tpp2021/

view this post on Zulip Karl Palmskog (Nov 24 2021 at 12:14):

@Yosuke Ito nice work! One thought that came across my mind on implementing actuarial software is the combination of CompCert+VST+Flocq (which can implement correct algorithms on real numbers in C). See for example this quite recent paper: https://jfr.unibo.it/article/view/11442

view this post on Zulip Karl Palmskog (Nov 24 2021 at 13:22):

I guess there are two implementation strategies for many computations on interest/premium/etc.: either use IEEE floats or fixed decimal. In C, I think one would have to use a support library for fixed decimal, but floats at least are available out of the box. With extraction to OCaml, I think the coq-bignums package has fixed decimal.

view this post on Zulip Michael Soegtrop (Nov 24 2021 at 14:11):

@Yosuke Ito : I wonder if you use some Coq formalization of probability theory, and if not how you formalize probability so that you can proof something e.g. about life table curves, which in the end express a probability.

view this post on Zulip Karl Palmskog (Nov 24 2021 at 14:51):

my understanding is that the formalization is currently probability-free, built on Coquelicot

view this post on Zulip Yosuke Ito (Nov 25 2021 at 12:26):

@Karl Palmskog Thank you for the advice. I did not know much about VST, but it looks very sophisticated and prospective. As you may have noticed, the calculation is the essential part in actuarial mathematics. (Are you familiar with this area?) I also appreciate you sharing the recent paper on VST!

view this post on Zulip Karl Palmskog (Nov 25 2021 at 12:27):

@Yosuke Ito I'm familiar with fixed-income mathematics (calculating yields on bonds and the like), which is related I guess

view this post on Zulip Karl Palmskog (Nov 25 2021 at 12:30):

@Yosuke Ito I have an example repository which shows the workflow with VST to verify a binary search function implemented in C with Coq: https://github.com/palmskog/coq-program-verification-template

If one can define some computable function in Coq related to actuarial math (e.g., calculcating some premium), then one can use this as the functional model of a C program and set up a similar workflow as in the example. When compiled with CompCert, a program verified with VST is then guaranteed to behave as the functional model.

view this post on Zulip Yosuke Ito (Nov 25 2021 at 12:36):

@Michael Soegtrop Thank you for your question. As Karl mentions, I do not use probability theory in Coq. To my knowledge, probability theory is not yet formalized. So I defined the life table (or function) axiomatically, and introduced some probabilities (such as survival rates) using that life table. In this approach, we do not need probability theory, and only easy calculations are required.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 12:40):

there are actually a bunch of different Coq formalizations of probability, the one closest to MathComp is infotheo: https://github.com/affeldt-aist/infotheo
... but it has only discrete random variables, to my knowledge. Some other options are discussed here: https://coq.discourse.group/t/finite-discrete-probabilities-in-coq/166/9

That's not to say the axiomatization in Actuary needs to be replaced, but maybe one could show that axioms could be implemented/realized by some Coq probability library for extra assurance.

view this post on Zulip Yosuke Ito (Nov 25 2021 at 12:44):

@Karl Palmskog Thanks, Karl. It looks amazing (if I understand your explanation correctly). Does it extract functions in Coq to verified C source codes?

view this post on Zulip Karl Palmskog (Nov 25 2021 at 12:46):

if you mean the VST example, you basically do the inverse of extraction. You first write the C code in a separate file, then you run clightgen on that C file to generate a Coq file. This Coq file contains the Coq representation of the C program, which is what you verify with VST inside Coq. If you look in the README file in my repository, I go through each file and what it means.

view this post on Zulip Yosuke Ito (Nov 25 2021 at 12:51):

@Karl Palmskog Thanks. I think I correctly understand. Actually my Master thesis is pure mathematics (algebra), and I am not so familiar with software development (but I studied C myself really hard).

view this post on Zulip Yosuke Ito (Nov 25 2021 at 12:53):

@Karl Palmskog Thank you also sharing probability theory in Coq. I knew infotheo, but I did not know the other.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 12:57):

C is unfortunately not an easy language to program in or specify properties of. Verification with VST tends to take a lot of time. Extraction to OCaml is easier, but hard to get good performance sometimes, and harder to integrate with other systems usually.

view this post on Zulip Yosuke Ito (Nov 25 2021 at 12:59):

@Karl Palmskog And I also agree that the axioms of life table should be guaranteed by probability distribution function.
Actuarial mathematics is known to be elegantly formalized by probability theory. I vaguely think that I will be able to construct beautiful package of actuarial mathematics when MathComp-Analysis is completed.

view this post on Zulip Yosuke Ito (Nov 25 2021 at 13:00):

Sorry for late response. English is very difficult language for us Japanese! (^^;

view this post on Zulip Yosuke Ito (Nov 25 2021 at 13:06):

@Karl Palmskog Thanks for teaching me some weak points in VST. In general, applying proof assistants in business seems not yet easy, but personally it is very worth researching and prospective.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 13:06):

@Yosuke Ito but in the actuarial software you use, do you know if you have fixed precision or floating point numbers? Do you always compute with precision of, say, 5 decimals, so the result is 0.54556 or 0.23456, in some value you want? Or does your program actually provide different numbers of decimals depending on the situation, and you know that the error is within some bound? (for example, 0.53455666 sometimes, other times 0.667)

view this post on Zulip Yosuke Ito (Nov 25 2021 at 13:08):

@Karl Palmskog Whether we use floating point or fixed precision depends on the situation, I think.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 13:08):

ah OK

view this post on Zulip Yosuke Ito (Nov 25 2021 at 13:10):

If we rigidly compute premiums and register them into the host computer, I think the premium rates have fixed points.

view this post on Zulip Yosuke Ito (Nov 25 2021 at 13:11):

But we also use ExcelVBA in some calculations, in which case floating points seems to be popular.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 13:16):

I see. As mentioned above, Coq has support for both fixed precision in bignums and then has floats in Flocq, which can be used in VST and extracted code. But the ideal might be to compute with constructive real numbers inside Coq, like they do in CoRN: https://github.com/coq-community/corn -- however, then I guess actuaries would have to learn Coq, which is probably not feasible.

view this post on Zulip Yosuke Ito (Nov 25 2021 at 13:16):

I know a well-known actuarial software called MG-ALFA by Milliman. However, I have never used such softwares, and do not know what kind of data types are used. Maybe I will ask some coworkers later.

view this post on Zulip Yosuke Ito (Nov 25 2021 at 13:18):

@Karl Palmskog Yeah, I introduced Coq to the audience in Japanese annual conference of actuaries, but few of them seem to start studying Coq. (^^;

view this post on Zulip Yosuke Ito (Nov 25 2021 at 13:19):

My goal was to let them know proof assistants. Coq is very strong software but seems unpopular in Japan.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 13:21):

I think Coq is probably more popular than Isabelle or Lean in Japan, right? Maybe partly due to Reynald (Affeldt) and Jacques (Garrigue)

view this post on Zulip Karl Palmskog (Nov 25 2021 at 13:22):

@Yosuke Ito just to check, are you aware of the Interval Coq plugin/tactic for reasoning about real numbers? To do advanced examples using Actuary, one probably needs that kind of automation. See for example this topic where Interval worked well.

view this post on Zulip Yosuke Ito (Nov 25 2021 at 13:23):

That's right. I learned Coq at Nagoya university from Jacques Garrigue. But few SEs in Japan know even the name of Coq.

view this post on Zulip Yosuke Ito (Nov 25 2021 at 13:28):

@Karl Palmskog Thanks. I know Interval. I think it also is a good candidate for application. There are many ways to calculate real numbers, so I may have to do trial and error.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 13:30):

@Yosuke Ito most SwEngs don't know about Coq, even outside of Japan :-)

view this post on Zulip Karl Palmskog (Nov 25 2021 at 13:32):

@Paolo Giarrusso it may be more interesting to talk about formal methods awareness. Europe seems to be the formal methods center of the world currently, and has been for some time. A few years ago, a US professor estimated FM professionals to number in thousands in Europe vs. a few hundreds in the US. Probably this ratio has not changed much.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 13:34):

That's a very interesting and broader discussion... is that including or excluding academics?

view this post on Zulip Karl Palmskog (Nov 25 2021 at 13:35):

https://www.cs.utexas.edu/~hunt/talks/2017-jason.pdf#page=20

view this post on Zulip Reynald Affeldt (Nov 25 2021 at 13:36):

Karl Palmskog said:

I think Coq is probably more popular than Isabelle or Lean in Japan, right?

I think we can say so based on the contents of domestic PL workshops and classes taught in CS departments.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 13:38):

we were hoping to measure the Japanese Coq user base by translating our in-progress Coq survey when it's done.

view this post on Zulip Michael Soegtrop (Nov 25 2021 at 13:44):

@Yosuke Ito : thank you for the details!

Btw.: the tools you need for verification of C code (VST, ...) are included in Coq Platform, but please note that you need the front end of CompCert (called clightgen) which converts C to something Coq can read. Clightgen is not free software, but you can use it for evaluation and research purposes.

view this post on Zulip Yosuke Ito (Nov 27 2021 at 00:17):

@Karl Palmskog I asked my coworker about the datatypes of MG-ALFA (an actuarial software). He says, the final result has the fixed number of decimals (it is 6, since the unit is one million), but in the intermediate value there must be more accuracy. From his answer, I'm not sure which datatypes are used. Actually, he seemed not to know in detail about the datatypes. To get the correct answer, maybe I have to look up the reference of MG-ALFA. But I'm not sure it is open to public.

view this post on Zulip Yosuke Ito (Nov 27 2021 at 00:20):

@Paolo Giarrusso Oh, that's a pity. In my understanding, proof assistants are only used when strong security is needed such as military system, space development, etc.

view this post on Zulip Yosuke Ito (Nov 27 2021 at 00:22):

@Michael Soegtrop Thank you for the advice! I did not know that Clightgen is not free.

view this post on Zulip Karl Palmskog (Nov 27 2021 at 00:26):

the final result has the fixed number of decimals (it is 6, since the unit is one million), but in the intermediate value there must be more accuracy.

OK, so then CompCert+VST+Flocq and IEEE floats probably make the most sense if one wants to verify actuarial software. You could still present the answer with a fixed number of decimals, and then you prove that this is the truncation of a float that has a more exact correct answer.

view this post on Zulip Karl Palmskog (Nov 27 2021 at 00:30):

In my understanding, proof assistants are only used when strong security is needed such as military system, space development, etc.

Proof assistants are popular at the moment for verifying software and protocols related to blockchains and cryptocurrency (Bitcoin, Ethereum, ...). Quite a few proof assistant researchers are indirectly or directly funded from blockchain related research grants.

view this post on Zulip Yosuke Ito (Nov 27 2021 at 01:17):

@Karl Palmskog Thank you for your suggestion. I would like to introduce your method in my paper to be in the annual proceeding of the Institute of Actuaries of Japan.
Also, thanks for letting me know the current application around blockchains. Maybe I have heard of it, but I did not know that there are proof assistants researchers who are funded in that area.

view this post on Zulip Yosuke Ito (Nov 27 2021 at 01:20):

By the way, one of the most direct application may be to check the correctness of the problems in the exam of life insurance mathematics. The other day I uploaded an example (Section Example4) in Examples.v in the Actuary package.

view this post on Zulip Karl Palmskog (Nov 27 2021 at 01:24):

well, it's not much of a method yet if there is no example, but it's probably nice to mention as a direction for future work. You can see some benchmark examples of floating point verification using VST here: https://github.com/cverified/cbench-vst

For proper demonstration, one would need to implement some actuarial function as a C program that is in, say, MG-ALFA, and verify it using the VST methodology.

view this post on Zulip Yosuke Ito (Nov 27 2021 at 01:29):

To be honest, the Actuary package now can deal with very limited area of life insurance mathematics. Some fatal problems are (1) the improper integrals are not well formalized in Coq, (2) if there are some singular points (not differentiable) in the life function, the lemmas in the Actuary package cannot manage it. (1) would be solved by MathComp-Analysis, but (2) may not be solved soon.
I have to admit that analysis is well formalized in Isabelle, so I'm now currently trying to formalize actuarial mathematics in Isabelle. When MathComp-Analysis is released, then it may be possible to translate Isabelle formalization into Coq.

view this post on Zulip Karl Palmskog (Nov 27 2021 at 01:33):

well, MathComp Analysis does have recent releases (e.g., https://github.com/math-comp/analysis/releases/tag/0.3.11), but I guess you are talking about some recent extension on improper integrals that has not been part of a release?

view this post on Zulip Yosuke Ito (Nov 27 2021 at 01:34):

@Karl Palmskog Yes, I agree that this kind of calculation should be future direction of development. I hope there are some actuaries who are familiar with this area. I also thank for sharing the link of the benchmark examples of VST.

view this post on Zulip Karl Palmskog (Nov 27 2021 at 01:35):

Isabelle also has more extensive probability theory, I believe (Borel sets, continuous random variables, ...)

view this post on Zulip Yosuke Ito (Nov 27 2021 at 01:39):

@Karl Palmskog Sorry, I do not see the detail of MathComp-Analysis, but I know that the monotone convergence theorem has recently formalized. I think probability theory will be formalized some years later, so for the time being I may try Isabelle.

view this post on Zulip Yosuke Ito (Nov 27 2021 at 01:41):

Isabelle goes ahead in formalizing mathematics, I think. But I like Coq too, because the theory of Coq itself is very clear (but it's just my impression).

view this post on Zulip Karl Palmskog (Nov 27 2021 at 01:43):

I personally use the HOL4 proof assistant that also has quite a lot of analysis and probability theory (maybe not as much as Isabelle). HOL4 has a verified compiler called CakeML with floating point support that can compile HOL4 functions to machine code: https://cakeml.org

So there may be many choices for the verification approach.

view this post on Zulip Yosuke Ito (Nov 27 2021 at 01:44):

Coq also has strength in extracting reliable codes. Isabelle has code generators, but to my knowledge, the generated code is not formally verified in default.

view this post on Zulip Yosuke Ito (Nov 27 2021 at 01:46):

@Karl Palmskog Thanks! HOL series are also a prospective choice, I think. I agree that there are some choices for which proof assistants we should use.

view this post on Zulip Karl Palmskog (Nov 27 2021 at 01:46):

Coq extraction to OCaml has similar reliability to Isabelle code generators, I think. CompCert+VST has higher reliability, but is more difficult to use. They are working on a compiler from Coq to machine code, but there are to my knowledge still gaps in the correctness proof: https://certicoq.org/

view this post on Zulip Karl Palmskog (Nov 27 2021 at 01:49):

I may have mentioned before, but I try to track the most useful and mature Coq libraries and tools here: https://github.com/coq-community/awesome-coq

view this post on Zulip Yosuke Ito (Nov 27 2021 at 01:59):

Oh, I did not know CertiCoq, thanks. I started studying Coq seriously last year and attended virtually various kinds of seminars overseas, but there are too many studies of proof assistants to follow. \(^o^)/
So sharing your knowledge helps me a lot.
It is sad for me that seminars in Europe will not be broadcasted by zoom next year. I cannot fully understand the contents of lectures, but they helped me know the current progress in formal verification.
And also for improving my English listening skills. (^ ^;

view this post on Zulip Karl Palmskog (Nov 27 2021 at 02:05):

There may be some seminars on Zoom next year as well, I guess we will see. In the meantime, in terms of knowledge sharing, maybe you will find useful a survey that I wrote with some collaborators about proof assistant verification of software: https://arxiv.org/abs/2003.06458

view this post on Zulip Yosuke Ito (Nov 27 2021 at 13:07):

@Karl Palmskog Oh, this survey is awesome...! Searching the history of proof assistants is quite hard for me. This survey covers most of the area I want to know. Maybe I will mention this survey on my paper. (^ ^)

view this post on Zulip Karl Palmskog (Nov 27 2021 at 13:09):

if you want to cite some specific paper mentioned in the survey, we have a BiBTeX bibliography here, which I try to maintain but haven't touched so much lately: https://github.com/proofengineering/proofengineering-bib/

view this post on Zulip Yosuke Ito (Nov 28 2021 at 01:05):

@Karl Palmskog Thanks! I didn't know this kind of repository. I sometimes struggle to make an entry in my BiBTeX bibliography, so I will check this page when I'm in trouble.

view this post on Zulip Karl Palmskog (Nov 28 2021 at 12:51):

the main use is probably that we hunted down a lot of DOIs (canonical identifying numbers) of proof assistant papers. So for example if the DOI is 10.1007/3-540-48167-2_3, you can see the paper at https://doi.org/10.1007/3-540-48167-2_3 (or you can use SciHub, of course...)

view this post on Zulip Yosuke Ito (Nov 28 2021 at 23:51):

@Karl Palmskog Oh, thanks for telling me how to use it. For me, it is interesting to see experts' real BiBTeX file. (^^)

view this post on Zulip Yosuke Ito (Jun 07 2022 at 12:45):

@Karl Palmskog I slightly updated the Actuary package and tagged v.2.3.
https://github.com/Yosuke-Ito-345/Actuary/releases/tag/v2.3
I'd also like to update the opam archive of Coq, but I'm not sure how to do it. Should I follow the instructions of Clone the repository and Update the repository in the following website?
https://coq.inria.fr/opam-packaging.html

view this post on Zulip Karl Palmskog (Jun 07 2022 at 12:53):

@Yosuke Ito yes, if you want to do the packaging yourself you need to fork this repo to your GitHub account: https://github.com/coq/opam-coq-archive

Then you need to clone the GitHub repo from your account to your machine. Then I suggest you create a branch called add-actuary-2.3. In this branch, you need to add the file: released/packages/coq-actuary/coq-actuary.2.3/opam (compare to here: https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-actuary/coq-actuary.2.2)

Then you need to fill the file with the new information but base it on the file for 2.2, in particular, you should now have:

url {
  src: "https://github.com/Yosuke-Ito-345/Actuary/archive/v2.3.tar.gz"
  checksum: "sha512=<result of: sha256sum v2.3.tar.gz>"
}

view this post on Zulip Karl Palmskog (Jun 07 2022 at 12:54):

after you have committed and pushed the branch with the new opam file, you should open a pull request based on your branch.

view this post on Zulip Karl Palmskog (Jun 07 2022 at 12:55):

don't worry too much in getting everything exactly right, since I can edit the content of your pull request

view this post on Zulip Karl Palmskog (Jun 07 2022 at 12:56):

I recommend taking a look at my old pull request for actuary 2.2 to see the idea:https://github.com/coq/opam-coq-archive/pull/1998 (click on "Files changed")

view this post on Zulip Yosuke Ito (Jun 08 2022 at 10:55):

@Karl Palmskog Thank you very much for the kind instruction! OK, I'll try a pull request later.

view this post on Zulip Yosuke Ito (Jun 08 2022 at 13:39):

@Karl Palmskog I've just sent the pull request to add coq-actuary v2.3. It was a little difficult for me, but I hope it went well. If I have any mistake, please let me know.


Last updated: Jan 29 2023 at 03:28 UTC