海外ニュース速報

· AI業界

Google DeepMindが形式証明検索でエルデシュ問題9問を解答

25秒でわかる内容解説

Google DeepMindは、大規模言語モデルと形式証明検索を組み合わせたAIエージェントが、数学の未解決問題であるエルデシュ問題の解答に成功したと発表した。最上位エージェントは353問中9問を自主的に解き、1問あたり数百ドルの計算コストで処理を完了させた。この手法は組み合わせ論やグラフ理論など複数の数理分野への展開も進んでおり、技術者にとってAI研究ツールの実用化を示す指標となる。

LLMと形式証明言語の組み合わせが未解決問題を解く

Google DeepMindは、大規模言語モデルと形式証明検索を組み合わせたAIエージェントが、数学の未解決問題であるエルデシュ問題の解答に成功したと発表した。最上位エージェントは353問中9問を自主的に解き、1問あたり数百ドルの計算コストで処理を完了させた。この手法は、言語モデルが生成した証明を形式証明言語Leanで検証する二重構造だ。確率的な推論の弱点を機械検証で補い、数学研究への実用性を高めている。

OEISの未解決予想492件についても、44件の証明に成功している。基本型エージェントでも同様の成功を再現できたが、難問では処理費用が高騰した。生成と検証を交互に行う単純な構成でも実用範囲内の結果が得られた点は、エージェント設計の指針となる。

論文ではこの手法が初めての大規模評価対象となり、Open Problemsの解決能力が定量的に示された。AbstractにはLLMの数学推論能力の向上と信頼性課題の解決策が明記されている。

We perform the first large-scale evaluation of this method's ability to solve open problems.

我々は、この手法が未解決問題を解く能力について、初めての大規模評価を実施した。

確率的な推論を機械検証で補強する手法の経緯

大規模言語モデルは数学推論で高い性能を示しているが、確率的な性質ゆえに計算結果の信頼性に課題が残る。これを補うため、生成された証明を機械が厳密に検証する形式証明検索が注目されてきた。言語モデルの推論出力をそのまま使うのではなく、Leanで型チェックや論理検証を行うことで誤りを排除できる。この二重構造が未解決問題への適用を可能にした。

論文は2026年5月21日にv1が提出され、6月8日にv2として改訂された。ファイルサイズは約1,291KBで、著者にはSwarat Chaudhuriらの名前が記載されている。形式証明言語Leanは、数学定理を機械可読な構文で記述し、コンパイル時に検証できる環境だ。arXivのComputer Science > Artificial Intelligence分野に分類され、PDFとHTML形式で公開されている。

関連するコードやデータもalphaXivやHugging Faceで確認できる。arXivLabsの枠組みで開発された実験機能も併記されており、オープンな研究コミュニティでの評価基盤が整っている。Submission historyにはv1とv2の提出時刻とファイルサイズが記録されている。技術者は論文のバージョン履歴を直接追跡できる。

技術者向け検証が進むHN報告とコスト分析

本研究の報告は2026年10月10日にHacker Newsで掲載された。コミュニティからのコメントは現時点で確認できていないが、論文データと計算コストの明細が公開されているため、技術者向けに詳細な検証が進んでいる。353問中9問という解答数は、単なるパターンマッチングを超えた推論能力を示す。OEISは整数数列総合辞典の略称だ。

492件中44件を証明した実績も、数列や整数論の分野で有効なことを裏付ける。 基本型エージェントとの比較により、モデルの規模や推論パスの設計が費用対効果に与える影響が可視化された。論文の引用ツールやConnected Papers、Hugging Faceとの連携情報も併せて公開されている。

Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars

我々の最も高性能なエージェントは、問題ごとのコストを数百ドルに抑え、353問の未解決エルデシュ問題のうち9問を自主的に解決した。

Scite Smart Citationsによる引用解析も利用可能だ。arXivLabsのパートナー企業も公開されており、連携プロジェクトの展開が期待される。技術者はHNのスレッドを更新し、計算コストの推移を監視できる。Hacker NewsのURLはarxiv.orgの論文ページへ直接リンクしている。

エージェントの解答実績と計算コスト
項目値
エルデシュ問題353問中9問解答
OEIS予想492件中44件証明
計算コスト問題ごとに数百ドル
展開分野組み合わせ論など5分野

数理研究分野への展開と検証手法の標準化

同エージェントは組み合わせ論、最適化、グラフ理論、代数幾何、量子光学の各研究分野で展開が始まっている。数理計算を伴う学術研究のワークフローに、AI検証パイプラインが組み込まれつつある。論文の最新版は2026年6月8日に公開された。今後は検証対象の数学分野を拡大し、コスト削減と解答精度の向上を並行して進める予定だ。

形式証明検索の手法が標準化されれば、大規模言語モデルの数学利用における信頼性基準が明確になる。技術者は各分野のLeanライブラリ整備と、エージェントの推論設計を並行して追う必要がある。同エージェントは組み合わせ論から量子光学まで5つの分野で展開中で、2026年6月8日に公開された最新版では検証手法の詳細が補足されている。

量子光学分野では光の量子状態の解析に応用される見込みだ。arXivLabsの連携情報も更新されており、学術界隈での採用事例が蓄積されつつある。技術者は各分野のドキュメントを定期的なチェックで追える。

出典