世界を動かす技術を、日本語で。

マスアポカリプス

概要

OpenAIによるAIが、数学界の長年の難問372件を「証明」したという歴史的ニュース。 証明の正当性や内容の理解は人間にはまだ困難で、専門家たちが必死に解析中。 AIによる証明の質や発表方法、今後の数学研究の在り方に大きな議論。 未解決の大問題(P≠NPなど)は依然として手付かず。 数学コミュニティの戸惑いと希望、そして新しい時代への適応。

AIによる数学的ブレイクスルーの衝撃

  • OpenAI が、 長年未解決だった372個の数学の難問 に対して「証明」を公開
    • Advisory groupには Timothy Gowers や Edward Witten など著名数学者が参加
  • 代表的な成果例
    • Unique Games Conjecture (UGC) の証明
      • UGCは多くの最適化問題のNP困難性を示唆
      • 証明には Lean certificate 付き(ただし全ての成果に証明書があるわけではない)
      • 人間による完全な理解は未だ進行中
    • L=BPL (確率的対数空間と決定的対数空間の等価性)などの古典的難問
    • Fourier変換と整数乗算のO(n log n)未満アルゴリズム の発見
    • Unitary Synthesis Problem の陽性解
    • Parity not in QAC0、 ランダム化と量子クエリ複雑性の大分離 など、理論計算機科学の主要問題への進展
    • 2次元ギャップハミルトニアンの面積法則 など物理数学分野の難問
    • 行列積のO(n^9/4)時間アルゴリズム などアルゴリズム分野の進展
    • 有理数上の多項式方程式の解の非計算可能性 など計算理論の根本問題
  • これらの成果は 個々でも「今年の大成果」級 であり、分野横断的にインパクト大

AI証明の現状と課題

  • 証明文書は AIによる自動生成 であり
    • 極めて読みにくい、 説明不足、 引用の混乱 などが多数報告
    • AIの助けなしでは読み解けない との声も
    • 新奇な構成や概念 が多く、人間の直感と異なるアプローチ
  • 証明の正当性検証 は始まったばかり
    • 数学者たちが 必死に解読・解説作業 を進行中
  • AIによる発表モデル の違い
    • OpenAIモデル :AIが証明を直接公開→人間が後追いで解説
    • Anthropicモデル :人間研究者がAI成果を消化・発表(対価あり)
    • それぞれに 長所・短所 が存在

数学コミュニティの反応と今後

  • 専門家の戸惑い・複雑な感情
    • 長年の目標がAIに先取りされる喪失感
    • それでも「UGCが正しかった」との 達成感・安堵感 も
  • コミュニティとしての適応
    • 数学者たちは「AIと共に新たな登山道を切り開く」役割へ
    • 人間同士の協力・解説の価値 は今後も変わらず重要
  • 未解決の大問題
    • P≠NP や P=BPP など、最難関問題は依然未解決
    • AIでも一朝一夕には突破できない壁の存在
  • AIの能力・安全性
    • OpenAI内部モデルは、 平均3時間/問題で5%の難問を解決
    • 一般公開の是非や安全性に対する懸念も

AI時代の数学の意味

  • 人間の創造性と冒険の意義
    • AIが「山頂」へワープさせても、 登山(過程)の価値 は消えない
    • 人間同士の協働・知的冒険 が今後も重要な役割
  • AI証明への懐疑論
    • 一部には「AIの証明は本物でない」「単なるパズル」との批判も
    • しかし、現実の進歩を無視できない段階に到達

まとめ

  • AIによる数学革命の幕開け
    • 証明の正当性・意義・人間の役割を巡る新たな議論
    • 数学者・研究者の適応と挑戦が続く時代

Hackerたちの意見

ちなみに、これがAIによって書かれたものでないことは、最初の文でわかるよね。 > 「ママ、聞いたよ!君が料理されたって!君が一生懸命取り組んできた数学の問題をロボットが解決したって!」うわっ!うちの8歳の子がまさにこんな感じで話すんだ。ダイニングテーブルで同じように言ってる姿が想像できるよ。ChatGPTに「今日は8歳か9歳の子供になりきって、ママの仕事がAIに取られたことをどうやって侮辱する?」って聞いてみたら、こんな返事が返ってきたよ。 > 「ママ、AIが君の仕事を奪ったんだって。ロボットですら『うん、これなら俺たちの方が上手くできる』って思ったみたい。」 > 「ママ、おめでとう!コンピュータに取って代わられたよ。今やSiriですら仕事を持ってるのに、君は持ってない!」 > 「ママ、AIが君の仕事を奪った?マジで?ロボットですら君の仕事を見て『俺がやるよ』って言ったんじゃない?」 > 「心配しないで、ママ。まだ役に立てるよ…AIに私のランチの作り方を教えるとか。」 どれもなんかミレニアル世代っぽい感じがするし、ちょっと awkward で機械的な皮肉だね。子供たちと語彙の変化が、最高のAI検出器になるって信じてるよ。

