詳細を読む
Anthropicは8月10日、未公開の最新モデルが150年以上未解決のリーマン予想で大きな前進を示したと発表しました。仮説が成り立つ解の下限を大幅に引き上げた成果で、結果は社内の数学者2人が確認し、証明支援ソフトLeanで形式化されています。AIが新しい数学的アイデアを生み出せるのかという長年の問いが、改めて突きつけられています。
注目されたのは達成の過程です。数学の専門教育を受けていない同社の社員が「本気で証明に挑んでみて」と促しただけで、モデルは1日半にわたり作業を自律的に進めました。合計で650通りのアイデアを試し、60体のサブエージェントを統括して3100万トークンを出力しています。
60体の内訳も論文の脚注で示されました。鍵となる数学的アイデアを生み出したのは2体のみで、13体がそれを補助し、30体は新しい発想に至りませんでした。残る13体は論証の正しさを検証し、2体が論文の初稿を書くなど、分業と相互検証を組み込んだ体制が成果を支えた形です。
数学へのAI進出はAnthropicだけではありません。OpenAIは未公開モデル「Astra」で長年の未解決問題10件を解いたと公表し、高次元での球の詰め込みや誤り訂正符号など、データ圧縮や暗号に直結する領域も含まれていました。7月にはAnthropicのモデルがヤコビアン予想を反例で覆しており、成果の連鎖が続いています。
一方で数学界には戸惑いが広がっています。6月に公表されたライデン宣言には3400人以上が署名し、証明は責任を負う特定の著者に帰属すべきだという価値観が損なわれかねないと警告しました。OpenAIの発表では非ソフィック群の成果をめぐり先行研究者の貢献を軽視したとの批判が出て、同社は後に表現を修正しています。
懸念の中心にはお金と人材もあります。Astraの10件の解答は約2000ドル相当のトークンで生成できたとされますが、研究費の乏しい大学が締め出される恐れが指摘されています。フィールズ賞受賞者のジェームズ・メイナード氏は、今回の成果を印象的だとしつつ概念的な飛躍とまでは言えず、評価にはまだ時間が必要だと語っています。