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

OpenAIのモデルが離散幾何学における中心的な予想を覆した

概要

  • 単位距離問題 に関する80年来の未解決問題をAIが解決
  • OpenAIのモデル が既存の最良予想を覆す構成を発見
  • 代数的数論 の新手法が幾何学問題に応用された点が注目
  • AIと数学者の新しい協働形態 の先例となる成果
  • 今後の数学・科学研究 におけるAI活用の可能性を示唆

単位距離問題のAIによるブレークスルー

  • 単位距離問題 は1946年にPaul Erdősが提起した組合せ幾何学の有名問題
  • n個の点 を平面に配置したとき、距離がちょうど1となる点のペアの最大数を問う
  • 長年の定説 では、点を格子状に並べる構成が最適と考えられていた
  • OpenAIの内部モデル がこの定説を覆し、多項式的な改善をもたらす無限族の構成を発見
  • 外部数学者 による証明の検証と、背景・意義を解説する論文も作成

問題の歴史と数学的背景

  • u(n) はn点から得られる最大の単位距離ペア数
  • 線上配置 ではn-1ペア、 正方格子 では約2nペアが得られる
  • 最良既知構成 は、n^{1 + C / log log(n)}の成長率
  • Erdősの予想 はn^{1+o(1)}が上限とするものだった
  • 今回のAI証明 は、n^{1+\delta}(δ>0)となる構成の存在を示し、予想を否定
  • Will Sawin による補強で、δ=0.014が明示可能と判明

代数的数論による新手法

  • 証明手法 は、Gaussian整数から一歩進んだ代数的数体の利用
    • Gaussian整数:a+bi(a,bは整数、iは虚数単位)
    • これを一般化した 代数的数体 の対称性を活用
  • 無限類体塔Golod–Shafarevich理論 などの高度な数論的道具を使用
  • これらの数論的構成が、ユークリッド平面の幾何学的問題に意外な形で応用された点が画期的

数学とAIの新しい関係

  • AIが自律的に未解決問題を解決 した初の事例
  • AIモデル は特定の数学分野や問題に特化せず、一般的推論能力で解に到達
  • 数学者との協働 により、解そのもの以上の新たな知見や研究分野の橋渡しが生まれる
  • Thomas BloomArul Shankar ら一流数学者もAIの創造性を高く評価

今後への示唆と意義

  • AIによる数学的発見 が他分野にも波及する可能性
  • 複雑な論理構造や遠隔分野の知識連携 をAIが担うことで、研究者の新たなパートナーに
  • 人間の専門性と判断力 は今後も不可欠
  • AIは探索・提案・検証を担い、人間が問題選択や解釈を主導 する新たな研究スタイルの到来
  • AIの進化と人間の協働 による、より豊かな知の地平の拡大

Hackerたちの意見

確かなことは、OpenAIのモデルがAnthropicやGoogleのモデルに比べて学術界で明らかにリードしているってことだね。学術関係の人たちにとって、OpenAIは選ばれるベンダーなのかな?

Geminiは学習に対してより良く訓練されているように思うし、Googleは教育的なベストプラクティスを最適化するために意図的に努力していると思う。(例えば、チュータリング、形成的フィードバック、認知負荷の最適化など)学術研究に関しては(このスレッドのテーマね)、なんとも言えないけど。

よりシンプルな説明をすると、もっと多くの人がChatGPTを使っているってことだね。

Xの数学者たちはみんなGPT 5.5 Proを使ってると思う。

限られたテストからだけど、Geminiはプロンプトを十分に詳細にすれば、見つけにくい情報を掘り出せるよ。Googleが「ウェブインデックス会社」だから、見つけにくいものを探すのは彼らのモデルにとって自然なことだし、これが私がこのモデルたちに求めている唯一の方法なんだ。ネットを一週間探しても見つからなかったら、巨大なプロンプトを与えて、探しているものを掘り出してもらうよ。

