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

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

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.