LeanContext 基准发布：129,826 道 Lean 全证明题
热点事件持续更新
LeanContext 基准发布：129,826 道 Lean 全证明题
1 篇报道1 个报道来源10 小时前更新
先了解这件事
AI 综述
Hang Zhang 等作者发布 LeanContext，一个包含 129,826 道 Lean 全证明生成问题的基准，用于衡量目标所选声明相对同类替代声明的优势，以及这种优势对训练的依赖。 研究把所选完整前置数学声明归为数学上下文（MC），其余局部源码命令归为环境上下文（EC）。在扩散模型与自回归模型上，训练包含 MC 时所选声明的优势更大。
AI 根据报道生成 · 2 小时前更新
最新进展11月6日 13:00
LeanContext：在 Lean 全证明生成中分离数学资源与局部形式上下文报道时间线
沿着报道，了解事件的不同侧面。
11月6日
- arXiv cs.AILeanContext：在 Lean 全证明生成中分离数学资源与局部形式上下文
LeanContext 是一个包含 129,826 道 Lean 全证明生成问题的基准，用于衡量目标所选声明相对同类替代声明的优势及其对训练的依赖。研究将所选完整前置数学声明归为数学上下文（MC）、其余局部源码命令归为环境上下文（EC），在扩散模型与自回归模型上，训练包含 MC 时所选声明优势更大。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。