Large language models~(LLMs) present an intriguing avenue of exploration in
the domain of formal theorem proving. Nonetheless, the full utilization of
these models, particularly in terms of demonstration formatting and
organization, remains an underexplored area. In an endeavor to enhance the
efficacy of LLMs, we introduce a subgoal-based demonstration learning
framework, consisting of two primary elements: Firstly, drawing upon the
insights of subgoal learning from the domains of reinforcement learning and
robotics, we propose the construction of distinct subgoals for each
demonstration example and refine these subgoals in accordance with the
pertinent theories of subgoal learning. Secondly, we build upon recent advances
in diffusion models to predict the optimal organization, simultaneously
addressing two intricate issues that persist within the domain of demonstration
organization: subset selection and order determination. Through the integration
of subgoal-based learning methodologies, we have successfully increased the
prevailing proof accuracy from 38.9\% to 44.3\% on the miniF2F benchmark.
Furthermore, the adoption of diffusion models for demonstration organization
can lead to an additional enhancement in accuracy to 45.5\%, or a $5\times$
improvement in sampling efficiency compared with the long-standing
state-of-the-art method. Our code is available at
https://github.com/HKUNLP/subgoal-theorem-prover.

本文介绍了一个基于小目标的证明学习框架和扩散模型，成功地将证明的正确率从 38.9％提高到 45.5％，或者比长期的最先进方法提高了 5 倍的采样效率。