Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL

The underlying logic of SMT is many-sorted first-order logic with equality (see e.g., [21]). We assume the usual definitions of well-sorted terms, literals, and formulas in this logic. We also assume the usual definitions of satisfiability and unsatisfiability with respect to one or more theories. SMT solvers determine the satisfiability of input formulas with respect to specific sets of supported background theories. Examples of SMT solvers include cvc5 [5], veriT [13], and z3 [18].

A refutation proof in a theory $T$ is a series of inference steps starting from an input formula $\phi$ and terminating with the unsatisfiable formula $\perp$. Such a proof certifies the unsatisfiability of $\phi$ in $T$. A proof format encompasses a list of proof rules specifying how specific conclusions can be drawn from specific assumptions and under what conditions. A (refutation) proof certificate is a realization of a refutation proof in a particular proof format consisting of a number of proof steps. We require each step in a proof certificate to be an application of a proof rule from the corresponding proof format. As an example, the Cooperating Proof Calculus (CPC) defines a set of proof rules used internally by the cvc5 SMT solver [2], and a CPC proof certificate is a sequence of steps based on those rules. Despite the fact that several SMT solvers can produce proof certificates [36, 17, 25, 8, 14], no standard proof format has emerged in the SMT community yet. A program that checks the well-formedness of a proof certificate is called a proof checker.

A useful informal notion for capturing the difficulty of checking a proof is its granularity, which roughly corresponds to the computational complexity of checking that a step is correct. In particular, steps (and thus the proofs containing them) are fine-grained if they can be checked efficiently, and coarse-grained otherwise. We are deliberately vague about what efficiently means in this context, but one suitable general definition would be requiring polynomial time in the worst case. We will often refer to very coarse-grained steps as holes. An elaborator is a tool that transforms coarse-grained steps into fine-grained steps. A translator transforms proof certificates from one proof format to another. Elaboration and translation are often performed simultaneously.

One way to define simple fine-grained rules in a user-friendly way is the domain-specific language RARE [33]. It is based on the SMT-LIB language and is designed for non-experts. Most rules that capture basic simplifications of SMT-LIB terms can be expressed in RARE. On top of this, RARE’s abstract types allow type-generic rules. For example, reflexivity can be expressed as a single rule that applies to all SMT-LIB terms. Lachnitt et al. [29] show that Isabelle lemmas can be generated from RARE rules automatically.

The Alethe proof format evolved from what was initially a custom proof certificate format for the veriT SMT solver. Its syntax is based on SMT-LIB [9]. Each step in an Alethe proof is either an assumption, an anchor opening a new subproof, or a regular step. Steps have a rule label, indicating the rule applied in that step, and a conclusion clause of the form (cl $F_1\mathrm{\cdots }{F}_n$), where $n\ge 0$ and each $F_i$ is a formula. Additionally they might have premises and arguments. Anchors introduce an additional context and can have a context argument to express transformations under binders like quantifiers. Assumptions either repeat input assertions or add new assumptions locally in a subproof.

Alethe has a natural-language specification that defines a total of 103 proof rules [7]. The SMT theory currently supported is the (quantified) theory of linear (real and integer) arithmetic with uninterpreted functions. Only two kinds of proof steps in Alethe proofs are considered holes. The first one is applications of a rule called hole, which is used to represent steps that do not correspond to any other Alethe rule. The second one is application of a rule called lia_generic, which is used to introduce any valid disjunction of integer linear inequalities, without any hints for proof checking. These steps are considered holes because they are extremely coarse-grained – filling them in can require super-polynomial work in principle.

Carcara [1] is an independent proof checker and elaborator for Alethe written in Rust. It can elaborate most lia_generic steps from veriT proofs by calling cvc5, which can output a fine-grained proof for unsatisfiable linear integer arithmetic queries. Carcara itself is not verified, meaning that it must be considered part of the trusted computing base when it is used to check proof certificates.

