AIと数学 -- 2022年 vs 2026年 この4年間で何が起きたのか？

【 AIと数学 -- 2022年 vs 2026年 (1) 】

このセッションでは、AIと数学の領域での変化を振り返ってみようと思います。

僕は、これまでも述べてきたように、AI技術は、

　AI-1 ： 「 大規模言語モデル＋α 」から
　AI-2 ： 「 大規模言語モデル＋形式的証明システム＋α 」へ

と発展・進化していると考えています。この変化の中心舞台が、AIと数学の領域です。

【 2022年 OpenAI "Theorem Prover Project" 】

AI-1からAI-2 への移行はいつから始まったのでしょう。
そこには明確な画期があったと僕は考えています。それが、当時 OpenAIにいた Ilya Sutskever が主導した "OpenAI Theorem Prover Project" です。

【 2026年 ”Ten Advances in Mathematics and Theoretical Computer Science”
 】

それでは、AI-1からAI-2 への移行の「始まり」ではなく、AI-1からAI-2 への移行そのものの画期となるのは、どのような動きでしょうか？　それは、今年 2026年7月 OpenAIが公開した論文 ”Ten Advances in Mathematics and Theoretical Computer Science” だと僕は考えています。

【 AI-1からAI-2 への移行の意味を考えることの重要性 】

変化の激しいAIの世界で、2022年ー2026年の4年間というのは、いろんな事があったとても長い時間です。Ilya Sutskever 自身 OpenAI を去りました。このAI-1からAI-2 への移行は、AI技術の変化を振り返りその未来を展望するうえで、決定的な出来事だと僕は考えています。もちろん、この「移行」は、完成したわけではありません。ただ、AIにとって、大きな扉が開かれたと、僕は考えています。

今回のセッションでは、2022年のプロジェクトの振り返りを中心に行います。

【 2022年 Ilya Sutskever が考えたこと 】

ディープラーニングの到達点：

「ディープラーニングは、言語・ビジョン・画像生成を含む多くの分野で目覚ましい成功を謳歌してきた。 ディープラーニングがまだそれらの分野と比肩しうる成功を収めていない一つの領域がある。それは、広い見通しとシンボルに基いた推論を必要とするタスクの中にある。」

我々のモデル(Theorem Prover)の限界：

「我々は、何度も我々のモデルが生成した証明手順の複雑さに、強く印象付けられてきた。しかし、こうした推論ステップを必要とする証明の多くは、現在のコンピュータの能力の地平
を超えたところにある。」

「我々が、たとえ挑戦的な数学オリンピックの選択された問題を解いたとしても、我々のモデルは、いまだこれらの競技の最も優秀な学生たちと競争するにはは
るかに遠い場所にいるのである。」

「我々のモデルはcutを生成するいくらかの能力を示したものの、彼らが生成したcutはたいていの場合、浅いものだった。(それらは、ごく少数の証明ステップ(tacticのこと)しか含ま
ず、必ずしも、証明の構造を深く変えることはなかった。)」

--------------

参考資料
--------------

● OpenAI　2022年2月

“Solving (Some) Formal Math Olympiad Problems”
https://openai.com/blog/formal-math/

“Formal Mathematics Statement Curriculum Learning”
https://arxiv.org/pdf/2202.01344.pdf

“Theorem Proving in Lean 4”
https://leanprover.github.io/theorem_proving_in_lean4/

● OpenAI　2026年7月

”Ten Advances in Mathematics and Theoretical Computer Science”
https://cdn.openai.com/pdf/ten-proofs-oai.pdf

”How the Ideas Came Together”
https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf

10の証明のGithub
https://github.com/openai/ten-proofs

----------------------------
2022年のOpenAIの取り組みのマルレクでの紹介
----------------------------

2022/03/26「コンピュータ、数学の問題を解き始める」 まとめページ
https://www.marulabo.net/docs/math-proof/
コンシェルジェαバージョン
https://www.marulabo.net/20220326md/

「コンピュータ、数学の問題を解き始める」 講演資料 pdf 
https://drive.google.com/file/d/12726t4yD0ouUngmFXSy2UIzvQptSdP6g/view


