Higher-order logic proofs can be verified faster and more reliably
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
Logic in Computer Science
Summary
Checking complicated math proofs made by computers can be tricky and prone to errors. The authors created a method to translate proof steps into a format that another system can check more easily. They tested this with a specific theorem prover for higher-order logic and found it could verify about 80% of the proof steps automatically. This also helped find some mistakes in the original prover, making the whole process more trustworthy.
What this means in practice
- •For software verification teams: Check complex software correctness proofs automatically with independently verifiable steps to reduce errors and increase trust.
- •For formal methods tool developers: Integrate a methodology for encoding and checking higher-order logic proof steps to improve interoperability and bug detection in theorem provers.
Authors
Melanie Taprogge, Frédéric Blanqui, Alexander Steen
Abstract
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.