Isabelle/HOL is a proof assistant based on higher-order logic with top-level polymorphism [32]. It follows the LCF [34] dogma; that is, its kernel only allows a small set of inference rules. From these, tactics can be built, which are programs that discharge proof goals. Techniques that can find proofs automatically help the user concentrate on the creative argument of their proof, without dealing with more tedious parts. Sledgehammer is a tool inside of Isabelle that calls external solvers to improve automation. To maintain high trustworthiness and avoid extending the trusted computing base beyond the Isabelle kernel, any result found by an outside tool has to be proven again inside Isabelle, based on some sort of directions from the external prover. This process is called replay and can easily fail unless the ATP provides detailed directions. These are typically in the form of a proof certificate, allowing Isabelle to implement a specialized tactic for each proof rule.

The $\mathrm{𝗌𝗆𝗍}$ tactic has been developed in Isabelle to interact with SMT solvers and replay their proof certificates. Figure 1 shows how the tactic works at a high level. The current goal (which is to be proven valid in the current context) is negated and encoded into an SMT-LIB problem together with a selection of premises from the context. The premises can be definitions or previously-stated lemmas and are selected by Sledgehammer based on relevance heuristics. A big part of the encoding consists in bridging the expressiveness gap between higher-order logic and the SMT solver’s many-sorted first-order logic. If the external solver finds a proof, the $\mathrm{𝗌𝗆𝗍}$ tactic checks that the assumptions in the returned proof certificate match the original premises, and if every proof step is correct. For the latter check, a set of specialized tactics, which we call reconstruction functions, are called. Each specific tactic called depends on the proof rule used in the step being checked. For the most part, there are separate tactics for each of the proof rules in the Alethe standard.

Figure 2 provides more details on the proof reconstruction process for Alethe proof certificates. First, a parser translates the certificate from a string to an AST capturing Alethe terms. Then, the proof processor transforms it to a different AST now using Isabelle terms. Finally, the replay function builds an Isabelle context which contains variable and type definitions. It checks if the assumptions in the Alethe proof correspond to the original assertions selected by Sledgehammer. Then, for each proof step, it calls the appropriate reconstruction function for the corresponding Alethe proof rule, producing an Isabelle theorem stating the soundness of the proof step with respect to a formalization in Isabelle/HOL of Alethe’s theory (i.e., linear arithmetic with uninterpreted functions).

Solvers for the Boolean satisfiability (SAT) problem support proof certificates of various granularities. External and internal elaborators and translators between coarse-grained formats, such as DRAT, intermediate formats like FRAT, and more fine-grained formats like LRAT or GRAT have been implemented [16, 4], although producing detailed proofs directly has recently become faster than producing coarse-grained proofs and then elaborating them [35]. Certified checkers for these formats exist in several ITPs [16, 30, 31].

While several proof formats exist for SMT solvers, translations between them have not been the focus of community efforts, probably because no one format has prevailed yet. Instead, most proof formats are specific to individual solvers [13, 26, 17]. cvc5’s internal elaboration capabilities allow the user to either output coarse-grained proofs quickly, or fine-grained proofs at the cost of some performance overhead [33, 8]. cvc5 also features internal translations to different formats such as the LFSC [38] and CPC formats [3]. SMTCoq translates LFSC proofs into the certificate format used by Rocq [20]. There are also ongoing efforts to translate proof certificates from various theorem provers to Dedukti [15, 24].

While many checkers for SMT proof certificates exist, certified checkers or checkers written in a trusted environment are more rare. They include SMTCoq (verification in Rocq) and the reconstruction in Isabelle by Schurr et al. [37] that we extend in this work. Schurr et al. rely on veriT’s fine-grained proofs, but show that proof granularity is a trade-off and acknowledge that some steps are not fine-grained enough. For example, Alethe allows proof steps whose conclusion can contain equalities that have been implicitly reordered. In contrast, cvc5 proofs are more fine-grained and provide such extra operations explicitly as proof steps. However, some other rules establish facts not needed by Isabelle. For example, the bind rule, which renames bound variables, is superfluous in Isabelle which uses De Bruijn indices.

Blanchette et al. [10] extended Sledgehammer so that it could call SMT solvers as oracles, i.e. using one of Isabelle’s internal tactics and without replaying a proof certificate. The authors point out that only after working together with SMT solver developers were they able to obtain reasonable results. This work represents the groundwork for our project.

