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

1. Problem Statement

Statement Autoformalization aims to translate natural language (NL) mathematical problems into formal language (FL), such as Lean 4, to enable automated theorem proving. While recent Large Language Models (LLMs) have improved this process, current state-of-the-art approaches suffer from two critical limitations:

1. Flat Sequence Generation: Most models treat formal code as a flat string, ignoring the inherent hierarchical and logical structure of mathematical statements. This leads to errors in operator precedence, scope, and logical dependencies.
2. Ineffective Error Repair: When generation fails, existing repair strategies often attempt to regenerate the entire statement (brute-force), which is computationally expensive and risks disrupting correctly generated sub-components.

2. Methodology: The DSR Framework

The authors propose DSR (Decompose, Structure, and Repair), a neuro-symbolic framework that restructures autoformalization into a modular pipeline. The process consists of three distinct stages:

A. Decomposition (Semantic Canonicalization & Structural Alignment)

Instead of translating the raw NL statement directly, DSR first decomposes it into logical components:

• Semantic Canonicalization: Removes linguistic noise and explicates implicit context (e.g., variable types, background assumptions) to create a "Lean-friendly" input.
• Structural Role Alignment: Segments the statement into distinct Conditions (premises/hypotheses) and a Conclusion (proof goal). This decoupling enforces a clear syntactic separation, guiding the model to instantiate conditions as variables and the conclusion as the proof goal, preventing logical inversions.

B. Structuring (Joint Generation with Operator Trees)

The core innovation is the joint generation of formal code and its structural representation:

• FL Components: The model translates NL components into linear Lean code fragments.
• FL Operator Trees (OPTs): Simultaneously, the model generates an Operator Tree for each component. An OPT is a labeled, ordered tree where operators are internal nodes and operands are leaves.
  • Significance: The OPT acts as a "semantic anchor," forcing the model to explicitly model the recursive topology of the logic rather than relying on statistical correlations. It also serves as a topological blueprint for the repair stage.
• Curriculum Learning: The training pipeline uses a four-stage curriculum. The model starts by learning simple linear code generation and progressively advances to joint generation of code and complex OPTs. This prevents the model from being overwhelmed by the simultaneous learning of complex logic and hierarchical topology.

C. Repair (Tree-Guided Strategy)

When the generated code fails to compile, DSR employs a hierarchical repair strategy guided by the OPT:

1. Structure-First Assembly: The code is reconstructed primarily from the OPT to ensure syntactic validity (e.g., matching parentheses).
2. Hierarchical Repair Loop: Instead of regenerating the whole statement, the system maps compiler error locations to specific nodes in the OPT. It attempts repairs in increasing order of scope:
   • Subcomponent-Level: Fixes specific subtrees (e.g., correcting a function name or type annotation).
   • Component-Level: If sub-repair fails, the entire logical component is regenerated.
   • Statement-Level: As a last resort, the full statement is repaired.
     This "surgical" approach preserves correct logic in unaffected parts of the tree.

3. Key Contributions

1. DSR Framework: A novel neuro-symbolic pipeline that decouples autoformalization into decomposition, structured generation (via OPTs), and tree-guided repair.
2. PRIME Benchmark: The introduction of PRIME (Problem Repository of Instructional Mathematics for Evaluation), a high-quality benchmark containing 156 expert-annotated theorems from undergraduate and graduate-level textbooks (covering Algebra, Analysis, Number Theory, etc.). Unlike previous benchmarks, PRIME ensures strict semantic consistency between NL and FL statements.
3. State-of-the-Art Performance: DSR establishes new records in autoformalization, consistently outperforming baselines (including specialized 7B/32B models and general-purpose LLMs like Qwen3-Max) under equivalent computational budgets.

4. Experimental Results

The framework was evaluated on ProverBench, ProofNet, and the new PRIME benchmark.

• Performance: DSR achieved the highest Consistency Check (CC) pass rates across all datasets.
  • On PRIME (the most difficult, graduate-level set), DSR achieved a CC of 67.95%, outperforming the strongest baseline (Goedel-V2-32B) by 1.28%.
  • On ProofNet, DSR achieved a CC of 79.51%, significantly reducing the gap between Syntax Check (SC) and CC (indicating fewer "compilable hallucinations").
• Ablation Studies:
  • Operator Trees: Adding OPT supervision improved performance, but only when combined with curriculum learning. Without curriculum learning, the model struggled with the complexity of full OPTs, leading to performance regression on difficult benchmarks.
  • Repair Strategy: The tree-guided repair strategy significantly outperformed global (statement-level) repair. While global repair sometimes achieved higher syntax pass rates, it degraded semantic consistency. DSR's surgical repairs preserved logical integrity while fixing errors.

5. Significance

This work represents a paradigm shift in autoformalization from monolithic sequence generation to modular, structure-aware reasoning.

• Semantic Fidelity: By enforcing hierarchical structure via OPTs, DSR ensures that generated code is not just syntactically valid but semantically faithful to the original mathematical intent.
• Efficiency: The tree-guided repair mechanism drastically reduces the computational cost of fixing errors by localizing the scope of regeneration, making the system more scalable for complex theorems.
• Foundation for ATP: By bridging the gap between human-readable math and machine-verifiable code with high fidelity, DSR serves as a critical enabler for future Automated Theorem Proving (ATP) systems, moving closer to the goal of fully autonomous mathematical discovery.