Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization
The paper introduces a reference-free proxy-judge framework to improve Autoformalization (AF), which generates formal proofs from informal sources. Instead of relying on costly gold standards, this method uses eight specialized judges that check correctness across four structural scopes. This system creates a reflective refinement loop where violations guide targeted repairs, geometrically reducing the error gap until a stable plateau is reached.