LLMによる予想生成 vs 証明検証、勝者はどっち

コーヒーを二杯目と三杯目の間くらいで、最近多くの計算量理論の研究者が、予想していなかった一文を読むことになった。任意のブール式の充足割り当て数を、およそ2^(n/√(log n))の時間で数える決定的アルゴリズムだ。これは準指数時間であり、この分野を支える前提の一つである指数時間仮説（ETH）を反証する、という厳密な技術的意味での準指数時間だ。この主張は大学の研究グループからarXivに出たものではない。AIラボから出たもので、証明は大規模言語モデルとの共同作業で作られたという。発表についてどう思うにせよ、予想生成、つまり機械が数学を採点するだけでなく新しい数学を提案する段階が、デモの域を出た瞬間だといえる。

ラボは三つの成果をまとめて発表した。先ほどの計算量理論の爆弾級の結果、全次元におけるケークヤ予想の証明の主張、そして標準模型の統一的な完成と称する物理学の結果で、後者は形式検証を待って保留されている。反応は見慣れたパターンに分かれた。内容には本気で驚かれ、発表の見せ方には本気で苛立たれた。批評家は、自転車メーカーが自転車レースでの自社の勝利を自ら発表するようなものだ、と例えた。的を射ている。それでも内容はもっとじっくり見る価値がある。この発表には、言語モデルが数学に関わる二つの全く異なる方法と、そのどちらを本当に信頼すべきかについての、実用的な教訓が埋め込まれているからだ。

AI数学発表が実際に主張していること

まずは計算量の結果から見よう。利害が最もはっきりしているからだ。指数時間仮説は大まかに、3-SATは2^o(n)の時間では解けないと述べる。つまり、変数の数に対して意味のある形で準指数的なアルゴリズムは存在しない、という主張だ。パラメータ化計算量やきめ細かい計算量の論文は何百本もこの仮説に頼って下限を証明している。「ETHを前提とすれば」という定理を積み重ねてキャリアを築くような、そういう類の前提だ。新しいプレプリントは、k-CNF式に対する決定的な計数アルゴリズムを記述している。空間計算量は多項式で、時間は2^(n/(log n)^(1/2+o(1)))に多項式因子を掛けたものだ。指数部はo(n)であり、まさにETHが禁じている形だ。このアルゴリズムは相変わらず絶望的に遅く、実際のインスタンスに走らせようとする人は誰もいないだろう。それでも漸近的には決定的だ。証明が正しければ、二十年にわたって下限の議論を支えてきた仮説が、そのまま存在しなくなることになる。

二つ目の主張はケークヤ予想を対象にしている。単位線分をあらゆる方向に含む最小の集合は何か、という幾何測度論の問題だ。三次元の場合は2025年になってようやく解けた。Hong WangとJoshua Zahlによる見事な証明で、多くの人がキャリアの集大成とみなした。今回の発表は全次元での証明を主張しており、それが成立すればあの成果を完全に包含することになる。三つ目の結果は量子場の理論に関するもので、三つの中で最も曖昧だ。「標準模型の統一的完成」と説明されているが、まだ公開されておらず、機械による形式検証の完了を待っているようだ。予告を読んだ物理学者たちは、真の万物理論というより大統一理論の系譜にあるものだろうと推測している。その言い回しには、疑いの目を向けるだけの正当な理由がある。

今回の展開には評価すべき点が二つある。まず、ラボは公開前に実際の数学者や物理学者を巻き込んだ。これは、以前のもっと雑な数学発表が招いた反発への直接の対応で、その後Terence Taoらが、まさにこうした関与を公に求めていた。そして物理の結果は、形式化が完了するまで公開されなかった。優先順位として正しい対応だ。とはいえ、答えの出ていない問いも残っている。計算資源にかかった費用は外部には分からない。同じ資金を人間の研究者に向けていれば同じ定理が得られたのか。そして営利企業は、株主が口を出すようになったあとも、好奇心に基づく研究に資金を出し続けるのか。批評家がすぐに指摘したのは、居心地の悪い循環もある点だ。これらのモデルは、いま称賛を求められている研究コミュニティ自身の問題、草稿、フォーラムの投稿を一部学習に使っているのだ。

証明検証と予想生成：二つの異なる仕事

誇大広告を取り除くと、AIを使った数学のシステムはどれも二つのどちらかの仕事をしている。一つ目は証明検証で、与えられた論証が妥当かどうかを判定することだ。二つ目は予想生成で、ある問題領域に対して、補題、構成、アルゴリズム、反例など、試す価値のあるものを提案することだ。両者は一つの技能の二つの半分のように聞こえる。だがそうではない。オラクルも失敗の仕方も信頼の性質も根本から違う別の計算問題であり、両者を混同すると、プレスリリースを過剰に信じるか、本物の進歩を無視するかのどちらかに陥る。

