An In-Context Learning Agent for Formal Theorem-Proving
This work addresses the problem of automating formal theorem-proving for researchers and developers in proof assistants, representing a novel method rather than an incremental improvement.
The paper tackles automated theorem-proving in formal environments like Lean and Coq by introducing COPRA, an in-context learning agent that uses a large language model (GPT-4) in a backtracking search with feedback loops, achieving significant performance improvements over few-shot GPT-4 and outperforming the state-of-the-art finetuned method ReProver on the pass@1 metric in benchmarks such as miniF2F and CompCert tasks.
We present an in-context learning agent for formal theorem-proving in environments like Lean and Coq. Current state-of-the-art models for the problem are finetuned on environment-specific proof data. By contrast, our approach, called COPRA, repeatedly asks a high-capacity, general-purpose large language model (GPT-4) to propose tactic applications from within a stateful backtracking search. Proposed tactics are executed in the underlying proof environment. Feedback from the execution is used to build the prompt for the next model query, along with selected information from the search history and lemmas retrieved from an external database. We evaluate our implementation of COPRA on the miniF2F benchmark for Lean and a set of Coq tasks from the CompCert project. On these benchmarks, COPRA significantly outperforms few-shot invocations of GPT-4. It also compares favorably against finetuning-based approaches, outperforming ReProver, a state-of-the-art finetuned approach for Lean, in terms of the pass@1 metric. Our code and data are available at https://github.com/trishullab/copra.