Aligning Faithfulness for Theory-Scale Autoformalization
cs.CL, cs.AI
Submitted: 2026-10-13
Updated: 2026-10-13
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Sources
- ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
- FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation
- Theory-Scale Auto-Formalization of Logics for Computer Science
- SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
- Language Models (Mostly) Know What They Know
- Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
- Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization
- Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance
- Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
- The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements
- MathAtlas: A Benchmark for Autoformalization in the Wild
- Formalizing Mathematics at Scale
- Autoformalization in the Era of Large Language Models: A Survey
- DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
- FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
- Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
Related papers
- Exploring Solution Divergence and Its Effect on Large Language Model Problem Solving
- Ishigaki-IDS-Bench: A Benchmark for Generating Information Delivery Specification from BIM Information Requirements
- Subliminal Steering: Stronger Encoding of Hidden Signals
- MedStruct-S: A Benchmark for Key Discovery, Key-Conditioned QA and Semi-Structured Extraction from OCR Clinical Reports
- The End of Transformers? On Challenging Attention and the Rise of Sub-Quadratic Architectures
- Untangling the Mechanisms of Misleading Context in Medical Question Answering