OpenAIは特にアカデミアをターゲットにして、トップの学者や大学、研究者に対して多くの無料/無制限の利用を提供してたよ。研究者として申請できる助成金も出してるし。他の研究所もやってるかもしれないけど、OpenAIが最初だったと思う。

AlphaFoldはもう数年の間に実際の発見に使われてるんじゃない?

OpenAIのモデルは、自動生成された定理証明データでたくさん訓練されてるみたい。GPT 5.5はLeanを書くのが本当に得意だね。

前にも言ったけど、AIはマクドナルドを管理する前にフィールズ賞を取るだろうね。難しいのは、数学をプレイするためのチェスボードを作ることだった(Lean)。今はただのパターン認識と計算だよ。LLMは始まりに過ぎないし、StockFishに似たより専門的な数学AIがすぐに出てくると思う。

それには同意できないな。フィールズ賞に値する仕事をする前に、マクドナルドを運営できるようになると思う。どちらかが起こる前にマクドナルドをうまく運営してると思うし、両方が起こった後にフィールズ賞を受賞することになると思う。

マクドナルドを運営するのは、今のところ統合とモダリティの問題だと思う。これらのモデルがその仕事に必要な推論能力や世界知識を欠いていることに疑いを持っている人はいないんじゃないかな。だから、根本的な技術的問題というよりは、プロセスエンジニアリングの問題だと思う。

AIはもうそれには古すぎるよ。

フィクションの「マナ」管理システムからのマクドナルドのディストピア感を管理する。これは「逆ケンタウロス」自動化がたくさん関わっていた。 > マナは常にやるべきことのリストを持っていた。レジからの注文が入ってくるので、マナは従業員にその食事を準備するよう指示した。定期的に掃除するトイレや、モップがけする床、拭くテーブル、掃く歩道、解凍するバンズ、回転させる在庫、洗う窓などもあった。マナはやるべき数百のタスクを管理し、一つずつ従業員に割り当てていった。 [...] > シフトの終わりには、マナはいつも同じことを言っていた。「今日はお疲れ様でした。手伝ってくれてありがとう。」それからヘッドセットを外して、充電のためにラックに戻す。ヘッドセットを外した最初の数分はいつも混乱する — 6時間か8時間、頭の中で何をすべきかを詳細に指示する声があったからね。レストランを出るためには、脳を再起動しなきゃいけなかった。 [0] https://en.wikipedia.org/wiki/Manna_(novel)

証明はLeanで書かれてるわけじゃないよ。英語で書かれてて、意味不明じゃないか確認するために人間の専門家による検証が必要なんだ。

マクドナルドが実現しない理由は政治的なものだけだね。フィールズ賞も同じようなもんだ。

難しい部分は、数学(Lean)をプレイするためのチェスボードを作ることだった。今はただのパターン認識と計算に過ぎない。でも、これはLeanでは検証されてない。純粋に普通の言葉でのやり取りだったと思う。多くの点で、これは君の言ってることとは真逆の、かなりエキサイティングなデモだと思う。検証は、証明をコンピュータにチェックさせたいときに必要になるんだ。現状では、この証明はその分野の数学者たちによって手動で検証されたものなんだ。

我々のローカルAIモデルは、すでにマクドナルドを運営できる能力があるよ。

もうすぐStockFishに似た専門的な数学AIが登場するだろうね。 ヒューリスティックに重み付けされた有向グラフ?すごい、誰もそんなことやったことないだろうね。

芸術や科学を自動化して、ハンバーガーを flip するために働く未来なんて最悪だね。

グウィン・ショットウェルの言葉を借りると、「ただの大きなマルコフ連鎖にしては、悪くないよね?」

エルデシュ、またはモデル?

エルデシュの問題が解決されたって話ばかり聞くのはなんでだろう?他にも解決されていない数学の問題がたくさんあると思うけど、r/singularityやr/accelerateで見かけるChatGPTの「数学のブレイクスルー」は全部エルデシュの問題なんだよね。

