Formalizing Life Table in Isabelle/HOL
Yosuke ITO
Sompo Himawari Life Insurance Inc.

The 19th Theorem Proving and Provers meeting (TPP 2023)
October 31st, 2023

Yosuke ITO (Sompo Himawari Life)

Formalizing Life TableOct. 31st, 2023

1 / 39

Disclaimer

123

The contents presented here are solely the speaker’s opinions and do
not reflect the views of Company.
There are some inaccuracies in explaining actuarial mathematics dueto the priority on intuitive understanding.
This presentation is a progress report on the library “ActuarialMathematics” in the Archive of Formal Proofs of Isabelle. The futureversion might be different from the one presented below.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

2 / 39Self Introduction
Professional Experience• Sompo Himawari Life Insurance Inc., December 2020 – Present.
I

Aggregates the business results of life insurance products.

• Meiji Yasuda Life Insurance Company, April 2014 – November 2020.
I Revised the reinsurance contracts.
I Determined the prices of life insurance products.
I Attended the approval negotiations with Financial Services Agency.
I Qualified as an actuary (Fellow of the Institute of Actuaries of Japan).
I Aggregated the business results of group life insurance.
I Calculated retirement benefit obligations of client enterprises.
I Validated the financial soundness of Employees’ Pension Plans.

Education• Nagoya University
I

Master of Mathematical Sciences, March 2014.

• The University of Tokyo
I Bachelor of Science, Mathematics Course, March 2012.
Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

3 / 39

Contents

1

Life Table

2

Actuarial Mathematics

3

Formalizing Life Table and Survival Model

4

Newly Formalized Lemmas

5Future Works and Applications

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

4 / 39

Contents

1Life Table

2

Actuarial Mathematics

3

Formalizing Life Table and Survival Model

4

Newly Formalized Lemmas

5

Future Works and Applications

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

5 / 39What Is Life Table? I

1

2

3

A life table, a.k.a. mortality table, “shows the rate of deaths occurringin a defined population during a selected time interval, or survival
rates from birth to death” [2].
A life table depends on its statistical population; we choose anappropriate life table on a case-by-case basis.
For example, the Ministry of Health, Labour and Welfare producesLife Tables of the people in Japan.
I

The 23rd Complete Life Table (2020)
https://www.mhlw.go.jp/toukei/saikin/hw/life/23th/

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

6 / 39What Is Life Table? II1

In life tables, the following symbols are generally used:lx , the number of people alive at age x;
d , the number of deaths between ages x and x + n; dx := 1 dx ;I n px , the probability that a person aged x lives for another n years;
In qx , the probability that a person aged x dies within n years; qx = 1 qx ;I µ , the force (instantaneous rate) of mortality at age x;x
I T , the person-years lived above age x;
x
In Lx , the person-years lived for n years from age x; Lx := 1 Lx ;I e̊x , the complete expectation of life at age x; e̊0 is the average longevity.
II n x

2These symbols and relevant formulas are important in actuarial
mathematics, e.g.
n px = lx+n /lx ,n qx = n dx /lx ,Z ∞1 dlx,
Tx =lx+t dt,
lx dx
0Z ∞
Z
1 ∞
e̊x =tlx+t µx+t dt.
t px dt =lx 00µx = −Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

7 / 39

Contribution
I updated the entry “Actuarial Mathematics” in the AFP (Archive ofFormal Proofs) compatible with Isabelle2023.
https://www.isa-afp.org/entries/Actuarial_Mathematics.html
123Formalized the theory of the life table in Isabelle/HOL based on themeasure-theoretic probability theory.
Showed some practical applications: verifying examination problems inlife insurance mathematics.
Newly formalized missing important theorems in analysis andprobability theory.

The formalization is mainly based on the online document “A Reading ofthe Theory of Life Contingency” by Marcel B. Finan [1], but not the same.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

8 / 39

Contents

1

Life Table

2

Actuarial Mathematics

3

Formalizing Life Table and Survival Model

4

Newly Formalized Lemmas

5

Future Works and Applications

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

9 / 39What Is Actuarial Mathematics?
1

2Actuarial mathematics is a branch of applied mathematics, which isused to evaluate financial risks of undesirable events.
It is related tocalculus,
probability theory,
I statistics,
I financial theory.
II

3

The traditional actuarial roles are considered asII

4determining the prices of insurance products,
estimating the liability of a company associating with the insurance
contracts.

Recently, the risk management skill of actuaries is required in a wider
range of businesses.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

10 / 39

Pricing a Term Life Insurance I“Term life insurance provides a death benefit that pays the beneficiaries ofthe policyholder throughout a specified period of time” [2].

Assumption
12345