The proof reconstruction approach for the incorporation of external provers into ITPs was pioneered by Böhme and Webers’ reconstruction of z3 proofs [12]. The closest work to ours is the aforementioned paper by Schurr et al. [37], which extends the original reconstruction of veriT proofs [23] by fine-tuning veriT and Isabelle, compressing proofs, and supporting somewhat fine-grained simplification rules. Along the way, they recognized that documentation on the proof format was needed, which resulted in the Alethe specification.

There have been several large-scale evaluations of proof automation in Isabelle. Böhme et al. [11] compared three first-order theorem provers on goals from seven Isabelle theory files, creating the original Judgement Day benchmark set. The aforementioned work by Blanchette et al. [10] extended the set and for the first time also included SMT solvers in an evaluation. Desharnais et al.[19] set a new standard by generating a set of $5000$ benchmarks from 50 randomly selected Isabelle libraries.

To our knowledge, our work is the first to contain a comparative evaluation, over the same problems, of two solvers that use the same reconstruction functions, enabling more interesting and detailed comparisons, as we discuss in Section 6.

The most common issue when attempting to produce Alethe proofs in cvc5 was the lack of direct counterparts for some rules in the CPC format, which closely follows cvc5’s internal calculus. This was addressed in most cases with a dedicated translation routine. For example, Figure 3 contains the CPC modus_ponens rule which concludes the formula $F_2$ from the premises $F_1$ and $F_1\to F_2$. Since there is no corresponding rule in Alethe, the same conclusion must be derived via a combination of other rule applications, as shown in the figure. This example also illustrates how in Alethe there is an emphasis on clausal forms and inference by resolution, with auxiliary rules that derive clauses from more general formulas, whereas in CPC there is more emphasis on Natural Deduction-style rules which apply directly to general formulas. As a result, numerous CPC rules have to be converted to Alethe by first applying Alethe rules that convert CPC rule premises to valid clauses and then applying the Alethe resolution rule to those clauses. The expansion of single CPC inferences to multiple Alethe inferences can lead to noticeably larger sizes for the resulting Alethe proof.

The above case is actually relatively benign. Some cases showed more serious incompatibilities between the Alethe and CPC proof calculi. A specific example is the way they handle the normalization of associative commutative (AC) operators, which involves flattening and removal of duplicates. In Alethe, the ac_simp rule establishes an equality between a term and its normalized form, where all nested occurrences of AC operators are flattened to completion.²²2The motivation for this rule is to directly represent a performance-critical simplification [6, Sec. 4.6] at the cost of a more coarse-grained rule. In CPC, on the other hand, a similar normalization is performed by the ACI_NORM rule, but only on the top-level applications of the AC operator in the original term. To translate an ACI_NORM step concluding $t_0=t_1$, we make use of the fact that ac_simp is strictly more powerful, so it can be used to derive two intermediate conclusions of the form $t_0=t^{\prime }$ and $t_1=t^{\prime }$, where $t^{\prime }$ is the result of the more aggressive normalization achieved by ac_simp. The CPC conclusion $t_0=t_1$ can then be derived via Alethe rules for symmetry and transitivity of equality. Alternatively, a rule could be added to Alethe to represent a more local version of AC simplification. This could be a possible avenue for improving the performance of cvc5 proof reconstruction in Isabelle.

In some cases, there is no reasonable way to translate a CPC step into Alethe – because it would require a huge number of steps, for example. In those cases, we extended the Alethe calculus itself. We only considered this as a last resort, however, since adding a rule to the standard impacts all of its users.

An example of a set of CPC rules that could not be directly represented or otherwise conveniently translated to Alethe is the set containing variants of ARITH_MULT_POS, which allows the two sides of an (in)equality to be multiplied by a positive factor. For equalities, the rule is as follows:

While Alethe does include arithmetic rules, they usually only work on normalized (linear) inequalities, so for the rule above it would be necessary to break up the equality into two inequalities, normalize both $m\ast l$ and $m\ast r$, and then perform the arithmetic step via Alethe’s la_generic rule, which is unfortunately expensive to check [1]. Moreover, using this translation would add a number of steps linear in the degree of nesting present in the input formula, which can be large. We deemed this unacceptable. We instead introduced new rules in Alethe which capture the rule above and each of its variants.

