Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal
  Theorem Proving
Xueliang Zhao Wenda Li Lingpeng Kong
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
\url{https://github.com/HKUNLP/subgoal-theorem-prover}.