BC-Prover: Backward Chaining Prover for Formal Theorem Proving
Yuhang He, Jihai Zhang, Jianzhu Bao, Fangquan Lin, Cheng Hong Yang, Bing Heng Qin, Ruifeng Xu, Wotao Yin · 2024
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.Besides, 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 goaloriented 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.