Interactive theorem provers have emerged as powerful tools for formal verification, aiding in the rigorous verification of mathematical proofs and software correctness. However, the process of constructing and manipulating proofs within these systems can be complex and laborintensive, often requiring significant expertise and time investment. In this work, we explore the integration of deep learning techniques to assist users of interactive theorem provers by recommending proof steps, aiming to enhance their productivity and efficiency. We develop a tailored tool designed to assist users of the HOL4 theorem prover, providing expert recommendations on the best tactics to employ based on the current state of a proof using a transformer-based model.

Publications

Conference Papers

[1] Nour Dekhil, Adnan Rashid, and Sofiène Tahar. HOL4PRS: Proof Recommendation System for the HOL4 Theorem Prover. in A. Kohlhase and L. Kovács (Eds.): Intelligent Computer Mathematics, Lecture Notes in Computer Science 14960, Springer Verlag, 2024, pp. 352-359. [Proc. Conference on Intelligent Computer Mathematics (CICM24), Montreal, Canada, August 2024].

[2] Nour Dekhil, Adnan Rashid, and Sofiène Tahar. Proof Recommendation System for the HOL4 Theorem Prover. Proc. Conference on Artificial Intelligence and Theorem Proving (AITP 24), Aussois, France, September 2024, (To Appear).

Source Code

Github Repository : HOL4PRS: Proof Recommendation System for the HOL4 Theorem Prover