Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916037676498944 |
|---|---|
| author | Liu, Xiaoyang Dong, Zineng Bai, Yifan Li, Yantao Liu, Yuntian Luo, Tao |
| author_facet | Liu, Xiaoyang Dong, Zineng Bai, Yifan Li, Yantao Liu, Yuntian Luo, Tao |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_19000 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees Liu, Xiaoyang Dong, Zineng Bai, Yifan Li, Yantao Liu, Yuntian Luo, Tao Machine Learning Artificial Intelligence 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. |
| title | Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees |
| topic | Machine Learning Artificial Intelligence |
| url | https://arxiv.org/abs/2604.19000 |