AIと数学 -- 2022年 vs 2026年 (2)

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

前回のセッションでも述べたように、僕は、AI技術は、

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

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

今回のセッションでは、こうした変化のさきがけとなった、2022年のOpenAIの "Theorem Prover" との対比で、今年2026年にAIと数学の領域でおきた様々な成果を紹介しようと思っていました。

高校生が一日で解く「数学オリンピック」の問題もうまく解けなかった2022年のOpenAIの "Theorem Prover" と比べて、2026年のOpenAIの "Ten Advances in Mathematics and Theoretical Computer Science" の達成は驚異的なものです。この分野のブレイクスルーが今年2026年に起きたという評価は妥当なものです。AIの進化は素晴らしい!

数学者のコミュニティから、「ライデン宣言」のような強い警戒が発せられたことも、今年がこの分野のターニングポイントであるそのことを示していると思います。

【 「ライデン宣言」の警告 】

僕は、「ライデン宣言」のAI観や数学観に賛成してはいません。ただ、「ライデン宣言」の次のような指摘には全面的に同意してます。(ただし、数学における評価プロセスの「定評ある」という評価を除いて)

「研究成果が、プレスリリースやブログ記事といった非公式なルートを通じて、多くの場合、科学的な評価に必要な研究論文やその他の情報開示を伴わずに発信される場合、適切な評価は危うくなる。」

「この慣行は、数学コミュニティにおける定評ある評価プロセスが行われる前に、市場のタイムラインに合わせて新しい成果を宣伝しようとするものである。多くの場合、これは報告内容の単純化につながり、例えば自動化ツールの重要性を過度に強調したり、それらのツールを可能にしたこれまでの人的貢献を過小評価したりすることになる。」

「このような過度な単純化は、世論に影響を与え、数学に対する認識を損なうだけでなく、特定の数学的課題を、商用製品の一般的な推論能力の指標として誤って用いるリスクをもたらす。」

【 2013年 vs 2026年 】

当初考えていた「2022年 vs 2026年」という対比だけでは、今年になって急速に拡大している「AIすごい。今では数学の問題も解けるんだ。」というAI観や数学観を増幅するだけだと思いなおしました。

本当にすごいのは、AIではなく数学のほうだと僕は考えています。
2022年に10年近く先立つ2013年の時点で、数学者のグループは、コンピュータを使って数学の問題を解くことについて、遥かに深い洞察に到達していました。それは、革命的で驚異的なものでした。

今回は、そのストーリーを紹介しようと思います。

https://drive.google.com/file/d/1yisTrxe0aT7LYqbHR6gVVRo3ah0GGKn8/view?usp=drive_link

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

"Univalent Foundations and the Large-Scale Formalization of Mathematics"
https://www.ias.edu/ideas/2013/awodey-coquand-univalent-foundations

"The Origins and Motivations of Univalent Foundations
A Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes"
https://www.ias.edu/ideas/2014/voevodsky-origins

"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

"How to prevent AI from harming mathematics"
https://www.nature.com/articles/d41586-026-02309-7

"Leiden Declaration on Artificial Intelligence and Mathematics" 
https://leidendeclaration.ai/

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

「コンピュータと数学」まとめページ
https://www.marulabo.net/docs/computer-math/

「コンピュータと数学」まとめページ コンシェルジェαバージョン
https://www.marulabo.net/20240831md/

「コンピュータと数学」講演資料 pdf
https://drive.google.com/file/d/1A6_DiD_xnl1zrW0lenzLPxGFxGNdRAQg/view?usp=sharing

「コンピュータと数学」講演動画再生リスト
https://www.youtube.com/playlist?list=PLQIrJ0f9gMcPZTGr3N85yw2FFNQTWg-WJ

「コンピュータと数学」Veovodskyが考えたこと
https://youtu.be/U1pYAhtMSQw?list=PLQIrJ0f9gMcMsKsm1SDM2blnV7fjjo360

「コンピュータと数学 1」Part 2 「計算=証明=プログラム」という認識の発展
https://youtu.be/9splwHpXehs?list=PLQIrJ0f9gMcPZTGr3N85yw2FFNQTWg-WJ

「コンピュータと数学」ショートムービー再生リスト
https://www.youtube.com/playlist?list=PLQIrJ0f9gMcMsKsm1SDM2blnV7fjjo360


コメント

このブログの人気の投稿

宇宙の終わりと黒色矮星

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

1 + 196883 = 196884