AIがまたもや世紀の難問を解く：ヤコビアン予想が覆される

7月21日、世界の目がワールドカップ決勝に釘付けになっている間、AIモデルが1939年以来数学者を悩ませてきた問題を解決した。ロンドンのインペリアル・カレッジのケビン・バザード氏が翌朝目覚めた時には、結果は既に検証されていた。昼食時には、彼の純粋数学科の同僚たちの話題はそれ一色となり、本稿執筆時点では、Anthropic社員レヴァント・アルペーゲ氏が結果を発表したXの投稿は2000万回以上の閲覧数を記録している。

問題はヤコビアン予想と呼ばれ、ドイツの数学者オットー＝ハインリッヒ・ケラーによる1939年の研究に端を発する。本質的には、数学者が「写像」と呼ぶものに関する問題であり、出力の集合が与えられたときに入力を決定できる条件を問うものだ。その基礎は、さらに1世紀前のドイツ人数学者カール・グスタフ・ヤコブ・ヤコビのヤコビアン行列式にある。現代の数学者たちはケラーの予想を証明することも、反証することもできずにいた。

アルペーゲ氏の結果は、空間内のすべての点でヤコビ行列式が一定値-2であるにもかかわらず、異なる3つの始点を同じ終点に写像することを示した。つまり、テストに合格しなかったため、ヤコビアン予想は誤りである。バザード氏はこの結果を「非常にエキサイティング」と評し、言語モデルが最終的に、約5年前にGoogle Deep Learningの科学者クリスチャン・セゲディ氏が警告した「スーパー数学者」に到達する可能性を示していると述べた。

しかし、これは数学者たちに不足感も残した。シカゴ大学のアクヒル・マシュー氏は、現在のAIモデルで純粋数学を解く場合、「どのように」は得られても「なぜ」は得られないと指摘する。同氏は「正しいことは検証できるが、物語を語ることができればなお良い」と語った。

数学者たちは以前にも自動化に直面してきた。ほとんどの人は数学を計算と見なすが、コンピューターは数十年前にその分野を征服した。しかしバザード氏は、大学の高等数学で数学が実際には推論であることを学ぶと説明する。理解とは「脳内に適合させる」ことであり、アイデアから結果を再生成できるようになることだ。形式数学では、その理解は論理的なステップの連鎖である「証明」によって示される。しかし、AIはまだそのような証明を生成する能力を持っていない。

バザード氏のキャリアプロジェクトは、疲れ切った博士課程の学生ではなく機械によって証明をチェックするプログラミング言語「Lean」である。同氏によると、彼が目覚めた時には証明はすでにLeanでチェックされていた。証明作成モデルと彼の証明チェックマシンが出会う時、数学における人類の最後の利点の一つが消える。

マシュー氏はより慎重で、この瞬間を「非常に急速で不安な変化」とし、特に若手数学者にとってそうだと述べた。コロンビア大学のマイケル・ハリス氏は6月のエッセイで、AI業界は推論を商業的に無価値と扱い、人間の数学者を「知能のベータ版」と見なしていると書いた。しかし同氏は、数学は疎外されない労働の最後の例の一つであり、人々が「遊びながら」生計を立てられる分野だと主張する。

しかし、数学者が「遊ぶ」ために公的資金を提供することに一般大衆が魅力を感じないかもしれない。AIが仕事を脅かす前から、トランプ政権の国立科学財団予算削減により数学研究への連邦資金は約72%減少している。一流研究大学の博士課程入学率は今秋15%減少し、2年連続の縮小となっている。

一部では、数学の専門職化の終焉は良いことだと考える。機械が「遊び」全体を民主化するというのだ。Yコンビネーターのギャリー・タン社長はXで「ジェントルマン科学者」の時代の復活を歓迎した。しかしアルペーゲ氏は趣味人ではない。彼はハーバード大学の卒業生総代であり、この種の問題をアルゴリズムで計算することに10年を費やしてきた。

バザード氏は、人間を数学のループに留める鍵は「味覚」、すなわち何を問うかを知ることにあるかもしれないと述べる。「人々は機械に質問させようとしてきたが、それらはひどいものだ」と同氏は言う。「質問はすべて退屈か、明らかに正しいか、明らかに間違っているかのどれかだ。」数学の金字塔―リーマン予想やケラーのヤコビアンなど―は、解決者ではなく提起者の名を冠している。「それは偶然ではない。正しい質問を思いつくには、優秀な数学者でなければならないのだ。」