はじめに
本連載は全４回の構成
各回で扱うこと
- 第１回（この記事）── 用語と歴史
- 第２回 ── AIの内部構造
- 第３回 ── 誰が動かしているか
- 全４回の記事：全体構成
- この初回記事の要約
- この初回記事が立てる問い
本記事について３つの断り書き
- （１点目）なぜ「６年間」なのか。
- （２点目）タイトルにある「30%から99.6%」について。
- （３点目）本記事で「確認できませんでした」と書く箇所について。
対話篇でお伝えする『本記事の主題』
- すでに人間が提唱していた予想を、AIが人間より先に証明した
- では、AIは新しい予想を立てられるのか
- AIは何を学習データにしているのか
- 【対処策１】解けた証明を学習データに戻す
- 【対処策２】モデルに問題を作らせる
- 【対処策３】大きなモデルが小さなモデルの教材を作る
- これ以外の対処策
- 楊志堅氏について
【筆者の見解】
- どんなタスクを解いているのか
- どのくらいの精度なのか
- AIは、どちらのスタイルを学び、どちらのスタイルで書いているのか
この記事について
想定読者
この記事を読む価値
TL;DR
- Neural Theorem Proverモデルについて
- どちらのスタイルで書いているのか
- 何が達成され、何が未達成なのか
- この分野の研究の牽引者（トップランナー）たち
- 何が争われているのか
第１部 ── まず、言葉を揃えます
- Neural Theorem Proving（ニューラル定理証明）
- autoformalization（自動形式化）
- premise selection（前提選択）
- benchmark（ベンチマーク、問題集）
- pass rate と pass@k
- expert iteration（専門家反復）
- step-level と whole-proof
- 補題、部分目標、Proof sketch について
- 用語のまとめ
第２部 ── 前史： 1997年から2020年
- 1997年 ── 骨格を書いて、隙間を埋めるという発想
- 2016年 ── 前提選択に、深層学習を使う
- 2018年から2019年 ── 環境とデータ集合が作られた
- 2020年 ── GPT-f
- GPT-f の入力・出力・学習データ
第３部 ── 物差しが作られた： 2021年
- miniF2F
- LISA ── Isabelle の証明を学ぶ
- PACT ── 証明の副産物を学ぶ
第４部 ── 骨格を書いて隙間を埋める： 2022年
- Thor ── ハンマーを振るう
- HyperTree Proof Search ── 木を探索する
- Draft, Sketch, and Prove ── そして1997年へ
  - Draft, Sketch, and Prove の入力・出力・学習データ
第５部 ── 誰でも試せるようになった： 2023年
- LeanDojo ── 開かれた環境
- ReProver ：入出力データおよび学習データ
- Baldur ── 証明を修復する
- Baldur：入出力データおよび学習データ
- Magnushammer ── 前提選択に Transformer を
- Llemma ── 数学に特化した公開モデル
第６部 ── 数値が跳ね上がった:2024年から2025年
- 2024年7月 ── AlphaProof と AlphaGeometry 2 が IMO で銀メダル相当
- 実際の問題文を見てみる
  - 第１問（代数、最も易しい問題）
  - 第６問（代数、最も難しい問題）
- なぜ、第６問が特別だったのか
- AlphaProof が生成した証明
- このコードの読み方
- 解けた問題と、解けなかった問題
- 対話篇： AlphaProofへの数学問題文の渡し方
- IMO のメダルについて
- ２年間の変化
- 2025年 ── 公開されたモデルが相次ぐ
- STP の入力・出力・学習データ
- 2025年 ── そして、学習し尽くされた
- Seed-Prover の入力・出力・学習データ
第７部 ── Lean と Isabelle の差は、なぜ生まれたか
- 評価の物差しが、言語の順位を決めている
- Isabelle 側の研究も、着実に進んでいます
第８部 ── 宣言的スタイルは、どう扱われているか
- 方向その１: 言語を作り変える ── MiniLang
- MiniLang は、AIではなく言語です
- 方向その２:　書き方を定める ── sorry-first workflow
- 方向その３:変換する ── Apply2Isar
- 方向その４:　移植する ── Lisar
- ProofAug ── 構造を利用する
- ProofAug の入力・出力
- ４つの方向を、整理します
- 補足: 機械が立てた予想を、機械が証明した
本連載の記事
次回予告
関連記事
- 実務での形式検証
- 定理証明支援系の入門
- 形式手法と、その限界
出典
- 分野の全体像
- ベンチマーク
- 時系列で扱った主要な研究
- AlphaProof と IMO 2024
- Lean と Isabelle の差
- 宣言的スタイルに関する研究
- 予想の生成
- AIによる数学の成果