過去・現在・未来

【 広がるビジョン 】 2017年に亡くなったVoevodskyは、Milner予想、Bloch-Kato予想を解くなど、代数幾何でグロタンディックが進もうとした道で、大きな業績を残した天才数学者です。 彼の最後の仕事は、数学の基礎とコンピュータという二つの世界に関係していました。 前回取り上げた数学での「間違った証明」の問題ですが、彼も、苦い経験がありました。 2000年頃、彼は1993年に自分が発表した論文の重要な補題が間違っていたことに気づきます。でも、その頃には、その論文は広く出回っていて、多くの数学者がその証明を「信じて」いました。彼が、その間違った補題なしでも、論文の結論が正しいことを証明できたのは、2006年になってからでした。 別のこともありました。1998年に共著で彼が発表した論文の証明に対して「正しくない」という批判が出されるのです。結論的には、彼は、正しかったのですが、彼が、最終的に、自分が正しいことを確信できたのは、2013年になってからでした。 Voevodskyは、考えます。「数学が、累積的（accumulative）な性格を持つのなら、もしも、そこに誤りが紛れ込むと、それも、累積する可能性がある。」と。 こうした問題に対する、Veovodskyのとった対応はラジカルで驚くべきものでした。 彼は、数学をその基礎から改めて考えなおしたのです。そして、集合論に変わる新しい数学の基礎づけ Univalent Foundationを構築します。 さらに、彼は、数学の証明に、コンピュータを使うべきだと主張した最初の数学者となりました。そして、そのためのコンピュータによる証明支援システムのライブラリーUniMthを開発しました。 彼の考えたことを、少し長くなりますが、彼のインタビュー記事から引用します。 彼は、「数学は今、危機的状況、いや、2つの危機に瀕している」といいます。 「第一は、それは、「純粋数学」と「応用数学」の分離に関連しています。 遅かれ早かれ、実用性のないことに従事している人たちに、なぜ社会がお金を払わなければならないのかという疑問が生じるのは明らかでした。 第二は、あまり明らかではありませんが、純粋数学の複雑さに関連しています。 遅かれ早かれ、論文が複雑すぎて詳細な検証ができなくなり、発見されないエラーが蓄積される過程が始まるという

【 数学者も証明を間違えることがあるということ 】 数学的知には、人間の認識によって獲得されたものとしては、独特の性質があります。 それは、いったん数学的に「真」であることが証明された定理は、時代が変わっても場所が変わっても、ずっと「真」のままであり続けることです。 そうして獲得された知は、個人というよりは人類の知として蓄積されていきます。それを数学的知の「累積性」といいます。 「フェルマーの定理」を証明したワイルズは、自分を「巨人の肩の上の小人」に喩えたのですが、それは彼の謙遜であると同時に、数学的知の体系が「累積的」であることを彼がはっきりと自覚していることを示しています。 それでは、 「数学的知の累積性」は、どのように保証されるのでしょうか？ ピタゴラスの「教団」は、いくつかの発見を「秘教」にしていたらしいのですが、ピタゴラスの定理を使うのに、我々はその「証明」を自分で繰り返し「再発見」する必要はありません。 もちろん、ピタゴラスの定理を使うたびに、ピタゴラスの遺産継承者に使用料を支払う必要もありません。 数学では、「数学的知の共有」は、数学という学問自体の前提と言っていいものです。 そういう意味では、コンピュータの世界でオープンソースのムーブメントが大きな影響力を獲得するはるか以前から、数学の世界はオープンソースの世界だったのです。 ただ、「情報の共有」が、「数学的知の累積性」を保証するとは限りません。「数学的知の累積性」にとって、一番重要なことは、その「数学的知」が数学的に正しいことです。 しかし、数学的正しさを証明する「数学的証明」は、現状では、いくつかの問題を抱えています。 一つには、数学者が正しいと思って提出した「証明」が、正しいものではない場合があるということです。 「フェルマーの定理」は、最終的には、1995年のAndrew Wilesの論文によって証明されたのですが、フェルマー自身は、この定理を証明出来たと信じていました。その「証明」は残っていませんが、それが誤った「証明」であったのは確かです。 Wiles自身も、95年の論文以前に一度、「フェルマーの定理を証明した」という発表を行うが、誤りが見つかり、それを撤回しています。 世紀の難問である「リーマン予想」は、何度か「証明」が発表されています。今までのところ、それらは誤った「証明」でした。 証

  【 マルレク「ことばと意味の構成性について」講演ビデオ公開しました 】 昨年の12月24日に開催した、マルレク「ことばと意味の構成性について」の講演資料と講演ビデオを公開しました。あわせてこのセミナーのまとめページ  https://www.marulabo.net/docs/discocat/  も更新しました。ご利用ください。 このセミナーは、現在ビデオ公開中の「AIは意味をどのように扱っているのか？-- ChatGPTの不思議」 https://www.marulabo.net/docs/meaning/   の内容を理論的に補うものです。 現在の「大規模言語モデル」の中核技術は、「ことばと意味」をコンピュータ上で扱う技術にあるのですが、その背景にどのような理論的問題があるかに興味ある方は、ぜひ、ご覧ください。 同時に、このセミナーは、サブタイトルの「カテゴリー論と意味の形式的理論」が示すように、先日の投稿「カテゴリー論の時代始まる」で紹介した数理科学へのカテゴリー論の応用の紹介になっています。　 第一部では、カテゴリー論の創世記の重要な達成であるローヴェールのFunctorial Semanticsを紹介しています。 第三部は、言語学と意味の理論へのカテゴリー論的アプローチである、Discocat理論の紹介です。 4月のマルレクでは、この分野の最新の研究動向を紹介する「意味の分散表現技術の現在」というセミナーを開催しようと思っています。ご期待ください。 今回公開したセミナーのテーマの一つである、「構成性 compositionality」という概念は、カテゴリー論の基本的な特徴と考えられているのですが、あまり見慣れないものかもしれません。 ただ、この「構成的 compositional」という概念は、大規模言語モデルを考える上で、重要な意味を持っています。 昨年の10月に、Google と OpenAIは、ともに、「大規模言語モデル」ではモデルの規模拡大だけでは AIの能力は伸び悩むという論文を発表します。 OpenAIは、"Scaling Laws for Reward Model Overoptimization" という論文を発表します。それは彼らが同年の4月に発表していた "Training language mo

