| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2026-07-03 13:30 ［招待講演］定理証明AIの統計的な証明可能性 ○園田 翔（理研）  NC2026-12 IBISML2026-12 |
|
| 抄録 | （和） | 定理証明AIは，Leanなどの証明支援系と推論モデル，検索，検証器フィードバックを組み合わせることで，高度な数学問題に対して実用的な成功率を示し始めている．一方で，古典的な計算量理論や証明論は主に最悪時困難性や証明の存在を扱うため，現実の偏った問題分布上で「有限の検証器呼び出し予算内に証明へ到達する確率」を説明しにくい．本講演では，対話型定理証明を決定論的な検証器遷移をもつ有限ホライズンMDPとして定式化し，この到達確率を統計的証明可能性として導入する．その上でCase Iでは，オフラインの行動価値回帰と貪欲探索により学習済み証明器の成功確率を評価し，局所的な価値推定誤差が平均証明長，データ被覆，マージン条件を通じてどのように蓄積するかを示す．Case IIでは，成功した教師証明からの模倣学習を，flatな証明列と階層的な証明DAGの表現で比較し，補題再利用やメモ化が重複した局所判断を減らすことで十分サンプル数を指数的に改善し得ることを示す．本講演の内容は [1,2] に基づく． [1] S. Sonoda, S. Akiyama, and Y. Uezato, “Why agentic theorem prover works: A statistical provability theory of mathematical reasoning models,” Proceedings of the 43rd International Conference on Machine Learning, 2026. [2] S. Sonoda, S. Akiyama, and Y. Uezato, “Exponential sample complexity separation between flat and hierarchical agentic theorem provers,” ArXiv preprint 2602.10512, 2026. |
| （英） | Modern theorem proving AI combines reasoning models with proof assistants, search, retrieval, and verifier feedback, yet classical worst-case hardness does not explain why such systems work on biased mathematical workloads. This talk formulates interactive theorem proving as a finite-horizon MDP with deterministic verifier transitions and defines statistical provability as the probability of reaching a verified proof within a fixed budget on a problem distribution. Case I analyzes offline action-value regression followed by greedy proving, showing how local value error accumulates through average proof length, coverage, and margins. Case II studies teacher-student imitation, contrasting flat traces with hierarchical proof DAGs and quantifying how reusable subproofs can reduce sufficient sample size. This talk is based on [1,2]. [1] S. Sonoda, S. Akiyama, and Y. Uezato, “Why agentic theorem prover works: A statistical provability theory of mathematical reasoning models,” Proceedings of the 43rd International Conference on Machine Learning, 2026. [2] S. Sonoda, S. Akiyama, and Y. Uezato, “Exponential sample complexity separation between flat and hierarchical agentic theorem provers,” ArXiv preprint 2602.10512, 2026. |
|
| キーワード | （和） | 定理証明AI / 対話型定理証明 / 統計的証明可能性 / / / / / |
| （英） | AI theorem proving / interactive theorem proving / statistical provability / / / / / | |
| 文献情報 | 信学技報, vol. 126, no. 91, IBISML2026-12, pp. 54-54, 2026年7月. | |
| 資料番号 | IBISML2026-12 | |
| 発行日 | 2026-06-25 (NC, IBISML) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | NC2026-12 IBISML2026-12 |
|
| 研究会情報 | |
| 研究会 | NC IBISML IPSJ-BIO IPSJ-MPS |
| 開催期間 | 2026-07-01 - 2026-07-03 |
| 開催地（和） | 沖縄科学技術大学院大学 |
| 開催地（英） | OIST |
| テーマ（和） | 機械学習、一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | IBISML |
| 会議コード | 2026-07-NC-IBISML-BIO-MPS |
| 本文の言語 | 日本語 |
| タイトル（和） | 定理証明AIの統計的な証明可能性 |
| サブタイトル（和） | |
| タイトル（英） | Statistical Provability of Theorem Proving AI |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 定理証明AI / AI theorem proving |
| キーワード(2)（和/英） | 対話型定理証明 / interactive theorem proving |
| キーワード(3)（和/英） | 統計的証明可能性 / statistical provability |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 園田 翔 / Sho Sonoda / ソノダ ショウ |
| 第1著者 所属（和/英） | 理化学研究所革新知能統合研究センター (略称： 理研) RIKEN Center for Advanced Intelligence Project (略称： RIKEN) |
| 講演者 | 第1著者 |
| 発表日時 | 2026-07-03 13:30:00 |
| 発表時間 | 60分 |
| 申込先研究会 | IBISML |
| 資料番号 | NC2026-12, IBISML2026-12 |
| 巻番号（vol） | vol.126 |
| 号番号（no） | no.90(NC), no.91(IBISML) |
| ページ範囲 | p.54 |
| ページ数 | 1 |
| 発行日 | 2026-06-25 (NC, IBISML) |
[研究会発表申込システムのトップページに戻る]