| Project/Area Number |
22H00520
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (A)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Review Section |
Medium-sized Section 60:Information science, computer engineering, and related fields
|
|---|
| 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
|
| Project Status |
Granted (Fiscal Year 2025)
|
| Budget Amount *help |
¥40,300,000 (Direct Cost: ¥31,000,000、Indirect Cost: ¥9,300,000)
Fiscal Year 2025: ¥10,010,000 (Direct Cost: ¥7,700,000、Indirect Cost: ¥2,310,000)
Fiscal Year 2024: ¥10,140,000 (Direct Cost: ¥7,800,000、Indirect Cost: ¥2,340,000)
Fiscal Year 2023: ¥10,140,000 (Direct Cost: ¥7,800,000、Indirect Cost: ¥2,340,000)
Fiscal Year 2022: ¥10,010,000 (Direct Cost: ¥7,700,000、Indirect Cost: ¥2,310,000)
|
|---|
| Keywords | 形式検証 / 数学の形式化 / Coq / 確率的プログラミング / プログラム検証 |
|---|
| Outline of Research at the Start |
今日, コンピュータプログラムは, デジタル情報の操作やそのネットワークに加えて, 外界との相互作用を行うため, プログラムの検証には, 形式論理と離散数学だけでなく, 実解析や確率論や幾何学などの数学が必要となり, プログラムの様々な副作用の厳密な検証が困難になっている. その複雑さを抑えるためには, プログラムの意味論の基礎的な研究と, 高度な数学に一貫性のある形式表現を与える統合的な研究の双方が必要である. 本研究では, 定理証明支援系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の可測空間の拡張を行い、超分布や高階関数（疑ボレル空間）などを扱える確率的プログラムの検証をサポートする。開発した一般的なモナドの持ち上げを、標準的な差分プライバシーにより具体化してプログラム論理を導出し、アルゴリズムの差分プライバシー検証を行う。量化代数的推論とローヴェア理論を取り組むことによって、プログラム検証のための等式推論の基盤を整備する。また、令和４年度形式化したカーネルに基づく意味論と確率密度関数の関係を明らかする。
確率測度やファジー化の一般化でもある関係計算理論の形式化とその等式証明による実現方法、幾何代数による形状変換の数式表現による形式化とその性質の等式証明による実現方法について考察する。また、フーリエ級数の形式化を開始する。
|
