Google DeepMindが開発したAIシステム「AlphaProof」が、国際数学オリンピック（IMO）で銀牌を獲得した成果の技術的裏側が、11月12日に《自然》誌に掲載された論文で初めて全面公開された。2024年のIMOでは、AlphaProofと専用の幾何処理システム「AlphaGeometry 2」が連携し、6問中4問を正解。28点の得点は、当該大会の上位10％に相当し、銀牌レベルの成績を達成。特に、正解者がたった5名の「第6問」を完答した点は、AIが数学的証明の最高峰の難問に挑戦し、人間の水準に到達した証拠と評価されている。 AlphaProofの核心は、形式化数学言語「Lean」を用いた厳密な証明生成と、強化学習による効率的探索の統合にある。従来の大規模言語モデルは、見た目は正しいが内容に誤りを含む「幻覚」を起こしやすい。しかし、Leanはすべての証明ステップを自動検証可能で、誤りが発生した場合に即座に検出できる。この信頼性を活かすため、研究チームはGeminiモデルを微調整し、自然言語の数学問題をLean形式に自動変換する「自動形式化」技術を開発。これにより、100万件の自然言語問題から8,000万件のLean証明文を合成し、強化学習の学習データを大幅に拡充した。 システムの構造は、AlphaZeroのアーキテクチャを踏襲。30億パラメータの変換器ネットワークが、Leanの証明状態を理解し、次の戦略（戦略ネットワーク）とその道筋の価値（価値関数）を出力。これらをもとに、特徴的な「積ノード（product node）」を用いた木探索アルゴリズムが、複数の子目標を同時に処理し、効率的に証明を進める。特に注目すべきは「テスト時強化学習（Test-Time RL, TTRL）」。難問に対して、AIは自ら問題の変形を生成し、易しいものから段階的に学習。このプロセスにより、第6問の複雑な証明に成功した。 AlphaProofは、人間の選手と異なり、問題解決に数分から3日間と時間差が生じるが、研究チームは「速度ではなく、証明の正しさと深さ」を重視。数学界の専門家も、この成果を「顕著な進歩」と評価。一方、2025年にはDeepMindは、自然言語で直接証明を生成する「Gemini Deep Think」を発表。4.5時間の制限内に35点（金メダル）を獲得し、形式化言語を経由せずに人間の理解に近い証明を生成。これは、形式化と自然言語の両道が今後統合される可能性を示唆している。 AlphaProofは、AIが数学的証明の「信頼性」を保証する道を開き、今後のAIと人間の協働の基盤を築いた。今後は、自然言語から形式化への自動変換、組合せ数学の弱さの克服が課題となる。