Another example of a CPC rule that is difficult to implement in Alethe is ARITH_POLY_ NORM, which infers the equality $s=t$ of any two terms $s$ and $t$ that can be normalized to the same sum of monomials. Since this rule performs a full normalization on the given terms $s$ and $t$, a translation into Alethe would require a full proof of how the two terms are normalized according to particular arithmetic simplifications. Thus, in this case too, we added a corresponding Alethe rule with the same semantics as the CPC rule.

A subtle aspect of Alethe, inherited from the SMT-LIB language, is that the sort of a number literal depends on the SMT-LIB logic associated with the problem. For example, the literal 123 is an integer in most logics, including those that permit real numbers. However, in logics with reals but not integers, the same literal becomes a real number. To complicate matters further, decimal literals (e.g., 2.45) are allowed in SMT-LIB only in logics with real numbers whereas they are allowed in Alethe also in proofs that do not involve reals. For example, the la_generic rule uses decimal coefficients to certify the validity of a set of linear inequalities in both real and integer arithmetic.

To simplify this situation, we changed the Alethe standard to be not so liberal with the type assigned to numeric literal. Specifically, now a numeral (e.g., 123) is always an integer, while a decimal (e.g., 12.0) is always a real. Furthermore, both numerals and decimals are allowed in rules, independently of the logic set in the input problem. Finally, Alethe now has a dedicated syntax for writing rational constants in fractional form. In SMT-LIB, they must be written using the division operator, e.g., (/ 1 3). This complicates parsing, since the entire term must be parsed to detect that it is to be treated as a constant. In Alethe, this rational number can now be written as the single literal 1/3 and parsed directly as a (real) constant.

The only case we encountered where a translation from CPC to Alethe is not possible is when the CPC proof contains steps introducing fresh terms without a proper justification, which is not allowed in Alethe. Each such step results in a hole in the Alethe proof. This case is exceedingly rare, however, and thus does not significantly impact our results. Nevertheless, finding a good long-term solution for such incompatibilities is an important ongoing challenge.

A common occurrence we encountered was needing to examine many different parts of the code base in order to fix a single bug or issue. This is a heavy burden for maintainers and potential developers, as they first must become experts on the whole system before being able to make a change. It would be much better if the code were more modular so that local changes could be made without having to understand everything else.

One might hope, for instance, that the code implementing reconstruction could be modified by a non-expert who just needs to add support for a single new feature or fix a bug with one operator. Unfortunately, this is not the case. For one thing, some transformations are done during parsing that affect what is seen in reconstruction in non-intuitive ways. For example, the SMT-LIB term (xor $x$ $y$) is converted during parsing to the disequality $\neg (y=x)$. This is to avoid introducing an $\mathrm{xor}$ operator in Isabelle. Therefore, a new developer looking to make a change to how $\mathrm{xor}$ is handled in the reconstruction function would be confused to discover that $\mathrm{xor}$ no longer appears after parsing.

To address such issues, we typically took one of two courses of action. In the cases where such design decisions seemed unjustified, we changed them. When changing was deemed too risky or difficult, we instead produced better documentation to explain the non-intuitive design decisions.

Fortunately, in many cases, we were able to successfully decouple different parts of the code. For instance, previously, the Alethe node data structure inside of Isabelle did not fully mirror the Alethe grammar. Specifically, in the grammar, both anchor steps and normal steps can have arguments, called step arguments and context arguments, respectively. The Alethe node data structure inside of Isabelle only contained a single field for arguments, which was used for both step and context arguments. Furthermore, for some steps, the proof postprocessor needs to communicate additional information to the reconstruction function. Any such information was also transmitted using the same argument field. Thus, the field was used for three different purposes. A developer working on the reconstruction function would have had to understand all the possible ways the argument field could be populated and take the appropriate context-dependent action. In this case, we changed the implementation so that the Alethe node data structure uses different fields for the different kinds of information.

We also tried to use strong modular design principles when adding new features. For example, in some cases, different strategies work better for the same Alethe rule, depending on which solver it comes from. This can happen, for example, when a rule is quite general and two solvers tend to use it in different ways. To address this, we made it easy to have the reconstruction code dispatch to different routines based on which solver generated the proof. As another example, we refactored a monolithic debug tracing capability to instead support debug traces for different components that can be turned on or off independently.

In general, a major goal of our work was to make it possible to work on or test many parts of the reconstruction pipeline separately and independently. We describe several tools we developed to aid with this goal in Section 5.

