OpenAI 数学证明智能体是否在推理时调用 Lean 验证器？
yoavgo · x · 2026-09-27
Yoav Goldberg 提出一个技术悬而未决的问题：OpenAI 等家的数学证明 agent 在运行时，是否在一个每隔几步就调用 Lean 形式化验证器的 harness 中工作，还是 Lean 主要用于训练阶段、推理时只依赖学到的行为？他倾向于前者，但目前没有公开答案。这关系到形式验证在 agent 工作流中是训练信号还是运行时保障。
「编程与Agent」频道最新
- Gary Bernhardt:汇编永远不适合当 agent 语言 — mgill25 · 2026-09-27
- OpenAI L7 工程师称做不了出站 IP 白名单 VLAN，专家指 IP 白名单已失效 — arthurcolle · 2026-09-27
- 用 Claude Code 打造代码渲染 MV《I'm Upping My P(doom)》 — SonglinYang4 · 2026-09-27
- 「Plan 模式已死」引热议:计划没消失,只是变成了没人记得的决策日志 — optima-pacifist · 2026-09-27
- 黑客松冠军：4000 次 Jev 判断只花 1.3 美元的生态模拟 — schwentker · 2026-09-27
- 一夜醒来 1500 个 agent PR，CodeRabbit 用 Triage 按风险排序救场 — schwentker · 2026-09-27