Pith. sign in

REVIEW 4 major objections 5 minor 63 references

LLM-based Satisfiability Checking of String Requirements by Consistent Data and Checker Generation

T0 review · 4 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read LLM-written checkers nearly double correct string-requirement results

desk verdict A solid empirical systems paper whose headline claim overreaches: the checkers are evaluated, not verified, so the real contribution is the demonstrated relative improvement, not the soundness guarantee. read the letter →

arxiv 2506.16639 v1 pith:242KCTUG submitted 2025-06-19 cs.SE

Boqi Chen , Aren A. Babikian , Shuzhao Feng , Dániel Varró , Gunter Mussbacher This is my paper · ORCID
classification cs.SE
keywords satisfiabilitycheckingnaturallanguagerequirementsstringconstraintslargemodelscheckergenerationtestdataSMTsolversfeedbackloop
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper claims that natural-language requirements over strings can be automatically checked for satisfiability without manual formalization by splitting the job between two roles for large language models: one role proposes a verdict (satisfiable with a witness string, or unsatisfiable), and the other generates checker programs that validate the proposal. The checkers come in two forms, SMT constraints for proving unsatisfiability and Python functions for checking concrete strings, and the approach feeds counterexamples and explanations back into the proposer until a budget runs out, then returns the closest-to-sound outcome. If correct, this makes requirements analysis feasible for non-experts and produces realistic test strings as a side effect, instead of demanding hand-built formal specifications. The experiments compare four LLMs on 340 requirement sets and show the hybrid feedback loop more than doubles generation success and F1 in some cases compared to direct LLM answering, approaching ground-truth-checker performance end to end.

What carries the argument

The load-bearing object is the verification-outcome checker: a process that takes the natural-language requirements plus a proposed SAT or UNSAT outcome and validates the proposal. Two concrete kinds are generated by LLMs: declarative checkers expressed as SMT constraints, which can establish unsatisfiability, and imperative checkers as Python functions, which can verify that a concrete string satisfies each requirement but cannot prove unsatisfiability. The argument is carried by a divide-and-conquer checker generator that splits requirements into batches and evaluates each checker syntactically and semantically, combined with a budget-limited verifier that iteratively repairs rejected outcomes through a feedback loop and falls back to the best saved outcome when the budget is exhausted.

What would settle it

Run the end-to-end system on a dataset where every requirement set has an independently written, human-audited ground-truth checker, and count how often the pipeline's returned verdict differs from the audited verdict; any agreed-but-wrong case in which the generated checker passes its ten test samples but contradicts the ground truth would falsify the central claim.

Watch

Extended reading notes

Core claim

The central claim is that a hybrid pipeline, in which an LLM derives a satisfiability outcome (SAT with a witness string, or UNSAT) and also generates declarative and imperative checkers for the same natural-language requirements, verifies string requirements more reliably than asking the LLM directly. In the evaluation over 340 requirement sets drawn from twelve textual categories, the generated checkers substantially improve both generation success rate and verification F1-score over the no-checker baseline, with certain cases more than doubling both metrics. End-to-end runs that use LLM-generated checkers approach the upper bound set by ground-truth checkers: generation success rate ratios above 95% in three verifiers and F1-score ratios up to about 88%. The approach degrades gracefully when no sound outcome is found within budget, returning the closest-to-sound saved outcome rather than refusing to answer.

Load-bearing premise

The whole pipeline rests on the assumption that an LLM-generated checker that passes syntax parsing and a small set of hand-built test samples actually encodes the requirement correctly; if the checker and the proposed answer share the same misunderstanding, they can silently agree on a wrong SAT or UNSAT verdict, a failure mode the paper itself identifies as critical.

Editorial extensions

If this is right

  • When no sound SAT or UNSAT verdict is found within budget, the system returns the closest-to-sound outcome (~SAT or ~UNSAT) instead of failing, keeping it usable in interactive workflows.
  • Three of the four evaluated LLMs achieved perfect testing accuracy on generated Python checkers, so imperative checkers are a reliable way to validate concrete strings, while SMT checkers remain the only path for validating UNSAT claims.
  • The hybrid checker configuration (Python for strings, SMT for UNSAT) with counterexample-plus-explanation feedback produced the best results, with GSR between 57.24% and 92.23% and F1 between 82.59% and 93.04% across LLMs in the ground-truth-checker setting.
  • End-to-end, using LLM-generated checkers, generation success rate ratios exceeded 95% of the ground-truth-checker bound in three verifiers, and F1 ratios reached up to about 88%.
  • Assessing each requirement independently (the IND batching method) consistently improved checker soundness over batched generation, with especially large gains for smaller LLMs.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper: the same checker-validated feedback loop should extend to any domain with a formalizable checker language, such as the numeric traffic-scenario requirements the authors mention for autonomous vehicles; the practical bottleneck would be generating trustworthy checkers, not the loop itself.
  • Beyond the paper: a cheap test of the critical failure mode would be to generate two checkers for the same requirement using different LLMs or different formalisms (SMT versus Python) and compare their verdicts on randomized strings; discrepancies would flag unsound checkers without needing a ground truth.
  • Beyond the paper: replacing the ten hand-built test samples with differential testing between Python and SMT checkers on many randomly generated strings could give stronger semantic soundness evidence at low cost, since the two formalisms fail in different ways.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 5 minor

