摘要

大型语言模型（Large Language Models, LLMs）在形式化定理证明领域展现出极具前景的研究方向。然而，这些模型在演示范例的格式设计与组织结构方面的充分应用，仍是一个尚未得到深入探索的课题。为提升LLMs在该任务中的有效性，本文提出一种基于子目标（subgoal-based）的演示学习框架，包含两个核心组成部分：首先，借鉴强化学习与机器人学领域中关于子目标学习的理论洞见，我们为每个演示示例构建独立的子目标，并依据相关子目标学习理论对这些子目标进行优化与精炼；其次，我们结合扩散模型（diffusion models）的最新进展，实现对演示范例最优组织结构的预测，同时有效解决演示组织中长期存在的两个复杂问题：子集选择与顺序确定。通过融合基于子目标的学习方法，我们在miniF2F基准测试上将当前主流的证明准确率从38.9%提升至44.3%。进一步引入扩散模型进行演示组织优化，可使准确率再提升至45.5%，相较于长期占据主导地位的最先进方法，实现采样效率提升达5倍。相关代码已公开，地址为：\url{https://github.com/HKUNLP/subgoal-theorem-prover}。