LLM-Enhanced Theorem Proving with Term Explanation and Tactic Parameter Repair✱
Xingpeng Liu, Hengzhu Liu, Xiaodong Yi, Ji Wang · 2024
There has been emerging researches on leveraging large language models (LLMs) to improve the automation of theorem proving. However, they are still suffering from low accuracy and efficiency. In this paper, we propose to strengthen the existing approach by enhancing a language agent, which provides automatic explanation of terms and repair of tactics parameters. Term explanation explains terms specific to the proof obligations formally and tactic parameter repair complements the potentially correct proof tactics as much as possible. Similar to the existing approach, the agent uses GPT-4 as query objects in a search policy. During the search, we add term explanation to the prompt, and then the policy selects a proof tactic and repairs it. The repaired tactics interact with the theorem prover (Coq), and the execution result is fed back to build the prompt for the next policy invocation. We evaluate our approach on subsets of the CompCert project implemented using Coq. Our approach proves 8.11% more theorems than the existing language agent COPRA, and demonstrates faster search and proof speed. Besides, when term explanation and tactic parameter repair are applied, the performance of the SOTA method PROVERBOT9001 can be also improved.