面向自然语言数学推理的风险控制型 Lean-as-Judge 方法

Lean 常被用于评判自然语言数学答案，但其信号存在局限性：许多答案无法形式化，且证明失败可能源于类型错误或库缺失而非答案错误。本文提出 COVCAL 方法，通过分析 Lean 追踪诊断信息，在有限样本下对接受的答案提供选择性风险边界认证或选择弃权。研究表明，该方法可行性高度依赖自动形式化的覆盖率；使用专用形式化器时，可在保持高准确率的同时接受近半数问题。本文贡献在于精确界定了在何种条件下及部分形式化信号可被信任。