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.

翻译：整合交互式定理证明器与自动化定理证明器存在多种范式，旨在将强大自动化的便利性与严格可靠性保证相结合。我们提出一种重构SMT求解器所发现证明的新方法，该方法旨在与现有技术形成互补。我们既不验证或重放SMT求解器生成的完整证明，也不仅凭求解器使用的前提集合重新发现其证明（这两种极端方式），而是探索一种通过利用求解过程中推导的事实（我们称之为提示）来引导交互式定理证明器内部自动化的方法。这使得从SMT求解器证明中提取更多信息成为可能，同时无需承担依赖SMT求解器本身带来的开销。我们在Lean证明助手中实现了一个名为QuerySMT的策略，该策略利用cvc5 SMT求解器生成的提示来改进Lean现有自动化能力。我们在相关Lean基准测试中评估QuerySMT的性能，将其与Lean中其他涉及SMT求解的工具进行比较，并证明cvc5生成的提示能显著提升现有自动化系统的性能表现。