「コンピュータ、数学の問題を解き始める」 講演ビデオの再生リスト
https://www.youtube.com/playlist?list=PLQIrJ0f9gMcNz3RKzDYCANRvt7NciY86X

講演ビデオ　第1部「Open-AI Theorem Prover」
https://youtu.be/ZehrcJpWl-M?list=PLQIrJ0f9gMcNz3RKzDYCANRvt7NciY86X

講演ビデオ　第1部「Open-AI Theorem Prover」mp4ファイル
https://drive.google.com/file/d/1FLIyXWAp3wTQgYiSA0Vw98OBXzatacAy/view?usp=sharing

講演ビデオ　第1部「Open-AI Theorem Prover」講演pdf
https://drive.google.com/file/d/1rh4vUaO6w8HunrTno2HulVXCsT9q-4Hg/view?usp=sharing

講演ビデオ　第2部 「Open-AI Theorem Proverは何を学習したのか？」
https://youtu.be/bA0nkOPERb4?list=PLQIrJ0f9gMcNz3RKzDYCANRvt7NciY86X

講演ビデオ　第3部 「数学者、証明にコンピュータを使い始める」
https://youtu.be/UNERLM4vdDg?list=PLQIrJ0f9gMcNz3RKzDYCANRvt7NciY86X

講演ビデオ　第4部 「形式的証明の背景と変化の意味を考える」
https://youtu.be/J4w3i6TijG8?list=PLQIrJ0f9gMcNz3RKzDYCANRvt7NciY86X

講演ビデオ　第4部 「形式的証明の背景と変化の意味を考える」mp4ファイル
https://drive.google.com/file/d/1IhiUFVddHH5ZllWmpwr82VEeNQhZa-Oo/view?usp=sharing

講演ビデオ　第4部 「形式的証明の背景と変化の意味を考える」講演pdf
https://drive.google.com/file/d/1roXvwkGcErS2F5npnQxJjlU6IDjtrg6Y/view?usp=sharing


セミナーに向けたショートムービーの再生リスト
https://www.youtube.com/playlist?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg

セミナーに向けたblog集
https://www.marulabo.net/docs/math-proof/#%E3%82%BB%E3%83%9F%E3%83%8A%E3%83%BC%E8%A7%A3%E8%AA%ACblog


コメント

コメントを投稿

このブログの人気の投稿

宇宙の終わりと黒色矮星

イメージ
【宇宙の終わりと黒色矮星】 図のようなストーリーで、「宇宙の終わりとエントロピー」という投稿を準備していたのだが、いろいろ雑念が湧いて気がすすまなくなる。その理由は別稿で。 この図は、「閉じられた部屋でのガスの拡散」というわかりやすいモデルで理解されるエントロピーの増大の法則が、あるフェーズから、宇宙規模でみれば、「全ての物質のブラックホールへの吸収・収斂」として現れると言うことを主張している。最初、ペンローズのこの話を読んだときには、目からウロコだった。 このストーリーにはもっと先がある。最近のシミュレーションでは、指数関数的に膨張する宇宙では、巨大なブラックホールに捕捉されるのは、宇宙全体の物質の10%程度だという。恒星起源のブラックホールは 10^67 年で、銀河系中心の巨大ブラックホールも 10^99年で、ホーキング放射で「蒸発」し姿を消す。 ブラックホールに捕捉されなかった宇宙の残りの90%の物質は、元それが属した銀河系から孤立したまま星の一生の進化を続ける。太陽の1.2倍程度の質量を持つ星は「白色矮星」になるのだが、「白色矮星」は 10^17年で「黒色矮星」に変わる。 「黒色矮星」は、現代の「宇宙の終末論」では、もっとも注目されている天体なのだが、それはまだ観測されていないと言う。というのも、この天体は光を出さないからだ。「黒色矮星」の中心は、最も安定な原子である鉄の「結晶」でできていて、温度は絶対零度近くに冷却されている。 「黒色矮星」は、とても長生きする天体である。陽子崩壊がおきるなら、黒色矮星の寿命は 10^32年程度だが、もし陽子が安定しているとすれば、太陽の 1.24倍程度の質量を持つ「黒色矮星」は、10^1600年後に突然崩壊して超新星爆発を起こす。もっと軽い、太陽の1.16倍程度の質量を持つ「黒色矮星」は、10^32000 年後（！）に超新星爆発を起こす。 このシナリオによれば、宇宙は、とてつもなく長い長い退屈な時間をかけて、その死を迎える。「黒色矮星」の超新星爆発は、宇宙の死を飾る最後の打ち上げ花火である。その後には、宇宙には何も起こらない。 この記事は、ジョン・バエズの "Black Dwarf Supernovae" を基にしたものだ。https://johncarlosbaez.wordpress.com/202...
続きを読む

