Formalization of Actuarial Mathematics in Coq · Coq users

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.

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.)

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.

Yosuke Ito (Jul 24 2021 at 06:58):

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.

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/

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

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.

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.

Karl Palmskog (Nov 24 2021 at 14:51):

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

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!

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

Karl Palmskog (Nov 25 2021 at 12:30):

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.

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.

Karl Palmskog (Nov 25 2021 at 12:40):

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.

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?

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.

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).

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.

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.

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.

Yosuke Ito (Nov 25 2021 at 13:00):

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

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.

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)

Yosuke Ito (Nov 25 2021 at 13:08):

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

Karl Palmskog (Nov 25 2021 at 13:08):

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.

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.

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.

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.

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. (^^;

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.

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)

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.

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.

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.

Paolo Giarrusso (Nov 25 2021 at 13:30):

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.

Paolo Giarrusso (Nov 25 2021 at 13:34):

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

Karl Palmskog (Nov 25 2021 at 13:35):

Reynald Affeldt (Nov 25 2021 at 13:36):

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

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.

Michael Soegtrop (Nov 25 2021 at 13:44):

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.

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.

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.

Yosuke Ito (Nov 27 2021 at 00:22):

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

Karl Palmskog (Nov 27 2021 at 00:26):

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.

Karl Palmskog (Nov 27 2021 at 00:30):

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.

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.

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.

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.

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.

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?

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.

Karl Palmskog (Nov 27 2021 at 01:35):

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

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.

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).

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

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.

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.

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/

Karl Palmskog (Nov 27 2021 at 01:49):

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. (^ ^;

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

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. (^ ^)

Karl Palmskog (Nov 27 2021 at 13:09):

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.

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...)

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. (^^)

Yosuke Ito (Jun 07 2022 at 12:45):

Karl Palmskog (Jun 07 2022 at 12:53):

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>"
}

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.

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

Karl Palmskog (Jun 07 2022 at 12:56):

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.

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.

Stream: Coq users

Topic: Formalization of Actuarial Mathematics in Coq

Yosuke Ito (Feb 14 2021 at 05:32):