Collaborative Theorem Proving with Large Language Models: Enhancing Formal Proofs with ProofRefiner

Authors: Haoyi Zhang, Andrew Liu, Zixuan Wang, Feiyang Wang
Primary area: transfer learning, meta learning, and lifelong learning
Keywords: agent-base system, reasoning

Abstract:
Abstract： Theorem proving presents a significant challenge for large language models (LLMs) because formal proofs can be rigorously verified by proof assistants like Lean, leaving no room for errors. Existing LLM-based provers typically operate autonomously, but they often struggle with complex and novel theorems where human insights are crucial. We propose a new framework that positions LLMs as collaborative assistants in theorem proving to address this. This framework enables the seamless integration of LLM inference into the Lean environment, allowing developers to build various proof automation tools. These tools offer features such as suggesting proof steps, completing intermediate goals, and selecting relevant premises, thereby enhancing the theorem-proving process. Users can leverage our pretrained models or integrate their own, supporting local and cloud-based execution. Experimental results demonstrate that our approach is more effective in aiding humans and automating the theorem-proving process than existing rule-based systems. Additionally, we introduce a system called ProofRefiner, which refines questions and answers through dynamic dialogue adjustments to ensure relevance and precision.

Decision: desk rejected
Reviewer scores: 0

Reviews and discussion:

Metareview: