Pith. sign in

REVIEW 2 major objections 5 minor 39 references

An exact model-checker oracle for natural-language to TLA+ generation does not yield one correctness number but a range spanning elevenfold, from 18.7% down to 1.7%.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-30 22:34 UTC pith:JJ6A6DLN

load-bearing objection Real methodological contribution on how exact oracles still leave a wide correctness range; the 1.7%/elevenfold floor is partly scoring convention, but the qualitative claim and the resource hold up. the 2 major comments →

arxiv 2607.23425 v1 pith:JJ6A6DLN submitted 2026-07-26 cs.SE cs.AI

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
show 3 more authors
George K. Thiruvathukal Konstantin L\"aufer Mohammed Abuhamad
This is my paper
classification cs.SE cs.AI
keywords benchmarkdatasetformal specificationTLA+model checkinglarge language modelsexecution-grounded evaluationcode generation
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Large language models are being asked to write TLA+ formal specifications from plain-language descriptions, but prior benchmarks score them by surface resemblance or by whether the output merely parses. This paper releases TLA+-Bench: hundreds of real specifications paired with runnable model-checking configurations so that a generated module is graded by walking its full reachable state space. The central result is about measurement itself. On one fixed set of model outputs, the three grading choices earlier work leaves unstated move the pooled correct rate sixfold; telling the model the interface names widens the span to elevenfold. Inside that range the picture is stable: every model produces valid TLA+ far more often than correct TLA+, open models stay near zero, and correctness collapses once problems leave the easiest tier.

Core claim

An exact oracle does not settle correctness on its own. The same frontier-model outputs admit a correctness envelope from 18.7% (interface names supplied) through 10.0% (default recovery) and 4.0% (behavior must be exercised) down to 1.7% (named property must be load-bearing). Inside the envelope every model is far better at valid than correct TLA+: the strongest reaches 16% by default and 26% with names given, open models at most 1%, and correctness falls from roughly 25% on basic specs to 2% on harder ones.

What carries the argument

The correctness envelope: the measured span of defensible correct rates obtained by making explicit the interface-supply choice and the two vacuity screens (substantive multi-state behavioral pass; mutation of named safety invariants to TRUE) that prior single-number benchmarks leave silent.

Load-bearing premise

That satisfying the properties named by a fixed reference configuration the model did not write is the right operational meaning of “correct” for this generation task.

What would settle it

Re-grade the released 300 frontier outputs under a reference-varying behavioral gate (perturb the gold properties or constants and demand the checker detect the change); if the envelope collapses to a single stable rate near the default figure, the measurement claim fails.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • A parse-only or resemblance-only benchmark for NL-to-TLA+ will badly overstate capability relative to full-state-space checking.
  • Resource builders who grade executable artifacts should report a range over interface and vacuity choices rather than one silent number.
  • Frontier models still top out near 26% even when interface names are handed to them, so interface recovery is only part of the gap.
  • Difficulty stratification is essential: pooled rates hide a cliff from basic to intermediate/advanced specs.
  • The released gold configurations, fixture flags, and model outputs let others recompute every envelope bound without re-querying models.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same three silent choices (which instances count, how much interface must be recovered, whether a pass must check anything) likely inflate reported rates in NL-to-SQL and code-generation benches that use fixed harnesses.
  • Configuration-binding as the dominant failure mode suggests future generators may gain more from interface-aligned decoding or two-stage name binding than from raw scale alone.
  • Shipping paired name-revealing and name-hidden descriptions turns identifier leakage into a controllable experimental axis for any public-code corpus evaluation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper introduces TLA+-Bench, a corpus of 1,300 TLA+ specifications (403 model-checked gold, 897 parse-only silver) from 13 public repositories, each with four model-written descriptions (two styles × two providers), difficulty labels, and runnable TLC configurations for the gold tier. Six LLMs are evaluated on a 100-specification evaluation set (gold system category minus 46 flagged trivial fixtures), graded by SANY parse plus TLC model check against the fixed reference configuration. The central claim is the "correctness envelope": on one fixed set of 300 frontier-model outputs, the pooled correct rate moves sixfold under grading-only changes (10.0% default → 4.0% substantive → 1.7% mutation-surviving), and elevenfold (18.7% → 1.7%) when the configuration-aware regime, a separate generation set with interface names supplied, is included. Within the envelope: all models are far more often valid than correct, open models score ≤1% correct, and correctness collapses from 25% (basic) to 2% (intermediate/advanced). Configuration-binding dominates the checker-grounded failure taxonomy. The paper is notably transparent about scope limits: property-scoped oracle, single sample per spec, non-uniform decoding, non-blind author-team audits.

