高階論理の自動証明を独立に検査する仕組みを作る
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
この論文をやさしく読む
ひとことで言うと
自動定理証明器が出した証明を、別の論理的な基盤で検査できる形に組み直す研究です。
何に役立つ？
証明器自身の実装だけに頼らず結果を検査したり、他のシステムで証明を再利用したりする助けになります。実装中にはLeo-IIIのバグも見つかっています。
この研究の面白いところ
個別の推論規則だけでなく、式を節形式に変える処理も含めて符号化する一般的な手順を設計し、高階論理の証明器に組み込んでいます。
どこまで分かった？
約80%という数値は生成された証明ステップの自動再構成率であり、問題全体や証明全体の成功率ではありません。要旨は試作システムの報告で、全ステップの対応完了を意味しません。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
本研究では、自動定理証明器の証明を論理フレームワークDeduktiで検証する際に共通する課題と要件を特定し、節形式への変換を含め、推論体系の規則と証明ステップの符号化を導く一般的な方法論を開発する。次に、この方法論を高階論理のEP推論体系に適用し、自動定理証明器Leo-IIIに組み込む。得られた試作システムは、生成された証明ステップの約80%を自動的に再構成する。これによりLeo-IIIは、独立に検査可能な証明再構成に対応した初の高階自動定理証明器となり、システム間で証明を再利用する基盤を提供する。この実装を通じて、Leo-IIIの複数のバグが発見された。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-21（UTC）
- 最新改訂
- 2026-09-21 · v1
- 査読・掲載
- 掲載先の記載あり
著者による掲載先の記載：LPAR-26 - 26th Conference on Logic for Programming, Artificial intelligence, and Reasoning, Oct 2026, Spetses Island, Greece。出版社での独立確認は未実施です。
更新履歴
- v1 2026-09-21 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
We identify common challenges and requirements for verifying proofs from automated theorem provers in the Dedukti logical framework and develop a general methodology for deriving encodings of calculus rules and proof steps, including clausification. We then apply this methodology to the EP calculus for higher-order logic and integrate it into the automated theorem prover Leo-III. The resulting prototype reconstructs about 80% of generated proof steps automatically, making Leo-III the first higher-order automated theorem prover to support independently checkable proof reconstruction and providing a basis for cross-system reuse. The implementation uncovered several bugs in Leo-III.
arXiv ID: 2609.24594 ／ 要約の誤りについて