5月、OpenAIの内部モデルは1946年以来未解決だったエルデシュの単位距離予想に対する反例を発見した。多くの専門家が証明を試みてきたが、OpenAIは反例を見つけたのだ。1ヶ月後、OpenAIはサイクルダブルカバー問題の証明を公開し、7月までにさらに10の未解決問題の解決策を発表した。9月にはナビエ・ストークス方程式の証明も行った。Anthropicはフェルマーの最終定理の形式化を公開し、リーマン予想に関する進んだ境界を発表した。モデルは突然数学が得意になったのだ。
私が興味を持つのは、これらのモデルがどのような種類の問題を解くかを予測できるかどうかだ。問題をLLMにとって扱いやすくするものは何か、これらの解決策に共通するものは何か。AIが人間とは異なる方法で問題を解くなら、その違いを特定することで、どこにAIを向けるべきかを決める助けになるはずだ。単位距離の反証には最も豊富な解説があるので、そこから始めよう。
問題の複雑さ
簡単なメンタルモデルがある。任意の問題を解くには、一連のヒントや洞察と、それらの間の作業が必要だ。これは驚くほど単純な日常問題から、一般相対性理論のような複雑なアイデアにもよく当てはまる（ボーナス参照）。その順序は次のようになる：
洞察 → 時間/努力 → 洞察 → 時間/努力 → 解決。
専門家は初心者よりも背景知識が多いため、必要なヒントは少なくて済む。単位距離証明に関するWTガワーズの解説では、彼は同様のアイデアを使っている。証明の難しさは、専門家がそれを再構築できる最短のヒント列の長さだと。彼はこれを専門家に対するコルモゴロフ複雑性と呼ぶ。単位距離問題の場合、彼のヒント列は3つの部分から成る：
反例を探す。
最もよく知られた構成を一般化する。
次数を増やす数体の列を試すが、有界ノルムの素イデアルで作業する。
ガワーズが提案する複雑さの公式は2^k + tで、kは最短ヒント列の長さ、tはそれを発展させるのに必要な作業量だ。これは厳密に見えるが、実際に数を当てはめようとするとそうでなくなる類の公式で、まさにそれがポイントだ。複雑さは問題を解くのに必要な洞察の数に対して指数関数的に増大する。
問題解決のほとんどはこれらの洞察の間の作業だ。ひらめきが訪れ、その後何ヶ月もかけてヒントを発展させ、次の概念的飛躍が可能になる。専門家にとって、費やした時間はこの作業の有用な代理指標であり、したがってtだ。最初の単位距離ヒントを誰かに与えても、一般化された構成に到達するには十分な作業が必要だ。
有用だが事後的だ。問題を見て、x個のヒントが必要だと予測することはできない。だから、問題の年齢、試行回数、付随する賞金が難易度を表す一般的な代理指標となる。
与えられたヒントの特性
典型的な洞察は問題の定式化を変える。問題の表現と理解が変わる。ヒントの価値を決める2つのことがある：
ヒントを与える前はどれほどありそうに思えなかったか、与えた後はどれほど明白に見えるか → これは人々が思うより難しい。単位距離では、多くの専門家が反例をありそうだとは考えなかった。
列のどこに属するか：ヒントには順序がある。3番目のヒントは、最初の2つの作業が十分に進んで実行可能になって初めて役立つ。これは、千の数学テクニックをリストしてすべての組み合わせを試すという素朴な力技のアイデアを打ち負かす。ヒント列は木をたどる。最初の洞察が問題を変え、続く選択肢を明らかにする。
人間は幅優先で問題を解く
kとtを組み合わせると、人間の探索パターンが得られる。候補の方向を生成し、浅く探索し、ほとんどを放棄し、いくつかにコミットする。有望な方向も、早期に十分な励みが得られなければ放棄される。これは人間の制約だ。アイデアの発展には何ヶ月もかかることがある。コミットする前に、研究者はそれがどこかに通じるという理由を必要とする：概念的約束、初期結果、または類似問題の経験。見つけるのに時間がかかるほど、試すためのハードルは高くなる。
ほとんどの研究ソフトウェアは、退屈で機械的で反復的な作業を自動化することでこの時間を短縮するために存在する。AIはそれを十分に短縮し、探索パターン自体が反転し、下流のすべてがそれに続く。
AIと複雑さ
まずt。モデルにとっての努力の等価物は計算とトークンで、1つの軌跡に費やされる（テスト時計算）か、並列エージェントに分散される（並列テスト時計算）。事前学習も、人間の研究者が探すか再構築する必要がある知識を提供する。個々の専門家はすべての過去の展開を認識しているわけではないので、時にはすでに行われたことをやり直すことになる。
より大きな違いはモデルの探索方法だ：
LLMは深さ優先
モデルに単一のプロンプトを与えると、解決策を返す。正しいかもしれないし、そうでないかもしれない。証明を求めると、良い証明に近いものを返す。これらのモデルのCoTも貪欲な深さ優先の方法で実行される。そしてプロセスはスケールする。並列エージェントに10のアプローチを与えると、結論に向けて発展した10の試みが得られる。すべて異なるかもしれないし、一部重複するかもしれない。それぞれが障害にぶつかるか、正しいように見える議論を生み出す。放っておくと、美しい誤った証明が得られる。
これは計算と資源の無駄のように思えるが、完成した軌跡を剪定して正しいものを特定できる自動検証器を追加するまでは。このチェッカーがあれば、不確実なアイデアに膨大な計算を費やすことが合理的になる。与えられたアイデアが機能するかどうかは数分でわかる。問題は、検証器が完成した議論しか判断できないことだ。半分発展したアイデアがどこかに向かっているかは教えてくれない。
対比
5分で機能するかどうかわかるなら、ヒントはどれほど良い必要があるか？人間にとっては、ヒントを追求するのに何ヶ月もかかる可能性があるため、品質の基準は高い。モデルにとっては、基準はほとんど消える。ヒントはありふれたものでも、ありそうにないものでも、ほとんど形成されていなくてもよい。それをたどることで、どこかに通じるかどうかが確立される。LLMは時間を計算と交換することを可能にし、より短い期間でより多くの問題を追求するのに役立つ。
失敗した試みはLLMへのヒント
モデルは決定的な方向性がなくても始められる。事前学習はすでに問題の歴史と過去の試みについての事前知識を与えている。間違った解決策はすべて、次の反復のための負のヒントとしてモデルに戻すことができる。システムはすでに失敗したこととその理由についての指示を蓄積する。大まかに言って、ハーネスは次のようになる：
ドラフター：ソルバーモデルに与えるプロンプトを書く。プロンプトはモデルの事前知識に基づき、前回の実行からのエラーを軽減し、行き止まりになったすべての有望なパス（これらは負のヒント）を考慮に入れる。
ソルバー：プロンプトを受け取り、1つまたは複数の候補解を思いつく。複数のサブエージェントを実行し、並列テスト時計算を使用して異なるパスを追求できる。
検証器/チェッカー：議論が有効で、要求された結果を確立しているかをチェックする。
たとえば、このCDCプロンプトを考えてみよう：
このタスクの目的のために、完全な肯定的証明が存在すると仮定する。→ これは、事前学習中に学んだ問題の未解決状態を、モデルが停止する理由として扱うのを防ぐ。
特に、特殊なグラフクラスの証明、一部のエッジが2回以外でカバーされるサイクルカバーの構成、有界長または指定サイクルの変種、別の未証明予想への還元、任意の固定グラフサイズでの計算検証、完全な非存在証明なしの候補反例は不十分である → これは実際の問題を解くための代替手段のカタログを排除する。
全体を通して敵対的エージェントを使用する：すべての候補証明は、正確な2重複、サイクルを装った繰り返しエッジの閉じたトレイル、平行エッジの2サイクル、非連結グラフ、切断頂点、還元によって導入されたブリッジ、CDCの同等ステートメントの循環使用についてチェックされなければならない → カタログ化された失敗モードは常設のチェックに昇格する。
さらに、学習された怠惰に対する1行：現在のアプローチが失敗した、またはエージェントが定理強度のギャップを報告したという理由だけで戻ってはならない
OpenAIはおそらく複数ラウンドの試みを実行し、ドラフターはエラーと失敗したアイデアを取り、次の反復をそれらから遠ざけた。これらの行のそれぞれが、指示として書かれた失敗したパスだ。
単位距離証明とツィマーマンの仕事の再構築
ガワーズの3つのヒントをハーネスのレンズを通して読んでみよう：
ヒント1：反例を探す：これは本当に難しい。なぜなら、コミュニティとモデルの事前学習の事前知識の両方が予想は真実だとしているからだ。ドラフターは最ももっともらしく、ソルバーが証明を追求し続けて失敗したためにこれに到達した。この枠組みは、モデルが受け入れられた見解を追求しなければならない方向として扱うのを止める。すべての失敗した試みは、反例を少しだけありそうにする。
ヒント2：最もよく知られた構成を一般化する。コミュニティの事前知識に最も近い。これは標準的な動きだ。実質的な作業は、一般化を十分に発展させて、それが何を許すかを発見することだ。これは大きなtのステップだ。しかし注意してほしい。これは反例の一般化であり、ほとんど誰も探していなかったものだ。
ヒント3：次数を増やす数体を試す。最初の2つのヒントが適用される空間を構築した後の標準的な機械だ。
順序が重要だ。ヒント3から始めると、その演習が反証であることさえわからない。一般化された構成を飛ばすと、ヒント3は作用するものがない。そして3つすべてがあっても、努力は膨大なままだ。反例のヒントは後から見れば明白で、なぜ誰も試さなかったのか不思議に思う。実際、何人かは試した。
最近OpenAIに雇われたジェイコブ・ツィマーマンは反例に取り組んだ。彼は数論を知っていた。次数を増やすことも考えた。そして彼は立ち止まった。反例を探すことは最初の洞察だった。それはまだ始まりに過ぎなかった。彼を止めたのはスキルの欠如ではなかった。それは、数週間沼地にいて、向こう岸があるという証拠がないという、適切に正気な感情だった。彼自身の言葉：
「非常に恐ろしいダイナミクスで、分析的体制を考え抜き、導きの直観を保持するのは難しく、多くの時間を消費し、しばしばうまくいかない。」
ジェイコブ・ツィマーマン、OpenAI数学者
心理学は何十年も前に問題解決のこの人間的側面を発見した。メトカーフとウィーブは15秒ごとに解く人に解決にどれだけ近いと感じるかを尋ね、通常の問題では報告された進歩感は上昇した。洞察問題では、答えを見つけるまで平坦なままだった。彼らは探索を維持する進歩感を報告しなかった。洞察問題には勾配がない。解くまでどれだけ近いかわからない。
したがって、専門家の問いは二重だ：誰かがそもそもその枝に入るか（ヒント）、そして入った後、通常の能力が仕事を終えるのに十分なほど長く留まるか？留まるコストはワーキングメモリ、士気、キャリアだ。そしてすべての既知の専門家が間違っていると考えるパスに留まることは、これら3つすべてを悪化させる。LLMにとって、これは大きな利点だ。アルル・シャンカールから：
「モデルはアイデアをかなり迅速に進めたが、決定的なアイデア（「楽観的に仮定すると...」で始まる段落）に達すると、証明にかなり組織的に取り組んだ。」
これは2つの問いに圧縮される：問題はいくつの洞察を必要とするか、そして方向が価値があるかどうかを判断する前に、それらの間にどれだけの作業があるか？ツィマーマンはAI側をこう述べる：
「これはAIシステムが優位に立つ一つの方法を示しているかもしれない。それは、既知のすべての方法を試すことができるだけでなく、数学者が圧倒されることなく、より長く、より危険な水域でプレーできることだ。もちろんこれはまだ堅牢に真実ではないが、これは前兆となる出来事かもしれない。」
他の証明
OpenAIのナビエ・ストークス方程式の証明は同じプロセスを示している。ざっと読んだところ、それは行われた作業を完了させる