【 カテゴリー論の時代始まる 】 20世紀を通じて、数学・物理を中心とする数理科学は、大きな発展を遂げました。それは、内部に多くの新しい研究領域を発生させながら、それぞれの領域は相互に越境し、さらにその領域を拡大し続けました。 前回見た、「計算」＝「証明」＝「プログラム」という認識も、新しい領域を巻き込み、長い時間をかけて獲得された、そうした認識の一例です。 21世紀になって、こうして拡大した数理科学の全体像を統一的に把握しようという探究がうまれてきます。 数理科学の専門化した諸領域の到達点を概観するのは、必ずしも容易ではないのですが、やがて、それらの間に驚くべき類似性が存在するという認識が生まれます。 今回のセッションで紹介する John Baezらの “A Rosetta Stone”論文は、数理科学の統一的把握の試みとして、もっとも成功した、もっとも影響力のあったものの一つです。 彼の認識の飛躍は、数学的には、数理科学の基礎にカテゴリー論をおくことで可能になりました。 1970年代、ペンローズは、ファインマン・ダイアグラムの一般化が、時空間の理解を改めることにつながるかもしれないことに気づきます。1980年代には、量子物理学とトポロジーとの間に、強力な類似性があることが明らかになっていきます。 弦理論では、この類似性を利用して、通常の場の量子論のファインマン・ダイアグラムを2次元のコボルディズムに置き換えて、時間の経過とともに弦が辿る世界のシートを表現します。 演算子とコボルディズムの類似性は、ループ量子重力や、より純粋に数学的な分野である「トポロジカル場の量子論」においても重要な役割をはたします。 バエズは、彼は、このアナロジーをさらに推し進めます。物理学とトポロジーだけでなく、論理学と計算理論もリストに加えて、数理科学の「パラレル・コーパス」を作成するのです！ 導きの糸となったのは、カテゴリー論の基本的な構成要素である、「オブジェクト」と「モルフィズム」の対応物を、これらの理論に中に見つけることでした。　 　・物理学でオブジェクトに対応するのは「システム」で、モルフィズムに対応するのは、「プロセス」。 　・トポロジーでオブジェクトに対応するのは「多様体」、モルフィズムに対応するのは「cobordism」。 　・論理学でオブジェクトに対応するのは「命題」、モ

【 当事者のIT技術者に見えにくい「リンク」】 先に、”Proof as Program プログラムとしての証明” という認識が、Curry-Howard対応の発見や従属型理論の登場の中で、生まれてきたことを述べてきました。 それは、論理的＝数学的証明は機械のプログラムで実行できるということ、ひるがえって言えば、機械は論理的＝数学的推論能力を持つという認識に他なりません。 この認識は、人工知能論にとって本質的に重要な認識であると、僕は考えています。 このセッションでは、改めて、「計算」＝「証明」＝「プログラム」という認識がどのように形成されてきたのかを、 振り返りたいと思います。 「計算」「証明」「プログラム」という三つの言葉は、もともと別の意味を持っています。それは今でも同じです。そして それぞれがそれぞれの歴史を持っています。 この三つの言葉の中で、「計算」の起源が一番古いものです。4000年以上前の古代バビロニアでは、2の平方根の値も知っていたし、ピタゴラスの定理で直角三角形の斜辺の長さを計算する「計算表」も持っていたといいます。人間は、具体的な「計算」を通じて数学の世界の扉を開きました。 「証明」の概念の起源は、2300年前のユークリッドに帰してもいいと思います。古代ギリシャ人は、具体的な数の「計算」とは異なる数学の世界があることに気づきました。プラトンは彼のアカデミアの門に、「幾何学を知らざるものこの門入るべからず」と掲げたと言われています。彼らにとって、「数学的証明」は「真理」に到達する、重要な方法だと認識されていたと思います。残念なことに、ギリシャ数学の伝統は中世ヨーロッパでは途絶します。 この中で、「プログラム」という概念が一番新しいものです。その起源は、コンピュータが登場した1950年代を遡ることはないのは明らかですので。 このセッションは、機械の能力を人間がどう認識してきたかを、「計算」「証明」「プログラム」という三つの概念の関係の認識の歴史をメイン・ストーリーにして述べたものです。 さきに、概略を述べておきましょう。（以前のセッションと内容的には重なっています。） まず、「計算」と「証明」が、本質的には同じものであるという認識が生まれます。1930年代のことです。 それから40年ほど経って、「プログラム」は「証明」とみなせるという認識が生まれま