Summary. The paper proposes a hybrid LLM-based approach to satisfiability checking of natural-language string requirements. The system uses LLMs to derive a satisfiability outcome (SAT with a witness string, or UNSAT) and to generate per-requirement checkers in two forms: declarative SMT constraints and imperative Python functions. The generated checkers are then used in an iterative feedback loop to validate and refine the LLM-derived outcome, with a fallback that returns the closest-to-sound outcome when the budget is exhausted. The evaluation covers four LLMs and 340 requirement sets drawn from twelve string-variable categories, measuring checker generation accuracy (RQ1), the effect of checker-based feedback with ground-truth checkers (RQ2), and end-to-end performance with LLM-generated checkers (RQ3). The reported results show that Python checkers can be generated with high testing accuracy, that ground-truth-checker feedback substantially improves generation success rate and F1-score, and that end-to-end performance approaches the ground-truth-checker upper bound for GSR in several configurations.

Significance. If the central claims held, the approach would be a practical step toward reducing manual formalization effort in requirements verification while improving LLM reliability. The paper has clear strengths: a modular architecture separating checker generation from outcome verification, a reasonably large dataset, an evaluation across four LLMs, and a public artifact. The RQ2 experiments with ground-truth checkers provide credible evidence that checker feedback improves LVO quality, especially for smaller LLMs, with more than doubled GSR and F1 in some cases. However, the headline claim that generated checkers 'ensure the correctness' of LLM-derived outcomes is not supported: the checker-soundness screen is an acknowledged over-approximation, and the paper itself admits a critical failure mode in which the LLM outcome and its checker are both wrong but agree. The contribution is best framed as heuristic validation that improves empirical accuracy, not as sound verification.

major comments (4)
  1. [Section V, 'Failure mode'; Abstract and Contributions] The claim that generated checkers 'ensure the correctness' of LLM-derived satisfiability outcomes is not supported by the paper. Section V explicitly states that 'a critical failure mode occurs when both the LLM output and its checker are flawed but agree, leading to incorrect results' and that feedback 'cannot fully eliminate the risk.' Since the checker itself is LLM-generated and accepted after only a 10-sample screen (Section VI-B), the verifier can return an incorrect SAT or UNSAT result. This is load-bearing because the central contribution over direct LLM generation is the correctness guarantee. Please weaken the wording throughout (e.g., 'validate' or 'improve') or provide an independent arbitration mechanism that actually establishes soundness.
  2. [Section IV, 'Checker soundness evaluation'; Section VI-B] The semantic soundness screen is an over-approximation and cannot support the 'soundness' terminology. Testing accuracy is defined as agreement with ground truth on 10 manually constructed samples per requirement (5 satisfying, 5 violating), and the paper itself says this 'provides an over-approximation of checkers' semantic correctness.' For Python checkers there is no formal equivalence check at all, and in the end-to-end setting SMT checkers are also not formally verified against ground truth. A checker passing this screen may be semantically wrong, and the same checker is then used to accept or reject LLM-derived outcomes. Please rename this step to something like 'testing-based screening' and explicitly state that it does not establish soundness in the deployment setting.
  3. [Section VI-D, RQ3 setup] It is not stated whether the 10-sample semantic soundness screen is applied to the generated checkers used in RQ3, or whether checkers are accepted on syntax alone. The text only says that 'we select the checkers generated by IND across all evaluated LLMs.' This ambiguity is important: if the semantic screen is not applied in RQ3, the end-to-end validator is even less constrained than RQ1 suggests; if it is applied, the acknowledged weakness of the 10-sample screen propagates into the end-to-end results. Please specify the exact acceptance criterion for checkers in RQ3, report how many generated checkers passed the screen, and state whether the screen is part of the reported end-to-end system.
  4. [Section VI, Table III and Figure 7] All comparative claims rest on single runs with no repeated trials, no error bars, and no significance tests. The temperature settings are low but not zero for GPT models, and the UNSAT subset contains only 57 cases, so F1 differences of a few percentage points may be within stochastic variation. This is load-bearing for claims such as 'feedback improves F1 in 8 out of 12 scenarios' and for the RQ3 ratio comparisons. Please provide repeated trials or variance estimates, and report the numeric values behind the radar plots in Figure 7 rather than only graphical ratios.
