一句话总结

René Thiemann 的章节考察并对比了两种主要方法：认证和验证，用于将自动演绎工具（如定理证明器、SAT/SMT 求解器和终止分析器）与证明助手集成，并回顾了这些方法的若干成功应用。

核心贡献

• 该章节回顾并比较了用于连接自动演绎工具（SAT、SMT、终止分析器）与证明助手的认证和验证方法。
• 经过验证的认证器已检测到演绎工具实现中多年未被发现的错误，并且现在它们被用于验证工具竞赛中大量自动生成的证明。
• 核心演绎技术的形式化验证已纠正了已发布证明中的错误，并使扩展的安全探索成为可能，而且一个经过验证的 SAT 求解器（IsaSAT）在 EDA-Challenge 2021 中优于未经验证的竞争对手。

引言

作者考察了证明助手与自动演绎工具（如 SAT、SMT 和终止分析器）之间的相互作用。可靠的自动化对于验证复杂属性至关重要，但手动认证这些工具的输出容易出错、效率低下，并且无法扩展到玩具示例之外。作者展示了证明助手如何形式化验证演绎工具所依赖的推理规则和终止排序，以词典序路径排序（LPO）和带状态递归路径排序（RPO）作为贯穿示例。这种形式化处理不仅提高了自动推理器的可信度（经过验证的认证器已发现长期隐藏的错误），还使开发者能够安全地修改或扩展核心推理规则，而无需担心引入错误。

方法

作者提出认证作为一种方法，用于验证来自不可靠的演绎工具的结果。为了满足高可靠性的需求，他们利用拥有小型可信代码库的证明助手。该方法允许对所用技术的正确性及其应用的正确性进行形式化验证。

一种主要工作流程是通过证明脚本生成进行认证。如下图：

该过程包含三个主要步骤。首先，作者开发一个库，将领域特定的概念和定理（如强规范化和项重写）形式化，其中不包含具体输入。其次，证明脚本生成器将给定的输入证书转换为证明助手的证明脚本。该脚本定义感兴趣的属性，并通过编码证书的证明来提供形式化证明。第三，证明助手检查该脚本。生成器可以以不同方式处理证书：可以将扩展证书中的推理树转换为引入规则，从基本证书重建树，或调用定制的策略。此外，还可以使用深层嵌入在证明助手内实现一个经过验证的算法，以确保排序关系 $\succ_r$≻r​ 对所有规则成立。

然而，由于运行证明助手的开销，证明脚本生成可能会很慢。为解决这一问题，作者引入了另一种工作流程：外部认证。当证明脚本主要由调用提供所需属性充分准则的已验证算法构成时，该方法适用。

如下图：

在此外部认证工作流程中，最初的库开发保持不变。第二步涉及为每个支持的属性和证书类型提供已验证的算法。这些算法被证明是充分条件（例如，如果算法接受输入 $I$I 和证书 $C$C，则属性 $P(I)$P(I) 成立），并被导出为可执行程序。最后一步在输入和证书上运行该可执行程序，并使用包装器选择合适的算法。

外部认证比证明脚本方法快得多，能够在合理时间内处理更多证书，尤其适用于需要大量计算的任务。为确保效率，作者通常采用细化方法，先证明抽象算法正确，然后将其细化为具有高效数据结构的可执行版本。虽然外部认证对证明助手的变更不那么脆弱，但其可信代码库较大，因为它依赖于代码生成器和外部编译器，并且排除了某些设计决策，例如为签名创建特定数据类型。