確かに、これはコミュニティとデータベースがあるからだと思う。

彼らが有名なのは、エルデシュが偉大な数学者だったからだよ。ちょうど一世紀前のヒルベルト問題みたいに。

これは興味深くて難しい問題の大きなセットだけど、数学者たちが何十年も、あるいは何世紀も持続的に注目してきたほど基礎的でも重要でもないから、実際にはLLMで解決できるかもしれないね。

エルデシュ問題は表現が簡単だから、AI数学の最初の年のベンチマークには最適だね。

エルデシュ問題だけじゃないよ - https://news.ycombinator.com/item?id=48213189

エルデシュの問題は、明示的に述べられたけど解決されていない数学の問題のかなりの割合を占めてる。十分に有名だから人々が気にかけるけど、興味がないからあまり解決しようとする努力がされていない。人々が既に述べられた問題を解決するのは、数学研究のニッチな活動なんだ。もっと多くの場合、人々は自分が興味を持っていることを研究して、それを解決できるようにフレームを作り、その後解決策を考え出そうとする。理想的なケースでは、フレームも解決策もそれ自体で面白いものになるんだよね。

このタスクの要約された思考の流れ(ブログ記事にリンクされてるやつ)は125ページもあるんだ。これはすごい規模の推論で、AnthropicがMythosでほのめかしていることにかなり似てる。

今日は、SQLモデルの3つの行を修正するために、LOTRの本2冊分に相当するものを生成したよ(PRも開いたし)、だから+1。

これについて知りたい人のために - https://cdn.openai.com/pdf/1625eff6-5ac1-40d8-b1db-5d5cf925d...

「LLMはただのトレーニングデータを補間している」って言ってる人たちへ:アイヤーや、異なる形で初期のウィトゲンシュタインは、数学的真理は世界について新しい事実を報告しないって考えてた。証明は公理や定義、記号、ルールにすでに含まれていることを展開するものだと思う。この考えはすごく魅力的だし、数学者に発見をクレジットすることに問題は感じない。だから、「既存の素材を再結合する」ことが無効化するわけではないか、たくさんのフィールズ賞を返さなきゃいけなくなる。

新しい数学が「発明」されるのか「発見」されるのかについての長年の議論を見てみて。僕が知っているほとんどの数学者は、発見されるものだと思っているよ。

そのアイデアは本当に魅力的だと思うし、数学者に発見をクレジットすることに問題はないと思う。ほとんどの発見は公理から示唆されるけど、時々新しい数学が(適切な言葉が見つからないけど)「創造」されることがある。デカルトやニュートン、ライプニッツ、ガウス、オイラー、ラマヌジャン、ガロアなんかは、数学を科学よりもアートに近いものとして扱っているよね。例えば、リーマン予想を解決するには、新しい種類の数学が必要だと多くの人が信じている。個人的には、LLMがそれを発明することはないと思う。

LLMが単にトレーニングデータを再構成しているわけじゃないのは明らかだよね。Claudeは、ほとんど死にかけてるプログラミング言語のArcでプログラムもできるし、新しい言語構造も使える。つまり、すべてのプログラミング言語の構造は既存のアイデアのリミックスに過ぎないか、LLMがトレーニングデータが存在しない領域でも働けるってことだよね。

なんか「問題解決」するときはいつもそう感じるんだよね。クリエイティブってわけじゃなくて、既に存在する概念空間のグラフを整理してるだけ。可能性が多ければ多いほど、ノード間の最適なルートに向かいやすくなるけど、ノードやエッジを「作った」わけじゃなくて、ただの因果関係の必然なんだよね。

既存の素材を再構成するのはその通りで、今回の場合、LLMは人間のグループよりも早くそのつながりを見つけるのに特別な位置にあったんだ。証明は、組合せ幾何学の問題に適用された非常に深い代数的数論の機構に依存してる。これらの全く別の分野に精通した二人の人間は、お互いに知識を教え合うのにかなりの時間を要するだろうし、それからやっとこの解決策にたどり着けるんだ。

