過去・現在・未来

 【 AIと数学 -- 2020年 vs 2026年 MIP*=RE定理とAIの未来 】 【 21世紀の「不完全性定理」としての「MIP*=RE定理」 】 「MIP*=RE定理」というのは、MIP*という複雑性のクラスが、「決定不能」だということを述べている定理です。それは、ゲーデルの「不完全性定理」に端を発する、一連の「決定不能」型定理の一つと考えることが出来ます。 それは、新興数理科学としての「コンピュータ・サイエンス」の「決定不能」型定理として登場したのですが、その定理は、狭い意味での 「コンピュータ・サイエンス」の枠を超え、純粋数学や物学の基礎理論に、重要な応用を持ちました。 エンタングルしたnonlocalゲームの値の「決定不能」性は、量子力学の基礎の「ティレルソンの問題」に対する否定的な答えを導きました。また、この結果は、数学の作用素環論の長年の難問だった「コンヌの埋め込み予想」否定的に解決することになりました。 【 「全知・全能だが時には嘘をつく」という「高度な知能」論 】 「MIP*=RE定理」をわかりやすく紹介した、「コンピュータサイエンスの現在」というセミナーで、丸山は次のように述べました。 「第一に考えるべきことは、この定理の証明で中心的な役割をはたす、可能的には無限個のエンタングルメントを共有し、時には人間を欺く「不実」で、しかしながら「全能」の「証明者」たちは何者かということである。」 「第二に考えたいのは、もっと問題を身近なものに引き付けて、「宇宙」ではなく「機械」と人間の関係、人工知能論の課題としてこの定理の含意を考えることである。」 【 人工知能の未来論と「高度な知能」論 】 第一の論点と第二の論点はつながっています。今回のセッションは、主要に第二の論点について、すなわち、MIP*=RE定理とその一見すると特異な「高度な知能」論が、AIの未来展望とどうつながっているかを述べてみようと思います。 「超知能」や「シンギュラリティ」についての議論は活発です。ただ、「人間の知能を超える」ことだけが「高度な知能」の基準になるかは少し疑問です。人工知能の未来論には、「高度な知能」とは何かという議論が必要だと僕は考えています。 【 今回のセッションのコンテンツ 】 ひとつは、「コンピュータサイエンスの現在」セミナーの内容をAIが音声で要約...

 【 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エンジニアによっても共有されていると思います。（ただし、そのためには数学の基礎そのものの見直しが必要なのだという認識をのぞいては。） 【 「2020年 vs 2026年」という視点 】 今回のセッションでは、「2013年 vs 2026年」に加えて、「2020年 vs 2026年」という視点の必要性を提案しています。2020年は、「MIP*＝RE定理」が登場した年です。 「MIP*＝RE定理」については、その概要を紹介した「コンピュータ・サイエンスの現在 — MIP*=RE定理とは何か？」と、その...

  このページは、2022年3月26日に開催したマルレク「コンピュータ、数学の問題を解き始める」の資料とそれにむけたblogのエントリーをまとめたものです。このセミナーの基本的な情報は以下にまとめられています。画像をクリックすると資料のページが開きます。 ただ、これらの資料はいずれも大部なものです。もう少し簡単にセミナーの内容にアクセスするために短いblogのエントリーを再掲しました。タイトルを見て興味が持てそうなところから、読んでみてください。  これらの編集作業は、マルレクのコンテンツをよりアクセスしやすく、利用しやすいものにしようという 「 MaruLabo KnowledgeHub プロジェクト(MKHP) 」の一環として行われています。 ----------------------------- 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 セミナーに向けたショートムービーの再生リスト https://www.youtube.com/playlist?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg ----------------------------- 「コンピュータ、数学の問題を解き始める」blog集 AIについての二つの見方 https://maruyama097.blogspot.com/2022/03/ai.html 誰が証明を行っているのか？ https://maruyama097.blogspot.com/2022/03/blog-post_5.html Dee...

 【 AIと数学 -- 2013年 vs 2026年】 先の投稿の最後のリンクは、音声ファイルへのリンクになっています。 Google Drive 上において「共有」をかけたものなので、Google Drive を使っていない方はうまく開けるかわかりません。お試しください。開けなかったらごめんなさい。 音声ファイルの中身は、2024年に丸山が行った「コンピュータと数学」というセミナーを、AIで概要を作ってもらったものです。 前回紹介した「コンピュータ、数学の問題を解き始める」というセミナーは、AIの側の取り組みとしては当時は画期的だったOpenAIの"Theorem Prover" が登場した2022年3月の時点で、理論的には、はるかに先行していた数学の側からのコンピュータ利用の試みを振り返ったものです。 【 AIの未来についての三つのビジョン 】 今回音声概要を公開した「コンピュータと数学」は、それから一年たった 2024年8月に、論点を整理して、開催したものです。二つのセミナーの内容は重複している点も多いのですが、次のようなを示しているのが特徴です。 「第一。僕は、未来の（あるいは、近未来なのかも）AIの発展の課題の焦点の一つは、人間の二つの基本的能力である「言語能力」と「数学的＝論理的能力」の「統合」の課題だと考えています。」 「第二。ただ、「大規模言語モデル」は人間の「言語能力」の理解に画期をもたらしたのですが、ただ、その方法の素朴な延長では、AIの数学＝論理的能力の飛躍は望めないだろうと考えています。」 「第三。そもそも、コンピュータは、それ自身で「数学的＝論理的能力」を持っているという考えかたがあるということです。 【 あらためて、「2013年 vs 2026年」を考える 】 今回の動画セッションのタイトルは、「AIと数学 -- 2013年 vs 2026年」に変わっています。 問題は、この間どのような変化があったのかを考えることにあります。その変化は、主要に、AIの側でおきた数学の問題へのアプローチの変化にあります。 特に、AIが10の数学の問題をどのように解いたかを詳述した""How the Ideas Came Together"はとても興味深いものです。セミナーの後半では、それを分析したいと思いま...

【 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観や数学観に賛成してはいません。ただ、「ライデン宣言」の次のような指摘には全面的に同意してます。（ただし、数学における評価プロセスの「定評ある」という評価を除いて） 「研究成果が、プレスリリースやブログ記事といった非公式なルートを通じて、多くの場合、科学的な評価に必要な研究論文やその他の情報開示を伴わずに発信される場合、適切な評価は危うくなる。」 「この慣行は、数学コミュニティにおける定評ある評価プロセスが行われる前に、市場のタイムラインに合わせて新しい成果を宣伝しようとするものである。多くの場合、これは報告内容の単純化につながり、例えば自動化ツールの重要性を過度に強調したり、それらのツールを可能にしたこれまでの人的貢献を過小評価したりすることになる。」 「このような過度な単純化は、世論に影響を与え、数学に対する認識を損なうだけでなく、特定の数学的課題を、商用製品の一般的...

【 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 が考えたこと 】 ディープラーニングの到達点： 「ディープラーニングは、言語・ビジョン・画像生成を含む多くの分野で目覚ましい成功を謳...