TPP2024 Program

Monday, November 25

12:50-13:00: Opening

13:00-14:00

A Kernel of Truth (Invited talk) (slides)

Pierre-Marie Pédrot (INRIA Atlantique)

In this talk we will dive into the innards of a proof assistant based on type theory. We will focus more precisely on the technical constraints that this foundational setting generates, notably about the importance of computation at large. Contrarily to the dry and out-of-fashion feeling that this kind of topic may convey, it actually is a lively research area with many consequences, both for design and usage of such software.

14:15-16:10

Formalizing Premium Calculation of Life Insurance (30mn) (slides)

Yosuke Ito (Sompo Himawari Life Insurance Inc.)

Calculating premiums of life insurance is not an easy task. It requires mortality rates, interest rates, and future projections. The area of numerical analysis of insurance is called actuarial science. I report the ongoing work of formalization of life insurance mathematics, which is the life insurance part of the actuarial science.

Coq/SSReflectでコンストラクタ数が引数に依存して変化するInductive 型とseq T型のconsの型をT -> seq (seq T) -> seq Tに変更した型を定義したい (slides)

Kenta Inoue

Coq/SSReflectに関する2つのショートトークです. 1つ目は「コンストラクタ数が引数に依存して変化する(ある形式の)Inductiveで定義された型」を定義したいときにCoqではどのように表現すればいいのか考察しました. 特に引数として型と自然数の対のリストを引数にとり, このリストの各要素(T_i,n_i)に対し, T_i型の引数とn_i個の再帰呼び出しを行う引数からなるコンストラクタを構成するようなInductive型について考察します. 2つ目はリストの型であるseq型のコンストラクタconsの型は型引数Tに対し, T -> seq T -> seq Tで定義されますが, これをT -> seq (seq T) -> seq Tに 変更して定義した型について考察します.

Verification of the Garsia-Wachs algorithm (slides)

Makoto Kanazawa (法政大学理工学部)

The Garsia-Wachs algorithm is an algorithm for finding a binary leaf tree with a given leaf sequence whose cost is as small as possible, where the cost is the sum of the costs associated with the leaf labels weighted by the depths of the leaves. The algorithm, along with a proof of correctness due to Kingston, is given in Knuth's The Art of Computer Programming, Vol. 3. I outline a formalization of this correctness proof in Dafny and make a few observations about the algorithm.

ブロックチェーンにおける支払い認証ポリシーの静的検証ツールの形式 検証 (slides)

Yoshihiro Imai (株式会社proof ninja)

本発表では、株式会社DMM Cryptoにおいて管理している支払い認証ポリ シーTAPの設定を検証するために開発したツールについて述べる。TAPは Fireblocksによって提供される、ブロックチェーン上の資産管理および支払 い認証における信頼性の高いソリューションを提供しているが、認証ポリシー が正確に設定され、安全に運用されていることを保証するための形式的検証 が求められる。本研究では、Coqを用いて支払い認証ポリシーの安全性を形 式的に証明するツールを開発し、ポリシーが意図通りに動作し、潜在的な脆 弱性を排除することを実証した。これによりブロックチェーンにおける支払 い認証ポリシーの信頼性と安全性を向上させるとともに、業務効率の向上に も寄与することが期待される。

16:25-17:55 (short talks, 15min each)

Automated Theorem Proving by HyperTree Proof Search with Retrieval-Augmented Tactic Generator (slides)

Sho Sonoda (Riken)

We developed an automated theorem proving system using a large language model (LLM). The LLM generates proofs (precisely, sequences of tactics) by interacting with the Lean theorem prover. Generation of the tactic sequences is based on a Monte Carlo tree search called HyperTree Proof Search (HTPS) combined with a retrieval-augmented generator (RAG) called ReProver.

Isabelle/HOLを用いた差分プライベートなアルゴリズムの安全な実装 (slides)

松岡和貴 (東京科学大学　理工学系情報理工学院数理・計算科学系数理・計算科学コース)

離散ラプラス分布を用いた差分プライベートなアルゴリズムを対象に、 定理証明支援系Isabelle/HOLを用いてその形式化と検証を行う。さらに、 Isabelle/HOLのコード生成機能を用いて差分プライバシーが検証された安全 な実装を得る。

標準的な様相論理のLeanでの形式化について (slides)

野口真柊 (神戸大学システム情報学科)

命題論理に様相演算子□と◇を導入した標準的な様相論理のLeanでの形 式化について，現在の進捗と今後の展望について軽く紹介する．

Postの対応問題のインスタンスの証明生成 (slides)

大森章裕 (東京科学大学 情報理工学院 数理計算科学系 南出研究室)

