SubgoalXL：基于子目标的专家学习在定理证明中的应用

形式定理证明是数学与计算机科学交叉领域的研究方向，随着大规模语言模型（LLMs）的发展，这一领域重新引起了广泛关注。本文介绍了SubgoalXL，这是一种创新的方法，通过结合基于子目标的证明与专家学习，以增强LLMs在Isabelle环境中的形式定理证明能力。SubgoalXL解决了两个关键挑战：专门的数学和定理证明数据稀缺，以及LLMs需要改进的多步推理能力。通过优化数据效率并采用子目标级别的监督，SubgoalXL从有限的人工生成证明中提取了更丰富的信息。该框架集成了面向子目标的证明策略与专家学习系统，迭代地改进形式陈述、证明和子目标生成器。利用Isabelle环境在基于子目标的证明中的优势，SubgoalXL在标准miniF2F数据集上实现了56.1%的新最先进性能，绝对提升了4.9%。值得注意的是，SubgoalXL成功解决了miniF2F中的41道AMC12题目、9道AIME题目和3道IMO题目。这些结果强调了最大化有限数据效用和针对复杂推理提供指导的有效性，为人工智能推理能力的持续发展做出了贡献。SubgoalXL的实现代码可在以下网址获取：https://github.com/zhaoxlpku/SubgoalXL。