Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof

DOI10.1007/978-3-319-20615-8_4MaRDI QIDQ3453106zbMATH OpenOpenAlexFDO

Authors Luís Cruz-Filipe, Peter Schneider-Kamp

Publication date 20 November 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1502.08008

Mathematics Subject Classification ID

Searching and sorting (68P10)

Abstract: In recent work, we formalized the theory of optimal-size sorting networks with the goal of extracting a verified checker for the large-scale computer-generated proof that 25 comparisons are optimal when sorting 9 inputs, which required more than a decade of CPU time and produced 27 GB of proof witnesses. The checker uses an untrusted oracle based on these witnesses and is able to verify the smaller case of 8 inputs within a couple of days, but it did not scale to the full proof for 9 inputs. In this paper, we describe several non-trivial optimizations of the algorithm in the checker, obtained by appropriately changing the formalization and capitalizing on the symbiosis with an adequate implementation of the oracle. We provide experimental evidence of orders of magnitude improvements to both runtime and memory footprint for 8 inputs, and actually manage to check the full proof for 9 inputs.

Recommendations

• Efficient, verified checking of propositional proofs
• A verified proof checker for higher-order logic
• Formalizing size-optimal sorting networks: extracting a certified proof checker
• scientific article; zbMATH DE number 7699423
• On extensibility of proof checkers
• Generating compiler optimizations from proofs
• Publication:3034850
• On the concrete efficiency of probabilistically-checkable proofs
• scientific article; zbMATH DE number 4009856
• Optimizing proof search in model elimination

Cites work

• scientific article; zbMATH DE number 3473265 (Why is no real title available?)
• scientific article; zbMATH DE number 2061716 (Why is no real title available?)
• scientific article; zbMATH DE number 3409355 (Why is no real title available?)
• A large-scale experiment in executing extracted programs
• Automated certified proofs with CiME3
• Certified Exact Transcendental Real Number Computation in Coq
• Computer Certified Efficient Exact Reals in Coq
• Extraction in Coq: An Overview
• Formalizing bounded increase
• Formalizing size-optimal sorting networks: extracting a certified proof checker
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Sorting nine inputs requires twenty-five comparisons
• Toward a lower bound for sorting networks

Cited in

(5)

• How to get more out of your oracles
• Sorting nine inputs requires twenty-five comparisons
• Formalizing size-optimal sorting networks: extracting a certified proof checker
• Formally proving size optimality of sorting networks
• ProofWatch: watchlist guidance for large theories in E

Describes a project that uses

Uses Software

• CiME
• Coq

This page was built for publication: Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453106)