| 研究課題/領域番号 |
22H00520
|
|---|
| 研究種目 |
基盤研究(A)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
中区分60:情報科学、情報工学およびその関連分野
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 上級主任研究員 (40415641)
|
|---|
| 研究分担者 |
才川 隆文 名古屋大学, 多元数理科学研究科, 研究員 (00897100)
勝股 審也 京都産業大学, 理学部, 教授 (30378963)
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2026-03-31
|
| 研究課題ステータス |
交付 (2024年度)
|
| 配分額 *注記 |
40,300千円 (直接経費: 31,000千円、間接経費: 9,300千円)
2024年度: 10,140千円 (直接経費: 7,800千円、間接経費: 2,340千円)
2023年度: 10,140千円 (直接経費: 7,800千円、間接経費: 2,340千円)
2022年度: 10,010千円 (直接経費: 7,700千円、間接経費: 2,310千円)
|
|---|
| キーワード | 形式検証 / 数学の形式化 / Coq / 確率的プログラミング / プログラム検証 |
|---|
| 研究開始時の研究の概要 |
今日, コンピュータプログラムは, デジタル情報の操作やそのネットワークに加えて, 外界との相互作用を行うため, プログラムの検証には, 形式論理と離散数学だけでなく, 実解析や確率論や幾何学などの数学が必要となり, プログラムの様々な副作用の厳密な検証が困難になっている. その複雑さを抑えるためには, プログラムの意味論の基礎的な研究と, 高度な数学に一貫性のある形式表現を与える統合的な研究の双方が必要である. 本研究では, 定理証明支援系Coq上, 実解析, 連続確率, 剛体幾何を形式化し, モナドと等式推論に基づいて, 形式的基盤の構築とその評価を行う.
|
| 研究実績の概要 |
本プロジェクトの目的は、外界の物理的対象と直接対話し動作するプログラムの品質評価のため、定理証明支援系上の検証基盤の設計に必要な検証技術の研究を行うことである。
令和４年度、数学と確率的プログラミング言語に集中した。数学の形式化に関して、MathComp-Analysisによる積分論の形式化を進展させ、新たな概念と定理（ラドン＝ニコディムの定理やカーネルなど）で拡張した。その積分論の形式化を用いて、連続確率論の包括的な形式化を開始した。具体的に、非可算濃度の確率論と離散型確率変数を考慮し、基本的な概念（期待値、分散など）の形式化ができた（コペンハーゲンIT大学と共同研究）。そのため、Infotheoという情報理論の形式化による有限確率形式化の一般化を行ってきた。
確率的プログラミング言語に関して、一階プログラミング言語の形式化に成功した。具体的に、カーネルを用いた意味論を形式化し、その形式化を等式推論によるプログラム検証に応用した。また、確率プログラムの記述のため、形式構文の設計を行った。また、具体圏の形式化を含む拡張として抽象圏の形式化を試み、型理論的宇宙の制約解決に関する問題を回避するため非可述的データ型を用いた最初の版を作成した（コペンハーゲンIT大学でこの結果について発表と議論）。また、確率論の定式化の一つの応用として確率的プログラムの差分プライバシーの検証のための論理の定式化がある。令和４年度はその一つとして差分プライバシーに適したモナドの持ち上げの一般論をCoqで形式化した。
等式推論技術に関して、Monaeというプログラム検証基盤を非決定性と詳細化で拡張した。連続確率を扱う等式推論の拡張を開始した。また、量子プログラミングに関する形式化実験を行ってきた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
本プロジェクトの形式化実験はCoq定理証明支援系上に行っている。その実験をMathComp-Analysisというライブラリとしてまとめるように努めていたおかげで、実験を順調に進めることができ、海外の研究者から協力を得られ、新たな発展もできた。 また、査読付き論文の発表ができた。
|
| 今後の研究の推進方策 |
令和５年度, MathComp-Analysisが提供する実解析の拡張を行う. 具体的に, 連続確率論の形式化の継続として, 基本的な分布(正規分布など)の形式化し, 確率分布間の距離の形式化を行う. また、積分と微分の関係を明らかにする定理(微分積分学の基本定理など)の形式化を行う. さらに, ベクトル空間の一般的な形式化を行い, 積分の形式化をLp空間で抽象化し, 微分の形式化を多変数へ拡張する. 以上の拡張によって, 例えば, ロボティクスの基礎となる幾何学と運動学の形式化が可能となる.
確率や非決定性などを扱うプログラミング言語の機能の意味論について形式化を見据えた理論を構築する. 令和５年度, その形式基盤を充実する. 令和４年度の確率的一階プログラミング言語の形式化を完成させる. 疑ボレル空間及びその一般論として具体層の形式化を行い, 高階関数を扱うようにする. そのため, MathComp-Analysisによる可測空間の拡張が必要である. また, 量化代数的推論とローヴェア理論を取り組むことによって, プログラム検証のための等式推論の基盤を整備する. また、令和４年度に開発した一般的なモナドの持ち上げを、標準的な差分プライバシーにより具体化してプログラム論理を導出し、いくつかのアルゴリズムの差分プライバシー検証をその中で行う。
様々な副作用を伴うプログラムに対し, 定理証明支援系Coq上において, プログラム検証を可能とするMonaeという形式基盤を開発してきた. 令和５年度, Monaeの汎用性を改善する. とくに, 連続確率分布に基づく確率的プログラムの検証を可能にする. そのため, 上記のMathComp-Analysisと連携し, 測度モナドを形式化する. 連続確率分布を考慮した等式推論を実現し, 超分布や高階関数などを扱える確率的プログラムの検証をサポートする.
|
