概要
京都大学大学院理学研究科 学習物理学特別講座 三内顕義(さんない あきよし)特定准教授(兼:国立情報学研究所大規模言語モデル研究開発センター客員准教授)らの研究グループは、東京大学・国立情報学研究所等と共同で、小規模な生成AI(8B(80億)パラメータ)と定理証明支援系 Lean を協調させる新手法「Prover Agent」を開発しました。本手法は難解な数学五輪(IMO)レベルを含む MiniF2F ベンチマークで86.1%の証明成功率を達成し、同スケールで世界最高性能を記録しました。特に IMO 問題カテゴリでは80%を突破し、これは一般に金メダリスト相当と評価される水準です。計算コストを他手法の約4分の1に抑えつつ高精度を実現した点が特長で、定理証明支援系を用いて計算や証明に間違いがないことが保証されているため、将来的には数学教育や安全なAI 判断根拠提示などへの応用が期待されます。
本研究成果は 2025年7月9日にICML AI for math workshopに採択されました。
1.背景
近年、生成AI は自然言語で高度な推論を示す一方、誤答や幻覚の問題が課題でした。数学の形式証明支援系 Lean は誤りを排除できますが、証明探索に膨大な労力が必要です。両者の長所を組み合わせ、少ない計算資源で信頼できる自動証明を実現することが本研究の目的でした。
2.研究手法・成果
・協調エージェント設計
自然言語推論LLM、Lean 用形式証明モデル、Lean 検証器を連携。
・補題自動生成
解けない問題に対し、人間の発想にならい中間補題を生成・証明。
・結果
MiniF2F 全体で 86.1%、IMO 問題のみで 80% を達成。これは国際数学五輪の金メダル(直近十年で平均69.5%がボーダーライン)に相当します。なお試行回数は 2,000 と、従来法(8,192)の 1/4 です。
3.波及効果、今後の予定
・大規模モデルに依存せずに高度な数理推論が可能となり、教育用の低コスト証明支援ソフトや、AI 判断根拠の厳密検証などへの展開が期待されます。
・今後は物理・生命科学証明や産業数理最適化へ応用範囲を拡大し、より大規模データセットでの実証を進めます。
4.研究プロジェクトについて
・事業名:文部科学省科学研究費補助金学術変革領域研究(A)「『学習物理学』の創成」
・課題番号:22A202
・連携機関:東京大学、国立情報学研究所、滋賀大学、理化学研究所
<用語解説>
1. Lean:定理の各論理ステップをコンピュータで厳密に検証するオープンソース形式証明システム。
2. MiniF2F:IMO・AIME などを含む 488 題から成る国際的定理証明ベンチマーク。
3. 8B パラメータ:学習済み言語モデルの規模を示す指標で、8 billion(80億)重みを持つ比較的小型モデル。
<研究者のコメント>
「小さなAIと形式証明を組み合わせることで、数学オリンピック級の難問を高速に解けるとは正直驚きました。今後は教育現場で“AI と一緒に証明を学ぶ”時代を切り拓きたいです。」(三内顕義)
<論文タイトルと著者>
タイトル:Prover Agent: An Agent‑based Framework for Formal Mathematical Proofs(エージェント協調による小型AI形式数学証明フレームワーク)
著 者:Kaito Baba, Chaoran Liu, Shuhei Kurita, Akiyoshi Sannai
掲 載 誌:arXiv(2025‑06‑24)
DOI:10.48550/arXiv.2506.19923v1
<研究に関するお問い合わせ先>
三内顕義(さんない あきよし)
京都大学大学院理学研究科 特定准教授
E-mail:sannai.akiyoshi.7z*kyoto‑u.ac.jp (*を@に変えてください)
<報道に関するお問い合わせ先>
京都大学広報室国際広報班
TEL:075-753-5729 FAX:075-753-2094
E-mail:comms*mail2.adm.kyoto-u.ac.jp (*を@に変えてください)