主要证据
- Lean-STaR: Learning to Interleave Thinking and ProvingS1 · 主要研究来源 · 论文 · 2024-07-14
Lean-STaR 训练定理证明器交替执行非形式思考与 Lean tactic
该方法从已知 tactic 反向生成思考文本，并对新发现且验证通过的证明执行专家迭代。
发生了什么？
Lean-STaR 通过训练模型在 tactic 前生成合成的非形式思考，将 miniF2F pass@64 从 43.4% 提升到 46.3%。
为什么重要？
它探索了思维链式推理与证明助手反馈之间的直接桥接方式。
重要性说明：Lean-STaR 在形式证明步骤前显式插入学习到的非形式思考，并与专家迭代结合。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 非形式化, 形式化, 混合
- AI 贡献
- 模型同时生成非形式思考与 Lean tactic，Lean 负责验证证明状态。
- 人类贡献
- 研究者设计合成思考生成、专家迭代与评测。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- lean-star, lean
- 机构
- carnegie-mellon-university
- 数学问题
- minif2f
- 方法
- expert-iteration, synthetic-thought, lean
全部来源与工件
- Lean-STaR: Learning to Interleave Thinking and ProvingS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
验证历史
- 2024-07-14 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
更正
当前没有记录的更正。