arXiv Artificial Intelligence· Hang Zhang, Qihao Ye, Litong Liu, Yunbei Zhang, Yugyung Lee, Yue Zhou, Bowen Liu, Emily First, Cheng Han, Qiao Zhuang·· 2 天前AI 评分26
LeanContext：在 Lean 整证明生成中分离数学资源与局部形式上下文
LeanContext: Disentangling Mathematical Resources from Local Formal Context in Lean Whole-Proof Generation
AI 导读
LeanContext 是一个包含 129,826 道 Lean 整证明生成问题的基准，用于衡量目标所选声明相对同类候选声明的优势及其对训练的依赖。研究将所选完整前置数学声明归为数学上下文（MC）、其余所选局部源码命令归为环境上下文（EC），在扩散模型和自回归模型上，训练包含 MC 时所选声明优势更大。
来源：arXiv Artificial Intelligence · arxiv.org