我们提出了第一个基于学习的、正确性保证的逐步数学积分系统。核心思想是学习一个由 GPT 变换模型表示的策略，该策略引导搜索正确的数学积分规则，由符号求解器执行。具体来说，我们引入了一个具有公理正确性的数学表达式操作的符号引擎，以及第一个逐步积分数据集。我们的 GPT 风格变换模型在该合成数据上进行训练，通过使用 50% 更少的搜索步骤，在准确性和效率方面超越了其自身的数据生成器，展现出强大的泛化能力。我们对最先进的 LLM 的实验结果也表明，在问答对数据集上微调 LLM 的标准方法不足以解决此数学任务。这说明了探索将 LLM 与符号推理引擎相结合的创造性方法的重要性，我们的工作就是一个实例。