LLM-SYM: Integrating Symbolic Methods and Large Language Models for Automated Theorem Proving

Interactive theorem provers (ITPs) are crucial tools in formal verification, enabling researchers to ensure software reliability and safety in critical systems. While effective, the process of writing proofs using ITPs is costly, involving repetitive tasks. Techniques for automating proofs using symbolic methods and machine learning have been proposed, but both have limitations: symbolic methods struggle with higher-order logic, while machine learning requires extensive training data. Although large language models (LLMs) are increasingly used in software engineering for tasks such as code generation, their effectiveness in theorem proving is hindered by a lack of sufficient training data and the iterative nature of proof generation. To overcome these challenges, we introduce LLM-SYM, an end-to-end framework that integrates symbolic methods with LLMs, enhancing LLMs’ theorem-proving capabilities through fine-tuning. Our approach extracts proof information from human-constructed proofs and employs symbolic methods to rewrite low-level proofs. We enhance data with tactics history and use curriculum sorting to optimize learning. We developed an interactive proof search agent to explore and verify tactics. Testing LLM-SYM on CompCert project reveals improvements over existing methods, and ablation experiments confirm the effectiveness of components within our approach.