Enhancing Automated Theorem Proving in Coq with Specialized Large Language Models and Tree of Thoughts

Abstract

This thesis explores the enhancement of formal theorem proving through the integration of Large Language Models (LLMs) within the Coq proof assistant environment. This work developed and evaluated a fine-tuned LLM capable of generating Coq code, trained to learn the relationship between tactics and proof states. It applied a Tree of Thoughts (ToT) reasoning framework to facilitate the exploration of possible proof paths, combined with the feedback from interaction with the Coq proof assistant at each step. The evaluation was run on three models – Llemma-7b, Llemma-7b fine-tuned, and GPT-4 – across 572 proofs from the CoqGym validation dataset, using GPT-4 as the state evaluator. A* and greedy search strategies over the ToT were compared to see the relative strengths of each. The results demonstrate that the A* search strategy outperforms the greedy approach as the proof tree grows, suggesting that the strategy's exploratory nature leads to more effective proof completion over time. Additionally, the fine-tuned model performed the best on a large number of proofs, yet the results are not substantial enough to be conclusive. Moreover, though the fine-tuned model had the highest overall proof success rate, the base Llemma} model generated legal tactics more frequently than both the fine-tuned model and GPT-4. This project highlights the efficacy of combining specialized LLMs and search strategies in enhancing the performance of automated theorem-proving systems. Code available on \href{https://github.com/piercemaloney/senior-thesis}{GitHub} and dataset and models at \href{https://huggingface.co/piercemaloney}{Hugging Face}.