面向自然语言数学推理的风险受控Lean-as-Judge

Lean越来越多地被用于评判自然语言数学答案，但其信号是不完整的：许多答案根本无法形式化，而证明失败可能源于类型错误的陈述或缺失的库事实，而非答案错误。在MATH-500上我们证明，该信号(i)高度依赖覆盖率，即在被证明覆盖率较高时胜出的证明答案96%正确，而覆盖率低时仅20%；(ii)稀疏且常常不忠实：一个7B自动形式化器仅对28%的题目给出某类证明，人工审计发现其中仅约43%的证明是忠实的。我们提出COVCAL，一个基于Lean轨迹诊断的选择器，它对被接受的答案认证有限样本选择性风险上界，否则弃权，在两种规则下运行（保守的Bonferroni界与更紧的dev-then-cal规则）。可行性取决于自动形式化覆盖率：使用7B形式化器时信号过于稀疏，Bonferroni在全部20个bootstrap划分上均弃权；而一个面向证明器特化的形式化器达到79%覆盖率，使其中17个划分变为可行，在0.98的接受准确率下接受约48%的题目。由于仅靠自洽性已达到91%准确率，我们的贡献在于精确刻画了在风险控制下、何时以及使用哪种形式化器时，部分形式化信号才可信。