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 diferent 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.
Axiom (, ) (, ) ()=⊥ ∈K[]
(∪Var(), (↦→)) LinComb (, (1, . . . , ), (1, . . . , ), )
(, ) (1)̸=⊥,..., ()̸=⊥, ()=⊥ Ext (, , ) Deletion ()
(, ) (, (↦→⊥)) ,1,...,∈K[] =1· ( 1)+·+ · ( ) mod⟨()⟩ (, (↦→)) (, ) ()=⊥ ∈/ ∈K[] (∪{}, (↦→−+)) 2−∈⟨()⟩
An LPAC proof certificate can be used to validate that a polynomial ∈ K[] can be derived from a
given set of polynomials ⊆ K[] (= the proof axioms) using polynomial addition and multiplication.
The semantics of LPAC can be seen in Figure 1. A more detailed explanation including correctness
arguments is given in [
Let denote a set of Boolean variables and let be a sequence of polynomials, which can be accessed via indices. An LPAC proof is a sequence of states (, ), with the initial state ({}, []). At any state, will only contain polynomials that are either axioms or can be derived from polynomials already contained in using the inference rules of the calculus.
Using the Axiom rule, we add polynomials to . The Deletion rule allows us to remove polynomials from when they are no longer needed, which helps to save memory during checking. The LinComb rule can be used to add polynomials to that can be derived as a linear combination of polynomials already stored in . Using the Ext rule we can add polynomials to the proof, which can be used to introduce placeholder variables for Boolean expressions .
Proof Checking: LPAC proofs can be checked using, e.g., Pacheck 2.0 [
In the following, we introduce the new proof rules PatternNew and PatternApply to add and instantiate proof patterns. In principle, these rules could be generalized and used to extend any polynomial proof system, including those that do not work over Boolean variables. Here, we focus on extending LPAC and instantiate the new rules to work for this particular proof system. For that, we also extend an LPAC proof from (, ) to (, , ), where denotes a sequence of patterns. Initially = []. Note that cannot be changed by any of the rules in Figure 1.
PatternNew: A pattern is identified with a unique index that will be used in the PatternApply rule to identify the pattern. A pattern has three components: sequence of inputs , sequence of proof steps , and set of outputs .
The sequence of inputs represents the axioms of the pattern. The proof steps form a self-contained proof fragment. In “Correct-LPAC-Proof(, )” it is checked whether the proof steps in can be derived PatternNew (, , , ) (,,) ()=⊥
Correct-LPAC-Proof(,) ⊆Conclusions() ext=ExtensionVar()
(,,∪(,,,ext)) PatternApply (, ext, , ( 1, . . . , ), {(1, 1), . . . , (, )})
(, , ) () ̸= ⊥ ext ̸⊆ ∀ ∈ (). ext : () ∈ ext injective on (). ext ∀ ∈ Var(()) : () 2 − () ∈ ⟨( ∪ ext)⟩ (1) ̸= ⊥, . . . , () ̸= ⊥ (). = { (1), . . . , ()} (1) = ⊥, . . . , () = ⊥ 1, . . . , ∈ K[ ∪ ext] (). = {1, . . . , }
(∪ext, (1↦→1,...,↦→),) by the LPAC inference rules using the axioms given in . The set of outputs contains those conclusion polynomials of the proof steps in , which will be stored as output polynomials of the pattern.
We explicitly extract any extension variables ext from the outputs of the pattern that have been added in the proof steps . When applying the pattern, these variables have to be instantiated as fresh variables. On the other hand, it is not necessary to store any internal extension variables of that are not contained in any polynomial in , since they are only used internally to derive the outputs . They are not needed for the application of the pattern.
After a pattern is checked for correctness, we only store , , and ext in . The proof steps are discarded. On a practical note, since a pattern can be seen as a standalone LPAC proof, we are free to (re-)use any variables and indices.
PatternApply: The index refers to a pattern in . The set ext contains all extension variables that will be added to the LPAC proof through the application of the pattern. These variables are not allowed to be contained in the set of variables of the current proof state (, , ).
The mapping connects the pattern () to the LPAC proof by mapping all variables (including those in ext) in () to polynomials over the variables ∪ ext. This mapping has to satisfy two conditions: First, it has to injectively map the extension variables used in () to the new extension variables in ext, that is, for all 1, 2 ∈ ext, we must have ( 1), ( 2) ∈ ext and ( 1) ̸= ( 2) if 1 ̸= 2. Moreover, has to comply with the Boolean axioms in the following way: for each variable in (), its image under must satisfy the condition () 2 − () ∈ ⟨( ∪ ext)⟩. This restriction comes from the fact that all variables are assumed Boolean in an LPAC proof and the Boolean axioms are used implicitly (see, for instance, the LinComb rule in Figure 1). In general, when a proof system treats certain relations implicitly, the mapping has to be consistent with those relations. In contrast, for a proof system that does not use any implicit relations, can map the variables from () to arbitrary polynomials.
The tuple (1, . . . , ) contains the indices to those polynomials of that are used as inputs to the pattern. We verify that these polynomials match the pattern’s inputs under the mapping , denoted by = in Figure 2. We do an analogous check for all the output polynomials in the set {(1, 1), . . . , (, )}. If the pattern is correctly applied, we store the polynomials as correctly derived polynomials in , i.e., we set () ↦→ .
Proof Checking: For the PatternNew rule, we have to apply the following checks during proof checking: (i) do we already have a pattern with index ; (ii) do and form a correct standalone LPAC proof; (iii) are all polynomials in conclusion polynomials of proof steps in or .
For the PatternApply rule, we have to apply the following checks: (i) does pattern () exist; (ii) are all variables in ext fresh variables that are not contained in ; (iii) does the mapping map the extension variables of the pattern injectively to the fresh variables in ext; (iv) does the mapping comply with the Boolean axioms ( ∪ ext); (v) do the input polynomials correspond to the input polynomials of () after the mapping is applied; (vi) do the output polynomials correspond to the output polynomials of () after is applied.
We illustrate the new proof rules on two examples. In the first example we show how patterns can help to reduce the size of the proof. In the second example we show how to treat extension variables in proof patterns.
Example 1. Let = {+2 −2, − − +1, +2−2, −− +1, −+1} . We use the PatternNew and PatternApply rules to derive 1 ∈ ⟨⟩ in an LPAC proof. We use as indices for the proof steps inside the pattern and as indices for the proof steps outside the pattern. 1 Axiom ( 1 , + 2 − 2 ) 2 Axiom ( 2 , − − + 1 ) 3 Axiom ( 3 , + 2 − 2 ) 4 Axiom ( 4 , − − + 1 ) 5 Axiom ( 5 , − + 1 ) 6 PatternNew ( 1 , [ ( 1 1 − 2 2 ) , ( 2 2 − 3 ) ] ,
[ LinComb ( 3 , ( 1, 2 ) , ( 1 , 2 ) , 1 − 2 3 ) ] , { 3 } ) 7 PatternApply ( 1 , { } , [ 1 ↦→ , 2 ↦→ 1 − , 3 ↦→ ] , ( 1, 2 ) , { ( 6 , − 2 ) } ) 8 PatternApply ( 1 , { } , [ 1 ↦→ , 2 ↦→ 1 − , 3 ↦→ ] , ( 3, 4 ) , { ( 7 , − 2 ) } ) 9 LinComb ( 8 , ( 5, 6, 7 ) , ( 1 , 1 , −1 ) , 1 )
The pattern created in this proof captures the derivation of a specific linear combination of two polynomials: Starting from 1 = 1 − 2 2 and 2 = 2 − 3, defined over variables 1, 2, 3, we can derive the linear combination 3 = 1 + 22 = 1 − 2 3. We then apply this pattern in two diferent ways.
First, we instantiate 1, 2, 3 by , 1 − , and , respectively. Note that this substitution complies with the Boolean axioms. For instance, ( 2)2 − ( 2) = (1 − ) 2 − (1 − ) = 2 − ∈ ⟨({, , , , })⟩ . Under this substitution, 1 and 2 reduce to the axioms 1 and 2, and the output polynomial 3 becomes − 2 . In the second application, we substitute 1, 2, 3 with , 1 − , and , respectively. Then 1 and 2 reduce to the axioms 3 and 4, and the output polynomial 3 becomes − 2.
By using the pattern, we have to compute the linear combination 1 + 22 only once and can then reuse it through instantiation in each application. In contrast, a classical LPAC proof would require computing each linear combination 1 + 22 and 3 + 24 separately.
Example 2. In this example, we algebraically mimic the Boolean resolution rule. That is, from ¬ ∨ ¬ and ∨ , we derive ¬ ∨ . Algebraically, the two axioms can be encoded as = {, − − + 1} . The goal is to derive ̄ ∈ ⟨ ∪ { ̄ − (1 − )}⟩, with ̄ being a new variable representing ̄ = 1 − . 1 Axiom ( 1 , ) 2 Axiom ( 2 , − − + 1 ) 3 PatternNew ( 1 , [ ( 1 12 ) , ( 2 23 − 2 − 3 + 1 ) ] , [ Ext ( 3 , ( 3 ) , ( 1 − 3 ) ) ,
LinComb ( 4 , ( 1, 2, 3 ) , ( 3 , 1 , 12 − 1 ) , 13 ) ] , { 3, 4 } ) 4 PatternApply ( 1 , {̄ } , [ 1 ↦→ , 2 ↦→ , 3 ↦→ , 3 ↦→̄ ] , ( 1, 2 ) ,
{ ( 3 , −̄ + 1 − ) , ( 4 , ̄ ) } )
LPAC with Patterns # Apply max || File Mem (MB) (MB)
We have extended Pacheck 2.0 with the PatternNew and PatternApply rules and show the efect of adding those rules on a small set of benchmarks that originate from multiplier verification. In that setting, we prove that the circuit specification is contained in the ideal generated by the circuit encoding.
Proof Generation: In our recent work on circuit verification [
To detect isomorphic subcircuits, we map all gate variables of a subcircuit to a standardized set of variables and check for syntactic equivalence. Using this approach, we are able to cache over 80% of the identified subcircuits. For each computation within a subcircuit, we store a corresponding proof pattern. Whenever a cached pattern is retrieved, we instantiate and apply the corresponding proof pattern to avoid the need for re-computation.
In the following, we use a subset of the benchmarks from [
Table 1 summarizes our results in two blocks: one for the original version of LPAC (“LPAC without Patterns”), the second one with our two new proof rules (“LPAC with Patterns”). None of the proofs contains Ext or Deletion rules. The second column lists the number of axioms, which is equal for both approaches. The next four columns represent LPAC proofs without patterns. We list the number of linear combination proof steps (“Steps”), the size of the proof file in MB (“File”), the used memory in MB (“Mem”), and the time needed to check the proof (“Time”) in seconds. The next seven columns show the results when our two new proof rules are added. We list the number of PatternNew steps (“#”), the total number of PatternApply steps (“Apply”), and the maximal number of steps in a pattern (“max ||”).
It can be seen that we can significantly reduce the number of proof steps when using patterns and we always improve on the file size of the proof and the memory and time used to check the proof.
Further improving the eficiency of proof checking is part of future work. In particular, we want to
investigate the efects of recently developed techniques for finding short proofs of ideal membership [
This research was supported by Austrian Science Fund (FWF) [10.55776/ESP666] and by the LIT AI Lab funded by the state of Upper Austria.
During the preparation of this work, the authors used ChatGPT in order to: Grammar and spelling check, paraphrase, and reword. After using this tool, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.