FormalRx is introduced, a comprehensive diagnostic evaluation framework that transforms autoformalization assessment from black-box judgments into actionable feedback, and enables systematic diagnosis and improvement of autoformalization systems.
Abstract
The veracious semantic alignment in autoformalization is significant for formal mathematical reasoning. However, existing evaluations provide only opaque binary verdicts or scalar scores, offering no interpretable insight into where or why translations fail. This opacity severely limits both human understanding and automated system improvement. To bridge this gap, we introduce FormalRx, a comprehensive diagnostic evaluation framework that transforms autoformalization assessment from black-box judgments into actionable feedback. At its core is SCI Error Taxonomy, a hierarchical classification scheme decomposing autoformalization errors into 28 distinct categories with strict priority ordering. Building on this taxonomy, FormalRx provides four critical diagnostic capabilities: alignment verdicts, error categorization, error localization, and correction. We instantiate the framework with a diagnostic model FormalRx-8B, trained on 56,287 NL-FL pairs with fine-grained diagnostic annotations, and release FormalRx-Test as the first fine-grained diagnostic benchmark. FormalRx-8B achieves F1-scores of 0.88 (verdict) and 0.71 (categorization), along with accuracies of 0.75 (localization) and 0.73 (correction), substantially outperforming both general-purpose LLMs and specialized baselines. By connecting evaluation with actionable insights, FormalRx enables systematic diagnosis and improvement of autoformalization systems.
Neurosymbolic systems rely on mathematical solvers to guarantee reasoning correctness, yet solvers are fundamentally blind to whether a formal translation maintains strict reference-equivalence to a designated formalization. We formalize this vulnerability as Verdict-Preserving-Unfaithfulness (VPU): a failure mode where an incorrect encoding executes successfully and matches the expected verdict. We theoretically prove that structural, verdict-only verification heuristics are mathematically bounded to chance-level detection on these deceptively valid traces. To resolve this, we introduce Generative Verification (GenV), which distills an offline Z3-equivalence oracle into a reference-free, continuous reference-equivalence score by repurposing the language model's native vocabulary space. Mechanistic analysis via decision-projected logit lenses and sparse autoencoders shows this generative readout natively extracts precise spatial error coordinates without explicit localization training. Empirically, our oracle-mined verifier (GenV+HN) achieves 0.961 AUROC in reference-equivalence verification, generalizes zero-shot across unseen translators and divergent formal styles, and yields an 11.3-point downstream accuracy gain in agentic test-time compute allocation.
Vikash Singh, Debargha Ganguly, Aman Goel et al.· 0 citations
FaithSieve is introduced, a Lean-assisted framework for fine-grained evaluation of natural-language mathematical proofs that demonstrates that decomposing proofs into fine-grained units and grounding them with faithful formal evidence significantly improves reliable evaluation of natural-language reasoning.
Ziyu Wang, Qiyu Dai, Yi-Shan Wu et al.· 0 citations
The"decompose-then-verify"paradigm for LLM factuality evaluation faces a fundamental trade-off: atomic facts, i.e., one sentence conveying one unit of information, often omit essential context, while broader statements lack the granularity needed for precise assessment. To address this, we introduce TriQua, a framework that flexibly models facts based on their complexity. Simple claims are extracted as standard triples, while complex claims are represented as hyperrelational facts by attaching auxiliary contextual qualifiers. This adaptive structure preserves the necessary context for accurate retrieval and verification without sacrificing atomicity. Furthermore, TriQua's verification process directly annotates concrete errors within specific triples and qualifiers, providing fine-grained explainability for error detection. Alongside the framework, we propose TriQuaScore to quantify the factuality of these structured fact units. Empirical evaluations show that TriQuaScore strongly aligns with human annotated factuality scores, TriQua achieves robust decomposition quality, and outperforms existing decomposition-based frameworks in evidence-based fact verification.
Jin Liu, Steffen Thoma, Achim Rettinger· 0 citations
Scientific autoformalization turns verbal accounts into executable mathematics, but executable code does not settle which model has been constructed. We examine two sources of structural uncertainty: the formalizer that generates a response law, and the recurrence that turns that law into trajectories. In secondary analyses of an openly archived crossed experiment, we studied 320 response maps generated by two pinned language-model formalizers from five engineered cognitive accounts within one sparse quadratic grammar and 16 randomized blocks. With whole blocks held out, source-account identity was recovered at 78.8% accuracy (chance 20.0%) and formalizer identity at 96.3% (chance 50.0%; both p<0.001). Program size was the stronger single feature family; a pre-specified exploratory comparison found no stable source-account predictive gain from local geometry beyond size. Holding every response map fixed, we then evaluated five recurrence families spanning 33 configurations and 1,013,760 finite-horizon trajectories. Added feedback, projection and leak produced sharply different outcome distributions. The consequential distinction was which comparisons survived: median cross-recurrence rank concordance was 0.73 for endpoint magnitude but 0.05 for settling, among the configuration pairs with defined rankings. Thus a common mathematical language did not erase translation provenance, and robust ordering under one observable did not transfer to another. Scientific autoformalization is usefully studied as model-space construction: the generated ensemble and its dynamical embedding are both part of the specification supporting a scientific claim.
This work proposes Sequential Epistemic and Action-Level Validation (SEAV), a verification-centric jailbreak evaluation framework that decomposes responses into ordered steps and evaluates both validity and correctness, and shows that enforcing correctness substantially reshapes measured robustness.
Qilong Wu, Sahil Wadhwa, Pranab Mohanty et al.· 0 citations
MathForm is introduced, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement, and outperforming multiple specialized 32B autoformalizers.
Lushi Pu, Weiming Zhang, Xinheng Xie et al.· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