amount insured: $10000
entry age: 30 years oldpolicy period: 1 year
annual mortality rate: 1%
annual interest rate: 2%

The expected payment after 1 year is $10000 × 1% = $100.
If the insurance company earns a 2% investment yield annually, therequired amount for this insurance can be discounted:$100≈ $98.
1 + 2%Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

11 / 39

Pricing a Term Life Insurance IIDefinition

The present value of a term life insurance on a person aged x payable at1
the end of the year of death within n years is written as Ax:nper unit
insurance amount:nX
k−1 px · qx+k−1
1Ax:n :=,(1 + i)kk=1

where i denotes the annual interest rate.
1
In the example above, A30:1≈ 0.0098.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

12 / 39

International Actuarial Notation I
There are various actuarial symbols used worldwide since at least 20th
century [3, Perryman 1949].

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

13 / 39

International Actuarial Notation II1

In life insurance mathematics, the relations between the actuarial
symbols are well examined, e.g.
Ax:n = 1 − d äx:n ,
where
11+i
d := 1 − v
v :=äx:n :=n−1X(the present value of 1 to be paid 1 year from now),(the annual effective discount rate),
k px vk(the present value of a life annuity due),

k=0
1 + p vn
Ax:n := Ax:nn x2(the present value of an endowment).

Actuaries use these symbols and formulas efficiently to calculate prices
of products, reserves of the company, etc.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

14 / 39Contents

1Life Table

2Actuarial Mathematics

3Formalizing Life Table and Survival Model

4

Newly Formalized Lemmas

5Future Works and Applications

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

15 / 39

Properties of Life Table
Graph of lx of the 23rd Male Complete Life Table (continuous line) [4]:12limx→∞ lx = 0.

lx is non-increasing.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

16 / 39

Life Table to Tail Distribution
Definition (Life Table)
A life table is a function l : R → R which satisfies all the following
properties:
1
2
3l0 > 0,lx = l0 for all x < 0,limx→∞ lx = 0,4

l is non-increasing,5

l is right-continuous.

F (x) := lx /l0 becomes the tail distribution of a random variable X :F (x) = P(X > x).
X is nothing other than the age at death. In survival analysis, the taildistribution is also called the survival function.
Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

17 / 39

Survival Model
1

When X is a random variable representing the age at death, actuarialstatistics can be written as follows:n px = P(X > x + n | X > x),n qx = P(x < X ≤ x + n | X > x),P(x < X ≤ x + h | X > x),h→+0hµx = lim
2e̊0 = E [X ].

Therefore, the life table can be formalized in the following order.
Survival Model. Introduce the age-at-death random variable X , anddefine actuarial statistics in the context of probability theory. Many
important formulas are proved without a life table.
Life Table. Define a life table axiomatically, and reduce it to thesurvival model. Formulas including the life table are derived byeasy translation from the survival model.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

18 / 39

Overview of the AFP Entry “Actuarial Mathematics”

1
2

Theories are developed as generally as possible.
This seems to be the first Bourbaki-Style formulation of actuarial
mathematics (still developing).

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

19 / 39

Implementation of Survival Model and Life TableThe survival model and the life table are formalized by using locale.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

20 / 39

Applications I
You can verify examination problems and solutions of life contingencies.

Question (MCQ No.3 of Exam LTAM, SoA, Spring 2022)
You are given the following survival function for a newborn:
S0 (x) = (1 − 0.01x)0.5 ,0 ≤ x ≤ 100.

Calculate 1000µ25 .

Answer
6.7.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

21 / 39

Applications II
Question (No.2-1-1 of Life Insurance Math, IAJ, 2016; my translation)
Suppose e̊x = ax + b for 0 ≤ x ≤ −b/a, where a (−1 < a < 0) and b are
constants independent of x. Find lx .

Answerlx = l0 ·

bax+b(a+1)/a.

There are some implicit assumptions (highlighted in yellow) in exam
problems.
Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

22 / 39

Contents

1

Life Table

2

Actuarial Mathematics

3

Formalizing Life Table and Survival Model

4

Newly Formalized Lemmas

5

Future Works and Applications

Yosuke ITO (Sompo Himawari Life)

Formalizing Life TableOct. 31st, 2023

23 / 39

Interchange of Differentiation and Lebesgue Integration
TheoremLet Ω be a measure space and a, b be real numbers. Supposef : (a, b) × Ω → R and g : Ω → R satisfy the following conditions:f (r , x) is an integrable function of x ∈ Ω for each r ∈ (a, b),for almost all x ∈ Ω, the partial derivative fr (r , x) exists for allr ∈ (a, b),
3 g is an integrable function,
4 for almost all x ∈ Ω, we have |f (r , x)| ≤ g(x) for all r ∈ (a, b).
rRRdThen we have dr Ω f (r , x) dx = Ω fr (r , x) dx for all r ∈ (a, b).
12

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

