Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees

• URL: http://arxiv.org/abs/2604.19000v1
• Date: Tue, 21 Apr 2026 02:36:55 GMT
• Title: Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees
• Abstract summary: Statement autoformalization acts as a critical bridge between mathematics and formal mathematics.<n>We introduce Decompose, Structure, and Repair (DSR), a neuro-symbolic framework that restructures autoformalization into a modular pipeline.
• Score: 10.346796782214485
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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 will be released to the public soon.

Related papers

• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  Large Language Models (LLMs) produce subtle errors that evade human detection.<n>Recent trends indicate that general-purpose LLMs now outperform smaller models explicitly fine-tuned for Lean.<n>We introduce an agentic autoformalization framework powered by general coding LLMs.
  arXiv  Detail & Related papers  (2026-06-30T05:05:03Z)
• Weave of Formal Thought [51.56484100374058]
  We introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations.<n>We present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation.<n>For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline.
  arXiv  Detail & Related papers  (2026-06-24T15:58:11Z)
• NED-Tree: Bridging the Semantic Gap with Nonlinear Element Decomposition Tree for LLM Nonlinear Optimization Modeling [6.424862571179283]
  We introduce NED-Tree, a systematic framework designed to bridge the semantic gap.<n>NED-Tree employs a sentence-by-sentence extraction strategy to ensure robust parameter mapping and traceability.<n>We present NEXTOR, a novel benchmark specifically designed for complex nonlinear, extensive-constraint OR problems.
  arXiv  Detail & Related papers  (2026-04-02T03:59:37Z)
• SMGI: A Structural Theory of General Artificial Intelligence [2.538209532048866]
  We formalize the Structural Model of General Intelligence (SMGI) via a typed meta-model $= (r,mathcal H,,mathcal L,mathcal E,mathcal M)$<n>We define general artificial intelligence as a class of admissible coupled dynamics $(, T_)$ satisfying four obligations.<n>We prove a structural generalization bound that links sequential PAC-Bayes analysis and Lyapunov stability.
  arXiv  Detail & Related papers  (2026-03-09T02:31:31Z)
• Multi-Agent Procedural Graph Extraction with Structural and Logical Refinement [66.51979814832332]
  model formulates procedural graph extraction as a multi-round reasoning process with dedicated structural and logical refinement.<n>Experiments demonstrate that model achieves substantial improvements in both structural correctness and logical consistency over strong baselines.
  arXiv  Detail & Related papers  (2026-01-27T04:00:48Z)
• LSRIF: Logic-Structured Reinforcement Learning for Instruction Following [56.517329105764475]
  We propose a logic-structured training framework LSRIF that explicitly models instruction logic.<n> Experiments show LSRIF brings significant improvements in instruction-following and general reasoning.
  arXiv  Detail & Related papers  (2026-01-10T05:11:38Z)
• SITA: A Framework for Structure-to-Instance Theorem Autoformalization [20.941850622174236]
  We develop a framework for structure-to-instance theorem autoformalization (SITA)<n>SITA bridges the gap between abstract mathematical theories and their concrete applications in Lean proof assistant.<n>We generate corresponding Lean definitions and instance declarations, integrate them using Lean's typeclass mechanism, and construct verified theorems by checking structural assumptions.
  arXiv  Detail & Related papers  (2025-11-13T14:33:51Z)
• DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
  DRIFT is a framework that decomposes informal mathematical statements into smaller, more tractable ''sub-components''<n>It retrieves illustrative theorems to help models use premises more effectively in formalization tasks.<n>We evaluate DRIFT across diverse benchmarks (ProofNet, ConNF, and MiniF2F-test) and find that it consistently improves premise retrieval.
  arXiv  Detail & Related papers  (2025-10-12T21:42:04Z)
• Enhancing Systematic Decompositional Natural Language Inference Using Informal Logic [51.967603572656266]
  We introduce a consistent and theoretically grounded approach to annotating decompositional entailment. We find that our new dataset, RDTE, has a substantially higher internal consistency (+9%) than prior decompositional entailment datasets. We also find that training an RDTE-oriented entailment classifier via knowledge distillation and employing it in an entailment tree reasoning engine significantly improves both accuracy and proof quality.
  arXiv  Detail & Related papers  (2024-02-22T18:55:17Z)
• Physics of Language Models: Part 1, Learning Hierarchical Language Structures [51.68385617116854]
  Transformer-based language models are effective but complex, and understanding their inner workings and reasoning mechanisms is a significant challenge.<n>We introduce a family of synthetic CFGs that produce hierarchical rules, capable of generating lengthy sentences.<n>We demonstrate that generative models like GPT can accurately learn and reason over CFG-defined hierarchies and generate sentences based on it.
  arXiv  Detail & Related papers  (2023-05-23T04:28:16Z)
• Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
  We propose a structure-modeled textual encoding framework for inductive logical reasoning over KGs. It encodes linearized query structures and entities using pre-trained language models to find answers. We conduct experiments on two inductive logical reasoning datasets and three transductive datasets.
  arXiv  Detail & Related papers  (2023-05-23T01:25:29Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.