コンピュータと数学

8月マルレク「コンピュータと数学 1 -- TuringからVeovodskyまで」へのお誘い

申し込みページはこちらです。https://peatix.com/event/4106633/view

AI技術の次の未来を展望する

「大規模言語モデル」ベースの現代の生成AI技術は、ネット上の膨大なテキストの集積を学習して、そこから、人間の「言語能力」と呼ばれているものの基本的部分 --「意味の理解」「新しい文の生成」「対話形のコミュニケーション」、「文字として蓄積された情報の活用」等 -- をコンピュータ上で実現することに成功しました。

それは画期的なものです。この連続セミナーは、歴史的な成功をおさめたAI技術の次の未来を展望することを目的としています。

それなら、「AIの未来」のようなタイトルの方が良かったと思われるかもしれません。

ただ、一見するとAIとの関係がはっきりしない、一般的な「コンピュータと数学」というタイトルを選んだのには理由があります。それは、AIの未来についてのつぎのような僕のビジョンに関係しています。

AIの未来についての三つのビジョン

第一。僕は、未来の（あるいは、近未来なのかも）AIの発展の課題の焦点の一つは、人間の二つの基本的能力である「言語能力」と「数学的＝論理的能力」の「統合」の課題だと考えています。

第二。ただ、「大規模言語モデル」は人間の「言語能力」の理解に画期をもたらしたのですが、ただ、その方法の素朴な延長では、AIの数学＝論理的能力の飛躍は望めないだろうと考えています。

それなら、「AIと数学」というタイトルがいいのではという考えもあると思います。でも、そうしたタイトルを選びませんでした。

一つには、大規模言語モデルベースの生成AI技術の華々しい成功の中で、ほとんどの人が「AI ＝ 生成AI」と思っている現状では、先の「第二」の論点は、なかなか伝えるのが難しいと感じたからです。

コンピュータは、それ自身で「数学的＝論理的能力」を持っている

もう一つには、僕がこのセミナーで伝えたいAIの未来について、もう一つのメッセージがあるからです。

第三。そもそも、コンピュータは、それ自身で「数学的＝論理的能力」を持っているという考えかたがあるということです。

こうした考えを進めれば、わざわざ、「大規模言語モデル」の上に数学的＝論理的能力を構築しようとするのは、コンピュータが本来持つ力を過少に評価しているのであって、それは余計な回り道だということになります。

僕は、こうした考えに魅力を感じています。こうした考えは、新しいものではありません。それは、コンピュータの歴史と同じくらい古いものです。ですが、生成AIの登場によってその考えが古びるものではないと僕は考えています。

「AI」という言葉は、少し窮屈

今回のセミナーでは、「AI」と言うことばをタイトルから外して、「コンピュータ」ということばに置き換えてみました。それで、すこしは自由にAIの未来を考えることができると感じています。

要するに、「AIの未来」を、「AI」を主語とするのではなく、「コンピュータ」を主語として、「コンピュータの未来」というパースペクティブで考えてみようというのが、今回のセミナーの趣旨です。僕の問題意識からすると、その焦点は、コンピュータの数学的能力だということになります。

もっとも、今回のセミナーが、「数学の歴史の話」でも「生成AI批判」でもなく、歴史的な成功をおさめたAI技術の次の未来を展望することを目的としていることを説明するのに、これだけグダグダ語らねばならないというのは、どこかでボタンを掛け違えたのかもしれませんね。ただ、このシリーズ少し続けてみようと思います。

今回のセミナーの構成

今回のセミナー「コンピュータと数学 1 -- TuringからVeovdskyまで」は、次のような構成をしています。

　Part 1 機械は考えることができるか？
　　・Turingが考えたこと
　　・Veovodskyが考えたこと

　Part 2 「計算 = 証明 = プログラム」という認識の発展
　　・Curry-Howard 対応
　　・Martin-LofのDependent Type Theory
　　・VeovodskyのHomotopy Type Theory I -- Dependent Type
　　・VeovodskyのHomotopy Type Theory 2 -- Univalent foundations

