Introduces Relaxed NFL intermediate language for LLM-based auto-formalization, with rule-plus-LLM elaboration to Core NFL and tactic-language discharge of verification conditions.
Rethinking and improving autoformalization: Towards a faithful met- ric and a dependency retrieval-based approach
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
years
2026 3verdicts
UNVERDICTED 3representative citing papers
Paraphrase sensitivity in Lean 4 autoformalization is dominated by code-generation failures that differ between undergraduate and Olympiad datasets across multiple models.
The signal-coverage matrix stratifies autoformalization outputs into true success, type-only, semantic-only, and both-fail cells, showing type-correctness gains are mostly type-stratum recovery with semantic errors largely unchanged.
citing papers explorer
-
Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language
Introduces Relaxed NFL intermediate language for LLM-based auto-formalization, with rule-plus-LLM elaboration to Core NFL and tactic-language discharge of verification conditions.
-
Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization
Paraphrase sensitivity in Lean 4 autoformalization is dominated by code-generation failures that differ between undergraduate and Olympiad datasets across multiple models.
-
The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization
The signal-coverage matrix stratifies autoformalization outputs into true success, type-only, semantic-only, and both-fail cells, showing type-correctness gains are mostly type-stratum recovery with semantic errors largely unchanged.