arXiv cs.AI· Hang Zhang, Qihao Ye, Litong Liu, Yunbei Zhang, Yugyung Lee, Yue Zhou, Bowen Liu, Emily First, Cheng Han, Qiao Zhuang·· 11 小时前AI 评分29
LeanContext：在 Lean 全证明生成中分离数学资源与局部形式上下文
LeanContext: Disentangling Mathematical Resources from Local Formal Context in Lean Whole-Proof Generation
AI 导读
LeanContext 是一个包含 129,826 道 Lean 全证明生成问题的基准，用于衡量目标所选声明相对同类替代声明的优势及其对训练的依赖。研究将所选完整前置数学声明归为数学上下文（MC）、其余局部源码命令归为环境上下文（EC），在扩散模型与自回归模型上，训练包含 MC 时所选声明优势更大。
正文 · AI 翻译
摘要：神经定理证明越来越多地使用检索到的前提和项目上下文来支持证明生成。评估这些资源需要衡量目标选定的声明相对于可比替代方案的优势，以及这种优势如何取决于训练。我们引入了 LeanContext，一个包含 129,826 个 Lean 整体证明生成问题的基准，以研究这些问题。我们将选定的完整前置数学声明归为数学上下文（MC），将剩余的选定本地源命令归为环境上下文（EC）。四种对齐的输入视图支持交叉训练和推理评估，并共享目标和原始 Lean 验证环境。对于基于扩散和自回归的模型，当训练包含 MC 时，选定的声明以更大的幅度优于可比替代方案。最终输入审计识别出目标所引用但被省略的声明。优先处理这些依赖关系使 LLaDA 和 Llama 在 2,000 个目标上的 Pass@32 分别提高了 1.40% 和 1.70%。该选择实验在不访问目标参考证明的情况下运行，并保持检查点、EC 和推理预算不变。代码和数据集可在 此 https URL 获取。
| 学科： | 人工智能（cs.AI） |
| 引用为： | arXiv:2611.08277 [cs.AI] |
| （或 arXiv:2611.08277v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2611.08277 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Hang Zhang [查看电子邮件]
[v1]
2026 年 11 月 5 日星期四 16:44:59 UTC（582 KB）
来源：arXiv cs.AI · arxiv.org