OpenAI、AI由来の数学的成果722件を公開。数学者たちは功績は誰のものかと問う

OpenAIは、社内のフロンティアモデルによって生成された数学的成果のコレクションを公開し、多くの証明に対するLean形式化と、改訂および引用のためのプロトコルを含むリポジトリを公表した。この公開では722件の成果が示され、そのうち162件が機械検証されている。

反応は、数学が正しいかどうかよりも、検証が実際に何をもたらすのか、そして成果が誰に帰属するのかに集中している。

Leanが検証するもの、しないもの

Leanは証明支援系である。それは形式化された議論の各ステップを明示された公理に対して機械的に検証するため、検証済みの証明には論理的なギャップが存在し得ない。コンパイルが通れば、議論は前提から帰結する。

これは強い保証であり、同時に狭い保証でもある。証明支援系が検証するのは、形式化された命題が帰結することである。その形式化された命題が、付随する散文が主張する内容を述べているかまでは検証しない。162件の機械検証済み成果のそれぞれについて、Leanファイルが誰かの思う定理を本当にエンコードしているか確認するには、依然として人間が読まなければならない。形式化は翻訳の一ステップであり、翻訳はずれる。

残りの560件にはそのような検証がない。つまり、公開されたコレクションは証拠として大きく異なる2つのカテゴリを混在させている。「722件の成果、162件が検証済み」と報告するのは、総数を報告するより誠実だが、それはまた、見出しの数字が検証済み部分を約4.5倍誇張していることも意味する。

功績問題に新たな形

数学者たちは、この分野が存在して以来ずっと功績の配分について論じてきた。そしてその議論は通常、誰が問いを立てたか、誰が鍵となるステップを見つけたか、誰がそれを論文にまとめたかに関するものだ。AI生成の成果は、前例のないバージョンの問題を持ち込む。

もしモデルが長年の未解決問題の証明を生み出したら、著者は誰なのか。現行の著作権枠組みの下では法的著者になり得ないモデル自身か。プロンプトを与えた研究者か。問題リストをキュレーションしたチームか。モデルを訓練し、重みを公開していない組織か。

OpenAIは、基盤モデルの責任ある公開に向けて取り組んでいると述べている。それまでは、コミュニティは同じシステム上で成果を再現したり、訓練データを検査したり、モデルの成功が訓練中に関連問題を見ていたことに依存していたかどうかを評価したりできない。公開と再現性は別の約束であり、今回のリリースは前者を果たしたが後者を伴っていない。

数学に固有のさらなる複雑さがある。この分野における帰属は理解によって成り立つ。証明は、それが導入するアイデアによって部分的に評価される。そして数学的アイデアが広まる方法は、人々がそれを読み、有用だと見出し、拡張することによる。誰も完全には把握していない機械生成の証明は、そのようには伝播し得ない成果である。引用はできる。しかし容易にその上に築くことはできない。

また、何年にもわたり査読を複雑にする実務的な非対称性もある。欠陥のある証明を発表した人間の数学者は、一般に誠実な誤りを犯したと理解される。評判上の結果は比例的なものだ。722件の成果を公開するモデルは、いくつかは正しく、いくつかは正しくないが、正しいものと誤ったものの比率自体が不明であり、誤ったものについて個人が責任を負うこともできない研究の集合を生み出す。学術誌は、著者が拡散しており、誤り率が一件の出来事ではなく分布であるような投稿を扱うようには作られていない。

引用の問題は直接的に続く。数学の進歩は、どの先行成果が信頼できるかを知ることにかかっている。Leanで機械検証された成果は有力な候補である。モデルによって主張され、誰にも査読されていない成果はそうではない。そして2つのカテゴリを単一のリリースで混在させることは、どちらもその上に築くことを難しくする。

同じ日のもう一つの話

OpenAIの数学リリースは、いくつかのファーストパーティの主張があり、サードパーティによる検証はあまりない週に登場した。

MistralはLarge 4を発表した。1兆パラメータのモデルで、オープンウェイトの中国製システムに対する西側で最強の答えとして位置づけられている。そのベンチマーク比較は、ある返信スレッドがArtificial Analysisの公表スコアと一行ずつ照合したところ不十分であり、具体的には競合の変種を都合よく選び、公表されたサードパーティの数値を誤って述べているという告発があった。

ReflectionはBeamを公開した。同じ争いを狙ったオープンウェイトモデルで、重みは同月後半に公開される。

そしてAnthropicは、ソフトウェア脆弱性を見つけるモデルへのアクセスを拡大し、独自のファーストパーティ数値を示した。

この週を通じたパターンは、能力に関する主張が、それを検証する能力より速く到着しているということだ。arXivは同じ圧力の別の現れに対応し、9月に記録的な40,363件の投稿を受け取った後、投稿者を月2本の論文に制限した。これは2年前の2倍の数字である。

競争は主張を使い物にすること

AIと数学の話には、スコアボードとして枠づけられる版がある。モデルは未解決問題をいくつ解けるか、というものだ。より有用な枠組みは、研究コミュニティにとって成果を使い物にするものは何かということであり、それにはモデルのリリースだけでは提供しないいくつかの要素が関わる。

査読者は議論を理解する必要がある。帰属は追跡可能でなければならない。他の研究者は、その成果を再導出せずにその上に築ける必要がある。そして広いコミュニティは、自らテストを実行できるだけの生成システムへのアクセスを必要とする。

最後の点で、このリリースは不十分である。他の誰も実行できないシステムによって生成された成果のコレクションは、貢献というよりデモンストレーションに近い。何が可能かを示す。しかし、分野が独立してその上に築けるものを手渡すものではない。

この移行の難しい部分は数学ではない。難しいのは、AIの能力が今や、それを検証するために存在する制度（査読、ベンチマーク再現、著者規範、引用慣行）を追い越しており、それらの制度は人間の時間尺度で動いていることだ。モデルは訓練実行で722件の成果を生成できる。そのどれが重要で、誰に功績があり、そこから何が続くかを解明するには、依然として何年もかかる。

述べておく価値のある対立見解がある。それは不合理ではない。コンパイルが通る形式証明は、誰が、あるいは何がそれを生み出したかに関係なく、証明である。数学は常に、由来ではなく成果そのものの価値で受け入れてきた。Leanが議論を検証するなら、その議論は成立する。この見方では、功績の議論は分野が通常の方法で解決すべき社会学的問題であり、再現性への固執は、人間の数学者にはかつて求められたことのない種類のアクセス要求である。人間の著者に思考過程を公開するよう求める人はいない。

反論はこうだ。人間の著者には自分の仕事を説明するよう求められるし、その説明こそ理解が宿る場所である。説明なしに届く証明は、たまたま検証済みの出力を持つブラックボックスである。分野はそれを引用できるが、教えることはできない。たとえ定理が真であっても、これは実際の損失である。

この週から出た実践的助言は、数学に限らずAI能力を購入する誰にでも当てはまる。証拠、権限、そして成功したデモンストレーションから再現可能な仕事への道筋を見せてもらうよう求めよ。ベンチマーク結果と動作するシステムは別の成果物であり、その間のギャップに驚きが潜む。