As we dug into the reconstruction code in Isabelle, we discovered that only a fragment of the full Alethe standard was supported. Worse still, there was no explicit indication of which fragment was supported exactly, and even active developers did not know for sure. Finally, it was unclear whether some parts of the code were there for backwards compatibility with older versions of veriT or whether the code was dead and should be removed.

We took several steps to address these issues. First of all, we added support for parts of the standard that were clearly missing. An example of this is the tautology rule, which was always pruned from veriT proof certificates due to a veriT option that was always enabled when called by Isabelle. As another example, reasoning about xor had not been implemented because none of the input problems from Isabelle contained it and veriT did not generate it. This, however, might not be the case for other solvers. We also discovered that some rules, such as div_simplify, were missing even though they do show up in veriT proofs. We attribute this to the fact that an insufficiently diverse set of test cases were used for the veriT reconstruction. We now support all of these rules as well as several others we discovered to be unsupported.

It was trickier to find and fix the rules that were only partially supported. For this, we created a library of regression tests. We discovered that many errors came from rules involving variadic operators. Terms such as (and $a$ $b$ $c$) are transformed into nested binary applications during parsing. This makes it harder to reconstruct rules that need to distinguish between applications of operators to multiple arguments and their equivalent representation as nested binary applications.

We also discovered cases where the Isabelle reconstruction supported proofs inconsistent with the Alethe standard. It was unclear whether this was the result of bugs or inconsistencies in veriT or of old code supporting previous versions of veriT or Alethe. Such code made it difficult to upgrade to a newer version of veriT, where these inconsistencies had been fixed. It also led to difficulties in the cvc5 integration. We made the decision to remove and update any code incompatible with the current Alethe standard and encouraged the veriT developers to fix any resulting discrepancies.

For some proof steps, especially those that are very fine-grained, providing a full translation into Alethe is overkill. In this section, we discuss how the proof rules generating these steps can be supported much more easily. This functionality is also useful when updating a solver to a new version containing additional proof rules or when supporting a completely new solver that outputs Alethe proof certificates but extends it with some custom rules.

We assume in Section 3 that a solver has a fixed proof calculus with rules that are rarely changed. However, this often only holds for coarse-grained proof rules. More fine-grained rules are more likely to change frequently for solvers under active development. A good example of this is the set of term rewriting rules. Modern SMT solvers have hundreds of different rewrite rules for simplifying and normalizing terms. Developers frequently add new rules or modify previous ones as part of their ongoing performance tuning efforts. The approach implemented in cvc5 is to use a DSL called RARE, initially proposed by Nötzli et al. [33], which makes it easy to add or modify the rewrite rules used by the proof calculus.

For a large subset of rewrite rules expressible in RARE, we offer an automatic solution for supporting them that does not require knowledge of the SMT solver or of the Isabelle ML code at all. Lachnitt et al. [29] already showed how the Isabelle plug-in IsaRARE can automatically translate a rewrite rule in RARE to a lemma in Isabelle. We build on this work by adding infrastructure that can automatically use IsaRARE-generated lemmas (or even hand-written lemmas) for proof reconstruction. All that is required is to register such lemmas with the reconstruction algorithm using a simple interface we provide.

Note that even if a solver does not use RARE, this feature could still be useful for supporting a solver’s fine-grained proof rules, as RARE is easy to learn and the reconstruction interface we provide for it is easy to use.

We call any testing code implemented in Isabelle that doesn’t interact with an external ATP internal. Before our work, internal testing tools were very limited, and debugging was a tedious process. Developers were able to see the generated SMT-LIB problem and the proof certificate coming back from an external SMT solver. And, they could see when a reconstruction function failed and could also see the Isabelle term corresponding to the conclusion of a proof step. While these utilities were useful, there were two significant problems with this workflow.

First, if the conclusion had not been translated correctly, it was not easy to determine which part of the integration was responsible for the mistake. For example, the context arguments of bind steps can rename bound variables. These arguments were, however, not fully parsed in Isabelle according to the Alethe standard – a problem that had not been detected earlier since veriT would only output certain combinations. The available internal debugging information would point to a failure in a reconstruction function, but the problem was actually during replay, where the code for adding new variables to the context was implemented.