　Part 3 コンピュータによる数学的証明
　　・連続体仮説の独立性証明
　　・Feit–Thompson定理の形式的証明
　　・ケプラー予想の証明

Turingは、「機械は考えることができるか？」という問題を、初めて提起しました。
Veovodskyは、「すべての数学的証明はコンピュータ・プログラムの形をとるべきだ。」と主張し、それを実行しようとしました。

二人のコンピュータ観には、大きな飛躍があります。

今回のセミナー「コンピュータと数学 1 -- TuringからVeovdskyまで」は、こうした飛躍をもたらしたものが、「計算 = 証明 = コンピュータ・プログラム」という認識が、「型の理論」の中で成立したからだと考え、「型の理論」の発展の歴史を紹介しています。

最後のパートは、コンピュータ・プログラムによる数学的証明の実例を紹介しています。

連続セミナー「コンピュータと数学」の展開について

連続セミナー「コンピュータと数学」は、今後、次のような展開を予定しています。 ご期待ください。

当初、今回のセミナーで取り上げると予告していたGATlabについては、「AIの未来」を「コンピュータと数学」という切り口から考えようとするアプローチの背景を、もう少し丁寧に紹介してから話してみたいと思っています。急なコンテンツの変更、お詫びします。

　「コンピュータと数学 1 -- TuringからVeovdskyまで」
　「コンピュータと数学 2 -- Turingマシンから量子コンピュータまで」
　「コンピュータと数学 3 -- GATlab」
　「コンピュータと数学 4 -- Agent Based Modelの数学」

Part 1 機械は考えることができるか？

Turingが考えたこと

AIの時代を切り拓いたのは、今から1950年のTuringの論文だと思います。その画期的な論文 “Computing Machinery and Intelligence" の冒頭で、彼はこう語ります。

「機械は考える事が出来るか? (Can machines think? )」という問題を考察することを提案する。

今なら、誰かが「AIは考えることができるか？」といっても、誰も驚かないし、そうした問題提起が大きな関心を集めることもないように思います。

もちろん、「生成AIで数学の問題が解ける」と主張しても、「生成AIで数学の問題は解けない」と主張しても、それが異端視されることはありません（多分）。

ただ、この論文が出された1950年ではそうではありませんでした。彼は、「機械は考えることができる」という主張が、「異端」とみなされるだろうことをはっきりと自覚していました。

↑ 見出しクリックでYouTubeへ； ↓ pdfはスクロールで全文読めます

Veovodskyが考えたこと

Voevodskyは、Milner予想、Bloch-Kato予想を解くなど、代数幾何でグロタンディックが進もうとした道で、大きな業績を残した数学者です。

2002年、26歳の時、彼はこうした業績でフィールズ賞を受賞します。

2017年、彼は動脈瘤で突然亡くなります。51歳でした。

多くの数学者が、早すぎる彼の死を悼みました。
数理物理学者のJohn Baezは、こう語りました。
「彼は、カントールやグロタンディックのような天才でした。」

重要なことは、彼の仕事は、数学の基礎とコンピュータという二つの世界に関係していました。

今回のセミナーのように、「コンピュータと数学」という問題を取り上げるのなら、Veovodskyは 21世紀の最も重要な人物の一人だと僕は考えています。

彼は、数学をその基礎から改めて考えなおしたのです。そして、集合論に変わる新しい数学の基礎づけ Univalent Foundationを構築します。

さらに、彼は、数学の証明に、コンピュータを使うべきだと主張した最初の数学者となりました。それは革命的な主張です。

↑ 見出しクリックでYouTubeへ； ↓ pdfはスクロールで全文読めます

Part 2 「計算 = 証明 = プログラム」という認識の発展

Curry-Howard対応 --「計算 ＝ 証明 ＝ プログラム」という認識の成立

重要なことは、「Curry-Howard対応」は、型付きラムダ計算をプログラムと見なせば、”Proof as Program”としても解釈出来るということです。

「計算 ＝ 証明」であることは、すでにGoedel, Church, Turingたちがコンピュータなどない1930年代に気付き、1950年代には "Church Turing Thesis" として広く知られるようになっていました。この時期は、ちょうどコンピュータが産声をあげた時期です。

