Summary (Overview)

• Novel Diagnostic Framework: FormalRx transforms autoformalization evaluation from opaque binary judgments into actionable, fine-grained diagnostics with four components: alignment verdict, error categorization, error localization, and statement correction.
• Sci Error Taxonomy: A hierarchical classification scheme decomposing autoformalization errors into 28 distinct categories across three dimensions (Semantic, Constraint, Implementation) with strict priority ordering for unambiguous classification.
• State-of-the-Art Performance: FormalRx-8B achieves F1-scores of 0.88 (verdict) and 0.71 (categorization), with accuracies of 0.75 (localization) and 0.73 (correction), substantially outperforming general-purpose LLMs and specialized baselines.
• Large-Scale Diagnostic Dataset: Construction of 56,287 NL-FL pairs with fine-grained diagnostic annotations through taxonomy-guided error injection, plus a 7,030-sample held-out benchmark (FormalRx-Test).
• Single-Pass Multi-Task Architecture: A unified generative approach performing all four diagnostic tasks in a single forward pass, mitigating error propagation between cascaded stages.

Introduction and Theoretical Foundation

Background and Motivation

Formal mathematical reasoning represents a frontier in AI for rigorous, verifiable logical inference. Proof assistants like Lean enable autoformalization—translating mathematical problems from natural language into formal statements—which serves as a critical bridge to mitigate reasoning unfaithfulness and hallucinations in LLMs. However, existing evaluation approaches suffer from fundamental limitations:

1. Syntactic validity checks (type-checking, BLEU scores) fail to capture semantic alignment
2. Rule-based equivalence checks achieve high precision but suffer from low recall and limited domain coverage
3. LLM-as-judge methods reduce semantic correctness to binary verdicts with no interpretable feedback

Data Foundation

The training data consists of 17,825 aligned NL-FL pairs from curated datasets including Formal-MATH, FIMO, Compfiles, PutnamBench, ProverBench, CombiBench, and Gaokao-Formal, plus Mathlib library entries. Notably, MiniF2F and ProofNet were deliberately excluded due to documented alignment issues.

Methodology

Sci Error Taxonomy

The taxonomy formally partitions the error space $\mathcal{E}$ into three dimensions $\mathcal{P} = \{S, C, I\}$ where for any distinct dimensions $D_1, D_2 \in \mathcal{P}$:

$$D_1 \cap D_2 = \emptyset \quad \text{and} \quad \bigcup_{D \in \mathcal{P}} D = \mathcal{E}$$

Semantic Errors (S1–S3):

• S1 Logical structure: Errors at the propositional level (quantifier/connective misuse)
• S2 Mathematical objects: Misrepresentation of types, functions, operators, exponents, coefficients
• S3 Mathematical concepts: Deeper misunderstandings (infinity, cardinality, geometric relationships)

Constraint Errors (C1–C5):

• C1 Variable constraints: Missing, redundant, or incorrect admissible value ranges
• C2 Range errors: Misspecified iteration domains for sums, products, or index sets
• C3–C5 Location-based catch-alls: premise, conclusion, and auxiliary construction errors

Implementation Errors (I1–I2):

• I1 Truncation errors: Discrete numeric type deviations (e.g., $3 - 5 = 0$ over ℕ)
• I2 Precedence errors: Parser binds operators differently than standard notation

Training Objective

Standard SFT with negative log-likelihood loss:

$$\mathcal{L}_{\mathrm{SFT}}(\theta) = -\sum_{i=1}^{N} \sum_{t=1}^{T_i} \log p_\theta(y_{i,t} \mid \mathcal{S}_i, \mathcal{F}_i, y_{i,<t}) \tag{1}$$

Data Synthesis Pipeline

1. Error Injection: Claude-Sonnet-4 generates misaligned variants from aligned seed pairs using taxonomy-guided prompts
2. Code Validity: All synthesized statements verified via Lean REPL
3. Label Validation: Independent LLM re-classification with 86.2% expert accuracy and 94.7% agreement

Empirical Validation / Results

Main Results (FormalRx-Test)

Key Findings

• Verdict prediction shows diminishing returns (base models already achieve 0.833–0.854 F1)
• Categorization shows the largest gap (23.4 points), confirming the need for task-specific supervision
• Scaling behavior differs by task: generative tasks (Localization, Correction) show clear improvements with scale, while classification tasks plateau at smaller sizes
• Out-of-domain transfer shows consistent improvements over backbones on ConsistencyCheck and EPLA benchmarks

Theoretical and Practical Implications

Theoretical Contributions

1. Partition-based error taxonomy: Provides formal guarantees of mutual exclusivity and collective exhaustiveness through set partition theory and priority ordering
2. Unified diagnostic framework: Demonstrates that all four diagnostic tasks can be jointly learned in a single forward pass, suggesting shared representations between them
3. Benchmark limitations exposed: OOD results reveal that verdict-only benchmarks are noisy indicators of diagnostic capability

Practical Applications

• Automated debugging: Identifies specific error types and locations in autoformalization outputs
• RLHF pipelines: High-fidelity correction signals enable more nuanced reward modeling
• Human-AI collaboration: Actionable feedback supports human oversight and correction

Conclusion

FormalRx establishes a transparent foundation for moving autoformalization beyond black-box assessments toward instructive, verifiable quality assurance. The framework's ability to provide error localization and correction suggestions bridges the gap between evaluation and model refinement.

Key Limitations and Future Directions

1. Taxonomy coverage: Built from bounded samples; long-tail errors may not map cleanly onto the 28 categories
2. Language specificity: Implementation dimension is Lean 4-specific; adaptation to Coq/Isabelle requires re-derivation
3. Out-of-distribution generalization: Performance advantage narrows on OOD benchmarks, highlighting the need for broader evaluation across more corpora and naturally occurring errors
4. Evaluation scope: External benchmarks only provide binary labels, restricting OOD evaluation to the verdict task