DeepIsaHOL · Reinforcement learning to improve proof-automation in theorem proving

Reinforcement learning to improve proof-automation in theorem proving

Context: Interactive theorem provers (ITPs), or proof assistants, are tools that aid in the mechanical validation of mathematical proofs. Due to their high reliability, researchers and engineers use them to develop safe and secure software/hardware or to certify complex mathematical results. Companies like Amazon, Apple, and ARM use ITPs to verify safety-critical systems. The DeepIsaHOL project was set with the long-term goal of improving the efficiency and accessibility of deductive verification methods using ITPs. In particular, the project focuses on the Isabelle proof assistant. The central challenge motivating the project was that while ITPs provide high reliability for developing safe and secure software/hardware and for certifying complex mathematical results, deductive verification is currently slow and costly compared to less reliable quality assurance methods like testing, simulation, or model checking. The premise was that the lack of robust, generic proof-automation methods within ITPs acts as a barrier to wider adoption. This affects both commercial entities and the broader mathematical community. Developing generic automation would accelerate the verification process, making it more cost-effective and enabling greater industrial and academic adoption. Overall objectives: The main objective of the project was to address the above lack of generic proof-automation methods within ITPs by training a machine learning algorithm to learn proof strategies embedded in a vast ITP library, thereby creating a generic method to automate the Isabelle proving process. The plan consisted of achieving three concrete research objectives: 1. Training a machine learning model that suggests proof methods given an ITP proof state. The training data consisted primarily of data extracted from Isabelle’s Archive of Formal Proofs (AFP), which contains over 298,700 theorems. 2. Creating a proof method in the ITP that seamlessly integrates the model's suggestions into Isabelle. This is the first proof method based solely on a machine-learning model integrated into Isabelle that completes mechanised proofs. 3. Measuring the model's performance on various benchmark problems and comparing it directly to established, powerful methods like Isabelle’s Sledgehammer tool. Pathway to impact: The project was highly interdisciplinary as it combined machine learning (ML) and formal methods, two relatively distant areas of computer science. It was innovative because it resulted in the first machine learning based proof method fully integrated into the Isabelle proof assistant. The project’s expected impacts are significant and multi-faceted, reaching scientific, societal, and economic domains: - Scientific & AITP Community: The training algorithms for the project's models are expected to serve as an extensible basis for other researchers and represent a new data point showcasing the generality of machine learning for theorem proving while also exposing its limitations. The project's evaluation algorithms can also serve as a basis for testing the ITP's proof methods. - Verification Community (Engineering/Industry): The project's generated proof methods are the basis for integrating more powerful machine learning methods into the verification community. It is expected that the final result evolving from these kinds of proof methods will serve as a frequently used tool for creating safe and secure software or hardware. This is particularly relevant for the formal verification of safety-critical systems, such as those involving cyber-physical systems. In time, tech companies that employ proof engineers are expected to see a corresponding increase in productivity. - Mathematical Community: The project is a step towards accelerating the certification of new mathematical results. If future machine learning based proof methods can prove 30% of the project's benchmark, they are likely to be adopted by most users, including many future mathematicians. - Broader impact: Overall, the project was a stepping stone in the widespread adoption of formal proofs, which is a significant opportunity to democratise science. Formal proofs enable anyone, regardless of their gender, race, religion, or age, to participate equally and indisputably in scientific endeavours.

Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз