对编程任务的定理证明者进行基准测试:YICES与Z3

2020-11-09 16:00:51

大多数程序员应该知道的一个巧妙的工具家族是“定理证明器”。如果你读的是计算机专业的大学,你可能已经接触到了…。但在编程时,您可能不会考虑使用它们。

虽然我确信它们可以用来证明定理,但我从来没有用过它们来证明定理。它们对于快速检验一些假设和找到有用的常数很有用。让我举一个简单的例子。

我们知道软件中的无符号奇数有乘法逆数。也就是说,如果给你一个数字3,你可以找到另一个数字,这样当你把它与3相乘时,你就会得到1。有一些高效的算法可以找到这样的乘法逆,但定理证明者可以在没有任何麻烦或领域知识的情况下做到这一点。您可以编写以下Python程序:

它的回报率将达到12297829382473034411。作为64位无符号整数,如果你用12297829382473034411乘以3,你会得到1。如果没有可能的解,定理证明者也会告诉你。所以它可以找到有用的常量,或者证明找不到常量。

对于一些相关的任务,我一直在使用流行的Z3定理证明器,它对我非常有用。但它有时可能会很慢。所以我向Geoff Langdale请教,他推荐了yices,另一种定理证明器,对于程序员所做的那种工作来说可能更快,例如,使用固定位整数值。

虽然我信任杰夫,但我想得出一些衡量标准。因此,我构建了以下基准。对于0到1000之间的所有整数,我尝试找一个乘法逆数。它并不总是有效的(即使数字没有倒数),但定理证明者将会弄清楚这一点。

所以,至少在这一次测试中,yices的速度是z3的15倍。我的Python脚本可用。您可以使用标准的pip工具安装z3和yices。请注意,您的系统上应该有yices,但作者提供了简单的说明。

我发现与Z3相比,yices的Python接口相当麻烦。因此,如果性能不是问题,Z3可能会为您提供很好的服务。

但为什么要提到业绩呢?回到上面的数字。要在15秒内解决1000个反问题,按每个数字计算真的是相当慢的。它大约是每个数字6000万个CPU周期。这是一个很容易解决的问题。当你开始提出更复杂的问题时,定理证明者可能很快就会变得无法使用。能够只快10倍的速度在实践中会产生很大的不同。

警告:这只是一次测试,它不能以任何方式确定YICS相对于Z3的优势(总体上)。