An In-Context Learning Agent for Formal Theorem-Proving
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916350060920832 |
|---|---|
| author | Thakur, Amitayush Tsoukalas, George Wen, Yeming Xin, Jimmy Chaudhuri, Swarat |
| author_facet | Thakur, Amitayush Tsoukalas, George Wen, Yeming Xin, Jimmy Chaudhuri, Swarat |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_04353 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | An In-Context Learning Agent for Formal Theorem-Proving Thakur, Amitayush Tsoukalas, George Wen, Yeming Xin, Jimmy Chaudhuri, Swarat Machine Learning Artificial Intelligence Logic in Computer Science Programming Languages 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. |
| title | An In-Context Learning Agent for Formal Theorem-Proving |
| topic | Machine Learning Artificial Intelligence Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2310.04353 |