分解、结构和修复：通过算子树进行自动形式化的神经符号框架

语句自动形式化通过将自然语言问题转化为形式语言，充当人类数学和形式数学之间的关键桥梁。虽然之前的工作重点关注数据合成和多样化的训练范例来优化端到端 大语言模型 (LLM)，但它们通常将形式代码视为平面序列，忽略了数学语句中固有的层次逻辑。在这项工作中，我们引入了分解、结构和修复（DSR），这是一种神经符号框架，可将自动形式化重组为模块化管道。 DSR 将语句分解为逻辑组件，并将它们映射到结构化运算符树，利用此拓扑蓝图通过子树细化来精确定位和修复错误。此外，我们还引入了 PRIME，这是一个由 156 个本科生和研究生水平定理组成的基准，这些定理选自经典教科书并在 Lean 4 中进行了专业注释。实验结果表明，DSR 建立了一个新的最先进的、在同等计算预算下始终优于基准的基准。数据集、模型和代码可在 https://github.com/XiaoyangLiu-sjtu/DSR 获取。