Significance. If the numbers hold, this is a useful datasets-and-benchmarks contribution with an unusual degree of methodological self-awareness. Strengths worth naming: every gold reference is SANY+TLC validated before inclusion; the grader is frozen and deterministic with a stated tie-break; model outputs are released so the default/substantive/mutation rows of Table 5 can be recomputed without re-querying any model; the configuration-aware bound is generated from released runnable configurations; trivial fixtures are flagged rather than silently dropped; and failure categories come from checker output, not inferred labels. The correctness-envelope framing — that an exact oracle yields a range of defensible rates, not one number — is a genuinely transferable point for execution-graded benchmarks. The internal findings (valid ≫ correct; difficulty cliff backed by κ≈0.8 IAA plus a construct-derived robustness check) are stable and appropriately hedged for n=100.

major comments (2)
  1. [§8.7 / §8.2 / Abstract] The envelope floor of 1.7% (5/300) is constructed by counting 12 of the 30 default-regime passes as non-surviving without any test, because their configurations name temporal properties with no mutable safety invariant. Only 18 passes were actually mutated, of which 5 survive. The true mutation floor therefore lies in [5/300, 17/300] = [1.7%, 5.7%], and if half the untested temporal passes are non-vacuous the headline range shrinks from elevenfold to roughly fivefold. §8.7 does disclose this ('scored against the rate rather than excluded... a conservative lower bound'), but the abstract, §1 contribution ❹, and Table 5 present 1.7% and 'elevenfold' as measured bounds on the same footing as the other rows. Request: add an upper-bound row or explicit range to Table 5, hedge the abstract/intro phrasing, or extend the probe to temporal properties so the floor is measured rather than assigned
  2. [§8.7] The survival criterion — 'replace every checked safety invariant named by the configuration with TRUE and re-run TLC; a pass survives when the mutated run still fails' — is under-specified for multi-property configurations. When a configuration names several invariants plus a temporal property, mutating all invariants at once means the mutated run can still fail only via another property (e.g., the temporal one), so 'survival' re-tests that property rather than establishing that the mutated invariant was load-bearing. Please state whether mutation is joint or per-invariant, and which property's failure counts as survival; per-invariant single mutations would give a cleaner attribution and are cheap at n=18.
minor comments (5)
  1. [Table 2] Table 2 legend renders as glyph soup ('/check-circleYes,/adjus◎Partial,/times-circleNo'); check the macro definitions before camera-ready.
  2. [§5 vs §8.7] §5 says the mutation bound 'acts on the safety-invariant subset of these 291', while §8.7 says temporal-only passes are counted as non-surviving rather than excluded. These phrasings describe the same rule differently; align them.
  3. [§8.2 / Table 5] The substantive and mutation rows reclassify the same 30 passes, so the envelope rates are paired, not independent. A paired (McNemar-style) comparison would be more informative than the per-row binomial intervals quoted in §8.3/§9, particularly for the 4.0% vs 1.7% gap (12 vs 5 passes).
  4. [Table 6] Table 6 reports only percentages; the underlying counts (4, 10, 16 correct) appear only in Table A4. Add counts to Table 6 or cross-reference, since small-count rows (e.g., GPT-5 4%) deserve visible denominators.
  5. [Appendix A11] Appendix A11 discloses that the exact GPT-5 description prompts were not recorded and are reconstructed. Since GPT-5 declarative descriptions are the evaluation input, consider archiving the release scripts' prompt templates verbatim going forward; the archived descriptions themselves make the current evaluation reproducible, so this is process feedback only.

Circularity Check

