AI4FM: using AI to aid automation of proof search in Formal Methods

形式化方法为软件工程带来了其他工程学科所熟悉的科学基础水平。这种方法使用规范语言与精确的含义，从而打开的可能性，证明一个设计（最终实现）满足specification.Such正式的方法已经走过了漫长的道路，因为他们的诞生，他们现在使用的应用程序更常见的安全关键系统，他们首先部署。对它们的潜力的重要认识来自于使用按钮式的、事后的方法，这些方法来自于模型检查的思想。可以被认为是自上而下的方法家族具有更大的潜在回报，但对用户来说也更具挑战性。任何事后方法都必须面对错误程序的前景-提取它们的规范可能是无益的。此外，软件开发中的大量浪费来自于当设计错误在插入之后（但可能在代码执行之前）被发现时的废弃和返工。事后和自上而下的方法都很重要：我们选择解决后者并解决其部署中的关键成本。为了证明自上而下的设计步骤是合理的，用户必须履行所谓的证明义务。这些都是小的证明，往往可以通过自动定理证明器。但是，如果它们不能自动被释放，工程师就面临着构造形式证明的不熟悉的任务。所谓的逻辑学的改进可以帮助提高定理证明器的能力。该项目旨在使用人工智能的学习技术来记录和抽象专家如何进行证明，以增加在没有（或最少）人为干预的情况下构建证明的比例。

Formal Methods bring to software engineering the level of scientific underpinning familiar in other engineering disciplines. Such methods use specification languages with precise meaning and thus open the possibility of proving that a design (ultimately the implementation) satisfies the specification.Such formal methods have come a long way since their inception and they are now used in applications far more common than the safety-critical systems where they were first deployed. Significant awareness of their potential has come from the use of push-button, post facto, methods that derive from ideas of model checking . The family of methods that can be thought of as top-down have more potential pay-off but are also more challenging for users. Any post-facto method has to face the prospect of incorrect programs - extracting their specifications can be unedifying. Furthermore, an enormous amount of the waste in software development derives from scrap and rework when design errors are discovered after their insertion (but possibly before there is even code to execute). Both post-facto and top-down approaches are important: we choose to address the latter and tackle a key cost in their deployment.In justifying a top-down step of design, the user has to discharge so-called proof obligations . These are small proofs that can often be discharged by an automatic theorem prover. But where they are not discharged automatically, an engineer is faced with the unfamiliar task of constructing a formal proof. Improvements in so-called heuristics can help increase the power of theorem provers. This project aims to use learning techniques from artificial intelligence to record and abstract how experts do proofs in order to increase the proportion of cases where proofs are constructed without (or with minimal) human intervention.