Benchmarking Automated Theorem Proving with Large Language Models (2024)

Abstract: Theorem proving presents a significant challenge for large language models (LLMs) due to the requirement for formal proofs to be rigorously checked by proof assistants, such as Lean, eliminating any margin for error or hallucination. While existing LLM-based theorem provers attempt to operate autonomously, they often struggle with novel and complex theorems where human insights are essential. Lean Copilot is a novel framework that integrates LLM inference into the Lean proof assistant environment. In this work, we benchmark performance of several LLMs including general and math-specific models for theorem proving using the Lean Copilot framework. Our initial investigation suggests that a general-purpose large model like LLaMa-70B still has edge over math-specific smaller models for the task under consideration. We provide useful insights into the performance of different LLMs we chose for the task.

## introduction as mathematical problems become increasingly intricate, the task of formalizing and generating verifiable math proofs becomes proportionally more challenging. the translation process from informal theorems and proofs to a standardized, machineverifiable, formal language, requires much effort and expertise from human mathematicians, creating a steep learning curve. this challenge has raised great interest in the potential of using ai to aid in the math formalization process, and more generally in automated theorem proving(atp). the integration of ai, specifically large language models(llms), in math formalization and theorem proving can not only accelerate the proof discovery process, but can also enhance the reliability and rigor of mathematical arguments by minimizing human error. while the ultimate goal may be to achieve fully autonomous proof generation without human as-sistance, current atp systems based on language models struggle when dealing with more complex proof problems. typically, these language models employed for theorem proving come from larger base models like bert and gpt, then finetuned on large amounts of mathematical text data such as @xcite . this limitation seen likely stems from the models' lack of flexibility when encountering mathematical areas not adequately covered by their training data. to address this inflexibility with autonomous proof generation, there are interactive theorem proving (itp) systems where proof assistants-software frameworks built for math formalization like coq, isabelle, and lean-are used in conjunction with human mathematicians in the proving process. this integration allows for the aid of proof automation tools with human intuition. the use of itp system proof assistants has become increasingly prevalent for ensuring a level of rigor and standard in formalizing mathematical language. lean is one such popular proof assistant as well as functional programming language for formalizing mathematics that supports itp by offering a framework for writing and verifying proofs. lean uses tactic style proving where proofs are generated step by step using tactics, or instructions used to manipulate the current state of a proof to the next state. from the start of a proof, users will continue the proof using the appropriate tactic based on the user's knowledge of the math problem and tactics. while a powerful proof assistant for mathematicians, it still requires a great deal of effort to find the ideal tactics. this is a common barrier across all itp systems; thus, the integration of large language models (llms) with proof assistants was introduced to offer intuitive, automated assistance in generating and verifying mathematical proofs. llms can automate tedious aspects of proof writing, such as identifying relevant lemmas and theorems and drawing from extensive math-ematical training data to uncover overlooked but crucial insights. however, despite the potential of llms, existing llm-based provers cannot assist humans in an interactive, seamless manner. current llmbased systems are typically trained and evaluated following machine learning standards that rely on extracted datasets from an itp's codebase rather than within the proof assistant itself. this disconnection results in models that, while effective in a controlled environment, are difficult to integrate into the practical workflows of proof assistants. this gap between llm training environments and proof assistant usage highlights a critical need for systems to bridge the two and enable more effective human-ai collaboration in theorem proving. recently, the effort to combine proof assistant, lean, with llms was achieved through a new framework leancopilot. leancopilot is an opensource framework that supports users to bring in pre-trained llms and use/build llm-based proof automation tools natively in lean @xcite . this makes llm-based proof automation available in lean and increasing accessibility in math formalization. it is based on leandojo's reprover algorithm for tactic generation and can be brought in as a package in lean through an ide of choice @xcite . it is able to run llms on most laptops without the need for gpus, a feature that increases accessibility for llm-based proof automation. while users can create their own tools, leancopilot also comes with a suite of built in proof automation tools. these tools were built using ctranslate2's c++ library for efficient llm inference with transformer models, running it via lean's foreign function interface(ffi). a more comprehensive review of these tools can be found in following sections: the performance of llms for theorem proving tasks can vary widely depending on the complexity of the proofs and the model architecture. recent research has demonstrated that while llms can effectively automate portions of proof generation, their success is highly contingent on the difficulty of the mathematical problems being tackled and the specific design of the model @xcite . this variability in performance motivates our work to benchmark llms specifically in the context of itp, as understanding these models' strengths and weaknesses is crucial for improving their utility in automating mathematical proof generation. in our research, we utilize leancopilot's ability to bring in llms to evaluate the performance of various llms for theorem proving. llms are commonly benchmarked for theorem proving by testing how many theorems they can generate proofs for. we evaluate the performance of llms trained for math tasks, pythia2.8b, llemma7b, leanstarplus7b, leanstarcot7b, against general llms, llama3-70b and byt5. we replicate the experiments used to evaluate leancopilot's builtin proof automation tools but instead to benchmark llms for proof generation. we evaluate the performance of these different llms for itp using leancopilot's built-in proof automation tool, suggest_tactics. this benchmarking will allow us to evaluate how different llms perform in assisting with theorem proving tasks across a selection of proof problems sourced from the mathematics in lean textbook. by systematically evaluating different llms, we aim to identify key factors that contribute to successful proof generation and highlight areas where further advancements are needed. ## related works the roots of itp lie in the broader field of automated reasoning, which emerged as a distinct area of study in the mid-20th century. while atp systems aimed to fully automate the process of deriving proofs, early researchers recognized the limitations of these systems, particularly in handling complex, domain-specific proofs that required a deeper level of human intuition and insight. the inception of itp was driven by the need to integrate human expertise into the proof construction process, allowing for a relationship between automated tools and human mathematicians. one of the earliest milestones in this direction was the development of the lcf (logic for computable functions) theorem prover by robin milner in the 1970s @xcite . lcf introduced a novel approach that combined a small trusted kernel, which ensured the soundness of proofs, with a flexible and extensible user interface that allowed human interaction. the lcf approach set a precedent for future itp systems by emphasizing the importance of human oversight in the verification process. the 1980s and 1990s saw the emergence of some of the most influential itp systems, notably coq and isabelle. these systems were built on the foundational ideas of the lcf approach but introduced significant innovations that expanded the scope and applicability of itp. coq, developed by thierry coquand and gérard huet, was based on the calculus of inductive constructions (cic), a powerful type theory that enabled the formalization of a wide range of mathematical concepts @xcite ). coq's ability to handle inductive types and support constructive mathematics made it a versatile tool for both theorem proving and the extraction of certified programs. coq's interactive environment allowed mathematicians to build proofs incrementally by using a rich set of tactics to guide the proof process while relying on the underlying formalism to ensure correctness. isabelle, developed by lawrence paulson, took a different approach by providing a generic framework that could support multiple logics @xcite ). isabelle's most notable contribution was its use of higher-order logic (hol), which allowed for the formalization of more complex mathematical structures and proofs. isabelle's architecture was designed to be highly modular, enabling users to extend the system with custom proof strategies and tactics. this flexibility made isabelle particularly popular in both academia and industry for formal verification tasks. as itp systems matured, the focus shifted towards enhancing their automation capabilities while preserving the essential role of human interaction. the concept of proof tactics, first introduced in lcf, became central to this effort. tactics are commands that automate common proof steps, allowing users to delegate routine tasks to the computer prover while focusing on more challenging aspects of the proof. these developments set the stage for the creation and release of lean, a modern proof assistant developed by leonardo de moura and his team at microsoft research (moura and ullrich, 2021). first released in 2013, lean was designed with a focus on combining expressive power, automation, and user-friendly interaction. it builds on ideas from earlier systems but introduces several unique features that distinguish it in the landscape of itp tools. lean is based on a version of dependent type theory, similar to coq, but it emphasizes a more unified approach to proof automation and user interaction. this is exemplified by lean's tactic framework, which allows users to construct proofs incrementally by applying tactics-commands that automate specific proof steps. lean's programming framework also enables users to write custom tactics in the lean language itself, making it highly extensible and adaptable to different domains of mathematics and computer science. lean's integration of a tactic language is an evolution of the earlier lcf and coq systems, which introduced tactics as a means of automating common proof steps. lean's tactic framework has been further enhanced to support more sophisticated proof strategies, making it an effective tool for both novice users and expert mathematicians. this combination of user interaction and automation makes lean a useful tool in the formalization of mathematics and the verification of complex systems, enabling better integration of human expertise with automated proof checking. ## methodology this section outlines our approach for benchmarking the capabilities of different llms, both mathspecific and general llms, in assisting with theorem proving using leancopilot. we replicate the benchmarking experiments used to evaluate the proof-automation tools in leancopilot, but instead to benchmark different llms for proof generation. in their experiments the authors @xcite ) evaluated leancopilot's suggest_tactics and search_proof against preexisting lean proof automation tool aesop. currently, leancopilot doesn't support bringing in different llms for their tools search_proof and select_premise, thus we will only benchmark using suggest_tactics. we benchmark the following llms: ## datasets on which the llms under consideration were trained in this section, we discuss the datasets on which the models were trained to get an idea of their internal knowledge base. ## results & discussion in this section, we will detail the results of our experiments with the mathematics in lean textbook problems. fifty (50) proof problems were randomly selected from the textbook for our experiments. as a reminder, for suggest_tactics, since the list of tactics are ranked from most likely to complete proof to least likely, we select the first tactic in the list of generated tactics as our input to the proof. in the following figures, we exemplify the solution with one problem from the textbook. this example problem is to prove the product of an even number with any natural number will be an even number. this problem is straightforward for most with a math background, thus is a good example to understand the results produced by different models. we observe similar behaviour with our selected test-set. ## observations our findings highlight the capabilities and diversity of modern language models in generating proofs within the lean proof assistant environment. all models showcased capabilities for proof generation, but as can be seen by leancotplus7b, leanstarplus7b, and llama3-70b in our qualitative exmaple, some models have difficulty with just tactic generation as opposed to proof generation. additionally, the tendency of some models, such as byt5, to rely heavily on broad automation tactics like simp_all can obscure the underlying reasoning processes and limit interpretability. interestingly, while llemma7b produced very intuitive results in our example problem, in our experiments, it was the only model that lagged behind in both autonomous proof and tactic generation. these results highlight the need for future research to develop models that strike a better balance between automation and mathematical transparency. ## conclusions in this study, we explored the integration of large language models (llms) with interactive theorem proving (itp) systems, specifically focusing on lean and the lean copilot framework. our experiments aimed to assess the effectiveness of various llms in generating and automating mathematical proofs, highlighting both the potential and limitations of current technologies. our results demonstrated that different llms exhibit varied capabilities in assisting with theorem proving tasks. as shown in our qualitative example, most models appeared to rely heavily on automation, generating long lists of tactics and/or employing tactics which were vague in mathematical reasoning. our future work would focus on benchmarking advanced models on complex theorems, developing models that enhance both automation and transparency, enabling more robust and accessible proof generation tools. our research reinforces the promise of integrating ai with formal proof systems while highlighting areas for continued development.