达夫尼证明中不强壮的根源是什么？

如何解决达夫尼证明中不强壮的根源是什么？

我偶尔（不是很频繁，但足够频繁）看到一个证明将在Dafny中运行，然后看起来无关紧要的东西会发生变化（例如，与该证明无关的变量名，函数定义，等等），则证明会失效。

我有兴趣了解发生这种情况的技术原因。我目前对E匹配和量词实例化有一个大概的了解。对我来说，这些算法对于这些看似无关的输入功能应该具有鲁棒性，这并不是显而易见的。他们为什么不会变得强大也不明显。我也不知道在实践中是否有任何E匹配实现的考虑会导致鲁棒性。

“健壮”的意思是“要么总是成功，要么总是不成功，与变量名之类的因素无关”。

因此，我有兴趣了解这种非鲁棒性的技术原因（无论是实际的还是理论的）。

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

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

解决方法

这些问题中没有一个简单的答案。下面，我将总结我对z3的经验。尽管达夫尼（Dafny）的人可能会提供其他建议，但我可能会猜测它适用于现有的所有此类（半）自动证明工具。

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

当您使用Dafny / Boogie等时，它们会在您的程序上执行大量转换，甚至简单的更改也可能导致后端求解器表现出截然不同的行为。 （请注意，sat永远不会变成unsat，反之亦然：那将是一个合法的错误。但是事情可能会变成unknown，或花费很多时间。）这是另一个{{3} }讨论类似现象。

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

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

因此，作为一名从业者，您实际上无能为力。不幸。特别是如果您在z3上使用诸如Dafny / Boogie之类的工具，它会增加自己的魔力。一个简单的想法就是使用您的许多核心：使用不同的种子，启发式方法，策略等，在您的许多核心上启动求解器的许多实例，并选择最快的结果。当然，这说起来容易做起来难。

总而言之，这些求解器/系统大多数都是黑盒。即使您对它们的内部知识了解很多，也很难始终“稳健”地使用它们。实际上，能够做到这一点可能值得获得博士学位。级别的学位论文工作，如果您能够提出一种不受此类差异影响的求解器/证明系统。

作为最终用户，并假设您使用的是SMTLib，您应该了解一些“常见”的技巧和陷阱，这些技巧和陷阱可有助于创建性能更好的模型。概述，请参见thread。

但是也没有必要绝望。情况越来越好，今天的求解器的性能要比去年提高很多倍。 this answer结果是跟踪进度的好方法。

祝你好运！