2023 Fiscal Year Annual Research Report
Formal Foundations for Verification of Physical and Probabilistic Systems
| Project/Area Number |
22H00520
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 上級主任研究員 (40415641)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
才川 隆文 名古屋大学, 多元数理科学研究科, 研究員 (00897100)
勝股 審也 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (30378963)
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
|
|---|
| Project Period (FY) |
2022-04-01 – 2026-03-31
|
| Keywords | 形式検証 / 数学の形式化 / Coq / 確率的プログラミング / プログラム検証 |
|---|
| Outline of Annual Research Achievements |
本プロジェクトの目的は、外界の物理的対象と直接対話し動作するプログラムの品質評価のため、定理証明支援系上の検証基盤の設計に必要な検証技術の研究を行うことである。
令和５年度、数学（とくに、確率論）と確率的プログラミング言語の形式化に集中した。数学の形式化に関して、MathComp-Analysisライブラリによる微分と積分の形式化を進展させ、新たな定理（ロピタルの定理、微分積分学の基本定理、カーネルに基づいたGiryモナドなど）で拡張し、ドキュメンテーションツールを開発した。その拡張は人工知能で使われている損失関数の性質を記述するための論理の形式化に応用した。確率論の形式化に関して、基本的な分布（ベルヌーイ、二項、連続一様など）の形式化を行った。Infotheoという情報理論のライブラリの有限確率の基盤の移植と拡張を行った。その拡張をロバスト統計に応用した（コペンハーゲンIT大学と共同研究）。
等式推論技術に関して、Monaeというプログラム検証基盤をOCamlプログラミング言語の検証ができるように拡張した。量子計算に関して、モナドの構築にまだ至っていないものの、MathCompの上でShor符号を含むいくつか量子回路を形式化し、その正しさを証明できた。確率的プログラミング言語に関して、令和４年度形式化した一階確率的プログラミング言語の意味論を、依存型に基づく構文の形式化で拡張した。その拡張を用いて、等式推論によるプログラム検証の応用例を増やし、連続確率分布を考慮した等式推論の実現ができた。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
本プロジェクトの形式化実験はCoq定理証明支援系上に行っている。その実験をMathComp-AnalysisとInfotheoとMonaeというライブラリとしてまとめるように努めていたおかげで、実験を順調に進めることができ、海外の研究者から協力を得られ、新たな発展もできた。また、査読付き論文の発表ができた。
|
| Strategy for Future Research Activity |
MathComp-Analysisが提供する実解析の拡張を行う。具体的に、連続確率論の形式化の継続として、標準的な分布(ベータ、正規など)の形式化を完成させ、確率分布間の距離の形式化を行う。また、微分積分学の基本定理を絶対連続関数で拡張する。令和５年度開始した偏微分の形式化を続けて、多変数を扱えるように基盤を拡張する。
様々な副作用を伴うプログラムに対し、Monaeの汎用性を改善するように、連続確率分布に扱うように基盤を拡張する。そのため、MathComp-Analysisと連携し、MathComp-Analysisの可測空間の拡張を行い、超分布や高階関数（疑ボレル空間）などを扱える確率的プログラムの検証をサポートする。開発した一般的なモナドの持ち上げを、標準的な差分プライバシーにより具体化してプログラム論理を導出し、アルゴリズムの差分プライバシー検証を行う。量化代数的推論とローヴェア理論を取り組むことによって、プログラム検証のための等式推論の基盤を整備する。また、令和４年度形式化したカーネルに基づく意味論と確率密度関数の関係を明らかする。
確率測度やファジー化の一般化でもある関係計算理論の形式化とその等式証明による実現方法、幾何代数による形状変換の数式表現による形式化とその性質の等式証明による実現方法について考察する。また、フーリエ級数の形式化を開始する。
|
