2022 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) |
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
勝股 審也 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (30378963)
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
才川 隆文 名古屋大学, 多元数理科学研究科, 研究員 (00897100)
|
|---|
| Project Period (FY) |
2022-04-01 – 2026-03-31
|
| Keywords | 形式検証 / 数学の形式化 / Coq / 確率的プログラミング / プログラム検証 |
|---|
| Outline of Annual Research Achievements |
本プロジェクトの目的は、外界の物理的対象と直接対話し動作するプログラムの品質評価のため、定理証明支援系上の検証基盤の設計に必要な検証技術の研究を行うことである。
令和４年度、数学と確率的プログラミング言語に集中した。数学の形式化に関して、MathComp-Analysisによる積分論の形式化を進展させ、新たな概念と定理（ラドン＝ニコディムの定理やカーネルなど）で拡張した。その積分論の形式化を用いて、連続確率論の包括的な形式化を開始した。具体的に、非可算濃度の確率論と離散型確率変数を考慮し、基本的な概念（期待値、分散など）の形式化ができた（コペンハーゲンIT大学と共同研究）。そのため、Infotheoという情報理論の形式化による有限確率形式化の一般化を行ってきた。
確率的プログラミング言語に関して、一階プログラミング言語の形式化に成功した。具体的に、カーネルを用いた意味論を形式化し、その形式化を等式推論によるプログラム検証に応用した。また、確率プログラムの記述のため、形式構文の設計を行った。また、具体圏の形式化を含む拡張として抽象圏の形式化を試み、型理論的宇宙の制約解決に関する問題を回避するため非可述的データ型を用いた最初の版を作成した（コペンハーゲンIT大学でこの結果について発表と議論）。また、確率論の定式化の一つの応用として確率的プログラムの差分プライバシーの検証のための論理の定式化がある。令和４年度はその一つとして差分プライバシーに適したモナドの持ち上げの一般論をCoqで形式化した。
等式推論技術に関して、Monaeというプログラム検証基盤を非決定性と詳細化で拡張した。連続確率を扱う等式推論の拡張を開始した。また、量子プログラミングに関する形式化実験を行ってきた。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
本プロジェクトの形式化実験はCoq定理証明支援系上に行っている。その実験をMathComp-Analysisというライブラリとしてまとめるように努めていたおかげで、実験を順調に進めることができ、海外の研究者から協力を得られ、新たな発展もできた。 また、査読付き論文の発表ができた。
|
| Strategy for Future Research Activity |
令和５年度, MathComp-Analysisが提供する実解析の拡張を行う. 具体的に, 連続確率論の形式化の継続として, 基本的な分布(正規分布など)の形式化し, 確率分布間の距離の形式化を行う. また、積分と微分の関係を明らかにする定理(微分積分学の基本定理など)の形式化を行う. さらに, ベクトル空間の一般的な形式化を行い, 積分の形式化をLp空間で抽象化し, 微分の形式化を多変数へ拡張する. 以上の拡張によって, 例えば, ロボティクスの基礎となる幾何学と運動学の形式化が可能となる.
確率や非決定性などを扱うプログラミング言語の機能の意味論について形式化を見据えた理論を構築する. 令和５年度, その形式基盤を充実する. 令和４年度の確率的一階プログラミング言語の形式化を完成させる. 疑ボレル空間及びその一般論として具体層の形式化を行い, 高階関数を扱うようにする. そのため, MathComp-Analysisによる可測空間の拡張が必要である. また, 量化代数的推論とローヴェア理論を取り組むことによって, プログラム検証のための等式推論の基盤を整備する. また、令和４年度に開発した一般的なモナドの持ち上げを、標準的な差分プライバシーにより具体化してプログラム論理を導出し、いくつかのアルゴリズムの差分プライバシー検証をその中で行う。
様々な副作用を伴うプログラムに対し, 定理証明支援系Coq上において, プログラム検証を可能とするMonaeという形式基盤を開発してきた. 令和５年度, Monaeの汎用性を改善する. とくに, 連続確率分布に基づく確率的プログラムの検証を可能にする. そのため, 上記のMathComp-Analysisと連携し, 測度モナドを形式化する. 連続確率分布を考慮した等式推論を実現し, 超分布や高階関数などを扱える確率的プログラムの検証をサポートする.
|
Research Products
(14 results)
