Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization
This work introduces a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness, and achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method.
Anna Mei, Michael R. Douglas
· 0 citations