While statement autoformalization has advanced rapidly, full-theorem autoformalization remains largely unexplored. Existing iterative refinement methods in statement autoformalization typicall improve isolated aspects of formalization, such as syntactic correctness, but struggle to jointly optimizing multiple quality dimensions, which is critical for full-theorem autoformalization. We introduce a reference-free iterative monotonic process for full-theorem autoformalization that leverages complementary feedback from theorem provers and LLM-based judges, without access to ground-truth proofs or existing formalizations at inference time. Our approach optimizes a masked composite objective over Formal Validity, Logical Preservation, Mathematical Consistency, and Formal Quality, guided by a responsiveness map that indicates how different LLMs acting as different roles preferentially improve each dimension. We further propose an acceptance policy that guarantees certified monotonic improvement, and provide conditions ensuring convergence and termination. Empirical experiments demonstrate the proposed process enables simultaneous improvement across multiple dimensions, achieving 93.44% formal validity and a 78.22% overall score on miniF2F, and 44.09% formal validity and a 29.79% overall score on ProofNet.

翻译：尽管陈述自动形式化技术发展迅速，但全定理自动形式化领域仍鲜有探索。现有陈述自动形式化中的迭代精炼方法通常仅能改善形式化的孤立方面（如语法正确性），难以协同优化多个质量维度，而这对于全定理自动形式化至关重要。我们提出一种用于全定理自动形式化的无参考迭代单调过程，该方法在推理阶段无需真实证明或现有形式化结果的情况下，综合利用定理证明器和基于LLM的评判器提供的互补反馈。我们的方法通过响应映射图（指示不同角色LLM对各维度的优先改进倾向）的引导，对形式有效性、逻辑保持性、数学一致性及形式质量构成的掩码复合目标进行优化。我们进一步提出可保证经认证单调改进的接受策略，并提供确保收敛性与终止性的条件。实证实验表明，所提过程能实现多维度同步改进：在miniF2F数据集上达到93.44%的形式有效性与78.22%的综合得分，在ProofNet数据集上达到44.09%的形式有效性与29.79%的综合得分。