今日、全く異なる文脈でウィトゲンシュタインに言及されたのはこれが二回目だ。彼の『論理哲学論考』にすごく共感することを思い出させてくれた。

大人なら、フィールズ賞や他の年次の「賞」が「再結合型」の革新と「新次元的思考」の革新の両方に与えられることを理解していると思いたいね。人間が毎年、すべての分野で「新次元的」な革新を生み出すわけじゃないし。確かに、LLMは「ただ」物を再結合してると思う。でも、もしすべてのニュートン以前やライプニッツの代数・幾何・三角法のテキストでLLMを訓練しても、微積分を作り出せるとは思わないな。(間違ってるかもしれないけど、証明されるのも構わない。)でも、こういうのはLLMが得意とする革新のタイプで、人間も「再結合型」の革新に優れている必要があることを否定するものじゃない。新しいアイデアを合成する面では、まだまだ人間ができることが多いと思う。

数学には創造的な側面があるんだよね。定義やルールが作られるから。

これはいい指摘だね。数学が発明されたのか発見されたのかという深い哲学的な問いがある。個人的には両方だと思ってる。とはいえ、「LLMはただ訓練データを補間している」というのは、感情やLLMに対する敵意から生まれる修辞的な表現として捉えられることが多い。彼らが言いたいのは、もっと強いバージョンで、「LLMは内部の概念や意味、論理のモデルを持たずに、訓練データから確率的に情報を吐き出している」ということ。これについては、約1年前にLLMが数学にかなり優れていることが証明された(IMOでの金メダル)ことや、より高い概念やカウントをモデル化するネットワークの小さな部分を指摘できる機械的解釈可能性の研究によって、すでに反論されていると思う。LLMが新しい数学的結果を証明したり反証したりすることは、まさにその証拠だよね。今のところ、これを否定する人たちとどう接するかも分からない。議論は進んでいて、もう興味深くもない。だから、あなたに同意するし、自分の言動も広い意味で自分の経験と遺伝的な遺産の補間だと言えるよ。他に何があるっていうの?創造性は、既存のアイデアや経験、スキルをちょっとしたランダムさや運を加えてリミックスすることかもしれないし(「偉大なアーティストは盗む」とかね)。でも、これがLLMについて似たようなことを言うときの人々の意図とは通常違うんだよね。

これがどれだけ実現可能かは分からないけど、特定の時期に限定した訓練セットを使うという思考実験が好きなんだ。その後、モデルが既に知っていることを発見するためにどれだけヒントが必要かを見るのは面白そう。例えば、1915年以前の物理知識で訓練して、古典力学から一般相対性理論に進むとか。

コーディングにLLMを多用している人には、これがあまり驚きではないはず。時間の問題だったんだよね。数学者は新しい方法で数学的ツールを構築し、応用することで新しい発見をする。直感に従ってつながりを探る、たくさんの反復作業があるんだ。LLMは本当の意味で「発見」をすることはできないけど、狭い目的であらゆる数学的ツールをモンテカルロ法で試してみて、何がうまくいくかを見つけて、それを基にしたり改善を組み合わせたりすることはできる。記事を読むと、まさにそうやって発見がなされたみたいで、LLMが「驚くべきつながり」を使って予想外の結果を超えたんだ。でも、その結果には人間の意図がなければ意味がないし、AIが使った新しい道筋を評価するための人間の理解(結果そのものよりもずっと価値がある)や、概念を探るための数学的言語(人間が作ったもの)が必要なんだよね。

このトピックについて、数学者による長くて面白い最近のエッセイがあるよ: https://davidbessis.substack.com/p/the-fall-of-the-theorem-e...

