AIと数学 -- 2020年 vs 2026年 MIP*=RE定理の意味
【 AIと数学 -- 2020年 vs 2026年 MIP*=RE定理の意味 】
【 「2022年 vs 2026年」から「2013年 vs「2026年」へ 】
2022年の"Theorem Prover"と 2026年の到達点の比較から考察が始まったのですが、その比較の視点はAIエンジニアリングの枠の中にとどまっている限りでは、あまり見通しの良いものではありませんでした。前回、僕は次のように述べました。
「当初考えていた「2022年 vs 2026年」という対比だけでは、今年になって急速に拡大している「AIすごい。今では数学の問題も解けるんだ。」というAI観や数学観を増幅するだけだと思いなおしました。本当にすごいのは、AIではなく数学のほうだと僕は考えています。2022年に10年近く先立つ2013年の時点で、数学者のグループは、コンピュータを使って数学の問題を解くことについて、遥かに深い洞察に到達していました。それは、革命的で驚異的なものでした。」
前回のセッションの「2013年 vs 2026年」という比較は、Voevodskyによって牽引されたコンピュータを数学の証明に利用しようというアプローチの起源に遡ろうというものでした。前回、Google Drive 上での音声ファイルの公開だったので、あるいは、アクセスできなかった方がいたかもしれません。今回、音声概要を、「数学でのコンピュータの利用のビジョンとその背景」というタイトルで、キチンとサーバー上に配置したので、ご利用ください。
こうした視点は、 AIが 単なる「 大規模言語モデル+α 」から「 大規模言語モデル+形式的証明システム+α 」へ変化しつつある現在、数学者だけでなく多くのAIエンジニアによっても共有されていると思います。(ただし、そのためには数学の基礎そのものの見直しが必要なのだという認識をのぞいては。)
一つは、「MIP*=RE 入門」セミナーの内容をコンヌ予想との関連で音声で要約した
「MIP*=RE定理とコンヌ予想」です。
-----------------
音声概要
-----------------
2013年 Voevodskyの登場
「数学でのコンピュータの利用のビジョンとその背景」
https://www.marulabo.net/wp-content/uploads/2026/08/UnivalentFoundation.mp3
2020年 MIP*=RE定理
「MIP*=RE定理とコンヌ予想」
https://www.marulabo.net/wp-content/uploads/2026/08/conjecture.mp3
----------------------------
「コンピュータ・サイエンスの現在 — MIP*=RE定理とは何か?」まとめページ
https://www.marulabo.net/docs/cs-mipstar/
https://drive.google.com/file/d/1Xbn-6rLMUoEp3_DfSOSvg8CdRXwsB1Wl/view
https://www.youtube.com/playlist?list=PLQIrJ0f9gMcPR_E6rMWidLQNaXW9R4WdD
https://youtu.be/-Q-pJRVDirY?list=PLQIrJ0f9gMcPR_E6rMWidLQNaXW9R4WdD
https://youtu.be/5FsO1xlXHvk?list=PLQIrJ0f9gMcPR_E6rMWidLQNaXW9R4WdD
https://youtu.be/pbtT8TXptzs?list=PLQIrJ0f9gMcPR_E6rMWidLQNaXW9R4WdD
-----------------------------
https://www.marulabo.net/docs/interactiveproof/
https://www.marulabo.net/docs/pcp/
コメント
コメントを投稿