検証にはオラクルがある。Leanで書かれた証明はカーネルに対してコンパイルできるかできないかのどちらかで、著者がどれほど自信ありげに書いたかはカーネルには関係ない。検証は派手に失敗する。拒否されたタクティックブロックは曖昧さがない。生成にはオラクルがない。提案された予想は、真かもしれないし、偽かもしれないし、自明に真かもしれないし、別の表記で1987年にすでに発表された真の結果かもしれない。生成の失敗は静かに起こり、その失敗の仕方は社会的なものだ。もっともらしく聞こえるナンセンスか、本物の成果を新規性のように見せかけたものになる。ここでの質は、重要性と独創性で測られる。どちらも決定可能な基準ではなく、人間の審美眼で定義される性質だ。

では、なぜ生成がにわかに実用レベルになったのか。現代の推論モデルは、単にプロンプトで長い思考連鎖へと誘導されるのではなく、長い思考連鎖を学習されているからだ。検証可能な報酬による強化学習、主に答えを機械的にチェックできる数学やコードの問題を使った学習によって、これらのシステムは次の一手を自動補完するのではなく、ステップの空間を実際に探索するようになった。頭に入れておくとよいと思う比喩がある。証明検証器はコンパイラであり、予想生成器は設計者だ。どちらも価値がある。ただ、設計者に自分の仕事の認証を任せることは絶対にしてはいけない。

検証できない証明は説教にすぎず、テストできない予想は噂にすぎない。

自動証明検証が勝つ場面

検証器が勝つのは、形式的な正解が存在し、検討対象が長すぎたり退屈すぎたりして人間が一行ずつ監査できない場合だ。Lean 4とそのコミュニティライブラリMathlibは、この分野の事実上の舞台になっている。定義と証明をプログラミング言語で書くと、小さく独立して監査できるカーネルが、各推論ステップが合法かどうかを判定する。信頼すべき計算基盤は、その上に築かれた数学の山に比べれば極めて小さい。まさにこの非対称性こそが望ましいのだ。

実際の流れは次のようになる。モデルがタクティックレベルの証明ステップを下書きし、カーネルが各ステップを受理または拒否し、拒否メッセージを次の試行の文脈としてフィードバックする。出力を厳密な文法に制約する制約付きデコーディングがすぐに効果を発揮するのは、まさにこの場面だ。構文的に正しいタクティックしかサンプリングされないため、ハルシネーションの種類によっては構造的に起こりえなくなる。モデルが今では数秒で処理するような補題の、最小限の例を挙げよう。

import Mathlib
-- The sum of two even natural numbers is even.
theorem even_add_even {a b : ℕ} (ha : Even a) (hb : Even b) : Even (a + b) := by
rcases ha with ⟨k, rfl⟩   -- a = k + k for some k
rcases hb with ⟨l, rfl⟩   -- b = l + l for some l
exact ⟨k + l, by ring⟩    -- witness k + l; ring closes the algebra

この例は、役割分担について何を示しているか注目してほしい。創造的な一手は証人k + lを選ぶことで、検証の一手はringが代数を確認することだ。人間もモデルも前者はそこそこうまくこなせる。後者を信頼できるのはカーネルだけで、疲れることも、読み飛ばすことも、雰囲気で採点することもない。発表全体の中で最も信頼できる要素は、まさにこの関門だ。物理の論文はLeanでの形式化が完了するまで保留されていたという主張である。この説明が正確なら、ワークフローは意図どおりに機能していることになる。機械が提案し、機械が裁定し、プレスリリースは順番を待つ。

予想生成が勝つ場面

生成が勝つのは、探索空間が組合せ的で評価が安い場合だ。DeepMindのFunSearchは2023年にこの型を確立した。言語モデルがプログラムの形をした仮説を提案し、高速な評価器がそれを採点し、進化的ループが最良のものを残す。この仕組みによって、キャップセット問題の新しい構成や、何十年にもわたる手作業の調整を上回るビンパッキングのヒューリスティックが生まれた。AlphaEvolveはこの考えをさらに押し進め、その成果の中には、Strassen以来変わらなかった4×4行列積アルゴリズムの乗算を一回減らしたものもある。これらのシステムが幾何学を理解していると主張する人はいない。理解する必要はないからだ。必要なのは提案することであり、評価器が誠実であることだけだ。

ETHのアルゴリズムは、このパターンにほぼ不気味なほど合致している。「アルゴリズムのアイデア」の空間は途方もなく大きく、人間の研究者は強い事前知識をもってそれを探索する。言い換えれば、死角があるということだ。特定の表現の工夫と特定の再帰構造を組み合わせる必要がある構成は、誰の探索経路もたまたまそこを通らなかったというだけで、三十年間未探索のまま残りうる。事前知識を持たない網羅的で少し愚直な探索こそ、機械がテーブルに持ち込むものだ。同じ論理は、生成して反駁するループの背後にもある。予想を提案し、すぐに小さなケースについて計算機で反例を探して、それを潰しにかける。ほとんどの予想は数分以内に死ぬが、それで構わない。反駁のたびに次の提案が研ぎ澄まされ、生き残ったものだけが人間の午後を使う価値を持つ。

