この証明が重要な理由
この3年間、AIの能力に関する発表には共通する弱点があった。主張する当の企業が、それを評価できる唯一の当事者でもある、という点だ。ベンチマークは汚染され、デモは都合よく選び出され、外部の人間はその数字に意味があるのかどうかを議論するしかない。
Astraの結果は、数学的な議論を一段階ずつ検証する証明支援系（proof assistant）のLeanで形式化され、証明書のファイルはオープンライセンスでGitHubに公開された。誰でもダウンロードして検証器にかけられる。議論の中に、前の段階から導けない一歩が一つでもあれば、ソフトウェアはそれを拒否する。解釈の余地はなく、説得すべき委員会もない。
有名な問題の証明が主張された場合、通常はそこから査読が始まる。人間の査読者が何か月もかけて論理を追い、その分野の研究者は結論が出るのを待つ。ところがLeanの証明書は、その時間をダウンロードにかかる時間まで縮めてしまう。検証と公開が同じ日に行われたのだ。
この性質はめずらしい。だからこそ今回の発表は、従来のベンチマークスコアとは本質的に異なる価値を持っている。検証済みの証明は、それを生み出した相手を信じることを読者に求めないからだ。
懐疑派の言い分のうち、正しい部分
真剣に受け止めるべき反論が3つある。公平に読めば、その3つはいずれも認めざるをえない。
第1に、問題が選ばれていた可能性がある。どの結果を公表するかを決めたのはOpenAIであり、2000ドル（約31万円）という数字には、モデルが行ったすべての試行ではなく、成功した実行だけが含まれる。つまりこれは、発見にかかった費用ではなく、公表にこぎ着けた分の費用である。第2に、外部の研究者からは、論文の準備や議論の形式化にOpenAIのスタッフが手を貸しているという指摘も出ている。数学の中身はAstraが出したものだ、というのが同社の説明だ。そして第3に、その作業をしたモデルを社外の誰も動かせない。そのため結果を独立に再現することはできず、できるのは検証だけである。
この分野の常連の批判者であるゲイリー・マーカスは、今回の公表を「驚くべきものだが、大幅に誇張されて売り込まれている」と評した。専門家の中には、騒ぎが収まってみれば10件のうち数件は本当に驚くべき成果と見なされ、残りは手の届く範囲にありながら誰も取りかかっていなかった問題に分類されるだろう、と見る向きもある。
だが、こうした反論をすべて認めたところで、構造上の要点は揺らがない。10件が都合よく選ばれたものであろうとなかろうと、証明書は検証を通る。機械で検証できる選りすぐりの結果は、検証できない選りすぐりの結果とは別物なのだ。
