Faithful Autoformalization via Roundtrip Verification and Repair

arXiv:2604.25031v2 Announce Type: replace-cross Abstract: When an LLM formalizes natural language, how do we know the output is faithful? We propose a roundtrip verification approach which does not require ground-truth annotations: formalize a statement, translate the result back to natural...