AI

AI「Claude Fable 5」が87年来の難問「ヤコビアン予想」を覆す反例を生成したとAnthropic研究者が報告


Anthropicに所属する数学者レベント・アルポゲ氏が、AIモデル「Claude Fable 5」を使って87年間未解決だったヤコビアン予想の反例を発見したと報告しました。


異なる複数の入力に対して同じ出力を返す関数では、出力だけを見ても元の入力を1つに決められません。数学では出力から入力へ戻す処理を「逆関数」と呼びますが、同じ出力に複数の入力が対応する関数は空間全体で入力を一意に復元する逆関数を持てません。

一方で多変数の関数が狭い範囲で元に戻せるかどうかは「ヤコビアン行列式」と呼ばれる値で調べられます。ヤコビアン行列式は各入力点で計算され、その点の近くにおける面積や体積の変化を一次近似で表す値で、ヤコビアン行列式がゼロであればその点での一次近似は少なくとも1方向の変化を失っており、その点の近くで出力から元の入力へ一意に戻せるとは保証できません。逆にゼロでなければその点での一次近似はどの方向の情報も失っておらず、少なくとも近くの範囲では入力と出力を逆にたどれることが保証されます。


ドイツの数学者オット=ハインリヒ・ケラーが1939年に一般形を定式化したヤコビアン予想は「複素数のn変数を同じn変数へ写す多項式写像においてヤコビアン行列式がゼロではない定数なら、多項式で表せる逆写像が存在するはず」と主張する問題です。「各点の近くで逆にたどれる」という局所的な性質から、「空間全体でも異なる入力が重ならず多項式の逆写像を持つ」と導けるかを問う問題で、過去にはヤコビアン予想を証明したとする論文が何度も発表されたものの、後から誤りが見つかっていました。

数学者アキル・マシュー氏から反例を探す案を持ちかけられたアルポゲ氏は、サッカーのワールドカップ決勝が行われている間にFable 5へ問題を検討させたとのこと。Fable 5が発見した多項式写像のヤコビアン行列式は常に-2という一定値を取るものの、「(0, 0, -1/4)」「(1, -3/2, 13/2)」「(-1, 3/2, 13/2)」という3つの異なる入力が「(-1/4, 0, 0)」という同じ出力を返し、「空間全体で逆写像を持つ」というヤコビアン予想が、3変数以上では偽であることが示されました。


ただし生成AIが数式を提示しただけでは、数式が反例として正しいとは確認できません。数式の展開や代入計算に小さな誤りが含まれていれば結論全体が崩れるため、反例を人間や検証ソフトウェアが独立して確認する必要があります。

そこで、公開後には定理証明支援システム「Lean」を使った形式化も進められました。インペリアル・カレッジ・ロンドンの博士課程で形式化数学などを研究するポール・ルゾー氏が反例をLeanで記述し、Google DeepMindが管理する数学予想のリポジトリ「Formal Conjectures」へ提出しました。記事作成時点でプルリクエストは審査中ですが、数式のヤコビアン行列式が-2になることや、異なる入力が同じ出力になるため写像が単射ではなく空間全体で逆写像を持たないことを確認できる状態になっています。

形式化数学プロジェクトのXena Projectは、次の課題は反例が正しいかを確かめることだけではなく、反例がなぜ成立するのかを人間が理解することだと述べています。

・関連記事
OpenAIが80年近く未解決だった数学予想の反証に成功、人間の数学者も「AIが補助役を超えた」と驚く発見 - GIGAZINE

専門家が60年解けなかった数学問題を23歳のアマチュアが解決、鍵はChatGPTの使い方 - GIGAZINE

数学研究におけるAI革命が到来、数学者たちは「これはまだ始まりに過ぎない」と考えている - GIGAZINE

16人の数学者がAIの精度や信頼性など数学分野への潜在的な脅威について警告する「ライデン宣言」を発表 - GIGAZINE

ChatGPT 5.5 Proが博士課程レベルの数学研究を1時間で実行、数学者が「人間の研究の最低ラインが変わる」と指摘 - GIGAZINE

in AI, Posted by log1d_ts

You can read the machine translated English article Anthropic researchers report that the AI….