Faithful Autoformalization via Roundtrip Verification and Repair.

arXiv:2604.25031v3 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, trans