人工知能：数学競技でメダル級のAIシステム

複雑な数学理論を証明できるAI（artificial intelligence；人工知能）システムを報告する論文が、今週のNature に掲載される。Google DeepMindのAlphaProofは、2024年国際数学オリンピック（IMO：International Mathematics Olympiad）で銀メダル級の成績を収めた。

数学者は、複雑な問題を解き、理論を証明するために計算ツールを用いる。AIシステムは、このプロセスを加速させる可能性がある。大規模言語モデルの一部は、有望な能力を示しているが、非公式な自然言語テキストで訓練・動作するため、その推論の正しさを検証するのは困難だった。Google DeepMind（英国）の研究者らは、強化学習を形式数学ソフトウェア環境（Leanと呼ばれる）内で機能させる方法を示した。これにより、推論が自動検証可能な証明を生成でき、この課題を克服する可能性がある。

AlphaProofは、数学的命題を証明するよう設計されている。このシステムは、8,000万の命題を自動形式化して訓練用データとした後、強化学習を通じてこれらの証明を見つけることを学習する。また、このシステムは、過去の数学競技問題において、従来最先端のAIシステムを上回る結果を示した。2024年には、AlphaProofは権威ある高校生レベルの数学競技会である国際数学オリンピックの複雑な問題に取り組んだ。AlphaProofは、幾何学問題解決システムAlphaGeometryと組み合わせて、競技会の6問中4問を解き、銀メダリストに相当する得点を達成した。

AlphaProofは、競技レベルの数学的推論分野で優れた性能を示したが、著者らはほかの難問形式の解決における限界を指摘し、今後の研究課題として提示している。これらの限界に対処することが、AlphaProofを複雑な数学的問題解決の有用なツールへと発展させる道を開くと結論づけている。

• Article
• Published: 12 November 2025

Hubert, T., Mehta, R., Sartran, L. et al. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature (2025). https://doi.org/10.1038/s41586-025-09833-y

News & Views: Mathematicians put AI model AlphaProof to the test
https://www.nature.com/articles/d41586-025-03585-5
 

doi: 10.1038/s41586-025-09833-y

「注目の論文」一覧へ戻る