主要证据
- Baldur: Whole-Proof Generation and Repair with Large Language ModelsS1 · 主要研究来源 · 论文 · 2023-03-08
- Baldur: Whole-Proof Generation and Repair with Large Language ModelsS1 · 主要研究来源 · 其他来源 · 2023-12-06
Baldur 使用语言模型生成并修复完整形式证明
与逐步预测证明动作并搜索后续路径不同，Baldur 微调语言模型一次生成完整证明；随后由独立的修复模型读取失败证明及证明助手的错误反馈，再提出修正后的证明。
发生了什么？
在包含 6,336 个 Isabelle/HOL 定理的基准上，Baldur 生成完整证明并修复失败结果；论文报告它相较 Thor 额外证明了 8.7% 的定理，而 Baldur 与 Thor 合计可全自动证明 65.7%。
为什么重要？
该工作使完整证明合成与反馈驱动修复成为可信的形式推理模式，补充了依赖搜索的定理证明路线，并预示了后来常见的“生成—检查—修订”工作流。
重要性说明：Baldur 将“完整证明生成 + 检查器反馈修复”确立为逐步形式证明搜索之外的一条独立路线，展示 Transformer 可以一次生成完整 Isabelle/HOL 证明，并利用失败证明与错误信息进行修复。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 主导、人类核验
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号, 混合
- AI 贡献
- 微调后的语言模型生成完整候选证明，并根据检查器反馈修复失败尝试；Isabelle/HOL 对最终证明文本进行机械接受或拒绝。
- 人类贡献
- 研究者设计完整证明与修复训练方案、构建评测流程、训练模型，并分析其相对既有定理证明系统的表现。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-11
技术细节
- 系统
- baldur, isabelle-hol
- 机构
- —
- 数学问题
- automated-theorem-proving
- 方法
- whole-proof-generation, proof-repair, language-models, proof-assistant-feedback
全部来源与工件
- Baldur: Whole-Proof Generation and Repair with Large Language ModelsS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- Baldur: Whole-Proof Generation and Repair with Large Language ModelsS1 · 主要研究来源 · 其他来源 · 访问于 2026-09-11
验证历史
- 2023-03-08 · 论文已发布 · E2 · 研究记录
公开研究记录报告了完整证明生成、修复方法及 Isabelle/HOL 评测。该状态仅记录论文已公开，不表示 Chronicle 已独立验证，也不表示存在可公开重放的完整产物。
更正
当前没有记录的更正。