コンピュータの利用が拡大する中、1980年代に確立した「Curry-Howard対応」の、“Propositions as Types”“Proofs as Terms” ”Proof as Program”という認識は、「計算 ＝ 証明 」に加えて「計算 ＝ 証明 ＝ プログラム」という認識が成立したことを意味します。

それは、Veovodskyの「すべての数学的証明をコンピュータ・プログラムの形で記述しよう」というUniMathのビジョンに受け継がれていきます。

↑ 見出しクリックでYouTubeへ； ↓ pdfはスクロールで全文読めます

Dependent Type Theory -- Martin-Löf

現在の「型の理論」の基本が出来上がるのは、1980年代になってからです。その中心人物は、Martin-Löfです。

現在のCoq, Agda, leanという証明支援システムは、彼のDependent Typeの理論に基礎付けられています。

Churchの単純な型を持つラムダ計算の体系は、基本的には、型A, 型Bに対して、型 A → Bで表現される関数型の型しか持ちませんでした。

それに対して、Martin-Löfは、論理的な命題にも、自然なスタイルで型を定義しました。
例えば、Aが型であり、Bが型であれば、A∧BもA→BもA∨Bも型であるというように。もちろん、それぞれは異なる型です。

Martin-Löf は、式 a = b にも型を与えます。

↑ 見出しクリックでYouTubeへ； ↓ pdfはスクロールで全文読めます

Homotopy Type Theory I-- Dependent Type

Homotopy Type Theory (HoTT)は、数学の一分野である「ホモトピー論」と、論理学・計算機科学の一分野である「型の理論」とのあいだに、深い結びつきがあるという発見に端を発しています。

ここでいう「型の理論」は、前回のセッションで紹介したMartin-LöfのDependent Type Theory （従属型理論）です。

Martin-LöfのDependent Type Theory では、a:A に、「Aは型であり、aはその項である」という解釈を与えます。ここで型Aは、基本的には論理式に対応し、項a はその論理式の証明に対応します。（Curry-Howard対応）

VeovodskyのHomotopy Type Theory では、a:Aは、それとは全く違った解釈が与えられます。そこでは、「Aは「空間」であり、aはその空間上の「点」である」という解釈が与えられます。

Homotopy Type Theory では、Dependent Typeの項は、どのように表現されるのでしょう。
Grothendieck constructionを利用します。Dependent TypeΠ(𝑥:𝐵).𝐸(𝑥) の項s(x)  : Π(𝑥:𝐵).𝐸(𝑥)は、fiber上の「点」section として表現されます。

このセッションでは、Grothendieck constructionの丸山のたとえ話での説明がなされています。

↑ 見出しクリックでYouTubeへ； ↓ pdfはスクロールで全文読めます

Homotopy Type Theory II-- Univalent foundations

Homotopy Type Theoryでは、空間Aの中で、点aと点bをつなぐ「道」がある時、aとbは、同じものと見なします。ただ、点aと点bをつなぐ「道」自体は、連続的に変化しうるものです。連続的に変化する「道」の「同一性」をあたえるものが、homotopyなのです。

homotopy同値による「空間」A内の「点」 a, b の「同一性」の定義は、型の理論で言えば、同じ型Aに属する項a, b の「同一性」の定義でした。ただ、従属型理論には、そもそも型𝛼と型𝛽は等しいことを主張する「同一性」の定義があります。この第二のタイプの同一性をどのように定式化すればいいのでしょう？

第一のタイプの同一性の定式化で有効だった、ある空間での点の同一性をhomotopy同値とfibrationで追求するというアプローチは、この問題ではあまり有効には見えません。なぜなら、ここでの問題の焦点は、点ではなく空間そのものの同一性にあるからです。

無限の階層を持ち、複雑に分岐した構造を持つ位相空間そのものを対象にし、それを構成する任意の空間に自明でない「同一性」あるいは「非同一性」を導入することは、不可能に思えます。

↑ 見出しクリックでYouTubeへ； ↓ pdfはスクロールで全文読めます

Part 3 コンピュータによる証明

このセクションでは、21世紀に入って急拡大したコンピュータによる数学の証明の代表的な事例を取り上げています。

