未公開の OpenAI 成果の噂が、AI の証明を読める前に MIT の三研究者の発表日を変えた。Dor Minzer と大学院生 Yumou Fei、Shuo Wang は9月11日、Unique Games に関する企業成果が近いと聞いた。14日には関連するが別の定理の粗い95ページ論文を公開した。OpenAI は10月6日、Unique Games 猜想の証明を主張する数学集を発表した。
人間側の突破は4月で、説明用原稿を整えていた途中だった。近接する企業成果の予想で、解説完成より優先権の公開が急務になった。二つの定理は互いを不要にせず、プレプリントも独立専門家審査に代わらない。
同じ証明の別版ではなく二つの結果
Subhash Khot は2002年に Unique Games を導入した。辺で結ばれた頂点へラベルを置く。各辺は置換制約を持ち、一端のラベルから他端の許されるラベルが一つ決まる。この一対一が名称の由来だ。
猜想は近似の計算困難性である。大まかには、ほぼ全制約を満たせる入力と、ごく一部しか満たせない入力を区別するのが難しい。解が存在しないという意味ではなく、厳密に定義した入力群について効率的な一般アルゴリズムが判断できる限界を扱う。
厳密最適解が高価なとき近似を使う最適化に影響する。Unique Games は最良の近似保証を本質的な困難性へ結び付ける。Raghavendra の2008年の枠組みは猜想を仮定し、広い制約問題で標準的半正定値計画の最適性を示す。幾何的緩和を解き離散選択へ丸める方法だ。
MIT の定理は完全な完全性、つまり初期入力の全制約が満たせる場合を扱う。2対1ゲームでは一方のラベルに他方の互換選択肢が二つあり、4対1では四つある。元の2対1主張より弱いが、通常の Unique Games が直接扱わない正確な完全性へ届く。
「ほぼすべて」と「すべて」の差
Minzer らの2018年の成果はほぼ完全な完全性だった。僅かな差でも、完全充足の出発点を要する帰着を妨げる。端点へ到達するのは見かけの改善ではない。
Fei と Wang は2025年から Minzer と研究した。新しい誤り訂正符号は有望だったが、帰着全体へ組み込む試みは何度も失敗した。4月の突破は二次方程式、中間検証層、Grassmann 型符号の内部検証器を組み合わせた。
これは確率的検証可能証明の技術で、長い符号化証明の少数箇所をランダムに見る。困難性帰着は受理すべき例と拒否すべき例の差を保つ必要がある。重要なのは符号単体でなく層の相互作用だ。
帰結の一つはグラフ彩色だ。三色で塗れるという約束があっても、任意の固定色数を許して有効彩色を探すことは NP 困難となる。色追加が効率的一般法を必ず生むわけではない。二頂点超を一辺で結ぶ超グラフの一部の独立集合にも帰結がある。
通常の Unique Games を対象とする OpenAI の主張とは異なる。MIT 側は企業論文の複製ではなく、独自経路と帰結を守った。
警告から三日で発表した代価
チームは数学が完成していても望む呈示ではないとした。9月14日の ECCC 原稿は95ページで、Minzer は第6節後をほぼ接続語なしと説明した。定義と中間証明はあっても読者への案内が少ない。
解説は研究基盤だ。動機、橋渡し、比較、説明が監査と再利用を助ける。時刻を素早く確保しても、共同体へこの仕事は残る。
相手の論証、モデル、正確な主張、日程は知らなかった。同じ人間の時間尺度に従う通常の二組競争ではない。予想される機械出力が専門評価前に人間の仕事を変えた。
OpenAI 発表の第二の問題は量
同社によれば内部モデルは約4,000問題を試し、377問題に関する722原稿を公開した。一つの集には理論計算機科学の40証明がある。試行、原稿、問題、証明は別単位で、解決済み問題数へ混ぜられない。
平均計算量は一結果あたり ChatGPT Pro の約三時間思考相当だという。Unique Games の正確な費用や全証明の共通予算ではない。約半分が発表時に形式検証済み、残りも可能との見込みは企業の将来判断である。
手稿は3SAT から無重み入力への明示的決定性多項式時間帰着と Lean 成果物を主張する。カット、被覆、順序、削除、クラスタリング、制約充足への帰結は新定理と既存帰着に依存する。
OpenAI は通常査読として発表せず、引用・解説改善を認め、重要な生成結果の理解を支援するとした。公開出力は重要な証拠でも、共同体の完成した評価ではない。
Lean は形式命題を検査する
Lean は符号化された仮定と規則から各段階が従うと確認する。モデルが文章を正しいと言うより強いが、専門家は意図した猜想との一致、取り込んだ仮定、コードと本文の対応を見る必要がある。
量化順序と誤差パラメーターに対するラベル集合サイズの依存が重要だ。依存が違えば似た命題でも弱くなる。完全性、健全性、明示性、多項式時間は標準的計算量主張に一致しなければならない。
検査済み導出も中心アイデア、新規性、先行研究への帰属、共同体合意を自動生成しない。検証と理解は同義ではない。急いだ人間原稿も精読と改善が必要で、人間著者は免除理由にならない。
再現も層がある。Lean 成果物と依存で検査を再実行できても、未公開内部モデルと部分要約・集計では全プロンプト、標本選択、介入は再現できない。検証再現と発見再現は別だ。
次に必要なのは OpenAI の形式と意図の独立照合、明瞭な MIT 原稿、機械規模の成果を審査できる公開方法である。既に発表時期と優先権は変わった。持続的な数学の前進は、確認可能な出力を他者が検討・応用・理解できる説明へ変えられるかにかかる。