BC -Prover: Backward Chaining Prover for Formal Theorem Proving (2024)

Abstract: Despite the remarkable progress made by large language models in mathematical reasoning, interactive theorem proving in formal logic still remains a prominent challenge. Previous methods resort to neural models for proofstep generation and search. However, they suffer from exploring possible proofsteps empirically in a large search space. Moreover, they directly use a less rigorous informal proof for proofstep generation, neglecting the incomplete reasoning within. In this paper, we propose BC-Prover, a backward chaining framework guided by pseudo steps. Specifically, BC-Prover prioritizes pseudo steps to proofstep generation. The pseudo steps boost the proof construction in two aspects: (1) Backward Chaining that decomposes the proof into sub-goals for goal-oriented exploration. (2) Step Planning that makes a fine-grained planning to bridge the gap between informal and formal proofs. Experiments on the miniF2F benchmark show significant performance gains by our framework over the state-of-the-art approaches. Our framework is also compatible with existing provers and further improves their performance with the backward chaining technique.

## introduction recent years have seen a surge of interest in mathematical reasoning tasks, such as premise selection @xcite , autoformalization @xcite and automated theorem proving @xcite . automated theorem proving poses a significant challenge, as it requires the prover to generate validated formal proofs fully automatically in a prohibitively large search space @xcite . therefore, interactive theorem proving (itp) has emerged as an alternative method for automating theorem proving. itp figure 1 : problem example: an input example form @xcite . proof construction: a sequence of tactics updates the state interactively to prove the goal. interaction at s 0 : given the value of σ -1 , the goal is to prove the value of σ. rw fails to rewrite the proof goal with h 1 . simp fails to simplify the proof goal with existing hypotheses. the have tactic successfully proves h 3 reversely by observing the goal. it corresponds to the color sentence in the informal proof. as lean becomes prevalent due to its superiority in interactive mathematical expression, a line of work has explored using language models for programmatically interacting with lean @xcite @xcite . in this paper, we also focus on itp with lean. generally, the itp task aims at constructing a proof (a sequence of tactics) of a proof state (transformed from a theorem statement) as illustrated in figure 1 . tactics are proofsteps for updating the proof state. they must be strictly verified by the proof assistant and utilize hypotheses to achieve the proof goal. unlike conventional program languages, formal proof language adheres to rigorous mathematical logic, leaving no room for hallucination @xcite . therefore, the itp task presents a significant challenge for llms. existing research on itp mainly falls into two paradigms: task-specific finetuning and prompting. task-specific finetuning methods have shown exceptional performance @xcite . they rely on prohibitive training costs on private datasets, making it impractical in real scenarios without open-source code or models @xcite . prompting methods, on the other hand, have already proven to be a powerful copilot in real-world applications @xcite . they explore the incontext learning ability of llms to infer proofsteps @xcite . our method is also based on the prompting paradigm. to produce more reliable tactics, most prompting methods involve informal proofs prior to proof construction @xcite . the informal proofs are solutions in natural language as shown in figure 1 : proof construction. however, directly applying the informal proofs as in-context examples can mislead the llms, as there are gaps between formal and informal proofs. specifically, informal proofs are often less rigorous and tend to skip steps, making them less reliable. to the best of our knowledge, both prompting and finetuning methods focus on generating forward-chaining tactics, ignoring the backward-chaining strategy. backward chaining is an inference method described colloquially as working backward from the goal @xcite . ignoring backward chaining could trap the exploration of proofsteps. as shown in figure 1 : interaction at s 0 , in order to prove the goal, a hypothesis h 3 should be proved first instead of using existing hypotheses. in order to alleviate the above problems, we propose bc-prover, a framework to operate backwardchaining for itp in lean. specifically, given a theorem and its informal statement, our framework first derives an informal proof and pseudo steps. pseudo steps are specific proof steps further elaborated based on the informal proof, aimed at providing a reference for the formal proof. during proof construction, vanilla provers proposed in previous works generate forward-chaining tactics to interact with @xcite . instead, inspired by literature in logic reasoning @xcite , our approach performs (1) backward chaining: drawing auxiliary hypotheses about the internal reasoning. as the pseudo steps indicate intermediate steps toward the goal, we employ llms to recursively discover provable sub-goals for ultimate proof-finding. to avoid producing misleading steps, our approach performs (2) step planning: planning the next proofstep conditioned on the current state. additionally, it augments the next proofstep with retrieval lemmas and plans similar to @xcite . experiments show that bc-prover achieves a higher pass rate on the minif2f benchmark compared with several sota baselines. bc-prover can also collaborate with finetuned models to obtain substantial improvement. we summarize our contributions as follows: ## methodology a problem statement consists of a theorem statement x t and its informal statement x h . x t will be transformed into an initial proof state s 0 = {h 1 , ..., h l , g 1 , ..., g m } that holds l hypotheses h and m goals g. a problem example is illustrated in figure 1 : problem example. the itp task can be formulated as follows: given x t , x h and s 0 , a prover needs to generate tactics iteratively to construct a proof. in each iteration, the prover searches for tactics to update the state. the iterations "s 0 ⇀ s 1 ⇀ • • • " finish until all goals are accomplished or the search ends. ## experiment setup in this section, we introduce the experiment setup for bc-prover. following @xcite , we evaluate bc-prover in lean. more experimental details and hyperparameters are in appendix a. baselines. baselines of two paradigms are compared, encompassing the state-of-the-art itp provers in lean. note that we exclude some baselines that are infeasible to compare with (details in appendix a.2). for example, approaches across different proof assistants are not comparable because of different experiment settings. implementation details. in this paper, the llm is instantiated to be gpt-4-turbo-2024-04 -09. ## conclusion in this work, we propose a novel framework, bc-prover. at the beginning, bc-prover generates pseudo steps for constructing proofs. during proof construction, bc-prover operates backward chaining and step planning to construct proofs in formal logic. the backward chaining searches for proofstep in a goal-driven manner. the step planning makes a detailed planning for each proofstep to invoke more accurate tactics. the experiment results on the benchmark demonstrate the superiority of our framework. our results demonstrate that future work on itp should incorporate backward chaining to search tactics more effectively.