没有标准参考答案的推理：自动形式化的替代评判器理论

复杂的推理任务越来越需要系统产生输出，其正确性无法通过与单个参考的精确匹配来判断。自动形式化（AF）是一个代表性的例子；它要求模型将非正式的数学或逻辑推理转化为形式上可检查的对象，但经过专家验证的形式化并不能扩展到玩具案例之外，并且单个非正式论证可以接受许多有效的形式化渲染。因此，进展取决于部分的、结构化的代理是否可以替代精确的参考。我们为 AF 引入了一个无参考替代评判器框架，用每轴属性检查向量取代了标准参考答案匹配。该框架沿着三个结构范围组织代理，这三个结构范围涵盖引出对象的全局属性、其子组件内部的每个模块属性以及将其重新对齐到非正式源的跨域属性，并将每个轴聚合到一个判决向量中。该向量驱动反射细化循环，其中违规坐标将控制器路由到匹配的修复目标，因此每次迭代仅更改被判断为错误的内容。在有限的判断噪声下，预期的内在差距以几何方式收缩到与噪声相关的平台。在 miniF2F、ProofNet、e-SNLI 和 ProntoQA 上的七个形式化主干中，细化持续提高了单次 ICL 基线的通过率，并且在基线有改进空间的基准上，每轴代理优于匹配的标量代理。因此，当精确参考不可用时，结构化替代评判器既提供了实际的细化信号，也提供了收敛的理论处理。