Text

Machine learning in interactive proving

Photo: https://unsplash.com/

Developed by ClearSy, Atelier B is an industrial tool that allows for the operational use of the B Method to develop defect-free proven software (formal software). Developing in B requires to write a formal specification, a machine-language implementation and to prove that the latter refines the former.

Non-trivial projects generate thousands of proofs, of which a rough half can be automatically proved, and the rest needs to be manually demonstrated using a tool called the Interactive prover. Proving with the interactive prover requires mathematical skills, experience, and a lot of time. Moreover, modifying the system during its lifetime, even with a simple name change, often leads to “breaking all the proof”, as demonstrations need to be slightly modified to adapt to the change of hypothesis. Therefore we believe that machine learning can help engineers in some aspects of the B development, being those interactive proving or adapting proof to change of hypothesis. The interactive prover relies on automatic theorem proving but needs to be driven by a developer who builds a proof by assembling elementary bricks, addition of hypotheses, proof by contradiction, proof by cases, and calls to inductive or deductive rules (a formula A => B). Within a system, there are proofs that solve several proof obligations and it is quite easy to automatically check if a proof solves more than the proof obligation for which it was designed; nonetheless, there can be proof obligations that would be solved with a small modification of the proof and those are impossible to detect automatically. We would like to develop a module within the Interactive prover that can learn interactive theorem proving from the developer and adapt it to unsolved proofs of the system. In this respect, ClearSy can provide a system written in B, with specifications and proof, and develop solutions in Atelier B; Clearsy can also bring expertise informal development and the specificity of the interactive prover.