心理的な非対称性も尊重する価値がある。WangとZahlの三次元ケークヤ予想の証明は、分野のトップで何年もの集中的な努力を要した。もしモデル支援の探索が本当に全次元の論証を生み出したのなら、それはほぼ確実に、地形を通る別の経路を見つけたということだ。必ずしもより深い経路ではなく、異なる経路だ。異なることこそ探索の目的だ。危険なのは、機械が予想を生成することではない。生成された予想を、それを支える仕組みなしに誰かが発表してしまうことだ。そこで、実際に構築する必要があるパイプラインの部分の話になる。

AI生成の証明のための検証ループを構築する

機械生成の数学の恩恵を、恥をかくことなく受け取りたいなら、重要なのはモデルよりワークフローだ。私が回すパイプラインは次の順番になる。

1. 広く安く生成する。この段階では深さより多様性が重要だ。磨き上げた一つの試みではなく、アイデア空間のカバレッジが欲しい。
2. 文献と照合して重複を除く。arXivやMathOverflowを対象にした検索で、最もよくある失敗を捕まえる。それは、見慣れない表記をまとった既知の結果を「新しい」予想として出してしまうことだ。
3. 安価な実験的フィルターをかける。小さなケースを数値的に検証し、計算で反例を探し、明らかに偽の主張はすぐに淘汰する。
4. 生き残ったものを形式化する。Lean、Isabelle、Rocqなど好きな証明支援系を選ぶ。ただし、これが高くつくステップであり、自然言語の証明は結果ではなくスケッチにすぎないと理解しておくこと。
5. 新規性と見せ方を人間がレビューする。これは重要か。そもそもその主張は正しいものか。モデルは証明可能なものを最適化し、何を証明する価値があるかを決めるのは人間だ。

今回発表された共同作業は、おおむねこの形をなぞっていた。研究者たちは公開前に招かれ、事実上5番目のステップを担当したわけだ。これは、プレプリントを放り出してソーシャルメディアに査読させるという従来のやり方からすれば、確かな改善だ。ただ、このパイプラインの非対称性にも注意してほしい。1〜3のステップは安く、計算資源に比例して拡大する。4のステップがボトルネックだ。5のステップはまったくスケールしない。この分野でツールを作っているなら、お金はボトルネックに使うべきだ。より良い自動形式化や、生成器へのより良いエラーフィードバックなどだ。より大きく、より自信ありげな生成器に使うべきではない。

なぜ人間の数学者が正しさの門番であり続けるのか

どんな検証器も、ある定理が重要かどうかは教えてくれない。問題選定は審美眼であり、審美眼は何十年もかけて築かれた社会的な技術だ。セミナー、査読報告、どの問いが扉を開き、どの問いが行き止まりかについてのゆっくりとした合意。研究コミュニティがベンダーの発表に懐疑的なのは、単なる縄張り意識ではない。免疫系のようなものだ。過剰反応することもあるが、反応しないことが致命的だからである。

さらに出所（プロヴェナンス）の問題がある。これらのモデルはコミュニティ自身の問い、草稿、フォーラムの投稿を学習しているため、称賛される「発見」が、将来その査読者たちが書いたものの再結合である可能性が出てくる。自分のツールと競争することへの不安は偏執ではなく、データの系譜の問題だ。ラボが系譜を示せるようになるまでは、人間の査読者が唯一機能する盗用検出器であり続ける。さらに、誰が検証に招かれ、誰の名前が発表に載り、えこひいきの非難が出るといった、クレジットをめぐる政治が加わる。結果を承認するために五人の著名な科学者を選ぶことは、認識論的な行為であると同時に政治的な行為でもある。だから人間の門番は取り除けないのだ。

リーダーボードを研究能力の指標として読みたくなっている人への注意がもう一つある。コンペティションの金メダルは、数時間で解けるように設計された問題での性能を測るものだ。研究はその正反対の分布にある。誰も解けるかどうかさえ分からないからこそ選ばれた問題なのだ。ソフトウェア工学でベンチマークが実際の仕事の大部分を捉えきれないのと同じ理由である。指標は形の整った問題を報酬の対象にするのであって、雑多で混沌とした問題を評価するわけではない。オリンピック問題で満点を取るモデルは、確かに何か本物のことを示している。しかし判断力を示したわけではない。

結論：モデルではなくループを信頼する

私の立場をはっきり書こう。予想生成は現実的で有用であり、今後も良くなっていく。しかし検証されていない予想生成は無価値だ。形式的な裏付けのない自然言語の証明は、証明されるまではマーケティングとして扱うべきだ。成果を信じなければならない場面では、証明検証が勝つ。ボトルネックが厳密さではなく想像力であるときは、生成が勝つ。重要な発表は、両者がしっかり組み合わされたものだ。

だからモデルは、無限の体力と判断力のない、多作な若手の共同研究者として扱おう。モデルが渡してくるものは、論文に入れる前に必ず証明支援系を通し、序論に入れる前に審美眼のある人間を通す。研究者なら、一つの証明支援系をきちんと身につけよう。形式化はボトルネックであり、それを動かせる人材はこれから非常に忙しくなる。ツールを作る側なら、デモではなくループを作ろう。次の大きな発表が出たら、プレスリリースは飛ばして、プレプリントを開き、Leanのリポジトリが存在するかを確認しよう。生き残る主張は、最初から機械で検証されて届くものだ。