Postの対応問題のインスタンスの集合であるPCP[3,4]を全て解決すると いう取り組みの過程で、その結果の信頼性を高めるためにIsabelle/HOLの証 明を生成した試みを紹介します。インスタンスの数が3170個と大量にあり、 それぞれへの結果を証明するためには適切な証拠を発見し、それを元に証明 を自動生成する必要がありました。自動生成の方針と、必要だったオートマ トン理論の形式化について話します。

重複を除き辞書順で最小の部分リストを返す効率的なアルゴリズムの Agdaによる検証 (slides)

城戸道仁 (法政大学大学院理工学研究科システム理工学専攻)

Richard Bird(2014)は、著作、関数プログラミングによる珠玉のアルゴ リズムデザイン(原題:Pearls of Functional Algorithm Design)にて、 Haskell のライブラリ関数 nub の型を変更することで、計算量がΘ(n log n)であり、リストから重複を取り除いた上で、辞書順で最小のものを返す関 数のプログラムが構成できることを示し、実際に構成したプログラムを著書 に著した。この関数の正当性を検証を定理証明支援系Agdaを用いて行う。

Complete graphs and independence numbers (slides)

Takafumi Saikawa (Nagoya University)

I will report on an ongoing formalization of graph-theoretic invariants. This is a continuation of the work presented at TPP2023, this time expanded by complete graphs and their characterization by independence numbers of graphs. This is a joint work with Kazunori Matsuda and Yosuke Tsuji.

Tuesday, November 26

9:00-10:30

λ-計算の代数と幾何 (40min talk) (slides)

Masahiko Sato (京都大学 情報学研究科)

It is well-known that the set Λ of open terms of type-free λ-calculus dose not behave naturally when we regard Λ as an algebra equipped with the operation of function application. For example, the standard translation of λ-terms into combinatory terms does not admit the ξ-rule of the λ-calculus ([1; page 153]). To be more precise, the situation is that (1) for the Combinatory Logic, there are combinatory algebras which are sound and complete with respect to CL, but (2) these algebras are not sound for the λ-calculus because of the ξ-rule. Selinger [2; page 558] introduced the notion of "absolute interpretation" and gave a lambda algebra which is closed under the ξ-rule. However, the ξ-rule still remains in the original λ-calculus. In this talk, we will introduce a modified version of the λ-calculus without the ξ-rule but can prove exactly the same set of equations (under the β-equality) as those provable in the original λ-calculus. The key idea is to re-define Λ as an algebra on which the free monoid generated by the set of variables acts. The idea is obtained by analyzing the difference between Frege style canonical judgments and Martin-Löf style hypothetical judgments. We proved our main results in Coq.
[1] Barendregt, H. P. (1984) The Lambda Calculus, its Syntax and Semantics. 2nd edn. North-Holland.
[2] PETER SELINGER, The lambda calculus is algebraic, JFP 12 (6): 549–566, November 2002.
(Joint work with Keisuke Nakano (Tohoku University))

ZF+￢ACの相対的無矛盾性証明のIsabelle/ZFによる形式化 (slides)

Daiki Funane (東北大学大学院情報科学研究科)

We formalize the relative consistency proof of ZF+￢AC using Isabelle/ZF proof assistant. Our approach assumes the existence of a transitive countable model of ZF and uses forcing to construct a symmetric extension which is a model of ZF+￢AC. We show that the symmetric extension satisfies ZF+￢AC by formalizing a relativized forcing relation based on the formalization of forcing by Gunther et al.

Leanを用いたGödelの第一・第二不完全性定理の形式化 (slides)

齋藤彰悟 (東北大学大学院理学研究科数学専攻)

Gödelの第一・第二不完全性定理のLean4を用いた形式化について報告す る．不完全性定理の形式化は80年代からすでに何度か行われているが，ここ では過去のものより強い結果であるCobhamのR_0上の第一不完全性定理と IΣ_1上の第二不完全性定理の証明の形式化を行った．

10:45-12:25

暗号プロトコルの形式記述に向けたLLMチャットボットの活用 (slides)

櫻田英樹 (NTTコミュニケーション科学基礎研究所)

LLM チャットボットを活用して暗号プロトコルの形式記述を効率的に作 成することを試みた．具体的にはLLM チャットボットが自然言語で記述され たプロトコル仕様を理解し，これを形式的な記述に変換する過程を説明する． この手法を用いることで，形式検証ツールへの入力作成の最初のステップを 支援し，形式検証ツールを使い始める際の労力を削減することを目指す．

A Formalization of Prokhorov's Theorem in Isabelle/HOL (slides)

平田路和 (東京科学大学)

This talk will be presented in Japanese with English slides.
本講演は，ITP2024で発表した"A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL"において，口頭発表では詳細に触れなかったプロ ホロフの定理を題材とする．プロホロフの定理によれば，ポーランド空間上 の一様に有界な有限測度の集合について，相対コンパクト性と緊密性は同値 である．プロホロフの定理は，中心極限定理やSanovの定理，輸送理論にお ける最適カップリングの存在性を示すために用いられる確率論における主要 定理の一つである．本発表では，プロホロフの定理とその証明で必要となる リースの表現定理，アラオグルの定理の特殊な場合のIsabelle/HOLにおける 形式化について論じる．

