セミナー紹介

全体概要

このセミナーは、「人工知能と数学」という表題のもと、現代の「大規模言語モデル（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]。

• 論理展開:
• LLMの能力（翻訳・要約・対話）と「意味の近さ」の表現の成功 [p.3]〜[p.6]
• 2022年のTheorem Prover・Alpha Code失敗という具体的挫折 [p.7], [p.9]
• 規模拡大では解決しない理由：LLMは人間の意味理解モデルに過ぎない [p.8]
• 本セミナーの視点：「コンピュータと数学の関係」として問い直す [p.10]

---

■ Part 1: 大規模言語モデルと数学

• この部の核心:

LLMが「翻訳的意味理解」を基盤とするがゆえに、数学的真偽の区別という最も本質的な能力を欠くことを示します。次に、機械翻訳→パラレルコーパス→RNNの「モノマネ」能力という技術的系譜をたどり、ChatGPTが「人間のフィードバックからの強化学習（RLHF）」という路線転換から生まれた経緯と、GitHubがその補完として機能するロジックを解説します [p.15]〜[p.108]。

• 論理展開:
• 「1+1=3」を真偽の観点で区別できない翻訳システムの根本的限界 [p.22]〜[p.24]
• パラレルコーパスの歴史（ロゼッタストーン〜現代の機械翻訳）と言語学習モデルの特性 [p.27]〜[p.37]
• RNNによる「モノマネ」能力の獲得（Sutskever 2011、Karpathy 2015）：数学論文・Cコードのモドキを生成 [p.60]〜[p.70]
• ChatGPTのRLHF：Labelerによる人間フィードバックが「真実のソース」を欠く構造的問題 [p.86]〜[p.102]
• GitHubは「人間の正しいフィードバックの宝庫」としてこの欠点を補完する可能性 [p.104]〜[p.107]

---

■ Part 2（20世紀）: 数学の基礎と計算科学

• この部の核心:

「証明可能性」＝「計算可能性」＝「プログラム」という三項同一性の認識が、ゲーデル・チャーチ・チューリング（1930年代）からカリー＝ハワード対応（1970年代）、Martin-Löfの従属型理論（1980年代）へと、約40〜50年のタイムラグをもって計算機科学に浸透していく歴史的過程を精密に追います。また、ホーア・ダイクストラらの「形式手法」が80年代に後退した背景として、IT業界内部の「数学観」の問題を明示します [p.113]〜[p.241]。

• 論理展開:
• 数学基礎論の歴史的鳥瞰：ラッセル型理論→ヒルベルトプログラム→ゲーデル不完全性定理→チャーチ＝チューリングのテーゼ [p.114]〜[p.120]
• ホーアの「An axiomatic basis for computer programming」（1969）とダイクストラの最弱事前条件：形式手法の登場 [p.133]〜[p.142]
• 1979年ACM論文「Social Processes and Proofs of Theorems and Programs」による形式手法への一方的非難と「社会的プロセスが数学的確信を決める」という誤った数学観 [p.150]〜[p.155]
• カリー＝ハワード対応：「命題は型、証明は項」（Proof as Types, Proof as Terms）の発見 [p.174]〜[p.188]
• Martin-Löfの従属型理論（Dependent Type Theory）：全称記号・存在記号を型として定式化 [p.193]〜[p.204]
• 「計算」＝「証明」＝「プログラム」の三項同一性の確立とCoq等の証明支援システムの誕生 [p.222]〜[p.240]

---

■ Part 3（21世紀）: 数学の基礎と計算科学の新しい動向

• この部の核心:

21世紀に入り、Baezの「A Rosetta Stone」論文が物理・トポロジー・論理・計算理論の驚くべき類似性をカテゴリー論で統一的に把握し、数学的知識の「累積性」を脅かす証明の誤り問題に対してVoevodskyがUnivalent FoundationとUniMathという根本的解答を提示した経緯を論じます。これがOpenAIのTheorem Proverにおけるmathlibの利用という「ファースト・コンタクト」へと接続されます [p.244]〜[p.321]。

• 論理展開:
• Baez「Physics, Topology, Logic and Computation: A Rosetta Stone」：カテゴリー論の「オブジェクト＝命題＝データ型」「モルフィズム＝証明＝プログラム」という統一表 [p.248]〜[p.258]
• 21世紀の形式的証明の拡大：四色問題（Gonthier 2004）、Feit-Thompson定理（2012）、ケプラー予想（Hales 2015）、連続体仮説の独立性（Han・van Doorn 2020） [p.280]〜[p.289]
• Voevodskyの「数学の二つの危機」認識（純粋数学と応用数学の分離、誤りの累積）と、Univalent Foundationによる集合論に代わる新しい数学の基礎づけ [p.292]〜[p.309]
• UniMathとmathlib：数学の全領域をCoq/Leanのソースコードとして形式化するプロジェクトの現在 [p.310]〜[p.319]
• OpenAI Theorem ProverがMathlibを主要訓練データ（25,000問）として採用した事実が示す、LLMと形式的証明の「ファースト・コンタクト」の意義 [p.320]〜[p.321]