Compiling in Lean isn't enough: agent formalizes 87.2% but only 57.7% are faithful
ucriverside · hf · 2026-10-21
UC Riverside, University of Arizona and UCSD measure how far Lean compilation overstates faithfulness in statement autoformalization. The criterion requires compilation plus agreement of two LLM judges from different model families; an independent random audit agrees with human majority on 91.5% of cases. Across eight systems on 227 university-level statements, the gap between compiling and accepted outputs ranges 1.3–29.5 percentage points: a tool-augmented agent compiles 87.2% of statements but only 57.7% are accepted, and human review confirms 23.8 of those 29.5 points are real translation errors.
More from Research
- Embedding arithmetic demo: cartoon − animation − comic = diagram — mayfer · 2026-10-23
- Omnii Genome: Single Generalist Model Outperforms AlphaGenome Across All Benchmarks — JosephJacks_ · 2026-10-23
- Domingos Cites New Result Claiming RL Is 'Basically Useless' vs Supervised Learning — pmddomingos · 2026-10-23
- Word Arithmetic on Embeddings: "Bathroom Minus Toilet Equals Kitchen" Beats SAE Probing — mayfer · 2026-10-23
- Wolfram Opens Rule 30 Prizes to AIs: $30,000 for Three Open Problems — cephaloform · 2026-10-23
- Stanford and Databricks use AI agents to reproduce medical findings and test analytical robustness — ChengleiSi · 2026-10-23