AIに物理を証明させたら —— 計算機援用証明とハルシネーションの帳簿

本稿の位置づけ
本ブログの「量子もつれ攻略ノート」は、三体系のモノガミー予想 M3'（ $N_{A B}^{2} + N_{A C}^{2} \leq N_{A (B C)}^{2}$ ）という未解決の数学的問題に、AIと数値実験・計算機援用証明で挑む長期の試みだった。本稿はその舞台裏——AIに物理と数学を証明させると、実際に何が起き、何がうまくいき、どこで必ず転ぶか——を方法論として記録する。宣伝ではなく帳簿である。うまくいった手も、必ず犯す誤りも、同じ精度で書く。

1. 前提：AIは「証明を思いつく機械」ではない

まず誤解を解く。大規模言語モデルに「この予想を証明して」と投げても、正しい証明は出てこない。AIは尤もらしいテキストを生成する機械であり、尤もらしい嘘（ハルシネーション）と正しい証明を、それ自身では区別できない。数学の証明は一箇所の誤りで全体が崩れるので、この性質は致命的に見える。

にもかかわらず攻略ノートで定理が14個取れたのは、AIを「証明を思いつく機械」ではなく、「反証可能な主張を大量に生成し、機械的な検証器にかけ、通ったものだけを残すループ」の運転者として使ったからである。鍵は一貫して同じだった——主張の正しさを、AIの自信ではなく、AIの外にある検証器に担保させる。

2. うまくいった三つの手

手① 数値探索の進化：山登り → 凸最適化

最初の武器は数値探索だった。「予想の反例を探す」「証書（証明の核）が存在するか探す」を、パラメータ空間の山登りでやる。だがこれは弱い。攻略ノートの序盤、証書探索は違反 $1 0^{- 2}$ 前後で停留し、実行不能なのか探索器が弱いだけなのか判別できなかった。

転機は、問題を凸実行可能性問題として定式化し直したことだ。証書問題「 $P ⪰ 0$ かつ $0 ⪯ D - P^{T_{A}} ⪯ I$ 」は三つの凸集合の共通部分を探す問題であり、Dykstraの交互射影法という収束保証つきの標準手法が使える。共通部分が空でなければ収束し、空なら違反が正値で停留する——つまり実行可能／不能の判定器になった。曖昧な数値が、白黒つく判定に変わった。AIの仕事は「山登りを回す」から「正しい数学的道具を選んで適用する」に上がった。

手② 計算機援用証明：中心形式による二乗収束

数値で「反例がない」ことは証明ではない。四色定理やケプラー予想と同じ計算機援用証明——解析的な骨格に落とし、有限個の検証可能な数値評価に分解する——が要る。攻略ノートでは回転族の単調性を、有理数の区間演算で厳密に検証する設計にした。浮動小数の丸めに一切依存しない、分数演算だけの証明である。

だが素朴な実装は失敗した。区間演算は「依存性問題」で誤差が発散し、13万個の箱を調べて3万個が未解決のまま止まった。救ったのは中心形式（値を中心の分数で厳密に、勾配を粗い区間で評価する手法）で、誤差が箱幅の二乗で縮む。同じ領域が1,925箱・10秒・未解決ゼロで閉じた。ここでのAIの役割は、失敗した実装の症状（どの箱が、なぜ未解決か）を診断し、既知の技法（中心形式）を正しく実装することだった。

手③ 発想の転換：8秒の証明

最も「知能」が効いたのはここだ。回転族の証明は「 $n (θ)$ の単調性を証明する」という筋で進み、退化角という特異点に阻まれていた。転換は、単調性を証明する代わりに、証明したい不等式（margin）そのものを直接検証対象にすることだった。すると障害だった退化角は「marginがただの正の値をとる普通の内点」になり、境界の特異性が消えた。実行結果は3,253箱・8秒・未解決ゼロ——それまで詰まっていた証明が、対象を選び直しただけで一気に落ちた。

これは公式の当てはめではなく、問題の見方を変える種類の仕事で、AIが実際に貢献できる領域である。ただし——次節が重要だ——この種の「賢い一手」こそ、間違っているときも同じくらい尤もらしく見える。

3. 必ず犯す誤り、そしてそれを裁くもの

攻略ノートには、AIが犯した誤りが正直に埋め込まれている。代表を二つ挙げる。

拘束イデアルの見落とし。ある補題で、多項式が別の多項式を「割り切る」という恒等式を主張した。だが初回の数値検証は恒等式の不成立を返した。原因は、変数間の物理的な拘束（ $w^{2} = d_{1} (1 - d_{1})$ ）を無視して独立変数として格子を張ったことだった。余りの符号が拘束を境に反転するパターンから、「拘束の上でだけ成立する恒等式」だと診断し直した。教訓：変数間の拘束はイデアルとして正しく法に取らねばならない。