└

「今のトレンディな言葉を使う」って追加したら、結果がちょっと機械的じゃなくなったよ。その中の一つには「料理された」って言葉が入ってたし、もう一つには「ネガティブオーラ」ってあった。無料のGoogle AIを使ったんだけど、(例は削除したけど…)うちの孫たちが言うことに微妙に近かったよ。編集:すごい、何百もの非AIコメントがフラグされてないのに、即フラグされた。HNがAI検出に何らかのヒューリスティックを使うと思ってたけど、そうじゃないみたい。

└

明らかに問題なのは、そんなジョークはひどいとしても、8歳の子供が作るにはちょっと高度すぎるってことだよね。父親に対してフェミニズムについて鋭いコメントをする小さな女の子のミームを思い出すな。

霧に包まれた山の頂上にテレポートされたクライマーのメタファーが好きだったな。テレポーターが存在する今、もっと高い山に登って探検するために使うべきだと思う。AIが存在しない世界には戻れないよね。

└

問題は所有権だね。AIからの知識を分配したり、助けてくれる人に報酬を与える手段がないんだ。経済的な目的のためのすべての象徴的かつ数値的な推論がAIによって行われる世界に急速に移行しているよ。

なんかサイケデリックなものを書いてる人が書いたみたいに感じる。すごく不明瞭で意味がわからない。以前の仕事の名前をたくさん出してるけど、なぜそれが不可能な結果にもかかわらず使えるのかについては話してない。 > 基本的に、この論文はひどく書かれていて、AIの助けなしでは読むのが不可能だよ。これは面白いし、このイベントの報道では見たことがなかったね。理解するのが大変そうだ - 他の人のごちゃごちゃしたコードを理解しようとしているみたいで、それでも正しい出力が出てる感じ。

└

これらの証明が、より人間に読みやすい証明の試みを競争で圧倒することでエコシステムにリスクをもたらすという恐れとも一致してるね。でも、もしかしたら、これらの証明を編集して注釈をつける数学インフルエンサーが増えるかもしれない。私たちに戻してくれるかもね。

└

数学の証明は、正しい出力を正しく出さなきゃいけないけど、それはちょっと違う話だよね。これはAIのIPO PRの力技みたいに見える。今のところ、証明がチェックされてないし、人間がそれを確認するのは難しいかもしれない。証明は明確であるべきなのに、ひどく書かれていて雑音が多いのは怪しい。雑音は、 brute force と認知の違いを示してる。人間の証明は論理的に正しいだけじゃなくて、認知的に洗練されていて一貫性があるはず。理解するのに何年もかかるかもしれないけど、論理の流れはわかりやすくて、曖昧じゃないはず。迷路を通る道はできるだけ短く、地図はできるだけ明確であるべきだよね。これはその逆のように聞こえる。迷路の中に本物の道があるかもしれないけど、あまりにも複雑で時間がかかりすぎると確認するのは不可能になる。次のステップは、証明が人間のスケールであるか、あるいは人間のスケールの証明が不可能であることを証明することを要求することだと思う。機械の証明が最高のものであることを示すのもありかも。ハルティング問題に引っかからずにそれが可能だと思うけど、証明はできない。

└

最近のAIのデフォルトな体験ってそんな感じじゃない?小規模だとAIモデルはアイデアを明確に表現できるけど、アイデアが大きくて複雑になるほど、出力は人間には適さなくなる。AIモデルは人間とは違う考え方をしてるみたいで、その特定のトピックの専門家が期待するように複雑なアイデアをコミュニケートするように訓練されてないんだろうね。

└

この証明の山は、オープンソースのリポジトリを圧倒する低品質なドライブバイPRの氾濫を思い出させるな。

└

genAIを使ったコード開発との類似点がたくさんあるね。驚くことじゃないと思うけど。

└

基本的にその論文はひどく書かれていて、AIの助けなしには読むのが不可能だ これ、過去1年の職場のPRを全部表してるよ。何も言ってない10,000段落以上のコメントの差分。ハンコ押して次に行くしかない、他にできることはない。

Hacker Newsで議論の続きを見る