「生成AI」の「華々しい成功」の影に隠れて、多くの人は気づいていないように見えるのですが、コンピュータによる知性の実現のSingularityは、この分野ですでに起きていると、僕は感じています。

連続体仮説の独立性証明

ヒルベルトは、1900年に、20世紀の数学が解くべき23の問題のリストを発表した。その問題提起は、20世紀の数学に少なくない影響を与えた。カントールの「連続体仮説」は、この23の問題の第一番目の問題に取り上げられている。

「世紀の難問」と呼ばれた連続体仮説の問題で、大きな前進があったのは、1940年のことだ。クルト・ゲーデルが、連続体仮説と選択公理の二つを満たす集合論のモデルを実際に構成して見せたのだ。この集合論のモデルの中では、連続体仮説は「真」である。

この結果は、連続体仮説を直接に証明したものではないことに注意しよう。それは、集合論と連続体仮説には矛盾がないこと、すなわち、集合論の中では連続体仮説の否定は証明できないことを意味している。

連続体仮説を最終的に解決したのは、J.P.コーエンだった。彼は、「強制法(Forcing Method)」というモデル構成法を創出し、連続体仮説の否定が成り立つモデルを構成した。

先のゲーデルの結果と合わせると、連続体仮説は、集合論の公理群からは独立であることが証明されたことになる。連続体仮説は、集合論の公理群からは証明できないのだ。

結果から見ると、カントールが、全力で連続体仮説を証明しようとして、成功しなかったのには理由があったのである。

コーエンの結果は、始祖のカントールが構想した、いわばカントール的集合論とは異なる、非カントール的集合論が存在することを明らかにした衝撃的なものだった。

ユークリッド幾何学の「第五公準」が、他のユークリッド幾何学の公理群からは独立で、それらから証明できないことの認識の成立が、非ユークリッド幾何学を成立させたのと同じことが、「数学の基礎」である集合論で起きたのである。

コーエンの結果とその方法は、1960年代の中頃には、集合論の構造についての認識を飛躍的に発展させた。

↑ 見出しクリックでYouTubeへ； ↓ pdfはスクロールで全文読めます

Feit–Thompson定理の形式的証明

2012年、Georges Gonthierは、Coqを用いて、群論のFeit–Thompson 定理の形式的証明に成功する。この定理は、1962-1963年にWalter Feit と John Griggs Thompson によって証明された、群論の基本的な定理の一つである。

「有限単純群の分類問題」は、Daniel Gorensteinをリーダーとする数学者の集団によって解決され、20世紀の数学の大きな成果の一つと呼ばれている。

ただ、その「証明」は、100人以上の数学者が、50年のあいだに数百の論文誌に発表した、膨大な量の「証明」の総和である。そのページ数は一万ページを超えると言われている。

Gonthierの ”Feit–Thompson theorem” の型式的証明も、膨大なものである。それは、15,000の定義、4,300の定理、17万行のソースからなる。この証明を、彼はチーム作業で、6年かけて完成させた。

↑ 見出しクリックでYouTubeへ； ↓ pdfはスクロールで全文読めます

ケプラー予想の証明

「ケプラー予想」は、入れ物の箱に同じ大きさのボールを、どのくらいたくさん詰め込むことができるかという問題に関する予想です。

何も考えずに、箱の上からボールを流し込むと、充填率（詰め込んだボール全体の体積を、容器の箱の体積で割ったもの）は、平均すると 65%程度になるといいます。箱の35%は、すきまになるということです。

もっと、びっしりと、ボールを詰め込みことはできないか？ケプラーは、もっとボールを詰め込むことができる二つの方法を考えました。

1611年、ケプラーは、どんなボールの詰め方をしても、この数字を超えるほど密にボールを詰め込むことはできないだろうと予想しました。これを「ケプラー予想」といiます。ケプラー自身は、この問題に証明を与えることはできませんでした。

1900年のヒルベルトの20世紀の数学が解くべき23の問題の 18番目にこの問題は、取り上げられています。

↑ 見出しクリックでYouTubeへ； ↓ pdfはスクロールで全文読めます