pass@k表示生成k次，至少1次成功的概率。

正向计算：

pass@1：只生成1次，至少1次成功的概率为 $p$。
pass@5：生成5次，至少1次成功的概率为，成功了1次，2次，…，5次的概率之和。
…

这就很麻烦随着k的增加！！！

反向计算：
pass@5：生成5次，至少1次成功的概率为，1 - 生成5次一次都没有成功的概率——$1 - (1 - p)^k$。

但是在实际使用中，并非知道这个 $p$。所以需要使用无偏估计：

例如一道题采样了10次，只有2次生产的 lean 证明通过了。

定于：

  • $n$: 总采样数
  • $c$：正确的次数
  • $k$: 计算pass@k所考虑的采样次数

公式为：

$$\widehat{\text{pass@}k} = 1 - \frac{\binom{n-c}{k}}{\binom{n}{k}}$$

所以 pass@5 = 1 - (8! / 5!×3!) / (10! / 5!×5!)

面试可能问题：

  1. 发现 SFT 后 pass@1 提升明显，但 pass@10 提升不明显，能否解释这意味着什么？又需要增加什么实验才能判断原因？

(回答技巧：复述问题 -> 陈述观点 -> 理由论证+实验验证 -> 抛出引导 or 总结陈述)

如果 SFT 后 pass@1 提升明显，但是 pass@10 提升不明显，我首先会认为，模型单次生成正确证明的能力增强了，但是多次采样能够覆盖的题目范围没有明显扩大。

我会考虑两个主要原因。

第一，SFT 可能主要提高了模型在已有能力范围内的生成稳定性。比如某道题原来生成 10 次就有很高概率成功，SFT 后只是让它第一次生成就更容易成功，因此 pass@1 提升明显，但 pass@10 的增益有限。

第二，SFT 可能使模型的输出分布更加集中，降低了证明路径的多样性，导致多次采样不能有效探索新的解法。

为了验证，我会设计三个实验。首先对每道题进行多次采样，比较训练前后不同题目的成功次数，判断提升是集中在容易题还是原本无法解决的困难题。其次分析生成证明的多样性，观察不同温度下是否存在有效证明策略减少的问题。最后绘制不同 k 下的 pass@k 曲线，分析多次采样的边际收益。

如果最终发现 SFT 主要改善容易题的正确率，我会考虑补充困难样本、优化数据难度分布，再通过强化学习探索提升困难题的求解能力。当然，强化学习是否真的扩大能力覆盖，还需要进一步实验验证。