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.

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`

.)

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.

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.

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/

@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

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.

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

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

@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!

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

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

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

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.

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

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.

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

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

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.

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

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

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

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

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

ah OK

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

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

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.

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.

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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.

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.

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

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.

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.

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.

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?

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

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

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

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

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.

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.

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

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/

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

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

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

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

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/

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

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

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

@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

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

after you have committed and pushed the branch with the new `opam`

file, you should open a pull request based on your branch.

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

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

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

@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