1 steps flagged

No load-bearing circularity: correctness is external TLC on third-party specs; FormalLM self-citation is disclosed and not used to force the envelope.

specific steps
  1. self citation load bearing [Section 2.2; Table 1]
    "The closest prior benchmark for natural-language to TLA+ generation is FormalLM [5], which is our own earlier benchmark; we state the delta explicitly rather than let the overlap be discovered. FormalLM derives descriptions from code comments, grades without an exact oracle, and is drawn entirely from the TLA+ Examples corpus with no specifications of its own."

    Minor only: the corpus nests the authors’ prior FormalLM set, so provenance is partly self-referential. It is not load-bearing for the envelope—the envelope is measured by TLC on new model outputs against gold configs, not by reusing FormalLM grades—so this does not force the main result.

full rationale

TLA+-Bench’s central claim—the correctness envelope—is an empirical measurement over fixed model outputs graded by SANY/TLC against reference configurations shipped with public third-party specifications. The rates (18.7% → 10.0% → 4.0% → 1.7%) are not fitted parameters renamed as predictions, nor quantities defined in terms of themselves. FormalLM [5] is the authors’ prior benchmark and is nested inside the corpus (Table 1), but the paper states the delta explicitly and does not treat FormalLM scores as proof of the envelope; the envelope is recomputed on new generations with an exact checker. GPT-5 is graded on GPT-5-written declarative descriptions—a mild self-description coupling—but the paper notes GPT-5 ranks lowest among frontier models, which undercuts any self-advantage story. Difficulty labels are author-assigned, yet defended by IAA and a construct-derived robustness check rather than by defining difficulty as the outcome. Methodological conservatism in the mutation floor (temporal-only passes scored non-surviving without a test) is a scoring-convention issue, not circular reduction of a derivation to its inputs. Overall this is an external-oracle benchmark paper with ordinary, non-load-bearing self-citation.

Axiom & Free-Parameter Ledger

4 free parameters · 6 axioms · 2 invented entities

Empirical systems paper: no fitted physical constants. Load-bearing commitments are domain assumptions about what TLC+reference-config decides, construction filters, and evaluation protocol choices (description source, single sample, fixture prune). No new physical entities; the ‘correctness envelope’ is a named measurement construct over existing checker outcomes, not an invented ontological object.

free parameters (4)
  • TLC wall-clock budget (300s) and SANY bound (60s) = 300s TLC / 60s SANY
    Resource-limit failure category and some pass/fail outcomes depend on this hand-chosen compute budget; paper notes slower hardware can reclassify runs.
  • Difficulty rubric tier cutoffs (basic/intermediate/advanced) = 3-tier rubric keyed to TLA+ construct depth
    Author-assigned construct-depth tiers drive the correctness-cliff claim; defended by IAA and a mechanical proxy but still a human coding scheme.
  • Description length guidance (provider-specific) = 80–120 (GPT-5 recon.) / 120–220 (Claude)
    Claude 120–220 words vs reconstructed GPT-5 80–120 words; confounds the shipped provider axis with prompt wording.
  • Generation token budget and decoding defaults = 16000 tokens; mixed temperatures
    16k token budget; temperature 0 only for Gemini; other models at provider defaults—confounds cross-model comparison.
axioms (6)
  • domain assumption TLC exploring the full reachable state space of a reference configuration decides property satisfaction exactly for that config and its bound constants (not general correctness or behavioral equivalence to the reference module).
    Stated in Sections 2.1, 3, 6; entire semantic gate rests on it.
  • ad hoc to paper A generated module is ‘correct’ when it SANY-parses and TLC reports no violation of the properties the fixed reference configuration names.
    Task definition in Section 3; this operationalization is the paper’s grading contract, not a theorem of TLA+.
  • domain assumption Model-written declarative descriptions (GPT-5), after a non-blind faithfulness audit (~83% fully faithful on the eval set), are adequate evaluation inputs for measuring NL-to-TLA+ capability.
    Section 6 audit + Section 9 limitation that descriptions are not practitioner-elicited.
  • ad hoc to paper Trivial fixtures (single reachable state) should be excluded from headline rates because they pass for every model; flags leave the choice open.
    Section 8.1 filter removing 46 of 146 system gold specs; fourth grading choice outside Table 5.
  • domain assumption Substantive-pass and mutation-to-TRUE probes are valid lower-bound screens for vacuous passes (temporal-only configs scored non-surviving under mutation).
    Section 8.7; grounded in classical vacuity literature [4,17] but the scoring rule for temporal-only passes is a paper-specific conservative choice.
  • standard math Public third-party TLA+ repository modules under redistributable licenses are legitimate benchmark instances when released unchanged with provenance and checksums.
    Standard dataset-construction assumption; Appendix A1/A4.
