分解、结构、修复：基于算子树的自动形式化神经符号框架
机器学习
2026-05-25 v2 人工智能
摘要
语句自动形式化作为人类数学与形式数学之间的关键桥梁，通过将自然语言问题翻译为形式语言来实现。虽然已有工作聚焦于数据合成和多样化训练范式以优化端到端的大语言模型(LLM)，但它们通常将形式代码视为平坦序列，忽略了数学语句中固有的层次逻辑。本文引入分解、结构、修复(Develop, Structure, and Repair, DSR)，一种神经符号框架，将自动形式化重构为模块化管线。DSR 将语句分解为逻辑组件并映射到结构化算子树，利用这种拓扑蓝图精确定位和通过子树修复错误。此外，我们引入 PRIME，一个来自标准教科书并由 Lean 4 expertly 注释的 156 题的基准测试。实验结果表明，DSR 在相当等计算预算下建立了新的状态-of-the-art，持续优于基线方法。数据集、模型和代码均可在 https://github.com/XiaoyangLiu-sjtu/DSR 查阅。
引用
@article{arxiv.2604.19000,
title = {Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees},
author = {Xiaoyang Liu and Zineng Dong and Yifan Bai and Yantao Li and Yuntian Liu and Tao Luo},
journal= {arXiv preprint arXiv:2604.19000},
year = {2026}
}
备注
Accepted to ICML 2026