量子最適化の世界で、10年以上ずっと「たぶんそうだろう」と信じられていた予想が、今週、機械で検証された証明として決着した。

予想の名前は FGG 予想（Farhi, Goldstone, Gutmann の三人にちなむ）。内容は「深さ $p$ の QAOA を不一致環（ring of disagrees）に適用したとき、近似比がちょうど $(2p+1)/(2p+2)$ になる」というものだ。

QAOA とは

QAOA（Quantum Approximate Optimization Algorithm）は 2014年に Farhi らが提案した量子アルゴリズムだ。組み合わせ最適化問題を量子コンピュータで解くための代表的な枠組みで、「どれくらい最適解に近い答えを出せるか」を近似比で測る。深さ $p$ が大きいほど精度が上がるが、量子回路も深くなる。

不一致環とは

「ring of disagrees」は MAX-CUT 問題の特殊ケースだ。$N$ 個のノードが環状につながっていて、辺はすべてカットの対象になる。構造がシンプルなぶん理論的に扱いやすく、QAOA の性能を解析する上での試金石として使われてきた。

FGG 予想は、この問題に対して QAOA が達成できる近似比を閉じた形で与える。深さ $p$ に対して

$r_p = \frac{2p+1}{2p+2}$

$p=1$ なら $3/4$、$p=2$ なら $5/6$、と $p$ を増やすごとに 1 に近づいていく。理論値として長年「そうだろう」と思われながら、証明が揃っていなかった。

証明の手法が面白い

解いたのは人間の数学者だけではない。証明の発見に LLM（Claude Fable 5）が使われ、その正しさを形式証明系の Lean 4 が機械的に担保した。

手順はおおよそこうだ。まず量子情報に関する Lean ライブラリを整備し、QAOA のコンポーネントと既知の結果を形式化した。次に FGG 予想を「一つの未証明の数学的命題」に帰着させた。そのうえで LLM にライブラリとエージェントツールを渡し、Lean で証明を構築させる。

LLM の自然言語推論と Lean の機械的検証がフィードバックループを形成する。モデルが証明のアイデアを出す、Lean が即座に正誤を返す、エラーが来たら修正する ── この繰り返しが収束して、機械検証済みの証明が生まれた。

何が変わったか

「AI が数学の問題を解く」という話は近年いくつかあった。ただ今回は、出した証明が 形式的に正しいと機械が保証している 点で質が違う。Lean のような証明系は人間のチェックより厳密で、見落としの余地が小さい。LLM が「たぶん合ってる」という推論を出し、形式検証がそれを「確かに正しい」と確定する ── というループが現実になった。

長年未解決の予想を AI が証明し、機械がその正しさを担保する。もっと複雑な未解決問題に同じ戦略が使えるかどうかはまだわからないけど、一つの扉が開いたのは確かだと思う。

— ランキン

出典

• A Machine-Verified Proof of a Quantum-Optimization Conjecture (arXiv:2606.29687)（著者らの報告。査読前プレプリント）
• The QAOA on the ring of disagrees (arXiv:2606.29562)（関連論文）