Core Concepts
大規模言語モデルを用いて、人間の定理証明プロセスを支援することができる。
Abstract
本論文では、Leanにおける定理証明の支援ツールとして、大規模言語モデルを活用する方法を提案している。
具体的には以下の3つのツールを開発した:
suggest_tactics: 現在の目標に基づいて、次の証明ステップとして使用できる戦術を提案する。
search_proofs: 大規模言語モデルによって生成された戦術と既存の rule-based 証明検索ツール(aesop)を組み合わせ、完全な証明を見つける。
select_premises: 現在の目標に最も関連性の高い前提を選択する。
これらのツールは、Lean Copilotと呼ばれる一般的なフレームワークの上に構築されている。Lean Copilotは、Leanの外部で事前に訓練された大規模言語モデルをLean内部で効率的に実行できるようにする。
実験の結果、search_proofsは、人間の介入を最小限に抑えつつ定理を自動的に証明できることが示された。また、人間とAIが協調して定理を証明する際にも、search_proofsは既存の rule-based ツールよりも優れた支援を提供できることが確認された。
このように、Lean Copilotと開発したツールは、人間と大規模言語モデルの協調による定理証明を可能にし、Leanユーザーの生産性を向上させることが期待される。
Stats
50の定理を評価した結果、search_proofsは64%の定理を完全に自動的に証明できた。
search_proofsは、人間が手動で入力する戦術の平均数が1.02個と、aesop(3.62個)やsuggest_tactics(2.72個)よりも少なかった。
search_proofsは、定理の証明ステップの81.2%を自動化できた。これは、suggest_tactics(48.6%)やaesop(35.2%)よりも高い割合である。
Quotes
"LLMsは人間の数学者を支援するのに役立つことが示された。これは、ITPにおけるLLMベースの証明自動化ツールの有用性、およびLean内部でLLM推論を利用可能にすることの重要性を示唆している。"
"Lean Copilotと開発したツールは、人間とLLMの協調による定理証明を可能にし、Leanユーザーの生産性を向上させることが期待される。"