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 时所选声明优势更大。
正文 · 原文
Abstract:Neural theorem proving increasingly uses retrieved premises and project context to support proof generation. Evaluating these resources requires measuring the advantage of target-selected declarations over comparable alternatives and how this advantage depends on training. We introduce LeanContext, a benchmark of 129,826 Lean whole-proof generation problems, to investigate these questions. We group selected complete preceding mathematical declarations as Mathematical Context (MC) and the remaining selected local source commands as Environment Context (EC). Four aligned input views support crossed training and inference evaluations with shared targets and original Lean verification environments. For both diffusion- and autoregressive-based models, selected declarations outperform comparable alternatives by a larger margin when training includes MC. Final-input audits identify omitted declarations referenced by the target. Prioritizing these dependencies improves Pass@32 by 1.40% and 1.70% for LLaDA and Llama, respectively, on 2,000 targets. The selection experiment operates without access to target reference proofs and holds checkpoints, EC, and inference budgets constant. The code and dataset are available at this https URL.
| Subjects: | Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2611.08277 [cs.AI] |
| (or arXiv:2611.08277v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2611.08277 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Hang Zhang [view email]
[v1]
Thu, 5 Nov 2026 16:44:59 UTC (582 KB)
来源：arXiv cs.AI · arxiv.org