@inproceedings{he-etal-2024-bc,
    title = "{BC}-Prover: Backward Chaining Prover for Formal Theorem Proving",
    author = "He, Yuhang  and
      Zhang, Jihai  and
      Bao, Jianzhu  and
      Lin, Fangquan  and
      Yang, Cheng  and
      Qin, Bing  and
      Xu, Ruifeng  and
      Yin, Wotao",
    editor = "Al-Onaizan, Yaser  and
      Bansal, Mohit  and
      Chen, Yun-Nung",
    booktitle = "Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing",
    month = nov,
    year = "2024",
    address = "Miami, Florida, USA",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/add-emnlp-2024-awards/2024.emnlp-main.180/",
    doi = "10.18653/v1/2024.emnlp-main.180",
    pages = "3059--3077",
    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."
}