形式化定理证明新突破：SubgoalXL框架让大模型在Isabelle中性能暴涨

香港大学与SambaNova Systems合作开发出SubgoalXL框架，通过子目标证明策略与专家学习框架应对形式化定理证明的数据稀缺及多步骤推理难题。SubgoalXL在miniF2F数据集上的通过率分别达到61.9%和56.1%，显著超越现有方法。这一成果展示了大语言模型在形式化定理证明中的潜力。
来源：https://mp.weixin.qq.com/s/2Vfn08ljWnoRTUx-Y3qwkQ