人工知能企業 Anthropic は、まだ公開されていない内部モデルが、数学史上最も重要な未解決問題の一つであるリーマン予想において顕著な進展を遂げたと発表しました。このモデルは、リーマン予想が成立するための最小解の下限を大幅に引き上げ、150年以上も数学界を悩ませてきたこの問題に新たな研究の手がかりを提供しました。現在、リーマン予想の完全な証明には100万ドルの懸賞金がかけられており、今のところ成功した者はいません。リーマン予想は、1859年にドイツの数学者ベルンハルト・リーマンによって提唱され、その核心命題は素数の分布の規則性に関わっています。
現代の人工知能モデルは完全な一般的証明を提供することはできませんが、Anthropicの最新の実験は、AIがこの分野での探索能力が外部の予想を大きく超えていることを示しています。この発見は、人工知能が独立して新しい科学や数学の思想を発見できるかどうかについての長期的な議論を再燃させる可能性があります。Anthropicによれば、深い数学のバックグラウンドを持たない内部の従業員がモデルに指示を出し、「真剣にリーマン予想の証明に挑戦するように」と求め、その後はモデルに自主的にタスクを進めさせました。次の36時間の間に、このモデルは650種類の異なる解法をテストし、60のサブエージェントが協力して作業を進め、合計で3100万トークンの計算資源を消費しました。
AIはリーマン予想研究において強力な潜在能力を示す
論文の脚注では、60のサブエージェントの役割分担が詳細に記録されています。その中で2つは核心的な数学的アイデアの開発を担当し、13は前者を補助するアイデアを提供し、30は新しいアイデアの開発を試みましたが成功しませんでした。13は検証者としての役割を担い、証明の正確性をチェックしました。最後に2つは論文の初稿作成を支援しました。この役割分担のモデルは、大規模言語モデルが複雑な数学問題において組織的な協調能力を示していることを示しています。異なるサブエージェントは、アイデア生成、検証、文書作成などのプロセスで効果的に協力しました。
この研究成果は、Anthropic内部の2人の数学者によって確認され、オープンソースの証明補助ツールLeanを用いて形式的に検証されました。Leanは、数学的証明のコンピュータ支援検証に使用されるプログラミング言語であり、自然言語で記述された数学的証明を機械が検証可能な形式的表現に変換することができ、証明の厳密性を保証します。これは、人工知能が数学の分野で初めての突破口を開いたわけではありません。今年に入ってから、いくつかのAIモデルがいくつかのエルデシュ問題を成功裏に解決しており、モデルの能力が向上するにつれて、得られた成果もますます注目されています。
数学界におけるAI研究ツールの受け入れには分裂が存在
OpenAIは最近、内部コード名Astraのモデルが10の重要な数学的成果に関する証明記録を発表し、Anthropicの別の独立した研究は長年存在していたヤコビ予想を成功裏に反証しました。これらの進展は、大規模言語モデルが数学の最前線の研究を推進する加速的な傾向を形成しています。しかし、AIが数学の分野に急速に浸透することは、学界内での興奮と懸念の両方を引き起こしています。今年の6月には、著名な数学者たちが共同で公開声明を発表し、人工知能が数学の核心的価値観を損なう可能性について懸念を示しました。
声明は特に、真の数学的証明は「具体的な発見者に帰属し、その発見に対して署名権を有し、正確性に責任を負うべきである」と指摘しており、AI支援の研究モデルはこの伝統的な基準を曖昧にする可能性があると述べています。しかし、数学界においてこれらの新しい研究ツールをどのように受け入れるかについては依然として分裂があります。フィールズ賞受賞者でケンブリッジ大学の教授であるティモシー・ゴールズは、声明に対する応答としてブログ記事でより複雑な積極的視点を提起しました。彼は「もし私たちが最終的に数学的定理が特定の数学者と関連付けられない世界に入るなら、それは星が天文学者の名前で呼ばれなくなり、さらにはほとんどの星が名前を持たないという事実よりも問題があるとは限らない」と書いています。
ゴールズの比喩は、数学研究が天文学的観測革命に類似したパラダイムシフトを経験している可能性を示唆しています。天文学者が望遠鏡を使ってますます多くの名前を付けられない天体を発見するにつれて、数学界もAIが生成した大量の成果に適応する必要があるかもしれません。