【 「証明支援システム」-- 人間と機械の「協働」の始まり 】 Dependent Type Theory 「従属型理論」の基本が出来上がるのは、1980年代です。その中心人物は、マーティン・レフです。 彼の理論が与えた影響を、二つほど見ておきたいと思います。 第一に、この理論は、21世紀になって急速に実装が進んだ Coq, Agda, Lean 等の「証明支援システム」に理論的基礎を提供しました。 「証明支援システム」というのは、“Proof as Program” という、証明をコンピュータのプログラムとして実行するというアイデアを、現実に実行可能にしたシステムのことです。 「証明支援システム」は、コンピュータが自動的に数学の問題の証明を与える「自動証明システム」ではないことに注意してください。それは、あくまでも人間が行う数学の証明を、コンピュータが支援するというシステムです。 ただ、「証明支援システム」で、証明を行なっていると、奇妙な感覚にとらわれることがあります。 　「僕は、コンピュータで証明を行なっている。 　　証明をしているのは僕だ。 　　コンピュータが、それを助けてくれている。」 　「でも、待てよ ... 」 　「本当は、証明をしているのはコンピュータで、 　　それを支援しているのが、僕なんじゃないか？」 以前は、「証明支援システム」を利用して「証明」を行う人は少数だったもので、こうした「主客逆転」の「感覚」を伝えることは、少し難しかったのですが、今年に入って状況は大きく変わったと思います。 その変化とは、いうまでもなく、GitHub Copilot が登場して、それを圧倒的に多くのプログラマが使い始めて、機械とのペア・プログラミングの経験が急速に拡大していることです。 まだ、「ChatGPTが、プログラムを全部書いてくれるので、人間のプログラマはいらなくなる」という議論も時々見かけるのですが、実際に使ってみた人は、プログラマの仕事は楽になるけど、形は変わってもやっぱり人間が必要なんだということに、いつか気づくと思います。GitHub Copilot は、基本的に、人間主導の「機械と人間の協働」なのです。 それは「大規模言語モデル」ベースの「プログラム開発支援システム」の限界だと思います。人間の役割が必要だということは、人間にとって悪いことではありま

【 「証明」＝「計算」＝「プログラム」】 数学と計算科学の接点を振り返っています。 ゲーデル、チャーチ、チューリングの「証明可能性」は「計算可能性」に等しいという発見から40年たった1970年代、数学と計算科学の接点で注目すべき二つの動きがありました。 一つは、計算機科学の側から生まれた、具体的なプログラムの分析を通じて、計算機科学の数学的基礎づけを目指す動きです。残念ながら、この「形式手法」と呼ばれる意欲的なムーブメントは。ITの世界では広く受け入れられることなく挫折します。 もう一つは、論理学＝数学の側から生まれた動きです。その代表的な成果は、「Curry-Howard対応」の発見と、それに基づくマーティン・レフの「従属型理論」の成立です。 今回のセッションでは、「Curry-Howard対応」の発見を取り上げます。 Curry-HowardのCurryは、関数型言語Haskellにその名を残しているCurry Haskell その人です。既に1934年に、Haskell Curryは、型付きラムダ計算の関数の型を示す矢印 → と、論理式“A → B” の中に出てくる含意を意味する矢印 → との間に、対応関係があることに気づいていました。 具体的には、「A → B が成り立ち、かつ、Aが成り立つなら、Bが成り立つ」という有名な「三段論法」の推論ルールと、「f が A → B という型を持ち、a がAという型を持つなら、f(a) は型 B を持つ」という型付きラムダ計算での型の計算ルールが、よく似ていることに気がついていました。 Howardは、このCurryの発見を、マーティン・レフらと共に、さらに深く考えました。 論理式 A → B が、 A → B という関数と同じ型を持つと考えられるのなら、他の論理式も、型を持つと考えることができるのでは？　例えば、論理式 A ∨ B は、型 A ∨ B を、論理式 A ∧ B は、型 A ∧ B を持つと考えることはできないか？ そして、この論理式（命題：Proposition）を型とみなすアイデアは、うまく機能するのです。こうした考えを、"Proposition as Type"と呼びます。 もう一つの飛躍は、命題が型Pを持つとしたとき、型Pの項pにあたるものが、命題Pの証明と考えることができ