Second, since the contracts between different modules were not clearly defined, it was not always clear what to expect when looking at a reconstruction function. For example, the parser sometimes removes or changes proof steps to increase performance. This is done, e.g., for subproofs that merely rename variables. For an inexperienced developer, this could come as a surprise if they did not know about this functionality.

The standard approach for debugging such issues was to add print statements to figure out which part of the code had failed. Thus, we added a general trace-based debugging capability. Tracing can be turned off or on for each part of the pipeline independently and with different verbosity levels. We then added output traces that show not only relevant variables with their values but also explain what the code is doing.

We have implemented a new function in Isabelle called $\mathrm{𝖼𝗁𝖾𝖼𝗄}\mathrm{\_}\mathrm{𝗌𝗆𝗍}$ that can check proof certificates generated by SMT solvers. $\mathrm{𝖼𝗁𝖾𝖼𝗄}\mathrm{\_}\mathrm{𝗌𝗆𝗍}$ takes two arguments: a file containing an SMT problem in SMT-LIB format and a file containing a proof certificate for that problem in Alethe format. The function parses the SMT-LIB input file, declares the constants and types in a new Isabelle context, imports the assumptions, and then checks the proof certificate via reconstruction.

While in principle the function is easy to implement (ignoring the inconveniences created by SMT-LIB’s very liberal rules on what can be an identifier), its development is complicated by the need to check that the assumptions in the proof certificate match the assertions in the SMT-LIB problem. When the $\mathrm{𝗌𝗆𝗍}$ tactic produces an SMT-LIB file, it always gives names to each formula being asserted, and solvers use these names in their proof certificates. This makes it easy to recognize the assumptions again during proof reconstruction. However, there is no guarantee that the file and certificate read by $\mathrm{𝖼𝗁𝖾𝖼𝗄}\mathrm{\_}\mathrm{𝗌𝗆𝗍}$ will follow the same policy. To address this, we added the capability to match assertions with assumptions syntactically. If that fails, we allow Isabelle to do some lightweight reasoning (using the $\mathrm{𝖺𝗎𝗍𝗈}$ tactic) to try to match assumptions with assertions. In effect, $\mathrm{𝖼𝗁𝖾𝖼𝗄}\mathrm{\_}\mathrm{𝗌𝗆𝗍}$ makes it possible to use Isabelle as a trusted proof checker for SMT (see Section 6.1). It also makes it easy to create diverse test cases for reconstruction simply by generating SMT-LIB problems.

While adding the capability to check external proofs helps to decouple the translation of proofs from their reconstruction, when the process fails, it might still not be clear if the error originates in the reconstruction function, the certificate parser, or an incorrectly built context during replay.

For instance, we had trouble replaying a certain rule, and only after a long and tedious debugging session did it become clear that the reconstruction function was not the issue. Instead, the replay had not properly deleted an underscore in an internal representation of a term.

To aid with debugging in such situations, we introduce a new Isabelle method that can be used with most rules and that directly applies a reconstruction function to a lemma written in Isabelle. Users can then write an Isabelle lemma corresponding to the expected result of parsing an Alethe proof step and check that the reconstruction function works correctly. The main challenge was to emulate the context built up during the normal reconstruction process. To keep this simple the method does not support for now rules that introduce subproofs since those rules create nontrivial dependencies on contexts.

The new functionality allowed us to discover several bugs in the reconstruction functions and significantly helped in the development of new rules. In general, it also allows examples to be kept as regression tests, since complete proofs are more fragile and may change during a solver update.

While it is helpful to check the reconstruction functions directly on Isabelle terms, this is mostly useful with hand-written tests. Checking the reconstruction of a step in an actual proof certificate would require translating that step to an Isabelle term. Even though this is possible, it is quite tedious and error-prone, and it becomes infeasible once variables have to be added to the context, e.g., as a consequence of reconstructing a subproof. This approach is thus not well suited for extensive testing of individual steps coming from actual proofs. Note also that, although our $\mathrm{𝖼𝗁𝖾𝖼𝗄}\mathrm{\_}\mathrm{𝗌𝗆𝗍}$ tool can be used to check the parser, processor, and replayer all at once, it is not suitable for testing the reconstruction function on a specific proof step: one would have to rely on that step being present in an end-to-end proof of an SMT-LIB input problem and, even then, the reconstruction could fail for reasons unrelated to the targeted proof step, or time out before reaching it.