invented entities (2)
  • Correctness envelope independent evidence
    purpose: Name and jointly measure the range of defensible correct rates under interface-supply and vacuity/behavior grading regimes on the same task.
    Core conceptual contribution (Section 8.2). It is a measurement construct over checker outcomes, not a new physical or formal object; independent_evidence is effectively true because bounds are recomputable from released outputs.
  • Gold vs silver quality tiers independent evidence
    purpose: Separate model-checkable specs (semantic gate) from parse-only specs (scale and future promotion).
    Dataset structure choice (Section 3–4); standard tiering, not an ontological postulate.

pith-pipeline@v1.2.0-grok45-kimik3 · 28697 in / 4301 out tokens · 87848 ms · 2026-07-30T22:34:21.410999+00:00 · methodology

0 comments
read the original 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.

Figures

Figures reproduced from arXiv: 2607.23425 by Anisa Ramos, Arslan Bisharat, Beatriz Santos, Brian Ortiz, Eric Spencer, George K. Thiruvathukal, Khushboo Bhadauria, Konstantin L\"aufer, Mohammed Abuhamad, Mujtaba Nazari, TaiNing Wang.

Figure 1
Figure 1. Figure 1: A worked example (full reference in Appendix A6). [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

39 extracted references · 20 linked inside Pith

  1. [1]

    Anthropic. 2025. Claude Opus 4.5. https://www.anthropic.com/news/claude- opus-4-5

    2025

  2. [2]

    Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, and Charles Sutton. 2021. Program Synthesis with Large Language Models.arXiv preprint arXiv:2108.07732(2021)

    Pith/arXiv arXiv 2021

  3. [3]

    Ayers, Dragomir Radev, and Jeremy Avigad

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. 2023. ProofNet: Autoformalizing and For- mally Proving Undergraduate-Level Mathematics.arXiv preprint arXiv:2302.12433 (2023)

    Pith/arXiv arXiv 2023

  4. [4]

    Ilan Beer, Shoham Ben-David, Cindy Eisner, and Yoav Rodeh. 2001. Efficient Detection of Vacuity in Temporal Model Checking.Formal Methods in System Design18, 2 (2001), 141–163

    2001

  5. [5]

    Thiruvathukal, Konstantin Läufer, and Mohammed Abuhamad

    Arslan Bisharat, Brian Ortiz, Eric Spencer, Khushboo Bhadauria, TaiNing Wang, George K. Thiruvathukal, Konstantin Läufer, and Mohammed Abuhamad. 2026. Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language- to-TLA+ Generation. InProceedings of the International Conference on Software Technologies (ICSOFT)

    2026

  6. [6]

    Thiruvathukal, Kon- stantin Läufer, and Mohammed Abuhamad

    Arslan Bisharat, Eric Spencer, Brian Ortiz, Khushboo Bhadauria, Mujtaba Nazari, Beatriz Santos, Anisa Ramos, TaiNing Wang, George K. Thiruvathukal, Kon- stantin Läufer, and Mohammed Abuhamad. 2026.TLA+-Bench: An Execution- Grounded Dataset for Natural-Language to TLA+ Specification Generation. doi:10 .5281/zenodo.21310317

    2026

  7. [7]

    Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. 2021. Evaluating Large Language Models Trained on Code.arXiv preprint arXiv:2107.03374(2021)

    Pith/arXiv arXiv 2021

  8. [8]

    Qian Cheng, Ruize Tang, Emilie Ma, Finn Hackett, Peiyang He, Yiming Su, Ivan Beschastnikh, Yu Huang, Xiaoxing Ma, and Tianyin Xu. 2025. SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems.arXiv preprint arXiv:2509.23130(2025). ICLR 2026

    arXiv 2025

  9. [9]

    Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. 2023. nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models. InComputer Aided Verification (CA V)

    2023

  10. [10]

    Yihong Dong, Xue Jiang, Huanyu Liu, Zhi Jin, Bin Gu, Mengfei Yang, and Ge Li

  11. [11]

    Timnit Gebru, Jamie Morgenstern, Briana Vecchione, Jennifer Wortman Vaughan, Hanna Wallach, Hal Daumé III, and Kate Crawford. 2021. Datasheets for Datasets. Commun. ACM64, 12 (2021), 86–92. doi:10.1145/3458723

    doi:10.1145/3458723 2021

  12. [12]

    Google DeepMind. 2025. Gemini 2.5: Pushing the Frontier with Advanced Rea- soning, Multimodality, Long Context, and Next Generation Agentic Capabilities. https://deepmind.google/technologies/gemini/

    2025

  13. [13]

    Aaron Grattafiori, Abhimanyu Dubey, et al. 2024. The Llama 3 Herd of Models. arXiv:2407.21783

    Pith/arXiv arXiv 2024

  14. [14]

    Binyuan Hui, Jian Yang, Zeyu Cui, et al. 2024. Qwen2.5-Coder Technical Report. arXiv:2409.12186

    Pith/arXiv arXiv 2024

  15. [15]

    Naman Jain, King Han, Alex Gu, Wen-Ding Li, Fanjia Yan, Tianjun Zhang, Sida Wang, Armando Solar-Lezama, Koushik Sen, and Ion Stoica. 2025. Live- CodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code. InInternational Conference on Learning Representations (ICLR). arXiv:2403.07974

    Pith/arXiv arXiv 2025

  16. [16]

    Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan

    Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan. 2024. SWE-bench: Can Language Models Resolve Real- World GitHub Issues?. InInternational Conference on Learning Representations (ICLR). arXiv:2310.06770

    Pith/arXiv arXiv 2024

  17. [17]

    Orna Kupferman and Moshe Y. Vardi. 2003. Vacuity Detection in Temporal Model Checking.International Journal on Software Tools for Technology Transfer (STTT) 4, 2 (2003), 224–233

    2003

  18. [18]

    2002.Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers

    Leslie Lamport. 2002.Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley

    2002

  19. [19]

    Cuong Chi Le, Minh V. T. Pham, Cuong Duc Van, Hoang N. Phan, Huy N. Phan, and Tien N. Nguyen. 2025. When Names Disappear: Revealing What LLMs Actually Understand About Code.arXiv preprint arXiv:2510.03178(2025)

    arXiv 2025

  20. [20]

    Thanh Le-Cong, Bach Le, and Toby Murray. 2025. Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast.arXiv preprint arXiv:2503.04779(2025). FormalBench

    Pith/arXiv arXiv 2025

  21. [21]

    Jiawei Liu, Chunqiu Steven Xia, Yuyao Wang, and Lingming Zhang. 2023. Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Lan- guage Models for Code Generation. InAdvances in Neural Information Processing Systems (NeurIPS). arXiv:2305.01210

    Pith/arXiv arXiv 2023

  22. [22]

    Jason Xinyu Liu, Ziyi Yang, Ifrah Idrees, Sam Liang, Benjamin Schornstein, Stefanie Tellex, and Ankit Shah. 2023. Translating Natural Language to Linear Temporal Logic with Large Language Models. InRobotics: Science and Systems (RSS)

    2023

  23. [23]

    Xinyu Liu, Shuyu Shen, Boyan Li, Nan Tang, and Yuyu Luo. 2025. NL2SQL- BUGs: A Benchmark for Detecting Semantic Errors in NL2SQL Translation. In Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining (KDD). doi:10.1145/3711896.3737427

    arXiv 2025

  24. [24]

    Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark. 2024. DafnyBench: A Benchmark for Formal Software Verification. arXiv preprint arXiv:2406.08467(2024)

    Pith/arXiv arXiv 2024

  25. [25]

    Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. In International Conference on Software Engineering (ICSE)

    2025

  26. [26]

    OpenAI. 2025. GPT-5 System Card. https://openai.com/index/gpt-5/

    2025

  27. [27]

    OpenAI. 2025. gpt-oss-120b and gpt-oss-20b Model Card. https://openai.com/ind ex/gpt-oss/

    2025

  28. [28]

    Kun Qian, Shunji Wan, Claudia Tang, Youzhi Wang, Xuanming Zhang, Maximil- lian Chen, and Zhou Yu. 2024. VarBench: Robust Language Model Benchmarking Through Dynamic Variable Perturbation.arXiv preprint arXiv:2406.17681(2024)

    Pith/arXiv arXiv 2024

  29. [29]

    Musfiqur Rahman, SayedHassan Khatoonabadi, and Emad Shihab. 2026. Open- ClassGen: A Large-Scale Corpus of Real-World Python Classes for LLM Research. InInternational Conference on Evaluation and Assessment in Software Engineering (EASE). arXiv:2504.15564

    Pith/arXiv arXiv 2026

  30. [30]

    Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. 2023. Clover: Closed- Loop Verifiable Code Generation.arXiv preprint arXiv:2310.17807(2023)

    Pith/arXiv arXiv 2023

  31. [31]

    Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, and Tiancheng Zhang. 2025. Autoformalization in the Era of Large Language Models: A Survey. arXiv preprint arXiv:2505.23486(2025)

    Pith/arXiv arXiv 2025

  32. [32]

    Colin White, Samuel Dooley, Manley Roberts, Arka Pal, Ben Feuer, Siddhartha Jain, Ravid Shwartz-Ziv, Neel Jain, Khalid Saifullah, Sreemanti Dey, Shubh Agrawal, Sandeep Singh Sandha, Siddartha Naidu, Chinmay Hegde, Yann LeCun, Tom Goldstein, Willie Neiswanger, and Micah Goldblum. 2025. LiveBench: A Challenging, Contamination-Limited LLM Benchmark. InIntern...

    Pith/arXiv arXiv 2025

  33. [33]

    Jiang, Wenda Li, Markus N

    Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with Large Language Models. InAdvances in Neural Information Processing Systems (NeurIPS)

    2022

  34. [34]

    Cheng Xu, Shuhao Guan, Derek Greene, and M-Tahar Kechadi. 2024. Bench- mark Data Contamination of Large Language Models: A Survey.arXiv preprint arXiv:2406.04244(2024)

    Pith/arXiv arXiv 2024

  35. [35]

    Dong Xu, Jialun Cao, et al. 2026. LiveFMBench: Benchmarking Formal Methods Reasoning of Large Language Models on Live Verification Tasks.arXiv preprint arXiv:2605.01394(2026)

    Pith/arXiv arXiv 2026

  36. [36]

    Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shix- ing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar

    Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shix- ing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. InAdvances in Neural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track. arXiv:2306.15626

    Pith/arXiv arXiv 2023

  37. [37]

    Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, and Dawn Song. 2026. VERINA: Benchmarking Verifiable Code Generation. InInternational Conference on Learning Representations (ICLR). arXiv:2505.23135

    arXiv 2026

  38. [38]

    {description}

    Hugh Zhang, Jeff Da, Dean Lee, Vaughn Robinson, Catherine Wu, Will Song, Tiffany Zhao, Pranav Raja, Charlotte Zhuang, Dylan Slack, Qin Lyu, Sean Hendryx, Russell Kaplan, Michele Lunati, and Summer Yue. 2024. A Careful Examination of Large Language Model Performance on Grade School Arithmetic. InAdvances in Neural Information Processing Systems (NeurIPS), ...

    Pith/arXiv arXiv 2024

  39. [2024]

    ACL 2024

    Generalization or Memorization: Data Contamination and Trustworthy Evaluation for Large Language Models.arXiv preprint arXiv:2402.15938(2024). ACL 2024

    Pith/arXiv arXiv 2024