計算機科学：AIは数学の超難問にも対応できるようになった

国際数学オリンピックで出題されるような幾何学問題を解くことができる人工知能（AI）システムについて報告する論文が、今週、Natureに掲載される。このAIシステムの性能は、これまでで最高性能の定理自動証明システムを上回っている。今回の研究は、人間のトップレベルのパフォーマンスに近いレベルで複雑な論理問題に取り組むことができるというAIの可能性を実証しており、これを実現することが、AI研究の非常に重要な目標となっている。

数学オリンピックに出題されるような数学定理の証明問題を解くことは、高度な論理的推論能力と問題解決能力の証明となる。しかし、現在の機械学習ベースのAIシステムでは、数学定理を証明することは困難だ。機械学習は、AIの一分野で、コンピューターに参照データを読み込ませて特定のタスクの遂行方法を学習させるが、定理証明（特に幾何学の定理証明）に関しては、訓練データとして利用できる人間の実演が非常に少ないために習得が難しい。

今回、Trieu Trinhらは、人間の実演を必要としない新しい定理証明の方法について報告している。Trinhらが開発したAlphaGeometryというシステムは、数百万件ものさまざまな複雑度の定理と証明を合成して自律的に訓練を行うニューラル言語モデルを採用している。AlphaGeometryは、この方法と記号推論エンジン（難問における数多くの分岐点を検索できる）を併用して、人間による直接入力なしに複雑な問題を学習して解法を見つけることができる。

Trinhらは、2000～2020年の国際数学オリンピック（トップクラスの高校生を対象とした数学の定理証明コンテスト）で出題された問題（30問）を使って、AlphaGeometryを検証した。AlphaGeometryは、30問中25問を解いて、これまでの最高記録（30問中10問の正解）を塗り替え、平均的な国際数学オリンピックの金メダリストのパフォーマンスに近づいた。注目すべきことに、AlphaGeometryは、人間が読んで分かる形で証明を作成し、さらに、2004年の国際数学オリンピックの設問に示された定理については、より一般化された定理が存在することを発見した。

現在のところ、AlphaGeometryの能力は幾何学の特定の領域に限定されているが、Trinhらは、この方法が数学の他の領域にも適用できる可能性があると示唆している。

doi: 10.1038/s41586-023-06747-5

「注目の論文」一覧へ戻る