CAPS: Collaborative Architectures for Proof Search

数论学家、证券分析师和数据科学家有什么共同之处？他们都可以使用工具来帮助他们，这些工具的核心是由自动定理证明器驱动的。数论家可以在证明助手中描述她的问题，并调用所谓的“锤子”来尝试自动证明问题或问题的一部分。安全分析师可能会执行软件模型检查器，以确保他的代码没有与内存访问相关的某些漏洞。数据科学家可以查询语义数据库，并为查询结果生成解释。所有这些工具的工作原理都是将它们的问题转化为一系列的子问题，由一个自动定理证明器来解决。虽然自动化定理证明器长期以来一直是各种应用程序的主力，但人们对安全和可靠软件系统领域的兴趣越来越大。随着软件系统变得越来越复杂，故障的可能性也越来越大，传统方法也在努力建立它们的安全性，同样，我们的软件系统也越来越容易受到那些试图利用我们对技术的依赖来达到他们自己邪恶目的的人的攻击。这些所谓的网络攻击正变得越来越复杂，积极寻求颠覆现有的检测方法。只有消除潜在的漏洞，我们才能真正保护自己。如上所述，在检查软件系统的安全性和安全性属性的方法中，一个共同的主题是在逻辑中描述软件的各个部分和所需的属性，并使用自动定理证明器来检查该属性是否成立。因此，对这种自动定理证明技术有很强的依赖性。自动定理证明器实现了一种称为“证明搜索”的方法，该方法使用大量的启发式方法来引导证明器进行证明。启发式的集合通常被收集到策略中，人们普遍观察到，在给定的问题上，一种策略可以快速解决问题，但另一种策略可能会偏离，永远找不到解决方案。其结果是，现代定理证明者利用多种策略组合来解决难题，并希望其中一种策略表现良好。然而，就像不同的问题在不同的策略下表现不同一样，一个问题可以包含在不同策略下表现不同的子问题。理想情况下，我们会在子问题级别选择不同的策略。CAPS项目将开发一种协作并行架构，允许多个证明者实例处理同一个问题，在不同的子问题上尝试不同的策略。这应该会产生协同效应。考虑一个不能被投资组合中的任何单一策略证明的问题，但它的每个子问题都在其中。在这种情况下，一个无法证明的问题变得可以证明了。此外，这种新的体系结构为并行性提供了新的机会，这是不适合正常证明搜索结构的东西。该项目的主要交付成果是在曼彻斯特开发的广泛使用的屡获殊荣的Vampire自动定理证明器中实现的新型协作并行架构。通过使用Vampire作为这项研究的载体，我们相信我们将能够将基础研究的结果转化为实用、可用和有影响力的工具。

What do a number theorist, a security analyst, and a data scientist have in common? They all have access to tools to help them, which at their core are powered by automated theorem provers. A number theorist can phrase her problem in a proof assistant and call on a so-called `hammer' to attempt to automatically prove the problem, or some part of it. A security analyst may execute a software model checker to ensure his code lacks certain vulnerabilities related to memory access. A data scientist may query a semantic database and generate an explanation for the result of her query. All these tools work by translating their problem to a series of sub-problems to be solved by an automated theorem prover.Whilst automated theorem provers have long been the workhorse for a variety of applications, there is a growing interest in the area of safe and secure software systems. As software systems grow more complex the potential for failure grows and traditional methods struggle to establish their safety, similarly, our software systems are increasingly subject to attacks from those who seek to exploit our dependence on technology for their own nefarious purposes. These so-called cyber attacks are becoming more elaborate, actively seeking to subvert existing methods of detection. Only by removing the underlying vulnerabilities can we truly protect ourselves. As described above, a common theme among approaches for checking safety and security properties of software systems is to describe parts of the software and desired property in logic and to use an automated theorem prover to check if the property holds. Therefore, there is a strong reliance on this automated theorem proving technology. Automated theorem provers implement a method called `proof search' that uses a large array of heuristics to guide the prover towards a proof. Sets of heuristics are commonly collected together into strategies and it is widely observed that on a given problem one strategy may solve the problem quickly but another may diverge, never finding a solution. The consequence is that modern theorem provers utilise portfolios of strategies to tackle difficult problems, with the hope that one strategy will behave well. However, in the same way that different problems behave differently under different strategies, a problem can contain sub-problems that behave differently under different strategies. Ideally, we would select different strategies at the sub-problem level. The CAPS project will develop a collaborative parallel architecture that allows multiple prover instances to work on the same problem, with different strategies being tried on different sub-problems. This should have a synergistic effect. Consider a problem that is not provable by any single strategy in a portfolio but where each of its sub-problems is. In such a case, an unprovable problem becomes provable. Furthermore, this new architecture offers a new opportunity for parallelism, something that does not fit naturally into the normal structure of proof search. The main deliverable of this project is a novel collaborative parallel architecture implemented in the widely-used award-winning Vampire automated theorem prover developed in Manchester. By using Vampire as a vehicle for this research we are confident that we will be able to translate the results of fundamental research into a practical, usable and impactful tool.