CAPS: Collaborative Architectures for Proof Search

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

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.