Recycling Algebraic Proof Certificates
Daniela Kaufmann, Clemens Hofstadler

TL;DR
This paper introduces an extension to algebraic proof certificates that enables proof parts to be reused, significantly reducing proof size and verification time in algebraic derivations.
Contribution
It extends the LPAC calculus with new proof rules for reusing proof segments, integrated into Pacheck 2.0, improving proof efficiency.
Findings
Reduced proof size in algebraic derivations
Decreased verification time with the new proof rules
Effective proof reuse demonstrated in experiments
Abstract
Proof certificates can be used to validate the correctness of algebraic derivations. However, in practice, we frequently observed that the exact same proof steps are repeated for different sets of variables, which leads to unnecessarily large proofs. To overcome this issue we extend the existing Practical Algebraic Calculus with linear combinations (LPAC) with two new proof rules that allow us to capture and reuse parts of the proof to derive a more condensed proof certificate. We integrate these rules into the proof checker Pacheck 2.0. Our experimental results demonstrate that the proposed extension helps to reduce both proof size and verification time.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
