analiza aiqbench
The paper targets a practical reliability problem in LLM-driven autoformalization: LLM judges can accept incorrect Lean statements, so the authors pair LLM semantic review with mechanical numerical and vacuity checks. Their reported gain is a lower rate of accepted errors on three labeled datasets, with the caveat that the evaluation is limited to those benchmarks and the FLMF library is only a partial formalization of DLMF. For readers tracking AI-assisted formal math, the useful takeaway is that verifiable, checkable feedback may be more dependable than LLM-as-judge alone.
Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization
arXiv:2610.20573v1 Announce Type: cross Abstract: We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof autoformalization pipeline, to construct the Formalized Library of Mathematical Functions (FLMF), a partial formalization of the NIST Digital Library of Mathematical Functions (DLMF). On three labeled datasets, our method achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method. Expert review of the results also identifies translation and source defects in existing datasets. Code available at https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git.
Abstract:We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof autoformalization pipeline, to construct the Formalized Library of Mathematical Functions (FLMF), a partial formalization of the NIST Digital Library of Mathematical Functions (DLMF). On three labeled datasets, our method achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method. Expert review of the results also identifies translation and source defects in existing datasets. Code available at this https URL.
Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI)
arXiv:2610.20573 [cs.LO]
(or arXiv:2610.20573v1 [cs.LO] for this version)
https://doi.org/10.48550/arXiv.2610.20573 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Text integral sub licența deschisă a publicației · 224 cuvinte
Subiecte conexe
How to Measure Intelligence Beyond Human Scale?
LessWrong · 31 iul. 2026
Why I Left Google DeepMind
LessWrong · 15 iul. 2026
Agentic Reward Modeling: Verifying GUI Agent via Progressive Trajectory-Grounded Interaction
arXiv · 28 iul. 2026
Benchtalks #2: The future of coding benchmarks
Snorkel AI Blog · 3 iun. 2026