minor comments (5)
  1. [Table III, Figure 6, RQ1 answer] The model name 'DeekSeek' appears in several places (Table III, Figure 6, and the RQ1 answer); it should be 'DeepSeek'.
  2. [Table II] In the provided rendering, Table II appears to have empty cells for GPT-4o-mini, GPT-4o, and DeepSeek-V3; please ensure every row reports syntax and testing accuracy, or explain any intentional omission.
  3. [Figure 7] The radar plots are difficult to read, especially for comparisons across four verifiers; a companion table with exact GSR, P, R, and F1 ratios would improve reproducibility and readability.
  4. [Section V, 'Budget check'] The term 'closest-to-sound' is used for the fallback outcome, but the selection rule is a majority/ratio heuristic over saved LVOs; consider defining the term more precisely or renaming it to avoid implying a formal soundness guarantee.
  5. [Reference [36]] The reference title 'Constrainsolver artifacts' appears to be a typo; it should likely be 'ConstraintSolver artifacts', and the anonymized/DOI status should be checked for consistency with the review process.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the verification chain is anchored to externally constructed ground-truth checkers and labels, and the admitted checker-outcome agreement failure is a soundness threat rather than a derivation circle.

full rationale

The paper's claimed derivation chain is not circular. In RQ1, checker quality is measured against manually constructed ground-truth checkers and, for SMT checkers, by formal equivalence proofs discharged with CVC5; this provides an external anchor independent of the LLM-generated checkers themselves. In RQ2, the verifier is evaluated using ground-truth checkers, establishing an upper bound that does not depend on the proposed checker generator. In RQ3, end-to-end performance is reported as a ratio to that ground-truth upper bound and measured with GSR, precision, recall, and F1 against externally determined SAT/UNSAT labels, not against the system's own outputs. The checker and the LVO are generated separately from the same NL requirements, so the checker is not defined in terms of the LVO; no equation or construction forces the checker to accept the LVO. The paper explicitly identifies the risk that 'both the LLM output and its checker are flawed but agree' and calls it a 'critical failure mode,' which is an honest validity limitation rather than a circular derivation. The only self-citation is [9], used for motivation and related-work positioning, and it is not load-bearing for any measured result. Therefore no prediction reduces by construction to its inputs, and the appropriate circularity score is 0.

Assumptions & free parameters 4 free parameters · 6 assumptions · 0 invented entities

The approach is empirical, so it introduces no mathematical axioms or invented physical entities. The listed domain assumptions are the load-bearing choices: reliance on CVC5 and manual inspection for ground truth, use of a 10-sample test to approximate checker correctness, representativeness of the 340 requirement sets, and stability of low-temperature LLM sampling. The hand-set budgets and temperatures are free parameters that affect quality but are not fitted to data.

free parameters (4)
  • verifier retry budget = 5 LLM calls
    Maximum number of retries in the checker-based verifier feedback loop, chosen by hand in Section VI-A. It affects the outcome quality and the graceful degradation behavior.
  • checker generator retry budget = 2 LLM calls
    Maximum retries per checker batch during generation, chosen by hand in Section VI-A. It bounds the effort spent on repairing unsound checkers.
  • LLM sampling temperature = 0 for open-source models, 0.01 for GPT models, 0.1 for controlled variation
    Chosen to minimize generation variance and to allow limited variation in retry experiments. Not fitted to data, but it influences reproducibility.
  • semantic testing sample count per requirement = 10 (5 valid and 5 invalid strings)
    Hand-constructed test set used to estimate checker semantic correctness. The paper acknowledges this is an over-approximation of true semantic soundness.
