Lean,CoqでAIに証明をしてもらう(各種不等式、Hahn-Banach、特異点解消定理、Weil予想)&LLMとの合体おすすめ論文
Gemni2.5とChatGPTに定理証明支援言語CoqとLeanでピタゴラスの定理、コーシー＝シュワルツの不等式、ヘルダーの不等式、ミンコフスキーの不等式の各不等式とHahn-Banachの定理、特異点解消定理、Weil予想の証明を書いて説明してもらいました(完全な証明ではない)。
不等式の証明
コーシー＝シュワルツ、ヘルダー、ミンコフスキー不等式の証明は長いので概略だけ書きます。
リンクはこちら
なぜか英語
日本語
証明概略
Coqにはmathcomp、Leanにはmathlibという数学の定理のライブラリがあります。Coqのほうが歴史が長くその分充実していますが、最近はmathlibの勢いがすごいです。
Geminiの説明ではCoqは実際にはmathcompライブラリを呼べばいいので証明概略だけを示されてしまいました。Lean, mathlibにも同様の関数が有りますが、ヘルダーの不等式、ミンコフスキーの不等式に関しては有限和の場合の証明を書き下してくれました。
ChatGPTのほうはライブラリをつかって一瞬で証明しています。
CoqとLean、mathcompとmathlibの比較(Gemini)
| 特徴 | Coq (MathComp/Coquelicot) | Lean (Mathlib) |
|---|---|---|
| 基礎理論 | 構成的型理論 (CIC) が基本。古典論理は公理として追加可能。 | 構成的型理論 (CIC) が基本だが、古典論理や選択公理を積極的に採用。より古典数学に近い記述が可能。 |
| ライブラリ | 標準ライブラリ、MathComp、Coquelicotなど、用途に応じて複数の主要ライブラリがある。MathCompは有限群論や代数に強み。Coquelicotは実解析。 | Mathlibという単一の巨大で包括的なライブラリに集約される傾向。コミュニティによる開発が活発。 |
| タクティク | auto, ring, field, lia, nra, ssr* (MathComp)。証明はタクティクのスクリプトとして記述されることが多い。 | simp, rw, calc, ring, linarith, refine, by_cases。タクティクモードとタームモードの組み合わせ。calc によるステップごとの計算が強力。 |
| 自動化 | auto, tauto, omega, lia, nra など。MathCompの ssr は強力な書き換え戦略を提供。 | simp, aesop, finish など。linarith, norm_num など特化型も。Lean 4ではタクティクの記述やメタプログラミングがより柔軟。 |
| 可読性 | 数学の証明に慣れていても、Coq特有のタクティクやライブラリ構成の学習が必要。MathCompのスタイルは独特だが強力。 | 数学の記法に近い記述を目指している部分が多い (calc など)。Mathlibの命名規則や構造に慣れが必要。 |
| コミュニティ | 歴史が長く、学術界での利用が多い。 | 近年急速に成長し、特に数学分野での利用が拡大。活発なコミュニティ。 |
| 対象の表現 | 例えば、ノルムや内積は型クラスやレコードを用いて抽象化される。R (実数) の公理化に複数のアプローチがある。 | 型クラスを多用し、抽象的なインターフェースを定義。is_R_or_C のような型クラスで実数と複素数を統一的に扱う。ennreal (拡張非負実数) の活用が特徴的。 |
| 証明の粒度 | 明示的なステップが多い傾向があるが、ssr などで大きなステップも可能。 | calc や simp により、証明の記述をある程度数学の直観に近づけることができる。一方で、詳細なタクティクによる制御も可能。 |
Coq (MathComp) は rewrite をベースとした等式変形と、apply による補題の適用が中心です。ssreflect のブーリアンリフレクションを駆使した証明スタイルは非常に強力です。
Lean (Mathlib) は calc ブロックによるステップごとの不等式評価が非常に読みやすく、数学の教科書に近い形で証明を追うことができます。また、simp タクティクによる自動化も強力です。
- Coq は、特にMathCompを用いる場合、非常に堅牢で形式化された代数構造の上で証明を構築します。タクティクは強力ですが、独自のスタイルに慣れが必要です。
- Lean (Mathlib) は、より数学の慣習に近い記法や証明の流れを意識しており、calc や ennreal のようなツールがそれを助けています。ライブラリの網羅性とコミュニティの活発さが特徴です。
としています。
Hahn-Banachの定理
関数解析の基礎となる定理であるHahn-Banachの定理について
日本語のざっくりした定理と証明の説明
日本語のやや詳しい定理と証明の説明
はIsabelleによる記述でhttps://mizar.uwb.edu.pl/JFM/Vol5/hahnban.htmlようですがLeanではどう書けるか聞いてみました。
ChatGPTはmathlibの組み込み定理を使ってしまいました。
Gemini 途中は省略されていますがZornの補題を使う基本的な点は踏まえていて上記のPDFのステップのとおりです。
特異点解消定理
特異学習理論の中核をなす定理でもあります。
ChatGPTによるとその証明は数年から十年規模の大規模プロジェクトになるそうです(そのような見立てを出してくることは驚きです)。 証明の骨子のLeanでの記述(ほとんどsorry)、未実装の概念を列挙してもらいました。実装のヒントがためになりそうです。
Geminiも同様に証明で必要となる代数的概念、部品であるスキーム、ブローアップ、正則局所環、ノーマライゼーションの現時点での実装の困難さを挙げています。 数学書には「明らかに」論理的な飛躍がありその行間を埋めるのはLLMには(人間にも)難しい。Leanやプログラミング言語実行環境を検証環境として取り込むことはできるが、プログラミングのリファクタリングと違って証明では新しい概念を発明し、サブゴールとする必要があり、証明の全体像が変わってしまうのを見出し戦略を変更するのが今のAIには困難であろうとしている。(「戦略的・創造的思考」と表現している。)
Weil予想
ずっと難しいテーマについて聞いてみます。雑に言うと代数曲線上で定義されたリーマンゼータ関数に対するリーマン予想が解かれているというものです。
わかりやすい解説としてはtujimotterさん
があります。
表に挙げられた部品の数だけで言うと特異点解消定理より実装されているものが多そうですが、未実装のエタールコホモロジーと完備有限位相群の行列跡などは自分も余り理解しておらず、難しそうです。
証明全体を記述しようとすると数年規模の大規模プロジェクトになる予想ですが、限定的な条件での結果であれば今でも十分到達可能な予想です。
LLM+定理証明支援系は使えるか
下でも挙げたLean CopilotやLeanDojoが紹介されていて最新研究のリンクは参考になります。
LLM、RAGを使った簡単なパイプラインを自ら提唱してくれました。
大学院レベル以上の概念になると雛形になるネット上の情報が少なく、長大な教科書を取り込む必要が有り、表記ゆれが全体の論理を破壊する可能性を懸念しています。
LLM を「自律エージェント」ではなく 優秀なジュニア共同研究者として使う——定義雛形・文脈検索・エラー説明を即座に返してもらい、人間が理論の骨格を与える——これが当面もっとも現実的な戦略です。
最近多くの人が思っていることと同じというかネット上の総意を学習してしまった結果かもしれませんし、人間に残された仕事があるという希望を見せてくれているだけかもしれません。
GeminiによるLLMと定理証明支援の連携に関するおすすめ論文
主にLean,CoqとLLM、機械学習を連携させた研究論文、プロジェクトのリンクです。
それだけでは分野として不足があるのかあるいはGeminiの調査能力が足りないのかプログラムのソースコードの生成支援も含まれます。
- LeanDojo
- ProofNet
-
Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean - LeanAgent: Lifelong Learning for Formal Theorem Proving
- HELoC: Hierarchical Contrastive Learning of Source Code Representation
この記事の内容も既存の定理の証明をLLMに聞いて形式検証用の記述を書いてもらった点で最も簡単化LLMと定理証明支援の連携と言えるかもしれません。
LLMによるも注目されています。プログラムの実行環境を組み込むという手法はすぐ思いつかれますが、それに基づいて極端に少ない学習データからブートストラップ的に学習を行う手法研究も最近では流行しています。おそらくはDeepseek proverは強化学習を使ってそのような学習を行っているようです。
Deepseek prover V2 Leanの実行環境を内蔵し、数学オリンピックなみの証明能力(とは？)を達成したらしいです。学習元の証明をサブゴールに区切った工夫も有ります。
その他の定理証明支援言語
Geminiの受け売りです。
- Haskell/Idris
Idrisは依存型を持つHaskellと言われますが、Haskellでもソースコードに言語拡張
{-# LANGUAGE KindSignatures #-}
を書くことで使うことができます(Haskell の依存型に入門する)。
- Agda: 依存型を持つ関数型プログラミング言語であり、定理証明器としても利用できます。CoqやLeanに近い立ち位置ですが、よりプログラミングとの親和性が高いと言われることがあります。
- Isabelle/HOL: LCF系の定理証明器で、長い歴史と多くの実績があります。特にハードウェアやセキュリティ分野の検証で使われています。
- HOL Light, HOL4: Isabelle/HOLと同じくLCF系の定理証明器です。
- PVS (Prototype Verification System): より自動化された推論機能を持つ定理証明器で、航空宇宙分野などで利用されています。ホームページが渋い。
おすすめリンク
ホモトピー型理論(HoTT)というのがあるらしく、Leanにも実装されているそうです。
- https://event.phys.s.u-tokyo.ac.jp/physlab2024/pdfs/poster/poster_calcphys02.pdf
- https://arxiv.org/abs/2212.11082
- https://gist.github.com/yamarten/a60e9e4e1893c881cfb0e874a5d05b37
Lean
カリー＝ハワード同型対応(数学の証明とプログラミング言語での関数の連なりとの等価性)がわかった気持ちになりました。
https://zenn.dev/palalansouki/articles/d3ec6573bbc2c8
https://www.ieice.org/ess/sita/forum/article/2024/202401191114.pdf
Coq
Elgamal暗号でSSReflectのトライアル #Coq - Qiita
整数を使った証明（整数精度のHaar変換）のトライアル #Coq - Qiita
Coqでの実用的な証明記述です。結局は人間が証明を書かざるを得ず、ちゃんと書こうとすると非常に冗長な記述になります。型推論やleanでの各種コマンド、タクティクス、そしてLLM Copilot的機能がその労力を削減してくれることを期待しています。
Coq/SSFeflect/Methcompによる定理証明
日本語の数少ない定理証明支援言語に関する本です。
Leanが流行りだす直前の状況です。
その他
Haskellにおける依存型
Isabellaによるハーンバナッハの定理の形式的記述と証明
感想
大学学部レベルの簡単な定理の証明ならmathcomp、mathlibに実装されている関数をライブラリとして呼んでくるだけであまり面白くないです。しかしlean,Coqの文法についてほとんど素人の状態で検証可能な証明コード(正しいとは限らない)を出してくるのは驚きです。lean,Coqの基本的書き方を学ぼうとしていたのでその目的には合致しています。それ以上の独自の証明記述には数学的難易度に関する事前知識や適切なテーマ設定(上記のElgamal暗号、整数精度のHaar変換）
)などの例を挙げられる数学的センスが要ります。LLMが出力した証明が間違っている場合に修正できるかも単なる試行錯誤以上に人間の数学的センス、知識がまだ必要そうです。更に難しい定理あるいは未解決問題に対してはmathcomp、mathlibの対応状況とその労力、実装の困難さの言い訳をしてきたのには驚きました。その見立てが正しいとは言えないもののLLMがない状態では実装程度を見積もるという発想すらでてきませんでした。
LLM+定理証明支援系の概略提示も元研究が既にあるとはいえLLM自身がLLMについて語っているという店で興味深いです。以前プログラミング言語の変換スクリプトを書いてもらおうとしたときにうまく行かず、なぜLLM自身がプログラムを変換するような変換スクリプトが書けないのかと問い詰めたことが有りましたが、LLM+定理証明支援系に関しては私自身単にくっつけただけのアイデアに満足してしまい、それ以上突っ込むことは今の所できていません。
Discussion