将数学命题自动形式化为结构化树，提升准确率与可修复性。
Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees
- 分步分解命题为逻辑单元，构建符号化操作树结构
- 在156个高阶定理上达到新SOTA，优于基线模型
- 适合需要高精度形式化推理的研究者与系统开发者
命题自动形式化是连接自然语言数学与形式化数学的关键桥梁，将自然语言问题转化为形式语言。以往工作主要关注数据合成与多样化训练范式以优化端到端大语言模型，但通常将形式代码视为扁平序列，忽视了数学命题中固有的层次逻辑。本文提出神经符号框架DSR（Decompose, Structure, and Repair），将自动形式化重构为模块化流程：先将命题分解为逻辑组件，并映射为结构化的操作树；再利用该拓扑蓝图，通过子树精炼实现错误的精准定位与修复。此外，我们构建了PRIME基准，包含156个来自经典教材的本科及研究生级定理，由专家标注于Lean 4。实验表明，DSR在同等计算预算下持续超越基线，建立新SOTA。数据集、模型与代码已公开于https://github.com/XiaoyangLiu-sjtu/DSR。
原文摘要 · Abstract (English)
Statement autoformalization acts as a critical bridge between human mathematics and formal mathematics by translating natural language problems into formal language. While prior works have focused on data synthesis and diverse training paradigms to optimize end-to-end Large Language Models (LLMs), they typically treat formal code as flat sequences, neglecting the hierarchical logic inherent in mathematical statements. In this work, we introduce Decompose, Structure, and Repair (DSR), a neuro-symbolic framework that restructures autoformalization into a modular pipeline. DSR decomposes statements into logical components and maps them to structured operator trees, leveraging this topological blueprint to precisely localize and repair errors via sub-tree refinement. Furthermore, we introduce PRIME, a benchmark of 156 undergraduate and graduate-level theorems selected from canonical textbooks and expertly annotated in Lean 4. Experimental results demonstrate that DSR establishes a new state-of-the-art, consistently outperforming baselines under equivalent computational budgets. The datasets, model, and code are available at https://github.com/XiaoyangLiu-sjtu/DSR.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。