assumptions (6)
  • domain assumption CVC5 with a 5-second timeout plus manual inspection of UNKNOWN results gives correct ground truth satisfiability labels for the dataset.
    The 340 requirement sets are labeled by manually translating them to SMT-LIB and running CVC5; the 56 UNKNOWN cases were manually relabeled. This grounds all evaluation metrics.
  • domain assumption Formal equivalence checking of generated SMT checkers against manually built ground-truth checkers is sound.
    The formal accuracy metric in RQ1 relies on CVC5 proving equivalence between generated and ground-truth SMT expressions, with timeouts and unknown results disregarded.
  • domain assumption Ten hand-picked test strings per requirement suffice to estimate checker semantic correctness for accepting checkers.
    Testing accuracy is explicitly an over-approximation in Section IV, yet it is the only semantic validation applied to LLM-generated checkers in the end-to-end setting.
  • domain assumption The 12 string-variable categories and 340 requirement sets are representative of real-world natural-language string requirements.
    The dataset is built from common programming exercises in technical interviews. The authors acknowledge possible selection bias and training-data leakage in the threats to validity.
  • domain assumption Low-temperature LLM sampling makes iterative feedback results stable.
    Temperatures are set near zero to reduce variation, but no repeated trials or confidence intervals are reported, so stability is assumed rather than measured.
  • domain assumption Natural-language requirements are unambiguous enough for LLM interpretation and checker generation.
    The approach assumes NL requirements can be converted into consistent formal checkers; ambiguity in NL is a known challenge and is cited in the related work.

how reviews work

0 comments
Cite this review

Pith. "Pith review of LLM-based Satisfiability Checking of String Requirements by Consistent Data and Checker Generation." pith.science (2026). https://pith.science/paper/242KCTUG

@misc{pith2026250616639,
  author       = {Pith},
  title        = {Pith review of: LLM-based Satisfiability Checking of String Requirements by Consistent Data and Checker Generation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/242KCTUG}},
  note         = {Machine review of arXiv:2506.16639}
}
read the original abstract

Requirements over strings, commonly represented using natural language (NL), are particularly relevant for software systems due to their heavy reliance on string data manipulation. While individual requirements can usually be analyzed manually, verifying properties (e.g., satisfiability) over sets of NL requirements is particularly challenging. Formal approaches (e.g., SMT solvers) may efficiently verify such properties, but are known to have theoretical limitations. Additionally, the translation of NL requirements into formal constraints typically requires significant manual effort. Recently, large language models (LLMs) have emerged as an alternative approach for formal reasoning tasks, but their effectiveness in verifying requirements over strings is less studied. In this paper, we introduce a hybrid approach that verifies the satisfiability of NL requirements over strings by using LLMs (1) to derive a satisfiability outcome (and a consistent string, if possible), and (2) to generate declarative (i.e., SMT) and imperative (i.e., Python) checkers, used to validate the correctness of (1). In our experiments, we assess the performance of four LLMs. Results show that LLMs effectively translate natural language into checkers, even achieving perfect testing accuracy for Python-based checkers. These checkers substantially help LLMs in generating a consistent string and accurately identifying unsatisfiable requirements, leading to more than doubled generation success rate and F1-score in certain cases compared to baselines without generated checkers.

Figures

Figures reproduced from arXiv: 2506.16639 by the authors.