機械の言語能力の獲得から考える embeddingの共有・蓄積・検索の未来

イメージ
機械の言語能力の獲得から考える embeddingの共有・蓄積・検索の未来 #01 「機械が言語能力を獲得した」ということについて https://maruyama097.blogspot.com/2025/12/blog-post_25.html #02 ことばから文字へ https://maruyama097.blogspot.com/2025/12/blog-post_51.html #03 情報の共有と情報の集積 https://maruyama097.blogspot.com/2025/12/blog-post_37.html #04 文字からembeddingへ −− 大規模分散システムの成立 https://maruyama097.blogspot.com/2025/12/embedding.html #05  文字からembeddingへ −−意味の分散表現論の系譜 https://maruyama097.blogspot.com/2025/12/embedding_25.html #06  意味の分散表現論の登場 https://maruyama097.blogspot.com/2025/12/blog-post_27.html #07  文の意味のベクトル表現の発見 https://maruyama097.blogspot.com/2025/12/blog-post_30.html #08  Interlude 1 −− ChatGPTが生まれた日 https://maruyama097.blogspot.com/2026/01/interlude-1-chatgpt.html #09 Interlude 2 −− OpenAI の分裂が残したもの https://maruyama097.blogspot.com/2026/01/interlude-2-openai.html #10  Transformerの登場 https://maruyama097.blogspot.com/2026/01/transformer.html #11  1/31 マルレク「機械の言語能力の獲得を考える」へのお誘い https://maruyama097.blogspot.com/2026/01/131...
続きを読む

1 + 196883 = 196884

【 1 + 196883 = 196884  −− ある数学的認識の飛躍の物語 】 このコラムのタイトル「1 + 196883 = 196884」 は、当たり前すぎて、かえって意味不明かもしれません。 ただ、もしも、あなたのクレジット・カードの最初の6桁の数字に1を足したものが、あなたのマイナンバーカードの最初の6桁の数字と完全に一致していたとすれば、この式は、単なる足し算以上の意味を持ちます。 もっとも、クレジット・カードとマイナンバー・カードの場合、こうした数字の一致は、全くの偶然と考えていいと思います。 このコラムの「1 + 196883 = 196884」の場合も、左側に現れる数字196883と右側に現れる数字196884は、実は、数学の別の分野から取られたものです。 ただ、クレジット・カードとマイナンバー・カードの数字の偶然の一致とは異なって、この等式は、一見無関係に見える数学の分野間の驚くべき繋がりを示唆する、重要な発見の糸口となりました。 1 + 196883 = 196884 という一見自明の等式は、20世紀の数学的認識のある飛躍の物語の、最初の主人公なのです。 【  John McKayが気づいたこと 】 1978年ごろ、McKayは、あることに気づきます。 当時は、「モンスター群」の存在は証明されていなかったのですが、FischerとGriessは、モンスター群が「存在するならば」、その最小の非自明な既約表現（最も基本的な「対称性のパターン」を捉える方法）の次元は 196883 であると予想していました。 McKayは、この数字 196883 が、数論の分野で基本的な対象である j-不変量 j(τ) の q-展開（フーリエ級数展開に類似したもの）に現れる係数 196884 に極めて近いことに気づきます。     「1 + 196883 = 196884 だろう ! 」 そればかりではありません。McKayは、さらにj(𝜏) の最初のいくつかの項の係数が、モンスター群 M の既約表現の次元 r(n) の単純な線型結合として表現できることに気づきます。 【 数学者の直感 】 先に進む前に、あらためて問題を整理しておきましょう。 第一。ここでの議論には、二つの全く異なる数学的対象、「j-不変量」と「Monster...
続きを読む