分解、结构与修复：一种基于算子树的自动形式化神经符号框架

语句自动形式化是连接人类数学与形式数学的关键桥梁。现有工作多将形式代码视为扁平序列，忽视了数学陈述固有的层次逻辑。本文提出“分解、结构与修复”（DSR）神经符号框架，将自动形式化重构为模块化流程：先将陈述分解为逻辑组件并映射为结构化算子树，再利用该拓扑蓝图精确定位并通过子树细化修复错误。此外，我们推出了 PRIME 基准，包含 156 个选自经典教材的本硕博级定理及其 Lean 4 标注。实验表明，DSR 在同等计算预算下持续超越基线，确立了新的最先进水平。