計算機科学：人間による論証なしに数学オリンピックの幾何学を解く

数学オリンピックレベルの数学定理の証明は、大学以前の数学において世界で最も秀でた人々の間でその難しさがよく知られているため、人間レベルの自動推論における注目すべき節目となる。しかし、現在の機械学習手法は、人間による証明を機械検証可能な書式に翻訳するコストが高いため、数学領域の大半には適用できない。幾何学については、翻訳に独特の難しさがあるため、訓練用データが極めて少なく、問題はさらに深刻である。今回我々は、さまざまなレベルの複雑さにわたって数百万の定理と証明を合成することで人間による論証の必要性を回避する、ユークリッド平面幾何学の定理証明器AlphaGeometryを提案する。AlphaGeometryは、我々の大規模な合成データで最初から訓練されたニューラル言語モデルを用い、困難な問題における無限の分岐点を通ってシンボリックな演繹エンジンを導く、ニューロシンボリックなシステムである。AlphaGeometryは、最新の数学オリンピックレベルの問題30問からなる検証セットにおいて25問を解き、10問しか解けなかった従来の最良の手法を上回るとともに、国際数学オリンピック（IMO）の平均的な金メダリストの成績に近づいた。特筆すべきことに、AlphaGeometryは、人間が読み取れる証明を生成し、人間の専門家による評価の下で2000年と2015年のIMOの幾何学問題を全て解き、翻訳された2004年のIMOの定理の一般化版を見いだした。

目次へ戻る