aiqbench analysis
This research introduces TLA+$-Bench, a rigorous dataset that evaluates large language models on generating executable formal specifications rather than relying solely on syntactic parsing or reference similarity. By grounding evaluations in actual model-checking over the full state space, it reveals massive variability—up to an elevenfold difference—in reported correctness rates depending on grading parameters like interface supply. This work fundamentally shifts how we measure progress in AI-assisted software verification by exposing that models frequently generate valid syntax without satisfying intended logical properties.
TLA$^{+}$-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation
arXiv:2607.23425v1 Announce Type: cross Abstract: Large language models increasingly write TLA$^{+}$ formal specifications from natural-language descriptions, but progress is hard to measure: existing resources grade by resemblance to a reference or by whether the output parses, neither of which shows correctness. We present TLA$^{+}$-Bench, a dataset and benchmark that grades by execution. Every gold specification ships a configuration the TLA$^{+}$ model checker runs over the full reachable state space, deciding exactly whether the specification holds the properties that configuration names. The dataset holds 403 model-checked gold and 897 parse-only silver specifications from 13 public repositories, subsumes prior TLA$^{+}$ generation data, and carries four model-written descriptions in two styles from two providers, with difficulty and category labels. Our main finding is about measurement itself: an exact oracle gives not one correctness number but a range. Varying only the grading choices earlier benchmarks leave unstated, on one fixed set of model outputs, the correct rate moves sixfold, from 10.0\% to 1.7\%; adding the interface-supply choice, where the model is told the configuration's names, widens the range to elevenfold, from 18.7\% to 1.7\%. We call this range the correctness envelope and measure each of its bounds. The findings inside it are stable. Every model writes valid TLA$^{+}$ far more often than correct TLA$^{+}$: the strongest is correct 16\% of the time by default and 26\% when given the interface names, open models at most 1\%, and correctness falls sharply with difficulty.
Authors:Arslan Bisharat, Eric Spencer, Brian Ortiz, Khushboo Bhadauria, Mujtaba Nazari, Beatriz Santos, Anisa Ramos, TaiNing Wang, George K. Thiruvathukal, Konstantin Läufer, Mohammed Abuhamad
Abstract:Large language models increasingly write TLA$^{+}$ formal specifications from natural-language descriptions, but progress is hard to measure: existing resources grade by resemblance to a reference or by whether the output parses, neither of which shows correctness. We present TLA$^{+}$-Bench, a dataset and benchmark that grades by execution. Every gold specification ships a configuration the TLA$^{+}$ model checker runs over the full reachable state space, deciding exactly whether the specification holds the properties that configuration names. The dataset holds 403 model-checked gold and 897 parse-only silver specifications from 13 public repositories, subsumes prior TLA$^{+}$ generation data, and carries four model-written descriptions in two styles from two providers, with difficulty and category labels. Our main finding is about measurement itself: an exact oracle gives not one correctness number but a range. Varying only the grading choices earlier benchmarks leave unstated, on one fixed set of model outputs, the correct rate moves sixfold, from 10.0\% to 1.7\%; adding the interface-supply choice, where the model is told the configuration's names, widens the range to elevenfold, from 18.7\% to 1.7\%. We call this range the correctness envelope and measure each of its bounds. The findings inside it are stable. Every model writes valid TLA$^{+}$ far more often than correct TLA$^{+}$: the strongest is correct 16\% of the time by default and 26\% when given the interface names, open models at most 1\%, and correctness falls sharply with difficulty.
17 pages, appendix included. Introduces TLA+-Bench, an execution-grounded benchmark and dataset for natural-language to TLA$^{+}$ specification generation. Dataset, evaluation code, and model outputs available at publication
Software Engineering (cs.SE); Artificial Intelligence (cs.AI)
arXiv:2607.23425 [cs.SE]
(or arXiv:2607.23425v1 [cs.SE] for this version)
https://doi.org/10.48550/arXiv.2607.23425 arXiv-issued DOI via DataCite (pending registration)
Full text under the publisher's open licence · 303 words
Related coverage
[AINews] OpenAI shuts off Cursor
Latent Space · Aug 29, 2026
Frontier AI Risk Report (February–March 2026)
METR · May 19, 2026
Informe de riesgos de la IA de frontera (febrero–marzo de 2026)
METR · May 19, 2026
Frontier Risk Report (February to March 2026)
METR · May 19, 2026