| 研究課題/領域番号 |
22H00520
|
|---|
| 研究種目 |
基盤研究(A)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
中区分60:情報科学、情報工学およびその関連分野
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 上級主任研究員 (40415641)
|
|---|
| 研究分担者 |
才川 隆文 名古屋大学, 多元数理科学研究科, 研究員 (00897100)
勝股 審也 京都産業大学, 理学部, 教授 (30378963)
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2026-03-31
|
| 研究課題ステータス |
交付 (2025年度)
|
| 配分額 *注記 |
40,300千円 (直接経費: 31,000千円、間接経費: 9,300千円)
2025年度: 10,010千円 (直接経費: 7,700千円、間接経費: 2,310千円)
2024年度: 10,140千円 (直接経費: 7,800千円、間接経費: 2,340千円)
2023年度: 10,140千円 (直接経費: 7,800千円、間接経費: 2,340千円)
2022年度: 10,010千円 (直接経費: 7,700千円、間接経費: 2,310千円)
|
|---|
| キーワード | 形式検証 / 数学の形式化 / Coq / 確率的プログラミング / プログラム検証 |
|---|
| 研究開始時の研究の概要 |
今日, コンピュータプログラムは, デジタル情報の操作やそのネットワークに加えて, 外界との相互作用を行うため, プログラムの検証には, 形式論理と離散数学だけでなく, 実解析や確率論や幾何学などの数学が必要となり, プログラムの様々な副作用の厳密な検証が困難になっている. その複雑さを抑えるためには, プログラムの意味論の基礎的な研究と, 高度な数学に一貫性のある形式表現を与える統合的な研究の双方が必要である. 本研究では, 定理証明支援系Coq上, 実解析, 連続確率, 剛体幾何を形式化し, モナドと等式推論に基づいて, 形式的基盤の構築とその評価を行う.
|
| 研究実績の概要 |
本プロジェクトの目的は、外界の物理的対象と直接対話し動作するプログラムの品質評価のため、定理証明支援系上の検証基盤の設計に必要な検証技術の研究を行うことである。
令和6年度、数学と確率的プログラミング言語の形式化に集中した。数学の形式化に関して、MathComp-Analysisライブラリによる積分とカーネルと確率論の形式化を進展した。特に、新たな定理（ガウス積分、カーネルの合成など）で拡張した。確率論の形式化に関して、ベータ分布や正規分布や独立などの形式化を行い、ベルヌーイサンプリングに応用した。そのため、統計学に用いられるチェルノフ不等式などの集中不等式の形式化を行った。以上の拡張を等式理論による確率的プログラム形式検証に応用した。また、確率的プログラミング言語に関して、令和４年度で形式化した一階確率的プログラミング言語の意味論をループで拡張し、国際雑誌で成果発表ができた。
InfoTheoという有限確率の基盤を含む情報理論のライブラリの移植が完成した。具体的に、Rocq定理証明支援系の標準ライブラリへの依存に最低限にし、上記のMathComp-Analysisとの相互互換性を高めたおかげで、確率論に関する定理などが共有できるようにした。また、InfoTheoの拡張を行い、セキュリティプロトコルの性質（正しさ、情報漏洩）の形式検証に応用できた。更に、Monaeという等式推論によるプログラム検証基盤を国際雑誌で成果発表し、新たなモナドと応用例で拡張した。令和5年度でMathComp-Analysis、InfoTheo、Monaeのために開発を開始したドキュメンテーションツールをリリースした。
|
| 現在までの達成度 |
現在までの達成度
2: おおむね順調に進展している
理由
本プロジェクトの形式化実験はRocqリとしてまとめるように努めていたおかげで、実験を順調に進めることができ、海外の研究者から協力を得られ、新たな発展もできた。また、査読付き論文を国際学会や国際雑誌で発表できた。
|
| 今後の研究の推進方策 |
昨年度、 MathComp-Analysisというライブラリの積分の形式化を新たな定理、連続確率論、測度論の概念などで拡張できた。 今年度、MathComp-Analysisを拡張を行う。具体的に、ソボレフ空間を追加し、微分の形式化を多変数へ拡張し、確率分布間の距離の形式化を行う。以上の拡張によって、関数解析学とベクトル解析のライブラリを充実させる。さらに、昨年度の量子プログラミングへの応用を踏まえ、複素解析の形式化を開始する。また、MathComp-Analysisの確率論の拡張として、InfoTheoというライブラリの有限確率と情報理論との融合に務める。
確率や非決定性などを扱うプログラミング言語の機能の意味論について形式化を見据えた理論を構築する。昨年度、確率的プログラミング言語の意味論と構文を拡張し、等式推論を用いて、具体的な確率的プログラムの検証できた。今年度、その形式基盤を充実する。具体的に、上記のMathComp-Analysisと連携し、測度モナドを形式化し、差分プライバシーに応用する。量化代数的推論とローヴェア理論を取り込むことによって、プログラム検証のための等式推論の基盤を拡張する。また、疑ボレル空間の形式化を行い、高階関数を扱えるようにする。
MathComp-Analysisを用いて、ロボティクスへの応用として、幾何学のための代数構造を整備し、制御理論の形式化を開始する。
|
