Dafny 证明中非鲁棒性的来源是什么？

Question

我偶尔（不经常，但经常）看到证明会在 Dafny 中工作，然后看起来不相关的东西会改变（例如，与证明不相关的变量名、函数定义、等等），证明就会失效。

我很想知道发生这种情况的技术原因。我目前对电子匹配和量词实例化有一个粗略的了解。对我来说，这些算法应该对这些看似不相关的输入特征具有鲁棒性并不明显；它们不会健壮的原因也不是很明显。我也不知道在实践中是否有任何关于 E-matching 实现的注意事项会导致不鲁棒性。

“健壮”是指“要么总是成功，要么总是不成功，与变量名等因素无关”。

所以，我有兴趣了解这种不稳健的技术原因（无论是实际的还是理论上的）。

我想在这里获得更多直觉的部分原因是，当我遇到这种情况时，我可以修补证明以使其更健壮。 （相反，现在通常发生的情况是我会以某种任意方式修补证明，它会得到修复，然后它会再次中断。）

我希望找到的答案类似于“Z3 使用算法 X，它使用复杂的启发式 Y 来确定何时放弃在搜索空间的一部分中查找，很明显 Y 取决于搜索顺序”。这样的答案可能不会帮助我写出更好的 Dafny 证明，但它会满足我的好奇心。

Answer 1

这些问题都没有简单的答案。下面，我将总结一下我使用z3的经验。虽然 Dafny 的人可能会提供其他建议，但我会大胆猜测它适用于现有的所有此类（半）自动化证明工具。

众所周知，即使更改变量名也会使 z3 响应 sat 或 unknown，请参阅此 thread 进行讨论。

当您使用 Dafny/Boogie 等时，它们会对您的程序执行大量转换，即使是简单的更改也会导致后端求解器表现出截然不同的行为。 （请注意，sat 永远不应该变成 unsat，反之亦然：这将是一个合法的错误。但事情可能会变成 unknown，或者需要大不相同的时间。）这是另一个 thread 讨论类似现象。

根本原因总是要追溯到 z3 用于解决问题的随机种子、选择的启发式方法以及大量可能影响搜索过程的设置。在您的终端上运行z3 -pd。截至今天，您可以调整 500 多个“参数”！尝试所有相关选项几乎是不可能的，更不用说选择“正确”的设置了。有研究在动态“修改”参数以选择性能最佳的集合用于回归目的，但这通常无济于事，因为问题和求解器不断变化。

您甚至可以通过改变 z3 参数 smt.random_seed=N 在完全相同的问题上获得不同的性能。对于 N 的不同值，性能可能会有所不同。

所以，作为一个从业者，你真的无能为力；很遗憾。特别是如果您在 z3 之上使用像 Dafny/Boogie 这样的工具，它会增加自己的魔力。一个简单的想法是使用您的多个核心：在您的许多核心上使用不同的种子、启发式、策略等启动求解器的多个实例，然后选择最快的结果。当然，说起来容易做起来难。

总而言之，这些求解器/系统中的大多数都作为黑盒工作。即使您对它们的内部结构了解很多，也很难始终“稳健地”使用它们。事实上，能够做到这一点，恐怕就配得上一个博士学位。水平论文工作，如果您能够提出一个不受此类差异影响的求解器/证明系统。

作为最终用户，假设您使用的是 SMTLib，那么您应该注意一组“常见”技巧和陷阱，它们有助于创建性能更好的模型。有关概述，请参阅 this answer。

但也没有必要绝望。情况正在好转，与过去相比，今天的求解器性能提高了许多倍。 SMT-competition 结果是跟踪进度的好方法。

祝你好运！