arXiv · cs.AI · Qian Cheng, Ruize Tang, Saad Mohammad Rafid Pial, Zhizhen Cathy Cai, Yiming Su, Jackson Clark, Munim Thahmid, Mahdiya Rahman Sukanya, Chris Newcombe, Igor Konnov, Stephan Merz, Xudong Sun, Murat Demirbas, Yu Huang, Markus Alexander Kuppe, Tianyin Xu · 7 小时前模型评分51
TLAPS-Bench 发布：用 人工智能（AI，Artificial Intelligence） 智能体为真实系统 TLA+ 规格做机器校验证明
TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System
导读
研究团队发布 TLAPS-Bench，这是一个面向 TLA+ 规格的机器校验证明基准与执行框架，包含来自 95 份真实系统 TLA+ 规格的 265 个证明目标，覆盖缓存一致性、拜占庭共识和预写日志。
分类置信度
中 · 待人工复核
- 存在未解决的相邻类别：ai-tooling，需要人工复核。
- 只有单一媒体来源，需要人工复核。
来源级别：媒体与个人
应用领域：科学研究
事件类型：研究发布
证据摘录
- “TLAPS-Bench is a benchmark and execution harness for constructing machine-checked proofs for real-world system specifications in TLA+ with agentic AI.”
- “TLAPS-Bench contains 265 proof targets (each encodes a property to prove) from 95 TLA+ specifications of real-world systems.”
- “We evaluated frontier AI agents, represented by Codex with GPT models, on a subset of 70 proof targets across 12 specifications.”
来源：arXiv · cs.AI · arxiv.org