ProofSketcher: 信頼性の高い数学・論理推論のためのハイブリッドLLM + 軽量プローフチェッカ
arXiv cs.AI / 2026/4/10
📰 ニュース
要点
- 本論文は、数学的および論理的推論の信頼性を高めるために、LLMと軽量で信頼できるプローフ検証カーネルを組み合わせたハイブリッドシステム「ProofSketcher」を提案する。
- Lean/Coqのように完全に形式化された証明の作成を要求する代わりに、LLMはコンパクトなDSL上の型付き証明スケッチを出力し、カーネルがそれを展開して明示的な証明義務（proof obligations）を生成する。
- この手法は、証明におけるLLMの典型的な失敗モード――たとえば省略された副条件、無効な推論ステップ、与えられた文脈から導出できない補題への引用――を、検証可能な構造を強制することで対処する。
- 中核となる考え方は、完全な形式化に通常必要とされる低レベルな詳細の「雪崩（avalanche）」を抑えつつ、定理証明器レベルの保証を維持することにある。
- ProofSketcherは、自然言語/LLMによる推論と、完全なインタラクティブ証明よりも小さな信頼計算量での厳密な形式検証を橋渡しするパイプラインとして提示される。
- categories: [
