TLAPS-Bench 发布:265 个真实系统证明目标,GPT-6.1 Sol 仅解出 44.3%
tianyin_xu · x · 2026-11-04
Murat Demirbas 发布 TLAPS-Bench,一个面向 agentic AI 的 TLA+ 形式化证明基准(与 Tianyin Xu 等合著,arXiv 2611.02849)。
- 基准含 265 个证明目标,来自 95 个真实世界系统的 TLA+ 规约,覆盖缓存一致性、拜占庭共识、write-ahead log 等此前未被证明过的性质
- 提供配套 proof harness:支持迭代式证明开发,为 agent 配备证明工具与库,并设有防 reward hacking 的保障机制
- 在 70 个目标、12 个规约的子集上评测前沿模型:最高的 GPT-6.1 Sol (max) 通过 pass@3 证明 31/70(44.3%) 个目标,并发现 46 个 bug
- 结论:机器检验正确性证明对当前 AI agent 仍是重大挑战,但也展示了明确的机会空间
论文与代码均已开源。
「编程与Agent」频道最新
- Shopify CEO 点赞：AI 助手 Tomo 用 Shop Pay 自主购物 — Jackyhuang · 2026-11-04
- Stripe 招兵买马，布局 agentic commerce 支付基础设施 — jeff_weinstein · 2026-11-04
- Xai 工程师 Yacine:AI 在我睡觉时自主干活,每天早晨都有突破 — yacineMTB · 2026-11-04
- 单卡 RTX PRO 6000 跑 8 个编码 agent，实测吞吐数据出炉 — AIFlow_ML · 2026-11-04
- 一套 AI 对话戏完整工作流：从剧本分镜到 1080p 成片 — DavidmComfort · 2026-11-04
- Agent37 推出月租 4.76 美元沙盒，价格仅为 Vercel 的 2% — rohanpaul_ai · 2026-11-04