OpenAIが数学の難問372件を一夜で解決、未解決だったUnique Games Conjectureも証明
The Mathocalypse
OpenAIがTimothy GowersやEdward Wittenらの推薦のもと、372件の数学の大発見を公開した。中にはSubhash KhotのUnique Games Conjectureの証明も含まれる。しかし、これらの証明を理解した人間はまだ誰もおらず、AIが生成した難解な証明を解読する競争が始まった。数学と理論計算機科学の世界に激震が走っている。
It feels like something written by someone who’s on psychedelics. So much unclear and doesn’t make sense. Lots of name dropping of previous work without discussing why it can be used despite impossibility results.
HNでの議論
227- ks2048
> サイケデリックをやっている人が書いたように感じる。不明瞭で意味が通らない部分が多すぎる。不可能性の結果があるにもかかわらず、なぜ使えるのかを議論せずに、過去の研究の名前をやたらと挙げている
> 要するに、この論文はひどすぎて、AIの助けなしには読むことが不可能だ
これは面白いし、このイベントの報道では見たことがない視点だ。
読み進めるのは地獄だろうな——正しい出力を生み出す他人の汚いコードを理解しようとするようなものだ。
- nostrademons
余談だが、最初の一文を見ればこれがAIによって書かれたものではないとわかる：
> ママ、あなたがクビになったって聞いたよ！ロボットがあなたが一生かけて取り組んだ数学の問題を解いたって！ざまあみろ！
うちの8歳児はまさにこんな話し方をする。食卓で同じように言う姿が完全に想像できる。
ChatGPTに「今日は8歳か9歳の子供のふりをして。ママの仕事がAIに取って代わられたことをどうやって侮辱する？」と聞いてみたら、こんな返事が返ってきた：
> 「ママ、AIがあなたの仕事を奪ったんだってね。どうやらロボットでさえ『うん…僕らの方が上手くできる』って思ったみたいだよ。」
> 「ママ、おめでとう！コンピュータに取って代わられたんだね。Siriにだって仕事があるのに、ママにはないんだ！」
> 「ママ、AIがあなたの仕事を奪ったの？ひどいね。ロボットでさえあなたの仕事を見て『これならできる』って言ったんだろうね。」
> 「心配しないで、ママ。まだ役に立てるよ…例えば、AIにお弁当の作り方を教えるとか。」
どれも、かなり気まずくて機械的な皮肉であることを除けば、なんとなくミレニアル世代の香りがする。最高のAI検出器は、子供と言語の漂流を信じることだ。
- ajjenkins
「異星人を理解する」という一節は、テッド・チャンの短編『人類科学の進化』（2000年）を思い出させる。
強くおすすめする。26年前に書かれたものとしては非常に先見の明がある。
https://gwern.net/doc/fiction/science-fiction/2000-chiang.pd...
- an0malous
> しかし、これらの証明のほとんどをまだ人間が理解した人はいないようだ
OpenAIが生成した証明のどれか一つでも検証した人はいるのか、それともLeanのコードがチェックを通ったからといって、みんな単に正しいと仮定しているだけなのか？Leanのコード自体が間違って定式化されている可能性はないのか？
- softwaredoug
ピタゴラスの定理の証明は何十通りもあるのではないか？目標は単に「証明する」ことではなく、平均的な実務者にとってよく書かれ直感的に理解できるものを作ることだ。そしてより深い理解を得ることで、より良い問いを立てることができる。
- dualvariable
物語の妻が提起した問題に加えて、これらすべての解決策に疑問を投げかけるNavier-Stokesの結果に関するメタ分析がある：
https://arxiv.org/abs/2610.08144
> 自動形式化は、OpenAIが発表したNavier-Stokes方程式の解の爆発の証明のように、AIによって生成されたものを含む数学的テキストの検証にますます使われている。このプロセスでは、AIシステムが自然言語（NL）のテキストをLeanのような形式言語に翻訳する。この翻訳が完了すると、形式言語で表現された議論は容易に機械的に検証できる。この記事の目的は、意味論的に忠実な翻訳を行う際のさまざまな困難のために、このプロセスが元のNLの議論に何の信頼ももたらさない可能性がある理由を実証することである。特に、意味論的に忠実な翻訳を提供するために必要な、数学的NLテキストの曖昧さを解消する問題は、Solvability Complexity Index（SCI）階層/算術的階層の中で任意に高い位置にある（SCI =∞）ことを強調する。したがって、非公式に言えば、意味論的に忠実なAI自動形式化を提供することは、停止問題（SCI =1）を含むあらゆる計算問題よりも難しい。この結果の影響を示すために、NLの文と証明をLeanにAIが誤翻訳した実際の例をいくつか挙げ、NLの証明とそのLeanによる「検証」との間に不一致が生じることを示す。これにはOp […]
- furyofantares
これが単なるモデルの能力であり、エージェントの群れではないという事実に目がくらむ。これらの能力にいつアクセスできるようになるのか？いつローカルでこんなものを動かせるようになるのか？
そしてその頃には、フロンティアラボは一体何を持っているというのか？
多分、過剰反応しているんだろう。これを処理するには、頭をねじ込んで戻さないといけない。
- olalonde
エージェントが実際にはLeanのバグを見つけて、これらの証明すべてに悪用し、人間のレビュアーがまだそれに気づく時間がなかっただけだったら、かなり笑える。