人工知能：強化学習を用いた国際数学オリンピックレベルの形式的な数学的推論
Nature 651, 8106 doi: 10.1038/s41586-025-09833-y
人工知能（AI）の長年の目標は、広範な領域で複雑な推論を行うことのできるシステムの構築であり、無限に広がる概念と厳密な証明の要求を伴う数学はその典型的なタスクである。最近のAIシステムは、人間によるデータに依存する場合が多く、通常は正しさを保証するのに必要な形式的検証に欠けている。対照的に、Leanなどの形式言語は、推論の根拠を確かなものにする対話型環境を提供し、強化学習（RL）は、そうした環境における学習のための機構を提供する。今回我々は、数百万の自動形式化問題での訓練によって、RLを通じて形式的証明を見いだすことを学習する、AlphaZeroに着想を得たエージェントであるAlphaProofを提示する。AlphaProofは、最も困難な問題に対して、推論時に数百万の関連する問題を生成して学習することで、問題に固有の深層適応を可能にする手法であるテスト時RLを使用する。AlphaProofは、過去の数学競技問題について最先端の結果を大幅に向上させた。AlphaProofをコアの推論エンジンとして用いた我々のAIシステムは、2024年の国際数学オリンピックで5問の非幾何問題のうち3問を解き、その中にはこの競技で最も難しい問題も含まれていた。この性能は、AlphaGeometry 2と組み合わせて複数日にわたる計算によって達成されたもので、銀メダリスト相当の得点に到達し、これは我々の知る限り、AIシステムが何らかのメダルレベルの成績を達成した初めての例である。今回の成果は、根拠の確かな経験からの大規模学習が複雑な数学的推論戦略を持つエージェントを生成することを実証するものであり、複雑な数学問題解決における信頼性の高いAIツールに向けた道を開く。
