分解谜题：面向形式定理证明的基于子目标的演示学习
Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving
AI总结：
本文提出基于子目标的演示学习框架，通过构建和细化子目标并利用扩散模型优化演示组织，将miniF2F上的证明准确率从38.9%提升至45.5%。
摘要：
大型语言模型（LLMs）在形式定理证明领域提供了一条引人入胜的探索路径。然而，这些模型的充分利用，尤其是在演示格式和组织方式方面，仍然是一个未被充分探索的领域。为了提升LLMs的效能，我们引入了一个基于子目标的演示学习框架，该框架包含两个主要要素：首先，借鉴强化学习和机器人领域中子目标学习的见解，我们提出为每个演示示例构建不同的子目标，并根据子目标学习的相关理论对这些子目标进行细化。其次，我们基于扩散模型的最新进展来预测最优组织方式，同时解决演示组织领域中持续存在的两个复杂问题：子集选择和顺序确定。通过整合基于子目标的学习方法，我们成功地将miniF2F基准上的现有证明准确率从38.9%提高到44.3%。此外，采用扩散模型进行演示组织可以进一步将准确率提升至45.5%，或者与长期以来的最先进方法相比，采样效率提高5倍。我们的代码可在\url{https://github.com/HKUNLP/subgoal-theorem-prover}获取。
英文摘要：
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}.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
