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.