講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編のPDF資料を快適に閲覧・印刷することができます。
セミナーの概要
本セミナーは2022年3月26日に開催されたマルレクの講義資料であり、「コンピュータが数学の問題を解き始める」という歴史的転換点を、二つの独立しつつも深く連関した視点から探求しています。
第一の視点は、OpenAIによるニューラル定理証明システム（Open-AI Theorem Prover）という、AIの最前線における挑戦的な取り組みです。このシステムは数学オリンピックレベルの問題を対象に、自然言語で与えられた数学の命題を形式言語Leanに翻訳し、形式的に証明することを試みます。Deep Learningが「広い見通しとシンボルに基いた推論」においてまだ限界を抱えているという率直な自己分析のもと、セルフ・プレイに代わるカリキュラム学習という新しいアプローチが提案されています。
第二の視点は、数学者自身がコンピュータを証明の道具として使い始めたという、数学コミュニティの内側からの変化です。連続体仮説の独立性証明、FeitThompson定理、ケプラー予想といった数学史に刻まれる難題が、Lean・Coq・HOL Lightなどの証明支援系を用いて形式的に検証されてきた過程が紹介されます。
そしてこの二つは単なる並列ではなく、深い結びつきを持っています。Open-AI Theorem Proverが学習した最重要データベース「mathlib」は、まさに後者の数学者たちによる形式的証明の蓄積から生まれたものだからです。論文タイトル「Formal Mathematics Statement Curriculum Learning」はそのことを端的に示しています。
さらに本セミナーは、Vladimir Voevodskyが提起した「数学的知の累積性への脅威」という哲学的問題意識を背景に、なぜ数学者が証明にコンピュータを使い始めなければならないのかという根本的な問いに向き合います。「計算＝証明＝プログラム」という三項同一性の認識を軸に、コンピュータ自身がすでに推論能力を持つという強い主張が展開され、数学・AI・哲学の交差点を照らし出す一作となっています。
講義のロードマップ
ここでは、セミナーの講演資料がどのようなパートから構成されているかを示します。また、それぞれのパートのポイントを紹介します。
■ Part 1: Open-AI Theorem Prover
LeanのためのニューラルネットワークベースのTheoremProverが、AMC12・AIME・IMOといった数学オリンピックの問題を対象にどのような証明を生成するかを具体的に示します。自然言語の問題をLean形式に翻訳し、TacticsとよばれるLeanの証明ステップを生成することで、形式的に検証された証明を返すという仕組みが明らかにされます。また、Deep Learningが数学的証明において直面する「無限の動作空間」と「セルフ・プレイ設定の不在」という二つの根本的困難と、それへの対処としてのカリキュラム学習戦略が率直に論じられます [p.12-60]。
■ Part 2: Open-AI Theorem Proverは何を学習したのか？
Open-AI Theorem Proverに与えられた三種類の訓練データminiF2F-curriculum・synth-ineq・mathlib-trainの内容と意義を詳細に解説します。特に最大規模のmathlib-train（25,000件）は、Leanの数学ライブラリmathlibから抽出された証明付き定理集であり、代数・解析・位相・圏論など広大な数学領域をカバーしていることが示されます。これらのデータがAIの「学習対象」として機能するためには、事前に人間の数学者たちによる形式的証明の蓄積が必要だったという重要な事実が浮かび上がります [p.63-99]。
■ Part 3: 数学者、証明にコンピュータを使い始める
数学者が主体となってコンピュータを証明に活用した三つの歴史的事例連続体仮説の独立性証明・FeitThompson定理・ケプラー予想を詳細に紹介します。いずれも、証明の規模や複雑さが人間の検証能力の限界を超えており、コンピュータによる形式的証明の必要性を説得力をもって示す事例として機能しています [p.102-141]。
■ Part 4: 形式的証明の背景と変化の意味を考える
なぜ数学者がコンピュータを証明に使い始めるのかという問いに対し、三つの理由人の手にあまる巨大問題の存在・証明の正しさの検証必要性・数学者自身の誤りを整理します。その中で最も根本的な動機として、Vladimir Voevodskyが「数学的知の累積性への脅威」として提起した問題意識を詳細に紹介し、Univalent Foundationという新しい数学の基礎づけへと議論を展開します [p.144-168]。
ページのナビゲート