#artificial intelligence
Apr 2026
Faithful Autoformalization via Roundtrip Verification and Repair
This work evaluates the framework on two statutory domains using two LLMs using two LLMs (Claude Opus~4.6 and GPT-5.2) with three repair baselines, finding diagnosis-guided scoped repair is the most effective method, with effectiveness contingent on the reliability of the diagnosis function.
Daneshvar Amrollahi, Jerry Lopez, Clark W. Barrett
· arXiv.org · 7 citations