Agent 自主生成形式化验证求解器
burny_tech · x · 2026-07-18
Lanyon 生成了一个端到端形式化验证的 PDE 求解器，覆盖线性平流、各向同性平流-扩散以及完整/各向异性平流-扩散方程。
- 规模：约 8,000 行经验证的仿真代码 + 10,000 行 Lean 4 证明
- 耗时：约 158 秒完成
- 结果：对二维到三维的多种方程，都给出了每一项性质的正确性证明
作者强调，这是首个针对平流-扩散方程的端到端形式化验证求解器，完全由 agent 自主生成。
「编程与Agent」频道最新
- 开发者观点:前沿模型需要验证自身成功的方式,否则会自行编造 — daniel_mac8 · 2026-09-11
- 别让 AI 自造成功标准:给它可验证目标才好用 — daniel_mac8 · 2026-09-11
- 从聊天到 Agent,推理延迟正在成为生产级瓶颈 — Euphoric_Sea632 · 2026-09-11
- Anthropic 研究员:99% 工程师已跑 300+ 自改进 agent 群 — AlishaOutridge · 2026-09-11
- Gergely Orosz 观察:AI Agent 提速十倍交付,却带来一堆小退化 — ducha_aiki · 2026-09-11
- 同题 Echo Maze 实测:三大模型看似成功,代码里藏着同一个 bug — eyishazyer · 2026-09-11