主要证据
- Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal ProofsS1 · 主要研究来源 · 论文 · 2022-10-21
- Draft, Sketch, and Prove implementation and result artifactsS1 · 主要研究来源 · 代码仓库
Draft, Sketch, and Prove 用非形式证明引导形式证明搜索
语言模型先生成高层形式证明草图，再由自动证明器完成其中的子目标。
发生了什么？
DSP 将非形式证明映射为形式 proof sketch，并在一组竞赛题上把自动证明性能从 20.9% 提升到 39.3%。
为什么重要？
该架构预示了后来“自然语言分解 + 验证器支持的形式证明”交替执行的系统。
重要性说明：DSP 将非形式推理显式作为语言模型与形式定理证明器之间的中间表示。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 非形式化, 形式化, 混合
- AI 贡献
- 语言模型负责起草和构造证明结构，形式证明器验证并完成子问题。
- 人类贡献
- 研究者设计三阶段工作流、评测问题与提示流程。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- draft-sketch-prove
- 机构
- meta-ai, university-of-cambridge
- 数学问题
- competition-mathematics
- 方法
- autoformalization, proof-sketch, language-model
全部来源与工件
- Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal ProofsS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- Draft, Sketch, and Prove implementation and result artifactsS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2022-10-21 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。