Figure 1
Figure 1. Approach overview not-necessarily-sound approach (e.g., LLMs), as detailed in Section V. It then checks (validates) the correctness of the intermediate verification outcome wrt. the requirements. The checker generator component is described in Section IV. NL requirements and the generated checkers are then given as input to the checker-based verifier, detailed in Section V, which outputs a verification outcome for t… view at source ↗
Figure 2
Figure 2. Overview of our divide-and-conquer approach for generating verification outcome checkers [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. LVO generation with feedback prompt template excerpt [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Overview of our checker-based NL requirements verification approach [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: An example requirement and its according checkers. [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 6
Figure 6. Figure 6: Accuracy of generated SMT constraints (in %) checker v, let vgt denote the ground truth checker corre￾sponding to v, and let E(v, s) represent the execution output of checker v on sample s. Testing accuracy is defined as: |{v|v∈V∧∀s∈Sv:E(v,s)=E(vgt,s)}| n . Testing acc…
Figure 7
Figure 7. Figure 7: Metric ratio of different LLM-based verifiers using LLM-generated checkers compared with the ground truth checkers; [PITH_FULL_IMAGE:figures/full_fig_p010_7.png]

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

63 extracted references · 44 canonical work pages

  1. [1]

    Normative requirements operationalization with large language models,

    N. Feng, L. Marsso, S. G. Yaman, I. Standen, Y . Baatartogtokh, R. Ayad, V . O. De Mello, B. Townsend, H. Bartels, A. Cavalcanti et al., “Normative requirements operationalization with large language models,” inRE 2024. IEEE, 2024, pp. 129–141

    work page 2024

  2. [2]

    Inconsistency detection in natural language requirements using ChatGPT: a preliminary evaluation,

    A. Fantechi, S. Gnesi, L. Passaro, and L. Semini, “Inconsistency detection in natural language requirements using ChatGPT: a preliminary evaluation,” inRE 2023. IEEE, 2023, pp. 335–340

    work page 2023

  3. [3]

    Ambiguity and Generality in Natural Language Privacy Policies,

    M. B. Hosseini, J. Heaps, R. Slavin, J. Niu, and T. Breaux, “Ambiguity and Generality in Natural Language Privacy Policies,” in2021 IEEE 29th International Requirements Engineering Conference (RE), 2021, pp. 70–81

    work page 2021

  4. [4]

    Generation of Formal Requirements from Structured Natural Lan- guage,

    D. Giannakopoulou, T. Pressburger, A. Mavridou, and J. Schumann, “Generation of Formal Requirements from Structured Natural Lan- guage,” inRequirements Engineering: Foundation for Software Quality, N. Madhavji, L. Pasquale, A. Ferrari, and S. Gnesi, Eds. Springer International Publishing, 2020, pp. 19–35

    work page 2020

  5. [5]

    Ambiguity in Requirements Specifica- tion,

    D. M. Berry and E. Kamsties, “Ambiguity in Requirements Specifica- tion,” inPerspectives on Software Requirements. Springer US, 2004, pp. 7–44

    work page 2004

  6. [6]

    Z3: An efficient SMT solver,

    L. De Moura and N. Bjørner, “Z3: An efficient SMT solver,” inTACAS

    work page

  7. [7]

    Decision procedures for path feasibility of string-manipulating programs with complex operations,

    T. Chen, M. Hague, A. W. Lin, P. R ¨ummer, and Z. Wu, “Decision procedures for path feasibility of string-manipulating programs with complex operations,”OSTRICH String Constraint Solver and Results, vol. 3, no. POPL, pp. 49:1–49:30, Jan. 2019

    work page 2019

  8. [8]

    Towards reasoning in large language models: A survey,

    J. Huang and K. C.-C. Chang, “Towards reasoning in large language models: A survey,” inACL 2023. ACL, 2023, pp. 1049–1065

    work page 2023

Show all 63 references
  1. [9]

    Exploring large language models for requirements on string values,

    A. A. Babikian, B. Chen, and G. Mussbacher, “Exploring large language models for requirements on string values,” inProceedings of the 2nd IEEE/ACM Workshop on Multi- disciplinary, Open, and RElevant Requirements Engineering,

  2. [10]

    Guiding enumerative program synthesis with large language models,

    Y . Li, J. Parsert, and E. Polgreen, “Guiding enumerative program synthesis with large language models,” inInternational Conference on Computer Aided Verification. Springer, 2024, pp. 280–301

    2024

  3. [11]

    Baldur: Whole-proof generation and repair with large language models,

    E. First, M. N. Rabe, T. Ringer, and Y . Brun, “Baldur: Whole-proof generation and repair with large language models,” inProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2023, pp. 1229–1241

    2023

  4. [12]

    Prover-verifier games improve legibility of llm outputs,

    J. H. Kirchner, Y . Chen, H. Edwards, J. Leike, N. McAleese, and Y . Burda, “Prover-verifier games improve legibility of llm outputs,” arXiv preprint arXiv:2407.13692, 2024

    2024 arXiv

  5. [13]

    Gpt-4o system card,

    A. Hurst, A. Lerer, A. P. Goucher, A. Perelman, A. Ramesh, A. Clark, A. Ostrow, A. Welihinda, A. Hayes, A. Radfordet al., “Gpt-4o system card,”arXiv preprint arXiv:2410.21276, 2024

    2024 arXiv

  6. [14]

    The llama 3 herd of models,

    A. Grattafiori, A. Dubey, A. Jauhri, A. Pandey, A. Kadian, A. Al-Dahle, A. Letman, A. Mathur, A. Schelten, A. Vaughanet al., “The llama 3 herd of models,”arXiv preprint arXiv:2407.21783, 2024

    2024 arXiv

  7. [15]

    Deepseek-v3 technical report,

    A. Liu, B. Feng, B. Xue, B. Wang, B. Wu, C. Lu, C. Zhao, C. Deng, C. Zhang, C. Ruanet al., “Deepseek-v3 technical report,”arXiv preprint arXiv:2412.19437, 2024

    2024 arXiv

  8. [16]

    Solving string constraints with lengths by stabilization,

    Y .-F. Chen, D. Chocholat ´y, V . Havlena, L. Hol´ık, O. Leng ´al, and J. S ´ıˇc, “Solving string constraints with lengths by stabilization,”Proceedings of ACM Programming Languages, vol. 7, no. OOPSLA2, Oct. 2023

    2023

  9. [17]

    Solving String Constraints Using SAT,

    K. Lotz, A. Goel, B. Dutertre, B. Kiesl-Reiter, S. Kong, R. Majumdar, and D. Nowotka, “Solving String Constraints Using SAT,” inCAV 2023. Springer, 2023, pp. 187–208

    2023

  10. [18]

    A decision procedure for string constraints with string/integer conversion and flat regular constraints,

    H. Wu, Y .-F. Chen, Z. Wu, B. Xia, and N. Zhan, “A decision procedure for string constraints with string/integer conversion and flat regular constraints,”Acta Informatica, vol. 61, no. 1, pp. 23–52, Mar. 2024

    2024

  11. [19]

    Towards Constraint Logic Programming over Strings for Test Data Generation,

    S. Krings, J. Schmidt, P. Skowronek, J. Dunkelau, and D. Ehmke, “Towards Constraint Logic Programming over Strings for Test Data Generation,” inDeclarative Programming and Knowledge Management. Springer, 2020, pp. 139–159

    2020

  12. [20]

    SMT-LIB The Satisfiability Modulo Theories Library,

    “SMT-LIB The Satisfiability Modulo Theories Library,” https://smt- lib.org/benchmarks.shtml

  13. [21]

    SMT-COMP 2024,

    “SMT-COMP 2024,” https://smt-comp.github.io/2024/

    2024

  14. [22]

    The SMT-LIB standard: Version 2.6,

    C. Barrett, P. Fontaine, and C. Tinelli, “The SMT-LIB standard: Version 2.6,” Department of Computer Science, The University of Iowa, Tech. Rep., 2017

    2017

  15. [23]

    Attention is all you need,

    A. Vaswani, N. M. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, L. Kaiser, and I. Polosukhin, “Attention is all you need,” in NIPS, 2017

    2017

  16. [24]

    A systematic survey of prompt engineering in large language models: Techniques and applications,

    P. Sahoo, A. K. Singh, S. Saha, V . Jain, S. Mondal, and A. Chadha, “A systematic survey of prompt engineering in large language models: Techniques and applications,”arXiv preprint arXiv:2402.07927, 2024

    2024 arXiv

  17. [25]

    Large language models understand and can be enhanced by emotional stimuli,

    C. Li, J. Wang, Y . Zhang, K. Zhu, W. Hou, J. Lian, F. Luo, Q. Yang, and X. Xie, “Large language models understand and can be enhanced by emotional stimuli,”arXiv preprint arXiv:2307.11760, 2023

    2023 arXiv

  18. [26]

    Large language models are zero-shot reasoners,

    T. Kojima, S. S. Gu, M. Reid, Y . Matsuo, and Y . Iwasawa, “Large language models are zero-shot reasoners,”NeurIPS 2022, pp. 22 199– 22 213, 2022

    2022

  19. [27]

    [Online]

    OpenAI, accessed: 2025-03-10. [Online]. Available: https://openai.com/ index/introducing-structured-outputs-in-the-api

    2025

  20. [28]

    LangChain,

    H. Chase and contributors, “LangChain,” 2022. [Online]. Available: https://github.com/langchain-ai/langchain

    2022

  21. [29]

    Solving complex path conditions through heuristic search on induced polytopes,

    P. Dinges and G. A. Agha, “Solving complex path conditions through heuristic search on induced polytopes,” inProceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16 - 22, 2014. ACM, 2014, pp. 425–436

    2014

  22. [30]

    The effect of batch size on the generalizabil- ity of the convolutional neural networks on a histopathology dataset,

    I. Kandel and M. Castelli, “The effect of batch size on the generalizabil- ity of the convolutional neural networks on a histopathology dataset,” ICT Express, vol. 6, no. 4, pp. 312–315, 2020. [Online]. Available: https://www.sciencedirect.com/science/article/pii/S2405959519303455

    2020

  23. [31]

    Evaluating large language models trained on code,

    M. Chen, J. Tworek, H. Jun, Q. Yuanet al., “Evaluating large language models trained on code,”arXiv preprint arXiv:2107.03374, 2021

    2021 arXiv

  24. [32]

    Chain-of-thought prompting elicits reasoning in large language models,

    J. Wei, X. Wang, D. Schuurmans, M. Bosma, F. Xia, E. Chi, Q. V . Le, D. Zhouet al., “Chain-of-thought prompting elicits reasoning in large language models,”Advances in neural information processing systems, vol. 35, pp. 24 824–24 837, 2022

    2022

  25. [33]

    Github copilot,

    “Github copilot,” https://github.com/features/copilot, accessed: 2025-03- 10

    2025

  26. [34]

    Cvc5/src/theory/incomplete id.h at main·cvc5/cvc5,

    “Cvc5/src/theory/incomplete id.h at main·cvc5/cvc5,” https://github. com/cvc5/cvc5/blob/main/src/theory/incomplete id.h

  27. [35]

    Burnstein,Practical software testing: a process-oriented approach

    I. Burnstein,Practical software testing: a process-oriented approach. Springer Science & Business Media, 2006

    2006

  28. [36]

    Constrainsolver artifacts,

    B. Chen, A. A. Babikian, S. Feng, D. Varr ´o, and G. Mussbacher, “Constrainsolver artifacts,” Jun. 2025. [Online]. Available: https: //doi.org/10.5281/zenodo.15679384

    2025 doi

  29. [37]

    A survey on evaluating large language models in code generation tasks,

    L. Chen, Q. Guo, H. Jia, Z. Zeng, X. Wang, Y . Xu, J. Wu, Y . Wang, Q. Gao, J. Wanget al., “A survey on evaluating large language models in code generation tasks,”arXiv preprint arXiv:2408.16498, 2024

    2024 arXiv

  30. [38]

    Advancing requirements engineering through generative AI: Assessing the role of LLMs,

    C. Arora, J. Grundy, and M. Abdelrazek, “Advancing requirements engineering through generative AI: Assessing the role of LLMs,” in Generative AI for Effective Software Development. Springer, 2024, pp. 129–148

    2024

  31. [39]

    Investigating ChatGPT’s poten- tial to assist in requirements elicitation processes,

    K. Ronanki, C. Berger, and J. Horkoff, “Investigating ChatGPT’s poten- tial to assist in requirements elicitation processes,” in2023 49th Euromi- cro Conference on Software Engineering and Advanced Applications (SEAA). IEEE, 2023, pp. 354–361

    2023

  32. [40]

    Generating requirements elicitation interview scripts with large language models,

    B. G ¨orer and F. B. Aydemir, “Generating requirements elicitation interview scripts with large language models,” inRE 2023 Workshops (REW). IEEE, 2023, pp. 44–51

    2023

  33. [41]

    Automated domain modeling with large language models: A comparative study,

    K. Chen, Y . Yang, B. Chen, J. A. H. L ´opez, G. Mussbacher, and D. Varr´o, “Automated domain modeling with large language models: A comparative study,” in2023 ACM/IEEE 26th International Conference on Model Driven Engineering Languages and Systems (MODELS). IEEE, 2023, pp. 162–172

    2023

  34. [42]

    On the assessment of generative ai in modeling tasks: an experience report with chatgpt and uml,

    J. C ´amara, J. Troya, L. Burgue ˜no, and A. Vallecillo, “On the assessment of generative ai in modeling tasks: an experience report with chatgpt and uml,”Software and Systems Modeling, vol. 22, no. 3, pp. 781–793, 2023

    2023

  35. [43]

    On the use of GPT-4 for creating goal models: An exploratory study,

    B. Chen, K. Chen, S. Hassani, Y . Yang, D. Amyot, L. Lessard, G. Mussbacher, M. Sabetzadeh, and D. Varr ´o, “On the use of GPT-4 for creating goal models: An exploratory study,” inRE 2023 Workshops. IEEE, 2023, pp. 262–271

    2023

  36. [44]

    Towards taming large language models with prompt templates for legal GRL modeling,

    S. de Kinderen and K. Winter, “Towards taming large language models with prompt templates for legal GRL modeling,” inBPMDS 2024. Springer, 2024, pp. 213–228

    2024

  37. [45]

    Fill in the blank: Context-aware automated text input generation for mobile GUI testing,

    Z. Liu, C. Chen, J. Wang, X. Che, Y . Huang, J. Hu, and Q. Wang, “Fill in the blank: Context-aware automated text input generation for mobile GUI testing,” inICSE 2023. IEEE, 2023, pp. 1355–1367

    2023

  38. [46]

    Fuzz4all: Universal fuzzing with large language models,

    C. S. Xia, M. Paltenghi, J. Le Tian, M. Pradel, and L. Zhang, “Fuzz4all: Universal fuzzing with large language models,” inICSE 2024, 2024, pp. 1–13

    2024

  39. [47]

    SMT solver validation empowered by large pre-trained language models,

    M. Sun, Y . Yang, Y . Wang, M. Wen, H. Jia, and Y . Zhou, “SMT solver validation empowered by large pre-trained language models,” inASE

  40. [48]

    Testing the limits: Unusual text inputs generation for mobile app crash detection with large language model,

    Z. Liu, C. Chen, J. Wang, M. Chen, B. Wu, Z. Tian, Y . Huang, J. Hu, and Q. Wang, “Testing the limits: Unusual text inputs generation for mobile app crash detection with large language model,” inICSE 2024, 2024, pp. 1–12

    2024

  41. [49]

    Tree of thoughts: Deliberate problem solving with large language models,

    S. Yao, D. Yu, J. Zhao, I. Shafran, T. Griffiths, Y . Cao, and K. Narasimhan, “Tree of thoughts: Deliberate problem solving with large language models,”Advances in neural information processing systems, vol. 36, pp. 11 809–11 822, 2023

    2023

  42. [50]

    Large language model guided tree-of-thought,

    J. Long, “Large language model guided tree-of-thought,”arXiv preprint arXiv:2305.08291, 2023

    2023 arXiv

  43. [51]

    Graph of thoughts: Solving elaborate problems with large language models,

    M. Besta, N. Blach, A. Kubicek, R. Gerstenberger, M. Podstawski, L. Gianinazzi, J. Gajda, T. Lehmann, H. Niewiadomski, P. Nyczyk et al., “Graph of thoughts: Solving elaborate problems with large language models,” inProceedings of the AAAI Conference on Artificial Intelligence,...

    2024

  44. [52]

    Metagpt: Meta programming for multi-agent collaborative framework,

    S. Hong, X. Zheng, J. Chen, Y . Cheng, J. Wang, C. Zhang, Z. Wang, S. K. S. Yau, Z. Lin, L. Zhouet al., “Metagpt: Meta programming for multi-agent collaborative framework,”arXiv preprint arXiv:2308.00352, vol. 3, no. 4, p. 6, 2023

    2023 arXiv

  45. [53]

    More agents is all you need,

    J. Li, Q. Zhang, Y . Yu, Q. Fu, and D. Ye, “More agents is all you need,” arXiv preprint arXiv:2402.05120, 2024

    2024 arXiv

  46. [54]

    Autogen: Enabling next-gen LLM applications via multi-agent conversation,

    Q. Wu, G. Bansal, J. Zhang, Y . Wu, B. Li, E. Zhu, L. Jiang, X. Zhang, S. Zhang, J. Liuet al., “Autogen: Enabling next-gen LLM applications via multi-agent conversation,”arXiv preprint arXiv:2308.08155, 2023

    2023 arXiv

  47. [55]

    Agentscope: A flexible yet robust multi-agent platform,

    D. Gao, Z. Li, X. Pan, W. Kuang, Z. Ma, B. Qian, F. Wei, W. Zhang, Y . Xie, D. Chenet al., “Agentscope: A flexible yet robust multi-agent platform,”arXiv preprint arXiv:2402.14034, 2024

    2024 arXiv

  48. [56]

    Llm-based multi-agent systems for software engineering: Literature review, vision and the road ahead,

    J. He, C. Treude, and D. Lo, “Llm-based multi-agent systems for software engineering: Literature review, vision and the road ahead,” ACM Transactions on Software Engineering and Methodology, 2024

    2024

  49. [57]

    Automated unit test improvement using large language models at Meta,

    N. Alshahwan, J. Chheda, A. Finogenova, B. Gokkaya, M. Harman, I. Harper, A. Marginean, S. Sengupta, and E. Wang, “Automated unit test improvement using large language models at Meta,” inCompanion Proceedings of the 32nd ACM International Conference on the Founda- tions of Sof...

    2024

  50. [58]

    Multi-step iterative automated domain modeling with large language models,

    Y . Yang, B. Chen, K. Chen, G. Mussbacher, and D. Varro, “Multi-step iterative automated domain modeling with large language models,” in ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings (MODELS), 2024, pp. 587–595

    2024

  51. [59]

    Leveraging graph-rag and prompt engineering to enhance llm-based automated requirement traceability and compliance checks,

    A. Masoudifard, M. M. Sorond, M. Madadi, M. Sabokrou, and E. Habibi, “Leveraging graph-rag and prompt engineering to enhance llm-based automated requirement traceability and compliance checks,” arXiv preprint arXiv:2412.08593, 2024

    2024 arXiv

  52. [60]

    Concretization of Abstract Traffic Scene Specifications Using Metaheuristic Search,

    A. A. Babikian, O. Semer ´ath, and D. Varr´o, “Concretization of Abstract Traffic Scene Specifications Using Metaheuristic Search,”IEEE Trans- actions on Software Engineering, vol. 50, no. 1, pp. 48–68, 2024

    2024

  53. [2008]

    Springer, 2008, pp. 337–340

    2008

  54. [2023]

    1288–1300

    IEEE, 2023, pp. 1288–1300

    2023

  55. [2025]

    Available: https://mo2re.github.io/assets/preprints/ BCM-LLMsForStringRequirments-MO2RE25.pdf

    [Online]. Available: https://mo2re.github.io/assets/preprints/ BCM-LLMsForStringRequirments-MO2RE25.pdf

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.