无需标准答案的推理：自动形式化的代理评判理论

View PDF HTML (experimental)

Abstract:Autoformalization (AF) requires both prover acceptance and fidelity to an informal source, but prover acceptance alone cannot establish fidelity, and expert-validated reference formalizations are costly to obtain. We introduce a reference-free proxy-judge framework, which separates correctness into grounding, statement faithfulness, coverage, and inference, and a theory of how imperfect checks shape iterative refinement. We establish three results. First, for a fixed sequence of candidates, an added proxy's false-positive and false-negative rates bound its effect on the pass-but-wrong rate. Second, damage to a correct formalization requires a false rejection that exposes it to further refinement, and harmful revisions are then retained through unguarded changes, missed changes, or prover progress that overrides judge warnings. Third, a decomposition of the final pass rate distinguishes continued refinement, generation of new candidates, and their success in passing the checks. We instantiate the framework with eight proxies and test these predictions on ProofNet and miniF2F in Lean~4 and on e-SNLI and ProntoQA in Isabelle/HOL. Under single-proxy removal, no prediction written before the runs is contradicted, and all traced breaks follow the identified failure routes. The results connect proxy reliability to the benefits, risks, and limits of refinement without reference formalizations.

Subjects:	Computation and Language (cs.CL)
Cite as:	arXiv:2606.09449 [cs.CL]
	(or arXiv:2606.09449v2 [cs.CL] for this version)
	https://doi.org/10.48550/arXiv.2606.09449 arXiv-issued DOI via DataCite

Submission history

From: Lei Xu [view email]
[v1] Mon, 8 Jun 2026 12:57:09 UTC (241 KB)
[v2] Wed, 14 Oct 2026 16:45:14 UTC (370 KB)