Hint-Based SMT Proof Reconstruction

TL;DR

This work addresses the integration of interactive and automated theorem provers by introducing a hint-based approach to reconstruct SMT proofs within a proof assistant. It presents QuerySMT, a Lean tactic that translates goals to SMT-LIB, gathers preprocessing and theory-reasoning hints from the cvc5 solver, and constructs a self-contained Lean proof script using grind and a refiner prover (duper). The results show that leveraging SMT hints substantially improves internal automation on arithmetic and inductive-type benchmarks, while avoiding dependence on the external solver in the final artifact. The study also analyzes limitations and proposes directions for extending the approach to other proof systems, additional SMT theories, and richer instrumentation for proof reconstruction.

Abstract

There are several paradigms for integrating interactive and automated theorem provers, combining the convenience of powerful automation with strong soundness guarantees. We introduce a new approach for reconstructing proofs found by SMT solvers which we intend to be complementary with existing techniques. Rather than verifying or replaying a full proof produced by the SMT solver, or at the other extreme, rediscovering the solver's proof from just the set of premises it uses, we explore an approach which helps guide an interactive theorem prover's internal automation by leveraging derived facts during solving, which we call hints. This makes it possible to extract more information from the SMT solver's proof without the cost of retaining a dependency on the SMT solver itself. We implement a tactic in the Lean proof assistant, called QuerySMT, which leverages hints from the cvc5 SMT solver to improve existing Lean automation. We evaluate QuerySMT's performance on relevant Lean benchmarks, compare it to other tools available in Lean relating to SMT solving, and show that the hints generated by cvc5 produce a clear improvement in existing automation's performance.

Figures (5)

• Figure 1: Overview of the querysmt tactic. Blue boxes indicate Lean stages. Yellow boxes indicate SMT stages. Stages in the green area directly transform the Lean goal and must be replayed in the final suggested proof script. Stages in the purple area do not transform the goal and therefore do not need to be replayed. Red dotted lines indicate information transfer between stages.
• Figure 2: A proof script suggested by querysmt. In this example, the skolemizeAll call produces (sk0 : Int) and (sk1 : Int $\rightarrow$ Int) from h2 and negGoal respectively.
• Figure 3: A simplified version of the proof script shown in \ref{['fig:proof-script-example']}.
• Figure 4: A proof script suggested by querysmt showcasing how Lean analogues for SMT-LIB's selector functions are constructed. Only one of the selector functions for lists is reproduced in the proof script because the other selector function (which retrieves the tail of a nonempty list) is not needed for the proof duper finds.
• Figure 5: Descriptions of SMT-related methods

Theorems & Definitions (3)

• definition thmcounterdefinition
• theorem thmcountertheorem
• corollary thmcountercorollary