To fill this gap, we developed a new subtool in the Carcara checker called $\mathrm{𝗌𝗅𝗂𝖼𝖾}$ that slices Alethe proofs with respect to any proof step in them. Specifically, $\mathrm{𝗌𝗅𝗂𝖼𝖾}$ takes a problem $Q$, a proof $P$, the identifier $s$ of a target proof step in $P$, and a depth limit $d$. It then produces a new problem $Q^{\prime }$ and new proof $P^{\prime }$. In the most basic configuration of $\mathrm{𝗌𝗅𝗂𝖼𝖾}$, $Q^{\prime }$ is the same as $Q$ while proof $P^{\prime }$ contains only the steps needed to generate step $s$, as well as the anchors of any subproofs of $P$ that rely on $s$. The input value $d$ indicates the maximum depth that $P^{\prime }$ can have as a proof tree with root $s$. If $s$ has a deeper proof tree in $P$, the proof is cut at depth $s$ by justifying any steps at that depth in $P^{\prime }$ as the application of the hole rule with argument "trust". Such steps are skipped during testing in Isabelle. The hole rule is similarly applied to step $s$ to conclude the empty clause (cl) from it.³³3Alethe proofs can only be refutations and so are required to end with the empty clause. Checking the new proof $P^{\prime }$ can be used to reveal any problems with step $s$ directly and results in a unit test for the proof rule used in that step. An example of a sliced proof with depth limit 1 is shown in Figure 4, where we can see that neither the original assumptions nor step s2 appear in the sliced proof, as they are not relevant for justifying target step s4.

An alternative configuration of $\mathrm{𝗌𝗅𝗂𝖼𝖾}$ allows the generation of even smaller problems and sliced proofs by focusing entirely on the targeted step. It can be used for a large class of steps not embedded in subproofs. In these cases, $P^{\prime }$ can be minimized by simply adding the premises and negated conclusion of the target step $s$ as assumptions. An example is shown in Figure 5, where all the assertions in the original problem from Figure 4 are discarded and a new SMT problem $Q^{\prime }$ is built out of the premises of step s4. These premises then become assumptions in the sliced proof.

We considered extending this configuration to steps within subproofs by always adding as an assumption either the negated conclusion of the target step $s$ or that of the last step $t$ in the subproof in which $s$ appears. Unfortunately, a combination of the limitations of the Isabelle reconstruction and the Alethe standard currently prevents us from taking advantage of this improvement. In future work, we plan to address this issue, which would extend the scope of this configuration.

In their “Seventeen Provers Under the Hammer” evaluation, Desharnais et al. [19] generate several benchmark sets from 50 randomly selected files from Isabelle’s Archive of Formal Proofs, selecting 100 goals per file (they avoid selecting consecutive goals because those are often similar to each other). Using these 5000 goals, several families of SMT-LIB benchmarks are generated (they also generate non-SMT-LIB benchmarks, but we ignore those here). The families vary based on how many facts are selected and added from Isabelle’s definitions and lemmas. In general, adding more facts increases the chance that the solver will prove the goal, although adding too many of them increases the risk of slowing down the search. The families are called “max facts $n$” for different values of $n$. Each family is based on the same set of 5000 goals, and benchmarks are generated by using the MePo relevance filter to add $n$ facts to each goal. The value of $n$ varies from 16 up to 1024.

For this experiment, we use our $\mathrm{𝖼𝗁𝖾𝖼𝗄}\mathrm{\_}\mathrm{𝗌𝗆𝗍}$ tool to run veriT and cvc5 on these benchmarks, have both of them generate Alethe proof certificates, and then check these proof certificates via reconstruction in Isabelle. Since we are only interested in comparing solvers using the Alethe pipeline, we did not run z3 as part of this experiment. All experiments are run on a cluster equipped with Intel(R) Xeon E5-2637 v4 CPUs and 8GB of memory per job.

We test the success of our translation approach with problems originating from Isabelle rather than on benchmarks from the SMT-LIB library, since Isabelle-generated benchmarks have a different structural profile than those generally found in SMT-LIB. For example, SMT-LIB benchmarks often contain huge (nested) conjunctions, while Isabelle-generated benchmarks do not. As another example, all Isabelle benchmarks that mention natural numbers use a particular encoding into integers, while SMT-LIB benchmarks use more heterogeneous encodings.

