人工知能：数学競技でメダル級のAIシステム
Nature
複雑な数学理論を証明できる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
An AI system that can prove complex mathematical theories is described in Nature this week. The system, Google DeepMind’s AlphaProof, has achieved a silver medal-worthy performance at the 2024 International Mathematics Olympiad (IMO).
Mathematicians use computational tools to solve complex problems and prove theories. AI systems could possibly speed up this process. While some large language models have shown promising capabilities, it has been difficult to verify the correctness of their reasoning as they are trained and operate on informal, natural-language text. Researchers at Google DeepMind show how reinforcement learning can be made to work within a formal mathematics software environment (known as Lean) to generate proofs whose reasoning can be automatically verified, potentially overcoming this challenge.
AlphaProof is designed to prove mathematical statements. It learns to find these proofs through reinforcement learning, after auto-formalizing 80 million statements to use for training. The system is shown to improve on results from previous state-of-the-art AI systems for historical mathematics competition problems. In 2024, AlphaProof tackled complex problems from the IMO, a prestigious high-school-level mathematics competition. AlphaProof, combined with a geometry-solving system called AlphaGeometry, solved four out of six problems from the competition, achieving a score equivalent to that of a silver medallist.
While AlphaProof has demonstrated impressive performance in the domain of competition-level mathematical reasoning, the authors note some limitations in solving other forms of difficult problems, which they suggest as avenues for future research. They conclude that addressing these limitations will pave the way for AlphaProof to become a valuable tool in complex mathematical problem solving.
- 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
「Nature 関連誌注目のハイライト」は、ネイチャー広報部門が報道関係者向けに作成したリリースを翻訳したものです。より正確かつ詳細な情報が必要な場合には、必ず原著論文をご覧ください。
