AIエージェントを使う数学者が31年来のKLS予想を証明、同じトークン量でもモデル単独では届かず

Microsoft Researchは10月21日、同社の研究者Xinzhi Zhangと共著者Zhao Songが1995年に提起されたKLS予想を証明したと発表した。数学にとっては31年越しの難問の解決であり、AIチームにとっては、こうした研究でエージェントと人間がそれぞれ何をしたのかを詳しく記した珍しい記録でもある。

どの次元でも平らな切断で十分

Kannan・Lovász・Simonovits予想は、対数凹分布と呼ばれる高次元の確率分布の幅広いクラスに関するものだ。そうした形を平らな面で切る最良の方法が、任意の形で切る最良の方法とほぼ同等かどうかを問う。予想によれば、その差は次元の数に依存しない定数で抑えられる。アルゴリズムが分布からサンプルを取り出すランダムウォークの理論も、この性質に支えられている。

2026年7月の時点で最良とされた結果では、この上界は次元とともにゆっくり増える余地が残っていた。著者らはまずその結果を精緻化し、AIエージェントとともに100を超える候補アプローチを検討した。その多くは高階テンソルを使う長い計算を伴った。そこから新しい判定基準が生まれた。10月1日版の論文はこの基準を繰り返し適用し、次元への依存を反復対数にまで抑えた。10月4日版は手順全体をさらに繰り返し、小さな誤差が際限なく積み上がらないことを示して証明を完成させた。ブログによれば、この発想は線形計画法の高速アルゴリズムに関する著者らの過去の研究から来ている。

結果はすでに他の研究者にも裏づけられている。同じ日に別の専門家グループが独自の完全な証明を公開し、Microsoft論文の初版を「決定的な一歩」と呼んだ。同日に出た3つ目の証明も、よく似た考え方に基づく。その後、初版の判定基準と他の研究を組み合わせたLean 4による形式化も公開された。

AIチームにとっては証明そのものより人間抜きの対照実験が重要

ブログは役割分担をはっきり書いている。AIツールは変種を試し、詳細な導出を行い、原稿の作成を手伝い、証明の内部チェックを担った。人間は方向を決め、有望なアイデアを選び、それらを最終的な論証に組み立て、証明を検証した。エージェントは並行して動き、研究者は各ラウンドの後に行き止まりを切り捨て、最も有望な途中結果を次のラウンドに渡した。こうした探索の筋道はおよそ100本に上った。

最も価値があるのは対照実験だ。著者らは同じ問題を、人間の誘導なしで複数の先端モデルに、ほぼ同じトークン予算で繰り返し解かせようとした。結果は目標に届かなかった。1回の大規模なモデル実行で研究を置き換えられると期待する企業にとって、これは有益な警告になる。今回うまくいったのは、探索と、エージェントを誤った方向から絶えず引き戻した人間の判断との組み合わせだった。

数学への影響は直接的だ。これまでKLS予想が正しいと仮定して初めて成り立っていた多くの定理が、無条件で成り立つことになる。凸幾何学、確率論、理論計算機科学の土台がそれだけ強くなる。

対照実験は今のところブログの一文にすぎない

Microsoftは、対照実験でどのモデルを使ったのか、何回試したのか、どれだけのトークンを消費したのかを公表していない。人間抜きでは失敗したという主張は、現時点では著者自身の証言であり、第三者が再現できる測定ではない。「100を超えるアプローチ」も、彼ら自身のプロセスの説明だ。

形式的な検証にも2つの層がある。公開済みのLean 4による形式化は初版の判定基準と他の研究を組み合わせたもので、今回の証明そのものを機械的に確認したものではない。著者らはLeanで検証済みの短縮版証明を持っているが、公開は最終確認の後になる。また、この結果自体が新しいサンプリングアルゴリズムをもたらすわけではない。変わるのは主に、既存のアルゴリズムについて何を証明できるかだ。

Lean版証明の公開と対照実験の詳細が論証の強さを決める

数学者にとって決め手になるのは、Leanで検証した短縮版証明と、それが査読を通るかどうかだ。同じ日に3つの独立した証明が出たことは強い信号だが、結果に最終的な重みを与えるのは査読である。

AIの世界にとってより重要なのは、Microsoftが対照実験のデータ、つまりモデル、実行回数、トークン消費量を公開するかどうかだ。それがあって初めて、行き止まりを切り捨てた人間がどれだけの仕事をしたのかを公正に測れる。人間が枝刈りする探索がほかの未解決問題にも通用するのか、今回だけうまくいったのかも見えてくる。

Lilithの判定

100体のエージェントが道を探し、1人の数学者がラウンドごとに行き止まりを消していった。彼抜きのモデルは同じトークン予算を与えられても証明を見つけられなかった。研究を1回の巨大な実行に任せようとする経営者は、この一文を二度読むべきだ。