グーグルDeepMindは現地時間7月25日、同社の強化学習ベースのシステム「AlphaProof」が、国際数学オリンピック(IMO)の問題を解く能力において銀メダル相当の成績を収めたと発表。全6問のうち4問に正解し、42点満点で28点を獲得した。言語モデルは同社の「Gemini」ベース。
AlphaProofは、関数型言語「Lean」を用いて数学的証明をするように設計されているのが特徴。事前に訓練された言語モデルと、チェスや将棋、囲碁などのゲームで学習したAlphaZeroの強化学習アルゴリズムを組み合わせている。
Leanを用いることで、数学的推論の正確性を厳密に検証することができるようになったという。これまでの自然言語ベースのアプローチでしばしば問題となる「もっともらしいが誤った」中間推論ステップや、ハルシネーション(幻覚)を含む解答を生成する問題を回避できる利点がある。
AlphaProofの訓練過程では、幅広い難易度と数学分野をカバーするため、数百万もの問題を証明または反証した。さらに、IMO(コンテスト)の本番中も、完全な解決策が見つかるまで問題の自己生成を繰り返したという。
AlphaProofについての技術的な詳細は近日発表予定。