結果には人間の意図がなければ意味がないし、AIが使った新しい経路を評価するための人間の理解(結果そのものよりもずっと価値がある)や、概念を探求するための数学的言語(人間が作ったもの)が必要だよね。これってただの人間中心主義じゃない?なんで理解は人間だけがするべきなの?知識は人間だけのものなの?もし他の種が重力と量子力学の矛盾を解決したとして、それを私たちに説明して理解させない限り意味がないの?

面白いのは、証明(反証)はエルデシュの元の予想の反例を見つけることで行われたってことだと思う。リンクされたPDFの数学者の反応の一つに同意するけど、実際の予想が正しいことを証明するよりは、ちょっと興味が薄いかな。僕の目には、予想が正しいことを証明するにはもう少し理論を練る必要があると思う。予想が正しい理由を、より大きな理論に基づいて説明しなきゃいけないからね。一方で反例の場合、モデルはただより高度な検索を行って正しい構造を見つけるだけで済む。もちろん、この検索は単純じゃなくて印象的で、反例との関連を証明するために多くのステップが必要だけど、新しい深い数学を発展させるのではなく、既存のアイデアをつなげてるだけなんだ。この偉大な成果を軽視するわけじゃないけど、僕は本当に進展があると思う!僕の感覚だけど、モデルは新しい数学を発展させる必要があるような、もっと複雑な予想を証明できる理論を練るところまで近づいてると思う。あとは、彼らがより長い時間軸で作業できるようになるだけだと思う。

この証明は、代数的数論から意外で洗練されたアイデアを持ち込んで、基本的な幾何学的な問題に取り組んでいる。これらの成果について読むほど、これらのモデルの力の多くは、あらゆる分野の前知識を持っていて、新しい領域に問題なく移行できることから来ている気がする。私にとって、この潜在的な美しさは、これらのツールが今日の科学における人間の超専門化を打破する手助けになるかもしれないってこと。重要な一方で、それは人間がアクセスできるツールやインスピレーションを制限することにもなる。

(ポスドクの)数学者として言わせてもらうと、これはかなりワクワクするね。私の専門外だけど、補足のコメントのドキュメントはかなり読みやすい。ここでの証明は文献の結果にかなりインスパイアされているようだけど、調整は簡単じゃない。少なくとも私には、全体の出版物が新しくて興味深いと考えるには重要な部分に見える。多くの同僚と私は、研究プロセスでLLMを使って実験してきた。かなり良い成果が出ているけど、こうやって私の研究課題を完全に解決することはあまりないかな。通常は、私の方での洗練や質問のやり取りがあって、最終的にアイデアが明らかになる感じ。伝統的な研究の洗練プロセスと似てるけど、より良い。もちろん、彼らが使っているモデルにはアクセスできないけどね =) 。それでも、この書き込みで気になったのは、モデルからの引用された最終回答に出典がないこと。数学のような分野では、ほとんどの研究が公に投稿されていて、入手可能だから、以前の結果の出典は社会的信用であり、抽象を見つけたり構築したり、注意を集中させる方法でもある。人間が編集した論文には当然これが含まれている。思考の連鎖の出版物を掘り下げてみたら、実際に(いくつかの)出典を見つけたよ。もしこのLLMに取り組んでいる人が読んでいるなら、これらが実際のモデルの出力に含まれることが私にとっては非常に重要なんだ。もう一つの注意点:HNや他の場所でのこういう記事に対するコメントは、通常かなりネガティブだったり落ち込んでいたりする。そうなる理由は大いにあるし、これらの企業が自分たちをどうマーケティングしているかや、技術の支持者がSNSでどう振る舞っているかを考えると、私も才能あるクリエイターが置き換えられるのを見ると、嫌悪感しか感じない。だけど、科学者にとっては、これらのツールがフロンティアにおける爆発的な複雑さの壁の問題に対処していると思う。毎日、最近の関連する進展を把握するのがますます難しくなっているから。数学者たちがこの時代にどれだけのスケールに達するか、非常に楽観的にならざるを得ない。