本文提出 LeanContext，一个包含 129,826 条 Lean 完整证明生成任务的基准，用于评估检索到的前置声明在证明生成中的作用。我们将选取的完整前置数学声明归为 数学上下文 (MC)，其余选取的局部源代码命令归为 环境上下文 (EC)。基准提供四种对齐的输入视图，支持交叉训练与推理评估，所有视图共享同一目标声明和原始 Lean 验证环境。
实验使用扩散模型和自回归模型两类生成器。结果显示，当训练过程中加入 MC 时，选取的声明相较于等价的替代方案能够带来更大的性能提升。通过对最终输入进行审计，我们能够发现目标声明所遗漏的依赖声明。将这些依赖加入输入后，LLaDA 在 2,000 条目标上的 Pass@32 提升 1.40%，Llama 提升 1.70%。
值得注意的是，选择实验在不访问目标参考证明的前提下进行，且保持检查点、EC 和推理预算不变。代码与数据集已开源，地址为 https://github.com/haaaardcvZ/LeanContext。
点评