人工知能（AI）が単純な計算を越え、複雑な数学理論を自ら証明する段階に達した。
グーグル・ディープマインドの研究陣は13日、国際学術誌「ネイチャー」にAIシステム「アルファプルーフ（AlphaProof）」に関する研究成果を掲載した。2024年7月にアルファプルーフが国際数学オリンピック（IMO）で銀メダル水準の成績を収めたのに続き、作動原理が学術的に検証された格好だ。
数学者は新しい理論を証明するために数年、時には数十年を研究する。証明は論理的に完璧でなければならず、一行の誤りも許されないためだ。これまでAIが数学の問題を解いたり予測モデルを作ることは可能だったが、証明という領域は異なっていた。言語モデルが生み出す説明の大半は自然な文章で構成されており、論理の正確さを機械的に検証するのが難しかった。
ディープマインドの研究陣はアルファプルーフを通じ、人間のように複雑な数学的推論を実行できるAIの可能性を示した。研究陣はリン（Lean）という数学証明用プログラミング言語を用い、すべての数学的表現と推論を形式化した。こうして構築した環境では、コンピューターが証明の正誤を自動で判別できる。
ここに強化学習を組み合わせ、AIが自ら問題に取り組み、正解に近い方式を見いだしながら、より複雑な証明を学習していった。強化学習とは、AIが自律的に試行し、正解に近いほど高い得点を受け取り、次第により良い解法を見つけていく学習手法である。
アルファプルーフは8000万件以上の数学命題を自動で形式化して学習した。特に難題を与えると、関連する数百万件の変形問題を生成し、これをリアルタイムで学習して適応力を高めた。
その結果、アルファプルーフは幾何問題解決AIの「アルファジオメトリー（AlphaGeometry）」とともに、2024年のIMOの6問のうち4問を解いた。これは人間参加者基準で銀メダルに相当する成績である。当時、AIが初めてIMOのメダル圏に入った事例として記録された。
研究陣は今回の論文を通じ、AIがどのように数学を理解し証明を学習したのか、そしてその過程が人間の論理的推論とどの点で似ているのかを説明した。研究陣は「大規模強化学習と形式論理環境の結合が、複雑な数学的思考を可能にした」と述べ、「この方式は今後、信頼できる数学AIツール開発の土台になる」と説明した。
研究に参加していないタリア・リンガー（Talia Ringer）米国アーバナ・シャンペーンのイリノイ大学教授は「アルファプルーフは数学の証明を一種のゲームのように学習するシステムだ」と評価した。さらに「アルファプルーフは学生が数日間解けなかった定理を1分で証明し、誤った定義を見つけ出して問題の誤りを指摘した」と付け加えた。
リンガー教授は「最近、OpenAIとグーグルが今年のIMOの問題で金メダル水準の成績を出した」と述べ、「AIの数学的推論能力が急速に進化している。この分野で一種の『宇宙競争』が始まった」と表現した。
しかし数学者の反応は分かれた。ケビン・バザード（Kevin Buzzard）インペリアル・カレッジ・ロンドン教授は、アルファプルーフが数学界の著名な難題であるフェルマーの最終定理の証明をリン言語に移すのにあまり役立たなかったと評価した。バザード教授はこれについて「自分の経験では、これまでいかなるAIシステムも使える水準に達していない」と述べた。
研究陣もこうした限界を認め、「アルファプルーフが競争水準の数学問題を解く能力は立証したが、依然として一部の複雑な問題や直観的推論が必要な領域では限界がある」とし、「これらの課題を解決できれば、アルファプルーフが今後の数学研究の強力な助力者になると見込む」と付け加えた。
参考資料
Nature（2025）、DOI: https://doi.org/10.1038/s41586-025-09833-y
Nature（2025）、DOI: https://doi.org/10.1038/d41586-025-03585-5