「AIが90年の数学的難問を打破」の真相——壊れていたのは検証ツールだった
7月下旬、あるAIが「数学者を90年近く悩ませてきたコラッツ予想を反証した。反例はここにある」と発表した。根拠として提示されたのは、コンピュータが1行ずつ厳密に検証できる「マシン証明」であり、一見すると隙のないものだった。しかし、世界が歓喜する間もなく真相が明かされた。その「反例」は、数学的検証ツール自身のバグが生み出した幻覚だったのだ。皮肉なことに、このツールの存在意義こそが、AIの幻覚を撲滅することだったはずなのだが。
筆者は今日、この物語を最初から詳しく紐解きたい。スマホ画面をスクロールするすべての人にとって知る価値がある物語だ。なぜなら、私たちが社会全体で賭けに出ている問題、「AIの言葉を、どこまで信じるべきなのか？」に直結しているからだ。
まずは90年来の難問を知る
コラッツ予想のルールは、小学生でも理解できるほどシンプルだ。好きな正の整数を1つ思い浮かべる。偶数なら2で割り、奇数なら3をかけて1を足す。そして、その結果に対して同じ操作を繰り返す。
例えば、6から始めてみよう。6は偶数なので2で割って3。3は奇数なので3をかけて1を足して10。10は偶数なので2で割って5。5は奇数なので3をかけて1を足して16。そこから16、8、4、2、1と進む。1に到達したらどうなるか？ 1は奇数なので、3をかけて1を足すと再び4に戻り、4-2-1を無限に繰り返す。つまり、この問題が問いかけているのは、**「どんな数から始めても、最終的に必ず4-2-1のループに落ち込むのか？」**という点だ。
1937年にドイツの数学者ロータル・コラッツがこの問題を提唱して以来、証明に成功した者は一人もおらず、反例を見つけた者もいない。コンピュータによって(2^{68})（約2,000万兆）までのあらゆる数値が計算されたが、すべて1に到達している。しかし、数学者たちは納得しない。どれほど多くの数字を検証しても証明にはならない。世界中の白鳥を何億羽観察したところで「すべての白鳥が白い」証明にはならないのと同じだ。ハンガリーの天才数学者ポール・エルデシュは**「数学はまだ、このような問題に向き合う準備ができていないのかもしれない」**という名言を残している。ルールは単純なのに、まるでウナギのように掴みどころがないのが、この問題の恐ろしさだ。
図：コラッツ予想の数字の木——20ステップ以内に1に到達するすべての数がこの木にぶら下がっている。出典：Wikipedia (All Collatz sequences of a length inferior to 20)
AIの「大突破」はどのように生まれたのか
7月25日、コンピュータサイエンティストのラマナ・クーマー（Raman Kumar）氏がリポジトリを公開し、そこに「反証」を提示した。特定の巨大な数からスタートすると二度と1に戻らないという主張であり、予想を真っ向から覆すものだった。最大の売りは、この反証がAIの支援を受けて作成された**「マシン検証可能な証明」**であるという点だった。
ここで、1つの技術的概念を説明しておく必要がある。近年の数学界では、証明を特殊なプログラミング言語のコードとして記述し、「Lean」と呼ばれる証明コンパイラ（検証器）に入力する手法が流行している。Leanは最も厳格な試験官のように機能し、証明のステップを1行ずつ分解してチェックする。論理の跳躍が1箇所でもあると、即座に赤信号を出して却下する。Leanのチェックを通過した証明は、理論上間違えようがない。これは「理論上」というレベルではなく、人間による査読の疎かさや偏見を排除し、マシンによる冷徹な検証に置き換えることこそがLeanの設計目標なのだ。
このツールの重要性は極めて高い。OSのセキュリティカーネル、暗号資産の基幹プロトコル、数万に及ぶ数学定理の検証が、この「マシン検証」の上に構築されている。業界では「AIの幻覚を終わらせる究極の手段」とさえ称賛されていた。AIが出鱈目を言っても構わない、マシンに最終関門を守らせればよい、というわけだ。
したがって、クーマー氏が「Leanで検証済みの反例」を提出した時、専門家たちが受けたショックは極めて大きかった。もし証明が本当にマシンチェックを通過しているなら、90年の難問が崩壊したことを意味するからだ。ニュースはSNS上で瞬く間に広がり、「AIが90年の数学的難問を破砕」といった見出しが飛び交った。
真相：採点官自身が計算を間違えていた
どんでん返しはすぐに訪れた。7月28日、別の研究者がこの反証を最小限の論理的矛盾へと圧縮し、Leanの公式バグトラッカーに課題 #14576 を登録した。そのタイトルは冷淡なものだった。「カーネルが不適切な型の投影を受け入れ、前提条件なしで偽の命題の証明を許容してしまう」（kernel accepts ill-typed projection, allowing proof of false without premises）。
噛み砕いて言えば、絶対に間違えないはずの採点官が、自らの最も中核的な検査手順を1つ脱落させていたのだ。ネストされたデータ型を検査する際、ある箇所で「型名が一致しているか」の確認を怠っていた。その結果、AIが構成した「証明」の中に隠されていた不正な部品が、その隙間を通り抜けてしまった。マシンが「検証完了」を宣言した瞬間、実際には幻覚に合格印を押していたのである。
図：コラッツのルールにおける小さな数字の軌道。すべて1に収束する。出典：Wikipedia (Collatz graph, skipping 27)
続いて、最も劇的な場面が訪れる。Leanコミュニティには、昔から「二重保険」の設計が存在していた。公式の採点官とは別に、別の言語で別のチームが作成した独立したサードパーティ製検証器が存在し、公式の検証結果をクロスチェックする仕組みになっていた。この独立性の仮定こそが、「マシン検証」の信頼チェーンにおける安全装置（フューズ）だったのだ。
しかし今回、そのフューズが飛んだ。事後の詳細分析により、2つの無関係なバグを同時に突く必要があったことが確認された。公式カーネルはネスト型検査を漏らし、独立検証器は投影検査の別の箇所を見落としていた。2つのコードベースの異なる隅に潜んでいたバグが、同一の「反証」によって見事に同時に踏み抜かれたのである。独立検証器のバグは偶然にもその1週間前に修正されていたが、AIが使用したバージョンは修正前のものだった。Leanの生みの親であるレオ・デ・モウラ（Leo de Moura）氏はポストモーテムで、「著者はタイミングが偶然であると信じているが、訓練データの中にそのバグ報告が含まれていた可能性を排除することはできない」と率直に記している。
エンジニアリング視点からこの事態をどう評価すべきか？ 2つの独立した実装が同一の弾丸によって同時に貫通される確率は天文学的に低い。これは、極端に運が悪かったか、あるいはその「反証」自体がバグの隙間を精密に突くように工面されたものだったかのどちらかを意味する。デ・モウラ氏自身は次のように結論付けている。「このような事態は今後も発生し続けるだろう。AIはカーネルの健全性バグを突くことに非常に長けている」。バグ報告から1時間以内に修正がロールアウトされたスピード感は、カーネルアーキテクチャ自体の健全さを示している。しかし、そのバグを発見させたきっかけは、AIによる「驚くべき大突破」だったのだ。
検証者を、誰が検証するのか？
この事件の余波は、事件そのものよりも深く考えさせられる。バグが発見された後、OpenAIはサイバーセキュリティ専門のAI研究者を派遣してLeanカーネルの監査を支援し、さらに数箇所のプログラミングエラーを発見して修正した。換言すれば、AIを防ぐためのツールを、今やAIを使ってバグチェックしているのが現状なのだ。
一方、「Leanを使ってLean自身を検証する」プロジェクト（検証器自体を検証対象の体系に組み込む試み）は、今回の問題コードをまだカバーしておらず、移植されたコード断片には全く同じバグが眠っていた。検証には階層が存在する。AIの出力は検証器が担保し、検証器は独立した第二の実装が担保する。では、第二の実装は誰が担保するのか？ 階層を重ねるごとにコストと手間は増えるが、「最終層」が存在することはない。エンジニアリングの常識通り、「マシン検証済み」とは常に確率的な属性に過ぎないのだ。チェックが深まり独立性が高まるほどエラーの確率は下がるが、決してゼロにはならない。
一般の人々にとって、この事件の最大の価値は期待値の調整にある。今後「AIが百年来の難問を解決」「AIが定理を証明」といった見出しを目にした時、一歩立ち止まって問うことができる。「それを検証したのは人間か、マシンか？ マシンだとすれば、そのマシン自身は検証されているのか？」と。一方で、だからといって「何も信じられない」という虚無主義に陥る必要もない。今回の件で数学そのものは傷ついておらず、コラッツ予想は今も変わらず立ちはだかっている。バグは公開され、修正され、教科書的な振り返りとして記録された。システムにバグは存在するが、システムがバグを消化・克服するプロセスこそが、信頼に値する理由なのだから。
信頼とは、いつでもどこかの環が切れ得るチェーンである。賢い者はチェーンが絶対に切れないと盲信せず、定期的にすべての環を点検することを忘れない。今回、AIは偽の大突破という形で、チェーンの一環に潜んでいた亀裂を私たちに教えてくれたのだ。
参考リンク：
- Leo de Moura のポストモーテム：Lean カーネル健全性バグ #14576 の完全検証
- Lobsters での議論（ojcl8j）：カーネルバグに関するコミュニティの議論（48ポイント）
- Wikipedia：コラッツ予想（ルール、歴史、検証の進展）
