講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編のPDF資料を快適に閲覧・印刷することができます。
セミナーの概要
このセミナーは、「人工知能と数学」という表題のもと、現代の「大規模言語モデル（LLM）」ブームの本質的な限界を正面から問い直し、コンピュータと数学の本来あるべき関係を歴史的・理論的に再定位する試みです。
出発点となるのは、ChatGPTに代表されるLLMが「ことばの意味」の表現において画期的な進歩を遂げた一方で、数学的推論という領域では根本的に非力であるという認識です [p.3〜p.9]。翻訳的意味理解を基盤とするLLMは、「1+1=2」と「1+1=3」を数学的真偽の観点から区別することができず、OpenAIのTheorem ProverやGoogleのAlpha Codeの失敗がそれを証明しました [p.7, p.81〜p.83]。
しかし、このセミナーの核心的主張はそこで終わりません。「大規模言語モデルという回り道を経ずとも、コンピュータはそれ自身の力で論理的・数学的推論を正しく行う能力を持っている」という認識を提示するのが、このセミナーの真のテーマです [p.10, p.25]。
その論拠は、20世紀の数学基礎論とコンピュータ科学の深い交差から導かれます。ゲーデルの不完全性定理からチャーチ＝チューリングのテーゼへと至る「証明可能性」と「計算可能性」の同一性の認識 [p.119]、カリー＝ハワード対応による「命題は型であり、証明は項である（Propositions as Types, Proof as Program）」という洞察 [p.178〜p.189]、そしてMartin-Löfの従属型理論からVoevodskyのUnivalent Foundationへと続く21世紀の展開 [p.192〜p.309]。これら全ての系譜が示すのは、「コンピュータはプログラムの実行という形で証明を計算する」という根本的認識です [p.240]。
さらに第三部では、数学の基礎づけ自体の刷新Baezの「A Rosetta Stone」が示す物理・トポロジー・論理・計算理論の深い類似構造 [p.248〜p.268]、そしてVoevodskyが「数学の二つの危機」への回答として構築したUniMathとmathlib [p.310〜p.321]が、21世紀における人間と機械の数学的「協働」の新たな地平として論じられます。
講義のロードマップ
ここでは、セミナーの講演資料がどのようなパートから構成されているかを示します。また、それぞれのパートのポイントを紹介します。
■ Part 0: はじめに「人工知能と数学」セミナーの問題意識
LLMの「言語能力」の画期的進歩を認めつつも、それが数学的推論に対して原理的に無力である理由を問い、「大規模言語モデルという回り道を経ずとも、コンピュータ自身が直接数学的推論を行う能力を持つ」という本セミナーの中心テーゼを提示します [p.3〜p.10]。
■ Part 1: 大規模言語モデルと数学
LLMが「翻訳的意味理解」を基盤とするがゆえに、数学的真偽の区別という最も本質的な能力を欠くことを示します。次に、機械翻訳→パラレルコーパス→RNNの「モノマネ」能力という技術的系譜をたどり、ChatGPTが「人間のフィードバックからの強化学習（RLHF）」という路線転換から生まれた経緯と、GitHubがその補完として機能するロジックを解説します [p.15〜p.108]。
■ Part 2（20世紀）: 数学の基礎と計算科学
「証明可能性」＝「計算可能性」＝「プログラム」という三項同一性の認識が、ゲーデル・チャーチ・チューリング（1930年代）からカリー＝ハワード対応（1970年代）、Martin-Löfの従属型理論（1980年代）へと、約40〜50年のタイムラグをもって計算機科学に浸透していく歴史的過程を精密に追います。また、ホーア・ダイクストラらの「形式手法」が80年代に後退した背景として、IT業界内部の「数学観」の問題を明示します [p.113〜p.241]。
■ Part 3（21世紀）: 数学の基礎と計算科学の新しい動向
21世紀に入り、Baezの「A Rosetta Stone」論文が物理・トポロジー・論理・計算理論の驚くべき類似性をカテゴリー論で統一的に把握し、数学的知識の「累積性」を脅かす証明の誤り問題に対してVoevodskyがUnivalent FoundationとUniMathという根本的解答を提示した経緯を論じます。これがOpenAIのTheorem Proverにおけるmathlibの利用という「ファースト・コンタクト」へと接続されます [p.244〜p.321]。
ページのナビゲート