TLA$^{+}$-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation
Arslan Bisharat, Eric Spencer, Brian Ortiz, Khushboo Bhadauria, Mujtaba Nazari, Beatriz Santos, Anisa Ramos, TaiNing Wang, George K. Thiruvathukal, Konstantin L\"aufer, Mohammed Abuhamad
Why It Matters
What makes this one worth your time
This work provides a more rigorous method for evaluating the correctness of formal specifications generated by language models, which is crucial for ensuring reliability in software engineering applications.
TLA$^{+}$-Bench offers an execution-grounded benchmark for evaluating natural-language to TLA+ specification generation.
Summary
The paper introduces TLA$^{+}$-Bench, a benchmark and dataset for evaluating the generation of TLA$^{+}$ specifications from natural language by large language models. It emphasizes execution-based grading to assess correctness, presenting a 'correctness envelope' that varies based on grading choices and interface information. The dataset includes 403 model-checked gold and 897 parse-only silver specifications.
Key contributions
- Introduction of TLA$^{+}$-Bench, a new benchmark and dataset for TLA+ specification generation.
- Demonstration of the variability in correctness assessment through the 'correctness envelope'.
- Provision of a dataset with model-checked gold and parse-only silver specifications.
Notable insights
- The concept of a 'correctness envelope' highlights the variability in correctness assessment based on grading criteria and interface information.
- Execution-based grading offers a more precise measure of specification correctness compared to resemblance or parsing checks.
Possible limitations
- Not stated in the abstract
Abstract
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.