ETHは、充足可能性問題が本質的にどれほど難しいかについての予想です。大まかに言えば、k-SAT（k ≥ 3）は、変数の数をnとしたとき、2o(n)時間では解けない、つまり、すべてのインスタンスをnに対して劣指数時間で解くアルゴリズムは存在しないと主張します。実用面では、ETHは計算困難性を考える際の基準になります。グラフ問題、データベースクエリ、計算生物学などに関する多くの条件付き下界は、ETHを前提に、特定の実行時間を大きく改善するのは難しいと論じています。ある問題がETH困難だと言うとき、それは、その問題を劇的に高速化できれば、この基準を覆すようなブレークスルーになるという意味です。

OpenAIの主張が対象とするのは固定幅SAT、つまり節の構造や変数間の相互作用に制約を加えたSATのインスタンスです。あらゆる固定幅SATのインスタンスを2o(n)時間、すなわちnに対して劣指数時間で解くアルゴリズムが構成されれば、k-SATの問題群には指数時間の下界があるというETHの包括的な主張と矛盾します。これにより、ETHを明示的に仮定した多くの条件付き計算困難性の結果が成り立たなくなります。ただし、ETHの否定はP = NPの証明と同じではありません。ETHは、実行時間の指数部分への依存の仕方に関する、より強く具体的な予想です。P = NPは、多項式時間と非決定性多項式時間の隔たりがなくなることを意味します。一方、特定のSAT問題群に対する劣指数時間アルゴリズムが示すのは、その問題群で漸近的に高速化できるということに限られ、すべてのNP問題が多項式時間で解けるとは主張しません。

証明をLeanで形式化することには大きな意義があります。定義を厳密にし、非形式的な議論に潜む多くの論理の抜けを埋め、人間の誤りの一部を防ぐ機械検証可能な成果物を作れるからです。OpenAIのチームによれば、自然言語による反証から24時間以内にLeanでの形式化が行われました。それでも形式検証が確かめるのは、形式体系の公理と定義に照らした構文上の正しさです。モデルの前提、漸近評価における隠れた定数、パラメーターの範囲、あるいはアルゴリズムが広く適用できるのか、特殊なインスタンス群に合わせたものなのかについて、コミュニティが解釈する作業に取って代わるものではありません。

OpenAIは、ETHを最初に提唱したラッセル・インパリアッツォ氏とラマモハン・パトゥリ氏、そしてMITのライアン・ウィリアムズ氏が率いるレビューグループを招きました。この3人は、研究の歴史的背景と高い専門性を併せ持っています。インパリアッツォ氏とパトゥリ氏は、提示された反証がETHの当初の定式化と本当に矛盾するかを見極め、ウィリアムズ氏はアルゴリズムの下界や関連する条件付き結果への影響を評価できます。彼らが主導することで、成果物を専門家が透明性をもって評価できるようになるでしょう。また、AI企業とアカデミアが協力する建設的なモデルを示すものでもあります。

今回の出来事は、新たな研究の進め方を示しています。生成モデルは予想を提案するだけでなく、機械検証可能な証明まで作成できるため、アイデアから形式的な成果物に至るまでのサイクルが短縮されます。研究チーム、資金提供者、プロダクトリーダーにとって、当面の課題は、検証基盤や成果物を公開するリポジトリへの投資、コミュニティ主導の監査への資金提供です。一方でリスクもあります。モデルが誤った補題を幻覚しながら型検査を通過させたり、定義を誤って適用したり、狭いインスタンスの仮定を利用したりする可能性があります。必要なのは、無条件に期待をあおることでも、反射的に退けることでもなく、分野の専門家が主導する、体系的で透明性の高い検証です。