Our second experiment demonstrates that proof steps can be supported without writing reconstruction functions and provides a case study for the functionality of our slicing tool.

We focus on cvc5’s term rewrite rules, which are supported via automtically generated lemmas as explained in Section 4.3. For our experiment, we use every rewrite rule that appears at least once in the cvc5 Alethe proofs of the Seventeen Prover benchmark sets. Then, we randomly select up to 50 instances of each rewrite rule.

We use our $\mathrm{𝗌𝗅𝗂𝖼𝖾}$ tool to generate benchmarks for each selected rewrite step and then check the resulting problems and proofs with $\mathrm{𝖼𝗁𝖾𝖼𝗄}\mathrm{\_}\mathrm{𝗌𝗆𝗍}$. We compare two ways of reconstructing the proofs. The first, which we call gen, uses a general tactic that first tries the simplifier with additional facts that we manually select for the goal. If that fails, it calls auto_tac. In general, we tried to be generous with the power this tactic has. In the second approach, we add lemmas proven by Lachnitt et al. as part of their effort to verify cvc5’s term rewriting rules and use their tool IsaRARE to generate lemmas for any newly added rules. We also instruct cvc5 to add the instantiations for the variables in the lemma and reconstruct the step by matching against the lemma. This can be slow since the right lemma needs to be fetched and the instantiation can be more costly than the matching the simplifier does.

The results are summarized in Table 3. They show that using lemma during reconstruction is faster and more robust, which is a confirmation of the value of developing custom reconstruction lemmas rather than just relying on generic Isabelle techniques.

Our final experiment looks at how the integration of cvc5 affects overall Sledgehammer performance. Sledgehammer is somewhat complex; however, it roughly works as follows. Given a goal to prove in Isabelle, it first calls a number of ATPs in parallel to attempt to solve the goal. Note that in this first phase, no proofs are requested and no reconstruction is attempted. Instead, whenever an ATP succeeds, it is asked for an unsatisfiable core, i.e., a (preferably small) subset of the problem that is unsatisfiable on its own. Next, all of the collected unsatisfiable cores are passed to a set of built-in simplification tactics in Isabelle, which often can then produce an Isabelle proof. When this fails, these problems are sent to the $\mathrm{𝗌𝗆𝗍}$ tactic which calls all of the available proof-producing SMT solvers and attempts to reconstruct any proof certificate obtained.

For our experiment, we use Mirabelle [11], a tool that automates calls to Sledgehammer. We run the experiment on Isabelle’s HOL Library.⁴⁴4Schurr et al.’s original experiments with veriT also included three AFP entries, but there were not many calls to the $\mathrm{𝗌𝗆𝗍}$ tactic for those files, so we decided to use only the HOL Library. Following Schurr et al. [37], we set the timeout to $10\mathrm{s}$ for the entire call to the $\mathrm{𝗌𝗆𝗍}$ tactic. In general, we followed their setup as closely as possible. Unfortunately, some Mirabelle options are no longer available in the latest version of Isabelle.

Our results⁵⁵5Run on an Intel i9-12900 with $128\mathrm{GB}$ RAM, running 3 Mirabelle instances at the same time with a limit of $30\mathrm{GB}$ given to the underlying Standard ML implementation. show that for the HOL Library, the $\mathrm{𝗌𝗆𝗍}$ tactic is called 267 times. Of these 267 queries, 257 can be solved by reconstrucing veriT proof certificates, and 119 can be solved by reconstructing z3 certificates. Together veriT and z3 succeed on 259. On the other hand, proof reconstruction using cvc5 succeeds on 243, including half (4/8) of the remaining problems unsolved by veriT and z3. Overall, cvc5 is significantly more successful than z3 but not as successful as veriT. We expect this is largely due to the observation already made that cvc5 proofs are slightly larger and take a bit longer to reconstruct. With only a 10 second timeout, veriT has an advantage. We expect that with a longer timeout or with more optimization effort, cvc5 would catch up and probably surpass veriT, as is seen in the first experiment which has a longer timeout.