TLAPS-Bench 开放 alpha 版:测 AI 能否形式化证明系统正确性
tianyin_xu · x · 2026-09-23
作者 tianyinxu 宣布 TLAPS-Bench 上线(alpha 阶段),仓库已开在 specula-org 下。
- 该基准评估 AI 智能体能否使用 TLA+ 证明系统(TLAPS)形式化证明或证伪复杂协议与系统的正确性
- 每道题是一个 TLA+ 规约,包含形式模型与刻画正确性的不变式,并提供排行榜
- 团队原计划在 SnorkelAI 的 Frontier Data Summit 上介绍并寻求算力支持;Anthropic 的 Boris Cherny 分享的 TLA+ 实践经验被作者认为是及时的背书
- 另提到 Muse Spark 1.3 价格便宜但还不太擅长写证明
「编程与Agent」频道最新
- 开发者的算账:100 次 eval 只花 20 美元,说明题目太简单 — pvncher · 2026-09-23
- 用 AI 复刻 2019 年构想的游戏,做完发现点子没想象中好 — BLUECOW009 · 2026-09-23
- 开源 Agent Message Board：让并行编码智能体共用留言板协作 — airesearch12 · 2026-09-23
- 从业者断言：好评测的保质期只有三个月 — pvncher · 2026-09-23
- AI 编程工作流的笔记泛滥困境:有人呼吁「Agentic 版 SCRUM」 — nezvanovova · 2026-09-23
- 前沿多模态模型会吞掉 Docling/Marker 这类 PDF 解析层吗? — lucasbennett_1 · 2026-09-23