アメリカのAI開発企業「アンソロピック」は、現在開発中の未公開のAIモデルが、数学界における最大の未解決問題の一つとされる「リーマン予想」の証明において、重要な進展をもたらしたと発表しました。
素数の分布に関する謎であるリーマン予想は、150年以上にわたり未解決のままであり、完全な証明には100万ドル（およそ1億5500万円）の懸賞金がかけられています。現在のAIモデルでも完全な証明には至っていませんが、今回の成果は、AIが新たな科学的・数学的アイデアを発見する能力を持っているという議論を再び活性化させるものとして注目されています。
アンソロピックによりますと、未公開のAIモデルはリーマン予想が成立する解の下限を大幅に引き上げることに成功したということです。
特に注目されているのは、その検証過程です。数学の専門的な訓練を受けていない同社のスタッフが、AIモデルに対して「証明に本格的に取り組むよう」指示を出したあと、モデル自身が1日半にわたって自律的に作業を調整したとしています。
この過程で、AIモデルは650種類の異なるアイデアを検証しました。合計60の「サブエージェント」と呼ばれるAIのプログラムが連携し、全体で3100万トークンを出力したということです。
論文の注記によりますと、60のサブエージェントのうち、2つが中核となる数学的アイデアの構築を担い、13がそのアイデアに貢献しました。また、30が新たなアイデアの構築を試みたものの失敗し、13が論理の正しさを確認する検証役を務め、残りの2つが初期の論文執筆を支援したとしています。
この発見は、アンソロピックの社内数学者2人によって確認され、オープンソースの証明支援システム「Lean」を用いて公式に証明されたということです。同社は今後もAIによる高度な推論能力の向上を目指す方針です。
大規模言語モデルによる数学分野での画期的な成果は、今回が初めてではありません。今年に入り、AIモデルによって複数の「エルデシュ問題」が解決されたほか、より高性能なモデルの登場により目覚ましい成果が報告されています。オープンAIも最近、社内モデル「アストラ」によって証明された10の主要な成果を公開しており、アンソロピックの別のプロジェクトでは長年の難問である「ヤコビ予想」の反証にも成功したとしています。
こうしたAIによる実績の増加は、数学界に期待と懸念の両方をもたらしています。今年6月に発表された公開声明では、著名な数学者のグループが、AIの普及によって「真の数学的証明は、発見の功績と正確性の責任を負う特定の著者に帰属すべきである」という数学界の重要な価値観が損なわれるおそれがあると懸念を表明しました。
一方で、新たな研究手法にどう向き合うべきか、専門家の間でも意見が分かれています。数学界の最高栄誉とされるフィールズ賞の受賞者であるティモシー・ガワーズ氏は、声明に対するブログ記事の中で、AIの影響が数学をより複雑で肯定的な方向に変えるのではないかと指摘しています。
ガワーズ氏は「数学の定理が数学者と結びつかなくなる世界が来たとしても、それは星に天文学者の名前がついていないことと同じであり、問題ではないのかもしれない」と述べています。