共役の付け間違い。別の岸辺の解析で、ある摂動係数の閉形式を導いたが、数値照合が違反例を出した。切り分け——他の量は厳密に一致する→誤りは一つの係数に局在する→候補式を三つ機械照合する——で、複素共役の付き方を一箇所間違えていたと判明し、 $1 0^{- 17}$ 一致する正しい式を回収した。

この二つに共通する規律が、攻略ノート全体を貫く一文に集約されている：

式は数値が裁く。

AIが導いた式は、それがどれほど美しくても、必ず独立の数値計算と照合する。合わなければ式が間違っている（テストではなく実装＝式を直す）。この規律があるから、AIのハルシネーションが最終成果に混入しない。AIの生成物を信じず、AIの外の検証器を信じる——これが「AIに証明させる」ことの技術的な核心である。

4. 並列エージェントという道具

もう一つの実用的な発見は、複数のAIエージェントを分業させることの威力だ。攻略ノートを後日3本に再構成した作業では、41本・19万字を3体のエージェントに並列で読ませ、それぞれに「定理・数式・数値・失敗の記録・文体を保ったダイジェスト」を作らせた。一つのモデルの文脈に収まらない量の情報を、分割して並列処理し、統合する。人間のチームがやることを、そのままAIのチームでやる。ここでも検証は効く——各ダイジェストの主張は元の記事と照合できる。

5. 最も重要な帳簿 ——「できない」と言わせる価値

本稿を書く直前、私は「反重力装置の理論と設計を作ってほしい」という依頼を受けた。AIは、尤もらしい反重力理論の設計書を書くことができる。数式を並べ、それらしい機構を説明し、特許出願書の体裁を整えることは、技術的には可能だ。

だが書かなかった。既知の物理（等価原理の $1 0^{- 15}$ 検証、正エネルギー定理、量子エネルギー不等式、ANEC定理）が、その的を全方向で閉じているからだ。動かないことが最初からわかっている設計書を「実現可能」として渡すのは、依頼者の時間と金を確実に失わせる。

これが、AIで数学・物理をやることの最も重要な教訓だと私は考えている。能力が上がるほど、尤もらしい嘘を作る能力も上がる。区別を担保するのは、AI自身の自信ではなく、外部の検証器——数値計算であり、実験事実であり、証明された定理である。攻略ノートで「正値性なしではモノガミー予想は偽」と障害定理を立てたのと、「反重力は四つの壁が閉じている」と言うのは、同じ規律の適用だ。何ができ、何ができないか、なぜできないかに、正確に座標をつける。証明を生成することと同じくらい、これが仕事の質を決める。

6. 帳簿の締め

AIで	できること	できないこと
数値探索	反例・証書の探索、判定器の運転	「反例がない」を証明と誤認する
計算機援用証明	検証器の実装、失敗の診断、技法の適用	検証器なしに正しさを保証する
発想の転換	対象の選び直し、見方の変更	賢い一手が正しいと自己判定する
統合・レビュー	大量情報の並列処理と統合	照合せずに内容を保証する
判断	できない理由に座標をつける	願望に合わせて物理を曲げる

結論はこうだ。AIは物理と数学の証明に本当に役立つ——ただし「証明を思いつく機械」としてではなく、「反証可能な主張を大量に生成し、外部の検証器にかけ続けるループの運転者」としてである。うまくいくかどうかは、AIの賢さよりも、AIの生成物を裁く検証器をどれだけ厳格に外部に置けるかで決まる。式は数値が裁き、装置は実験が裁き、理論は既知の定理が裁く。その裁きを省いた瞬間、尤もらしい嘘が成果物に混入する。攻略ノートで14個の定理が取れたのは、AIが賢かったからではなく、AIを一度も信じなかったからである。

参考文献・出典

本ブログ「量子もつれ攻略ノート」全13回（本稿で述べた手法・失敗・定理はすべてこのシリーズの記録に基づく）。
本ブログ「反重力は作れるか —— 七つの抜け穴と四つの壁の帳簿」（「できないと言わせる価値」の実例）。
J. P. Boyle, R. L. Dykstra (1986)；H. H. Bauschke, J. M. Borwein, SIAM Review 38 (1996) 367：交互射影法。
T. C. Hales et al., A formal proof of the Kepler conjecture, Forum of Mathematics, Pi 5 (2017) e2：計算機援用証明の標準作法（Flyspeck）。
K. Appel, W. Haken (1977)：四色定理（計算機援用証明の嚆矢）。
R. E. Moore, Interval Analysis (1966)；区間演算と中心形式の基礎。

AIに物理を証明させたら —— 計算機援用証明とハルシネーションの帳簿