Delayモナドを用いた一般再帰関数に対する等式変形による検証 (slides)

川上竜司 (名古屋大学 多元数理学研究科)

副作用を含む計算は、モナドと呼ばれる構造を用いることで関数型プログラムの中でうまく表現できることが広く知られている。 CoqのライブラリMonaeは、そういったモナド構造に着目した、等式変形による副作用を含む計算に対する検証ツールである。 一方で、Coqでは無矛盾性を保証するため停止性を確認できる関数しか定義することができない。 従って本研究では、MonaeにDelayモナドを追加することで、非停止な関数を含む一般再帰関数を表現し検証することに取り組んでいる。 本講演では、1.Delayモナドをどのように実装したか　2.それらを用いた検証 例　3.現在取り組んでいるDelayモナドと他のモナドとの組み合わせ　につ いて説明する。

On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System (slides)

Satoshi Matsuoka (産業技術総合研究所工学計測標準部門データサイエンス研究グループ)

We show that any many-valued function can be represented by a linear lambda term that is typed in second-order polymorphic type system.

13:30-15:10

ペトリネットにおける到達可能性問題の変種間の還元可能性の形式化 (slides)

手塚 凜 (千葉大学大学院 融合理工学府) ・ 山本 光晴 (千葉大学大学院 理学研究院)

ペトリネットにおけるいくつかの到達可能性問題の変種間の還元可能性 が1976年にHackによって示されている。本研究では、この証明をMathComp上 で形式化した。この中には、還元先の決定問題に用いる新しいペトリネット を構成する必要がある非自明なものもいくつか含まれる。これらをアドホッ クに形式化するのではなく、系統的に証明するための共通手順を作成し、そ れに従って形式化を行った。

Axiomatic real numbers for verified exact real-number computation (slides)

Sewon Park (Kyoto University)

In this talk, I present cAERN, our axiomatic formalization of real numbers of computable analysis in dependent type theory, and the Coq proof assistant. The axioms argued to be sound for realizability interpretation enable us to extract certified exact real-number computation programs from proofs. I will further introduce our recent progress in cAERN in hyperspace computations and ordinary differential equation solving. This talk is based on my joint work with Holger Thies and Michal Konečný.

Combining cost and behavior in type theory (slides)

Yue Niu (National Institute of Informatics)

Leanを用いたスイッチング回路の安全性検証 (slides)

瀬川秀一 (北陸先端科学技術大学院大学)

スイッチング回路の安全性検証における客観性と網羅性を確保するため、 定理証明支援系Leanおよび数学ライブラリMathlibを用いた検証を試行して いる。検証にあたり、すでに構築された特殊関数やODEに関する定理を活用 し、製品ごとに求められる特性を証明する。証明を効率的に実現するには、 状態空間の理論やハイブリッドシステムの検証理論の定式化が必要である。 本発表では、検証手法の概要および証明の進行状況について紹介する。

15:25-16:40

TPPmark 2024 (20min)

Jacques Garrigue (Nagoya University) and provers

Slides and answers

導出原理の逆適用による定理の自動生成手法の提案 (25min) (slides)

西島海斗 (山口大学)

本研究では，一階述語論理における証明技法の一つである導出原理を逆 方向に適用することで，新たな定理を自動生成する手法を提案する．現在， 定理証明コーパスが量・質ともに不足しており，データ不足が機械学習型の 自動定理証明器の性能向上を妨げていた．本手法では，結論から仮定を逆推 論することで多様な定理を生成し，データセットを拡充することを目指す． 提案手法の具体的なアルゴリズムの設計と実装について詳述し，今後の実験 計画についても述べる．

Coq証明支援系によるDNA計算の形式化 (15min) (slides)

早川銀河 (九州大学 数理学府 数理学専攻)

DNA分子のもつ性質を利用して計算するモデルの一つとしてスティッカー システムというものがあり、一部のスティッカーシステムは有限オートマト ンと同等の計算能力が有ることが知られている。今回、Coq,ssreflectを用 いてオートマトンを模倣するスティッカーシステム を構成し、その正しさ を形式的に示した。

Coqによる実解析のための実用的な補題の開発 (15min) (slides)

石黒吉洋 (名古屋大学)

Coqで確率プログラムの意味論を検証するために、我々はMathComp-Analysisを拡張してきた。 特に、基本的な確率分布を形式化するために、微積分の基本定理や積分の変数変換などの限定的なバージョンなど、微分と積分に関する様々な定理を作成した。 本講演では、Coqでの確率論における重要な補題であるガウス積分の定式化に焦点を当て、連続関数の積分の評価をより扱いやすくする非有界区間への補題の一般化についても説明する。