OpenAI、数学論文を3本撤回

では、撤回された3本の証明はLean検証なしのものだったのか？

もしそうなら、なぜLeanで検証された証明と自然言語の証明を混ぜたのか？

Aaronsonのブログを読んでいて疑問に思った：

https://scottaaronson.blog/?p=10169

少なくとも、我々はそれが証明であるとかなり確信している！他の372の画期的成果のいくつか（すべてではない）と同様に、Lean証明書がある。しかし、これらの証明のほとんどをまだ誰も理解していないようだ。

明らかなことは、検証済みのものと、良いアイデアがあるかもしれないが間違いもあるかもしれないものの二つに分けてリリースすることだろう。後者は人間が検証するにははるかに高コストになるだろう。

よく見れば、これらの完全にAI生成された証明の多くは崩壊すると思う。Leanでさえ、コンパイルは通るが意図とは異なることを述べている理論を構築できる。ただ、証明の量が圧倒的に多いため、abc予想のように問題を発見するまでに何年もかかるだろう。

整数乗算のO(n log n)を打ち破るという論文もかなり怪しいと思う。確信はないが、あまりに出来すぎているように思える。そこには微妙な欠陥があるに違いない。単に私が論文のこれらの小さな数字を嫌っているだけかもしれないが、間違っている、いや不自然にさえ思える！光速をほんのわずかに超えられると主張する物理学論文にも同様に懐疑的だろう。ここでn log nが自然な限界である理由はないが、いくつか良い直感は見えるので、エレガントな形で表現できない何か別のものがあるというのは、私には非常に「非数学的」に思える。

このようなダンプをするなら、すべて形式化されるべきだ。手作業でレビューするにはあまりに多くの資料があり、さらにAIが書いているので人間の作品に比べて読みにくい。

なんというタイムラインだ、OpenAIのモデルは優秀すぎて、何百もの数学論文を出版する。

最新モデルは以前に出版された数学論文の誤りさえ見つける！！！*

* これまでのところ、欠陥があり撤回が必要だったのはOpenAIの数学論文だけだ。

ソフトウェアエンジニアリングの慣行が数学と出会うとこうなる。「openai/math リリース1.3.42：論文139と140を撤回、論文47の符号エラーを修正、以前撤回された論文85を復元、論文101の議論をリファクタリング」。

撤回が、実際の数学者が論文を見て誤りに気づいたためなのか、それともモデルを走らせて校正したためなのか興味がある。後者なら、出版前に必ずやっていただろうから初めてではないはずだ。どちらの選択肢も興味深い含意がある。

約400本中3つの誤り（今のところ）なら、まだかなり良い的中率だ。

つまり数学は「ボードに投げてくっつくか見てみる」段階に入ったのか。。

これはOpenAIがさらなる仕事を盗んでいるだけだ。

彼らが出版することに問題はない。プロセスや彼らの関わり方にも問題はない。彼らが実際にこれらの作品の管理者として行動していることは喜ばしい。

それはさておき、問題を検証している人々に報酬を支払うべきだ。本当に腹立たしいのは、この検証過程で出版されたものは何でも次のトレーニングセッションに吸い上げられることが分かっている点だ。