Reproduce “An In-Context Learning Agent for Formal Theorem-Proving” on OpenResearch

About this paper

Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, Swarat Chaudhuri

COPRA, an in-context learning agent, leverages a general-purpose large language model (GPT-4) to perform formal theorem-proving in Lean and Coq. It achieves competitive or superior performance against finetuned state-of-the-art models on challenging benchmarks like miniF2F and CompCert, proving 29.92% of miniF2F-test problems within 60 queries without environment-specific training.

Key insights

• In-context learning with a high-capacity, general-purpose LLM can effectively guide formal proof search, achieving performance competitive with or exceeding finetuned models without specialized training.
• A structured agent architecture that combines stateful search, dynamic interaction with the proof environment, execution feedback, and knowledge retrieval is critical for harnessing LLMs for complex, multi-step reasoning tasks.
• The scale and capabilities of the underlying LLM (e.g., GPT-4) are crucial for robust performance, though the agent framework itself improves the efficacy of weaker LLMs.

Summary by alphaXiv.