analiza aiqbench
This paper is a benchmark and harness for testing whether AI agents can build machine-checked proofs of real-world distributed system specifications in TLA+. The best agent proved 31 of 70 evaluated targets (44.3%), so the work shows both real capability and substantial remaining gaps in end-to-end formal verification. For AI readers, the notable points are the reward-hacking safeguards and the use of formal proofs as a checkable ground truth for agentic reasoning.
TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System
arXiv:2611.02849v1 Announce Type: new Abstract: TLAPS-Bench is a benchmark and execution harness for constructing machine-checked proofs for real-world system specifications in TLA+ with agentic AI. Proving correctness of complex system specifications requires discovering inductive invariants, reasoning about intricate state transitions, and decomposing proofs into tractable obligations. TLAPS-Bench provides a proof harness that supports iterative proof development atop the TLA+ Proof System (TLAPS), where agents are equipped with proof tools and libraries, with safeguards against reward hacking. Using the harness, we have employed AI agents to prove desired properties for important system specifications that were not proved before, spanning cache coherence, Byzantine consensus, and write-ahead logs. 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. The highest-scoring model, GPT-6.1 Sol (max), proved 31 (44.3%) proof targets. The results show challenges and opportunities in end-to-end proof development.
Abstract:TLAPS-Bench is a benchmark and execution harness for constructing machine-checked proofs for real-world system specifications in TLA+ with agentic AI. Proving correctness of complex system specifications requires discovering inductive invariants, reasoning about intricate state transitions, and decomposing proofs into tractable obligations. TLAPS-Bench provides a proof harness that supports iterative proof development atop the TLA+ Proof System (TLAPS), where agents are equipped with proof tools and libraries, with safeguards against reward hacking. Using the harness, we have employed AI agents to prove desired properties for important system specifications that were not proved before, spanning cache coherence, Byzantine consensus, and write-ahead logs. 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. The highest-scoring model, GPT-6.1 Sol (max), proved 31 (44.3%) proof targets. The results show challenges and opportunities in end-to-end proof development.
35 pages (10-page main text, references, and appendix), 7 figures, 20 tables. Benchmark and harness: this https URL
Artificial Intelligence (cs.AI); Distributed, Parallel, and Cluster Computing (cs.DC); Logic in Computer Science (cs.LO); Software Engineering (cs.SE)
arXiv:2611.02849 [cs.AI]
(or arXiv:2611.02849v1 [cs.AI] for this version)
https://doi.org/10.48550/arXiv.2611.02849 arXiv-issued DOI via DataCite (pending registration)
Text integral sub licența deschisă a publicației · 210 cuvinte
Subiecte conexe
Improving Adversarial Transferability on Vision-Language Pre-training Models via Surrogate-Specific Bias Correction
arXiv · 10 iun. 2026
Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation
arXiv · 6 iun. 2026
Semiparametric Double Reinforcement Learning with Applications to Long-Term Causal Inference
arXiv · 25 aug. 2026
From 1D Benchmarks to Complex 3D Geometries: Can Agents Reliably Specify Problems for Automated PDE Simulation?
arXiv · 2 nov. 2026