Satisfiability Modulo Theories (SMT) solvers are widely used as backbones of formal methods tools in a variety of applications, often safety-critical ones. These tools rely on the solver's correctness to guarantee the validity of their results. Producing and checking proofs is the de facto standard to ensure the correctness of SMT solvers independently from implementations, which are often prohibitively dificult to verify. Arithmetic reasoning is one of the foundations of SMT reasoning, and therefore it is essential to support proof production and checking for it. In this extended abstract, to accompany a keynote talk at the 2023 SC-Square Workshop, we survey recent work (both the author's and from the literature) and discuss challenges on the production and checking of proofs from SMT solvers for arithmetic reasoning.
State-of-the-art SMT solvers, in order to optimize performance, generally have large and complex codebases written in system languages. This makes it hard to guarantee that the solver results are not compromised by implementation issues, which can happen despite the best eforts of developers. To increase trust, a possible solution is to formally verify or to qualify the solvers. However, these approaches are costly and once accomplished tend to “freeze” the systems, since changes require a new verification or qualification process. Moreover, the sheer complexity of the task frequently leads to compromises, with systems being less performant than the state of the art, thus hindering their usability.
An alternative is to make confidence in the results independent from the implementation via
machine-checkable certificates of the correctness of these results. For SMT solvers, certificates
are models, for satisfiable results, and proofs for unsatisfiable results. While satisfiable results
generally denote a desired condition is not valid, unsatisfiable results ensure it is, which
significantly increases the importance of proofs. But while model production is well established
in state-of-the-art SMT solving (although in the presence of, for example, transcendental
functions, there are challenges [
The main challenge for producing proofs is to justify the combination of heterogeneous,
theory-specific algorithms used by solvers to derive unsatisfiability, while keeping the solver
performant and providing enough details to allow scalable proof checking, i.e., checking that
is fundamentally simpler than solving. We have tackled this issue in previous work [
Once proofs are produced, the challenge is to check they are correct. Proof checkers are given
the proofs produced by the solvers and validate whether the steps in the proof are correct with
relation to the proof calculus of which the proof is an instance. To maximize trustworthiness,
the proof checker should be small and simple (ideally, even formally verified). Alternatively,
the proof can be embedded in a highly trusted system such as a skeptical interactive theorem
prover. The SMT community is increasingly embracing this approach, with proof production
becoming a major focus in recent years [
When considering interactive theorem provers or formally verified checkers as the targets of
SMT proofs, the dificulty is to embed in these systems the formal calculus representing the
proofs, which requires proving this calculus correct with relation to the logic of these systems.
This task is already complex for the overall reasoning performed by SMT solvers [
In this paper we discuss the state of the art and current challenges in proof production and proof checking for SMT solvers, in particular for their arithmetic reasoning.
Recently [
The proof architecture is intertwined with the CDCL( ) architecture [
The modules in Figure 1 are used to solve an input formula in the following manner: the pre-processor receives and simplifies it in a variety of ways into formulas 1, . . . , . For each , the pre-processor stores a proof : → justifying its derivation from . The propositional engine receives 1, . . . , and clausifies them into 1 ∧ · · · ∧ . A proof : → is stored for each clause . Note that several clauses may derive from each formula. Corresponding propositional clauses 1p, . . . , p, where first-order atoms are abstracted as Boolean variables, are sent to the SAT solver, which checks whether their conjunction is satisfiable. The propositional engine and the theory engine work in a loop where the SAT solver asserts literals, which witness the satisfiability of 1p, . . . , p, and the theory engine checks their satisfiability modulo a combination of theories . If the literals are -unsatisfiable, a lemma . : ⃗ → ⊥
1 ...
1p ... p : ⃗ → ⊥
:
Theory Combination : 1 1 2 : 2 1 2 : ...
⊥ : → ⊥ {⃗, ⃗} for each , with not necessarily distinct from +1. not possible, then all the clauses 1, . . . , generated until then are jointly unsatisfiable, and the SAT solver yields a proof : 1 ∧ · · · ∧
→ ⊥ ifrst-order clauses, as are the derivation rules that conclude abstraction does not need to be represented in the proof. . Note that the proof is in terms of the ⊥ from them. The propositional
The post-processor of the propositional engine connects the SAT assumptions with the clausifier proofs, building a proof : 1 ∧ · · · ∧ → ⊥. Since theory lemmas are -valid, the resulting proof only has preprocessed formulas as assumptions. The final proof is built by the SMT solver’s post-processor combining this proof with the preprocessing proofs : The resulting proof :
→ ⊥ justifies the -unsatisfiability of the input formula.
The arithmetic reasoning performed by the solver happens in the pre-processor, where
rewrite rules are used to simplify arithmetic terms occurring in the input, and in the theory
solvers, where the main arithmetic reasoning takes place. We will focus on the current state and
challenges related to arithmetic reasoning in the theory solvers, where we discuss separately
about linear (Section 2.1) and non-linear reasoning (Section 2.2), given the significant diferences
between producing and checking proofs for them. The arithmetic pre-processing reasoning is
comparatively simple and less prominent, and the challenges are mostly related to the handling
of numerous rewrite rules [
We also note that the majority of the arithmetic reasoning in SMT solvers takes place on
quantifier-free formulas, since solvers employ dedicated procedures for logic fragments without
quantifiers that are supplemented by instantiation techniques [
The workhorse of linear arithmetic solving in SMT solvers is an adapted version of the simplex
algorithm [
The simplex algorithm will determine the satisfiability of a conjunction of theory atoms
⋀︀ ∑︀ , ◁▷ ,0 for real constants , , real variables , and relations ◁▷∈ {≤ , <}. The
Farkas lemma shows that if this conjunction is unsatisfiable, then there exist Farkas coeficients
> 0 such that ∑︀ (∑︀ , ) = 0 and ∑︀ ,0 ◁▷ 0, where ◁▷ is ≥ when any ◁▷ are
strict or > otherwise. Moreover, the simplex algorithm can be instrumented to compute these
coeficients for unsatisfiable queries, with minimal overhead. Thus, solvers can compute Farkas
coeficients during solving and provide them when proofs for the unsatisfiability of a given
conjunction of inequalities is requested, which is the case to state the validity of the theory
lemma produced by the solver, which corresponds to the negation of this conjunction of literals.
A proof checker then can use the coeficients to reduce the respective linear combination to false
and thus prove the validity of its negation, the theory lemma. In the Alethe proof format for
SMT solvers [
In cvc5, we have instrumented the solver to provide real linear arithmetic proofs in a more ifne-grained manner. This is motivated to facilitate the algorithm that must be applied during proof checking to justify the reduction of the linear combination to false. We have instrumented cvc5 to leverage the Farkas lemma by allowing bounds ∑︀ , ◁▷ ,0 to be scaled by constants and also summed (the comparator for the sum is strict if and only any summand’s comparator is). The Farkas coeficients give a linear combination of bounds that can be shown to be equivalent to false via simple theory rewriting rather than a more complex algorithm, as above, which sufices to show the unsatisfiability of the conjunction. For example, < − 1 and − ≤ 1 sum to − < 1 − 1, which rewrites to false.
Some SMT solvers, such as Z3 [
Instrumenting solvers to produce the justification for the integer reasoning they provide can
still be challenging, however. For example, the veriT solver often produces no justifications
for the integer reasoning it applies, and cvc5 also fails to do so in some cases [
In Carcara [
SMT solvers adopt diferent solutions to solve non-linear arithmetic problems. For example,
the MathSAT solver uses incremental linearization [
− | 1 . . . , (1 ∧ · · · ∧
) → ◇ 0
where the “− | 1 . . . , ” notation means that this rule takes no premises and has 1 . . .
and as arguments, where the former are variables compared to zero (less, greater or not
equal), and is a monomial from these variables, with ◇ being the comparison (less or equal)
that results from the signs of the variables. Moreover, all variables with even exponent in
should be given as not equal to zero while all variables with odd exponent in should be
given as less or greater than zero. Another challenge regarding incremental linearization is that
these proof rules must be reflected in the proof checkers. For example, in our work-in-progress
integration between cvc5 and the Lean interactive theorem prover [
Since the incremental linearization technique uses multiple lemma schemas in the refinement
loop, all of them must be instrumented to produce proofs to capture the reasoning of this
technique. While this is relatively simple for some lemmas, which can be proven via propositional
and basic arithmetic rules rather than dedicated proof rules, some, such as the one above and
the tangent plane lemma3, need involved proof rules. It is still work in progress in cvc5 to
produce proofs for all the lemma schemas used in the incremental linearization procedure, let
alone to reflect them in proof checkers.
2.2.2. Proofs for Cylindrical Algebraic Coverings
Proofs for the infeasible subsets generated by cylindrical algebraic coverings are much more
complex, even though they are more accessible than for regular CAD-based theory solvers [
In cvc5 we have an initial proof calculus based on the above idea. The calculus consists of two rules for excluding an interval in some dimension: one based on an assertion and a 3See the ARITH_MULT_TANGENT rule in https://cvc5.github.io/docs/latest/proofs/proof_rules.html partial assignment, and the other one based on a full covering of the next dimension. They are combined and essentially follow the computation of the solver (pruned from unneeded branches). Constructing the actual proof rule applications is complicated by the fact that the premise of a subtree, i.e., the description of the interval that is excluded, is only known when the subtree is closed. We thus generate proofs lazily to manage the construction of a tree-shaped proof and the issue of lazy premises.
The cylindrical algebraic covering proofs are still coarse-grained proofs, with their proof
checking not being inherently simpler than solving. Therefore, currently only marginal gains
can be expected from the cvc5 proofs versus not providing any details at all. In particular, the
second proof rule that lifts a covering to an interval in a lower dimension rests on a significant
portion of CAD-related theory. The proper formalization of CAD theory and its foundational
algorithms in interactive theorem provers is a significant challenge in this respect and subject
of past and future research [
As in the case of linear arithmetic proofs where solvers give no details, for non-linear
arithmetic one can also rely on powerful tactics in interactive theorem provers to attempt to
check these steps, until more fine-grained steps are not produced by the solvers. Recent work
by Kosaian et al. [
Much work has been done for instrumenting SMT solvers to produce proofs for arithmetic reasoning as well as to to check these proofs in ad-hoc tools, verified checkers or in interactive theorem provers. However, there are still multiple challenges to be addressed, as shown in the previous sections, specially as SMT solvers are extended to employ more advanced reasoning techniques from the computer algebra community. Combining eforts from the satisfiability checking and the symbolic computation communities will be fundamental to better address these challenges and allow for more trustworthy SMT solvers. 4It is the first complete multivariate quantifier elimination algorithm formalized in Isabelle/HOL, whereas univariate or incomplete multivariate ones, which are considerably simpler, already existed.