24 / 39

Tail Expectation FormulaTheorem

Let X : Ω → R be a random variable, and define F (u) := P(X ≤ u). If X
R∞
R0
is integrable on Ω, we have E [X ] = 0 (1 − F (u)) du − −∞ F (u) du.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

25 / 39

Conditional Probability Space
Definition (Conditional Probability Space)
Let M := (Ω, F, P) be a probability space, and suppose A ∈ F satisfies
P(A) > 0. If we define123

FA := {C ∩ A | C ∈ F },PA (B) := P(B | A) for B ∈ FA ,M  A := (A, FA , PA ),then M  A becomes the probability space.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

26 / 39Complementary Cumulative Distribution Function
Definition (Complementary Cumulative Distribution Function)
For a random variable X , define F (x) := P(X > x) for x ∈ R. Thefunction F is called the complementary cumulative distribution function orthe tail distribution.

Lemma
In any probability space, we have F (x) + F (x) = 1.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

27 / 39

Hazard Rate
Definition (Hazard Rate [2])• The hazard rate refers to the rate of death for an item of a given age(x).

• The hazard rate for any time can be determined using the following

equation:h(t) = f (t)/R(t)F (t) [sic] is the probability density function (PDF), ... . R(t), on theother hand, represents the survival function, ... .

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

28 / 39

Contents

1Life Table

2Actuarial Mathematics

3

Formalizing Life Table and Survival Model

4

Newly Formalized Lemmas

5

Future Works and Applications

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

29 / 39

Future Works

123

Upgrade the theory of the life table.
Formalize the remaining part of actuarial mathematics inIsabelle/HOL: the pricing model, the evaluation model, etc.
Give the probabilistic foundation to the previous work coq-actuary:https://github.com/Yosuke-Ito-345/Actuary

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

30 / 39

Future Applications

12

3

Prevent errors in examination papers of actuarial mathematics.
Detect errors in actuarial documents, e.g. statement of calculation
procedures.
Formally verify programs in actuarial software, e.g. MG-ALFA.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

31 / 39References[1] Marcel B. Finan.
A reading of the theory of life contingency models: A preparation for exam MLC/3L.
https://faculty.atu.edu/mfinan/actuarieshall/mlcbook2.pdf, 2011.
[2] Investopedia.
Dictionary.
https://www.investopedia.com/financial-term-dictionary-4769738, 2023.
[3] Francis S. Perryman.
International actuarial notation.
In Proceedings of the Casualty Actuarial Society, Vol. 36, pp. 123–131, 1949.
Also available as https://www.casact.org/sites/default/files/database/proceed_proceed49_49123.pdf.
[4] 厚生労働省.
第 23 回生命表（完全生命表）の概況.
https://www.mhlw.go.jp/toukei/saikin/hw/life/23th/dl/23th-11.pdf, 2022.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

32 / 39

Q&AAny Questions?
(English Available)

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

33 / 39

Contents

6Appendix

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

34 / 39

Life Tables in JapanThe Ministry of Health, Labour and Welfare produces 2 kinds of Life
Tables in Japan.
12Complete Life Tables are made every 5 years based on the Annual
Vital Statistics and the Population Census.
Abridged Life Tables are made every year based on the Provisional
Annual Vital Statistics and the Population Estimates.

https://www.mhlw.go.jp/english/database/db-hw/vs02.html

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

35 / 39

Specific Life Tables
Definition (Smooth Life Table)
A life table l is smooth when12

l is continuous, andthere exists a finite subset S ⊆ R such that l is differentiable on R \ S.

Definition (Finite Life Table)
A life table l is finite when lx = 0 for some x.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

36 / 39

Examples of Survival Model
De Moivre’s Law: s(x) = 1 − ωx , 0 ≤ x ≤ ω.
1OωxConstant Force Model: s(x) = e −µx , 0 ≤ x.
1x

O
Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

37 / 39

Ultimate AgeDefinition

Let s be a survival function.
12Define ψ := inf{x ∈ R | s(x) = 0}. This is my original notation.
When s is finite, define ω := min{x ∈ N | s(x) = 0}. This notation isinternationally used.

ω−1
Yosuke ITO (Sompo Himawari Life)

ψFormalizing Life TableωOct. 31st, 2023

38 / 39Extension of Almost-Everywhere-Defined Function

In measure theory, we often extend an almost-everywhere-defined function
to a measurable total function. I coined the function measurize toformalize this operation.

Yosuke ITO (Sompo Himawari Life)

Formalizing Life Table

Oct. 31st, 2023

39 / 39