用于自动形式化的单调无参考精炼方法

尽管语句级自动形式化进展迅速，但全定理自动形式化仍鲜有探索。现有迭代方法通常仅优化单一维度，难以兼顾多质量指标。本文提出一种无参考的单调迭代过程，利用定理证明器与基于 LLM 的评判器提供的互补反馈，在无真实证明参考的情况下，同步优化形式有效性、逻辑保持性、数学一致性及形式质量。该方法引入响应图谱指导不同角色 LLM 的改进方向，并设计接受策略以确保认证的单调提升与收敛。实验表明，该方法在 miniF2F 和 ProofNet 数据集上均实现了多维度的同步显著提升。