Abstract

Interactive theorem proving is a complex process that often requires significant expertise, user intervention and deep domain knowledge, making it challenging for users to construct valid proofs. The HOL4 theorem prover, while a powerful tool in formal verification, presents usability challenges due to the intricate nature of proofs and the cognitive load placed on users. This thesis proposes an innovative solution to enhance the accessibility and efficiency of interactive theorem proving through the development of an AI-driven Proof Recommendation System that leverages Large Language Models. The proposed methodology focuses on two primary tasks: proof step recommendation and complete proof generation. For the proof step recommendation, models such as BERT, RoBERTa, and T5 were fine-tuned on datasets derived from HOL4 theories to predict the next logical step(s) in the proof construction. This capability aims to guide users through the proof process, making it less daunting and more manageable, especially for those with a limited experience. In the proof generation task, sequence-to-sequence models, including MarianMT and T5, were utilized to generate complete proof sequences based on the given theorem statements. This task is particularly challenging due to a need to capture complex logical patterns and ensure the validity of the generated proofs. The training involved rigorous hyper-parameter tuning and evaluation to optimize the performance of models. Experimental results demonstrate that our proposed approach not only reduces the cognitive load on theorem provers but also enhances the efficiency and accessibility of interactive theorem proving compared to related work. The tool, called HOL4PRS, achieves significant accuracy in recommending proof steps and generating proof sequences, facilitating more widespread adoption of HOL4 in critical verification tasks across various industries. This thesis contributes to the field by showcasing how integrating AI into formal verification processes can significantly advance the capabilities and applications of the interactive theorem provers.