Pith. sign in

REVIEW 4 minor 47 references

Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects

T0 review · 0 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read The paper argues that fully automatic LLM-based formalisation of software requirements is blocked by five recurrent barriers, and that the field is converging on hybrid, human-in-the-loop pipelines.

desk verdict A competent position paper that organises known challenges in LLM-based formalisation; the experimental appendix is too thin to carry weight, but the synthesis is useful for newcomers. read the letter →

arxiv 2507.14330 v3 pith:XDIYH5KY submitted 2025-07-18 cs.SE

Arshad Beg , Diarmuid O'Donoghue , Rosemary Monahan This is my paper
classification cs.SE
keywords largelanguagemodelsformalspecificationssoftwarerequirementsverificationsemanticambiguityneuro-symbolicreasoninghuman-in-the-loopACSL
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

The paper sets out to establish that large language models will not, on their own, soon automate the translation of natural-language software requirements into formally verifiable specifications. It identifies five recurring barriers—semantic ambiguity, the absence of ground-truth datasets, tool interoperability, lifecycle traceability, and explainability and user trust—and argues that each of these stands in the way of full automation. A sympathetic reader should care because formal verification is mandatory in safety-critical domains, and generating the formal specifications is the long-standing bottleneck. The authors conclude that the realistic route forward is semi-automated toolchains in which LLMs propose specifications, symbolic verifiers check them, and human experts review and refine the results.

What carries the argument

The mechanism carrying the argument is a proposed pipeline architecture rather than a single theorem or identity: natural-language requirements plus domain ontologies enter through different prompting strategies (zero-shot, few-shot, chain-of-thought); the LLM produces specifications in a tool-neutral JSON-LD intermediate format; adapters translate that format into target languages such as ACSL for Frama-C or JML for OpenJML; verification tools and symbolic reasoning return feedback; and human reviewers validate outputs and feed corrections back into the prompts. The empirical anchor is a re-simulation of the methodology of [3], in which PathCrawler's concrete symbolic path inputs and outputs are used to guide the LLM toward context-aware ACSL annotations, and Frama-C's WP plugin with four SMT solvers checks the resulting goals.

What would settle it

Have independent formal-methods experts review the LLM-generated ACSL annotations from Appendix A's Tritype experiment and re-run Frama-C's WP plugin with any corrected specifications: if the previously unproved goals (7 of 20 for Z3 and CVC4, 5 for Alt-Ergo and CVC5) become provable, the paper's attribution to solver limitations is undercut. The opposite experiment—an end-to-end LLM pipeline, without human review, producing verified specifications for a substantial suite of industrial-scale requirements—would directly falsify the claim that full automation is blocked.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central finding is a barrier analysis: fully automatic, end-to-end translation from informal requirements to verified formal specifications is not attainable with current LLM technology. The paper argues that the field is instead converging on hybrid pipelines that combine LLM generation with symbolic reasoning and iterative user interaction, and that assertion-level synthesis is markedly more reliable than full contract generation, citing 89% correctness for hardware assertions against frequent verification failures for full JML and ACSL contracts. Its own re-simulation of an LLM-plus-symbolic-path workflow on a triangle-classification program produced ACSL annotations that left 5 to 7 of 20 verification goals unproved across four SMT solvers, which the authors attribute to disjunction-heavy logic and subtle arithmetic constraints in functional specifications. The paper also reports that PathCrawler achieved full branch coverage but labelled every generated test case 'unknown', which it treats as evidence that postconditions were not robustly specified. The proposed response is a modular pipeline in which natural-language requirements and domain ontologies feed LLM prompting strategies, outputs are stored in a tool-neutral JSON-LD format, verification tools and symbolic reasoning provide feedback, and human reviewers remain in the loop.

Load-bearing premise

The conclusions rest on the assumption that the literature sample and the small Tritype re-simulation are representative, and in particular that the LLM-generated ACSL specifications used in the solver comparison are semantically correct; if those specifications themselves harbour errors, the unproved verification goals reflect bad inputs rather than solver limits or automation barriers.

Editorial extensions

If this is right

  • If the barrier analysis is correct, LLM-based formalisation should be built as a semi-automated workflow with a human reviewer, not as a one-shot fully automatic translation.
  • Assertion-level synthesis is the near-term deliverable, while full contract synthesis should be treated as a research problem requiring iteration and external validation.
  • Solver and verifier feedback can be used during generation to refine LLM outputs, so verification becomes part of the specification-writing loop.
  • Standardised, annotated benchmark datasets spanning multiple industries are a precondition for measuring progress and training better models.
  • Tool-neutral intermediate representations would let the same LLM output target multiple verification backends, reducing interoperability barriers.

Reading between the lines

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

  • Editorial inference: if the LLM-generated ACSL specifications used in the appendix are not independently verified as correct, the solver comparison is not a clean test; a corrected-specification rerun would likely show that specification quality, not solver power, is the binding constraint.
  • Editorial inference: the same hybrid pipeline would transfer naturally to hardware-verification assertions and regulated-documentation compliance, where traceability and reviewability are already mandatory.
  • Editorial inference: a direct test of the paper's prediction would measure prompt-instability across zero-shot, few-shot, and chain-of-thought strategies on assertion-level versus full-contract tasks; the paper expects larger variability on full contracts.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

0 major / 4 minor

Summary. The paper is a position paper on using LLMs to generate formal software requirements specifications. It synthesises a focused body of recent work (nl2spec, SpecGen, AssertLLM, SpecSyn, Laurel, SAT-LLM, etc.) and identifies five recurring challenges: semantic ambiguity, lack of ground-truth datasets, tool interoperability, lifecycle traceability, and explainability. It then proposes the VERIFAI research agenda, built around human-in-the-loop formalisation, multimodal artefact alignment, standardised benchmarks, neuro-symbolic reasoning, and interactive traceability tools, with a JSON-LD tool-neutral intermediate representation. The authors also report initial Frama-C experiments in which they re-simulate the methodology of [3] on the Tritype example, comparing Alt-Ergo, Z3, CVC4, and CVC5, and they make supporting material available in a GitHub repository. The conclusions—that semantic ambiguity, lack of ground truth, tool interoperability, traceability, and explainability are significant barriers to full automation, and that hybrid semi-automated toolchains are the realistic near-term path—are stated as preliminary.

Significance. The main value of the paper is its structured, well-referenced synthesis of an active research area. The conclusion that the field is converging on LLM-plus-symbolic-plus-human toolchains is consistent with the external literature the authors survey and does not depend on the authors' own experiments. The paper is appropriately scoped as a position paper, explicitly labels its empirical work as initial, discloses AI-assisted drafting of descriptive text, and provides a public repository for reproducibility. The experimental appendix is the weakest component: the narrative and Table 3 disagree on solver failure counts, and the interpretation of unproved goals rests on an unverified assumption about the correctness of the LLM-generated specifications. These are fixable local issues rather than threats to the paper's central qualitative position.

minor comments (4)
  1. [Section 1, contribution bullets] The appendix references in the contribution bullets are inconsistent. The 'State-of-the-Art Synthesis' bullet says 'Section 2, supported by Appendix A', but Appendix A describes the Tritype experiments rather than the literature survey. The 'Experimental Evaluation' bullet says 'Appendices B and C' contain the solver comparisons, but Appendix C contains the challenge descriptions; the empirical tables are in Appendices A and B. These references should be corrected.
  2. [Appendix A, narrative and Table 3] The narrative around Table 3 is internally inconsistent with the table. The text states 'Z3 and CVC5 each failed to prove seven goals—Z3 due to timeouts and CVC4 due to unknown statuses', and then 'Alt-Ergo and CVC5 fared slightly better, with only five unverified goals each.' Table 3 reports Z3 with 7 timeouts, CVC4 with 7 unknown, Alt-Ergo with 5 timeouts, and CVC5 with 5 timeouts. The narrative misattributes CVC5's failure count and conflates CVC4 with CVC5; the text and table must be aligned.
  3. [Appendix A and Section 4.2] The interpretation that the 5–7 unproved goals reflect solver limitations ('disjunction-heavy logic or subtle arithmetic constraints') is not fully supported. Section 4.2 states that every LLM-generated ACSL specification was manually reviewed by a formal-methods expert, but PathCrawler labelled all of its own test cases 'unknown' and no independent oracle (e.g., a from-scratch expert specification or a proof assistant) was used. If the LLM-generated specifications contain errors, Table 3 is an artefact. Please either add an independent oracle or explicitly present the comparison as an exploratory case study rather than a solver evaluation.
  4. [Section 5; Appendix C, F2; Appendix A] There are several typos: 'anaysis' in Section 5 should be 'analysis'; 'spreedsheets' in Appendix C, F2 should be 'spreadsheets'; 'EV A' in Appendix A should be 'EVA'; and 'isoceles' in the Tritype comment should be 'isosceles'. These should be corrected in a copy-editing pass.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: central claims are literature-synthesized position statements, with no fitted inputs renamed as predictions and no load-bearing self-citation.

full rationale

The paper's central conclusions — that semantic ambiguity, lack of ground truth data, tool interoperability, lifecycle traceability, and explainability block full automation, and that human-in-the-loop, neuro-symbolic, and benchmark-oriented approaches are the near-term path forward — are position statements grounded in a broad synthesis of external literature, including Req2Spec, SpecGen, AssertLLM, nl2spec, Laurel, SAT-LLM, and prompting-strategy studies. No quantitative claim or prediction in the paper is derived from parameters fitted to a subset of data and then applied to a closely related quantity. The only self-citation, reference [2], is the authors' own VERIFAI project description; it is used to state the project's aims and proposed framework, not as evidence for the paper's empirical or analytical claims, so it is not load-bearing. Appendix A's solver comparison rests on an assumption that the manually reviewed LLM-generated ACSL specifications are semantically correct, and PathCrawler's all-'unknown' verdicts weaken the strength of that comparison; however, that is a reliability limitation of an auxiliary experiment, not a case where the conclusion is equivalent to its input by construction. The 'challenges' are framed as recurring themes from the surveyed literature rather than as outputs forced by the authors' own measurements or definitions. Consequently, no step in the claimed derivation chain reduces to a fit, a self-citation chain, or a definitional equivalence.

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

This is a position paper, so its ledger contains planning assumptions and proposed artifacts rather than fitted parameters. The central synthesis is grounded in externally published tools and benchmarks; the authors' own VERIFAI framework and JSON-LD schema are unvalidated proposals that the paper correctly labels as future work.

assumptions (4)
  • domain assumption Formal verification against a formal specification is a sound way to ensure software correctness.
    Motivates the entire research agenda; stated in Section 1 without formal proof.
  • domain assumption The focused literature selection in Section 2 is representative of the state of the art in LLM-based formalisation.
    No systematic search protocol, inclusion criteria, or quality assessment is given; the RQs are answered by narrative synthesis.
  • ad hoc to paper Human expert review can make LLM-generated specifications reliable enough for verification use.
    Assumed in Section 4.2 where the authors state every generated ACSL spec was checked by at least one author; only demonstrated on one small program.
  • ad hoc to paper A JSON-LD tool-neutral schema can be translated into multiple formal verification languages with acceptable effort.
    Proposed in Section 4.2 as a plan; currently only custom scripts to ACSL and JML exist.
invented entities (2)
  • VERIFAI framework
    purpose: Semi-automated pipeline that combines LLMs, NLP, ontology-based modelling, artefact reuse, symbolic verification, and human-in-the-loop review to generate formal specifications.
    A proposed research framework described in Sections 3 and 4 with no completed implementation or evaluation; its only evidence is a preliminary re-simulation of another group's methodology.
  • JSON-LD tool-neutral intermediate schema
    purpose: A planned interchange format to store LLM-generated specifications and export them to Frama-C, OpenJML, Dafny and other tools without custom translators.
    Described as future work in Section 4.2; no prototype, schema, or translation results are provided in the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects." pith.science (2026). https://pith.science/paper/XDIYH5KY

@misc{pith2026250714330,
  author       = {Pith},
  title        = {Pith review of: Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XDIYH5KY}},
  note         = {Machine review of arXiv:2507.14330}
}
read the original abstract

Software correctness is ensured mathematically through formal verification, which involves the resources of generating formal requirement specifications and having an implementation that must be verified. Tools such as model-checkers and theorem provers ensure software correctness by verifying the implementation against the specification. Formal methods deployment is regularly enforced in the development of safety-critical systems e.g. aerospace, medical devices and autonomous systems. Generating these specifications from informal and ambiguous natural language requirements remains the key challenge. Our project, VERIFAI^{1}, aims to investigate automated and semi-automated approaches to bridge this gap, using techniques from Natural Language Processing (NLP), ontology-based domain modelling, artefact reuse, and large language models (LLMs). This position paper presents a preliminary synthesis of relevant literature to identify recurring challenges and prospective research directions in the generation of verifiable specifications from informal requirements.

Figures

Figures reproduced from arXiv: 2507.14330 by the authors.

Figure 1
Figure 1. Methodology adopted for initial and future experiments on manual annotations linking specification fragments to source code and natural-language requirements. We are exploring semi-automated approaches where the LLM proposes initial links for human validation. These links could be stored in a graph database to support version-aware navigation and visual trace maps, which would be particularly valuable in regulated s… view at source ↗
Figure 2
Figure 2. Output of the Pathcrawler for TriType Example Analysis of Tritype Example Note: We used OpenAI’s ChatGPT-4o to assist in generating descriptive analysis text based on the output of the PathCrawler tool. All generated content was reviewed and verified by the authors. The function Tritype is: /* Should return the type of the triangle which has sides of these lengths. 3 = not a triangle 2 = equilateral triangle 1 = iso… view at source ↗
Figure 3
Figure 3. Graph of Execution Times of Alt-Ergo, Z3, CVC4 and CVC5 [PITH_FULL_IMAGE:figures/full_fig_p018_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Mapping between challenges (C1 – C5) and future research (F1- F5) directions in LLM-based formalisation decisions. F2: Multi-modal Artefact Alignment - Software requirements can be documented through a combina￾tion of raised through text, diagrams, tables, and spreedsh…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

47 extracted references · 25 canonical work pages

  1. [3]

    Granberry, W

    G. Granberry, W. Ahrendt, M. Johansson, Specify what? enhancing neural specification synthesis by symbolic methods, in: N. Kosmatov, L. Kovács (Eds.), Integrated Formal Methods, Springer Nature Switzerland, Cham, 2025, pp. 307–325

    work page 2025

  2. [1]

    Formal Methods: From Academia to Industrial Practice. A Travel Guide

    M. Huisman, D. Gurov, A. Malkis, Formal methods: From academia to industrial practice. a travel guide, 2024. URL: https://arxiv.org/abs/2002.07279. arXiv:2002.07279

    work page Pith review arXiv 2024

  3. [2]

    A. Beg, D. O’Donoghue, R. Monahan, Formalising software requirements using large language models (2025). URL: https://arxiv.org/abs/2506.10704. arXiv:2506.10704

    work page Pith review arXiv 2025

  4. [4]

    Robles, N

    V . Robles, N. Kosmatov, V . Prevosto, P. Le Gall, High-level program properties in frama-c: Definition, verification and deduction, in: Leveraging Applications of Formal Methods, Veri- fication and Validation. Specification and Verification: 12th International Symposium, ISoLA 2024, Crete, Greece, October 27–31, 2024, Proceedings, Part III, Springer-Verl...

    work page doi:10.1007/978-3-031-75380-0_10 2024

  5. [5]

    J. O. Couder, D. Gomez, O. Ochoa, Requirements verification through the analysis of source code by large language models, in: SoutheastCon 2024, 2024, pp. 75–80. doi: 10.1109/ SoutheastCon52093.2024.10500073

    arXiv 2024

  6. [6]

    X. Quan, M. Valentino, L. A. Dennis, A. Freitas, Verification and refinement of natural language explanations through llm-symbolic theorem proving, 2024. URL: https://arxiv.org/abs/2405.01379. arXiv:2405.01379

    arXiv 2024

  7. [7]

    W. Fan, M. Rego, X. Hu, S. Dod, Z. Ni, D. Xie, J. DiVincenzo, L. Tan, Evaluating the ability of large language models to generate verifiable specifications in verifast, 2025. URL: https://arxiv.org/ abs/2411.02318. arXiv:2411.02318

    arXiv 2025

  8. [8]

    Cosler, C

    M. Cosler, C. Hahn, D. Mendoza, F. Schmitt, C. Trippel, nl2spec: Interactively translating un- structured natural language to temporal logics with large language models, 2023. URL: https: //arxiv.org/abs/2303.04864. arXiv:2303.04864

    arXiv 2023

Show all 47 references
  1. [9]

    Mandal, A

    S. Mandal, A. Chethan, V . Janfaza, S. M. F. Mahmud, T. A. Anderson, J. Turek, J. J. Tithi, A. Muzahid, Large language models based automatic synthesis of software specifications, 2023. URL: https://arxiv.org/abs/2304.09181. arXiv:2304.09181

    2023 arXiv

  2. [10]

    Nayak, H

    A. Nayak, H. P. Timmapathini, V . Murali, K. Ponnalagu, V . G. Venkoparao, A. Post, Req2spec: Transforming software requirements into formal specifications using natural language processing, in: Requirements Engineering: Foundation for Software Quality: 28th International Work...

    2022

  3. [11]

    L. Ma, S. Liu, Y . Li, X. Xie, L. Bu, Specgen: Automated generation of formal program specifications via large language models (2024). URL: https://arxiv.org/abs/2401.08807. arXiv:2401.08807

    2024 arXiv

  4. [12]

    W. Fang, M. Li, M. Li, Z. Yan, S. Liu, H. Zhang, Z. Xie, Assertllm: Generating hardware verification assertions from design specifications via multi-llms, in: 2024 IEEE LLM Aided Design Workshop (LAD), 2024, pp. 1–1. doi:10.1109/LAD62341.2024.10691792

    2024

  5. [13]

    M. Li, W. Fang, Q. Zhang, Z. Xie, Specllm: Exploring generation and review of vlsi de- sign specification with large language model, 2024. URL: https://arxiv.org/abs/2401.13266. arXiv:2401.13266

    2024 arXiv

  6. [14]

    L. M. Reinpold, M. Schieseck, L. P. Wagner, F. Gehlhoff, A. Fay, Exploring llms for verifying technical system specifications against requirements, 2024. URL: https://arxiv.org/abs/2411.11582. arXiv:2411.11582

    2024 arXiv

  7. [15]

    Gervasi, B

    V . Gervasi, B. Nuseibeh, Lightweight validation of natural language requirements, Softw. Pract. Exper. 32 (2002) 113–133. URL: https://doi.org/10.1002/spe.430. doi:10.1002/spe.430

    2002 doi

  8. [16]

    Y . Xu, J. Feng, W. Miao, Learning from failures: Translation of natural language requirements into linear temporal logic with large language models, in: 2024 IEEE 24th International Conference on Software Quality, Reliability and Security (QRS), 2024, pp. 204–215. doi:10.1109...

    2024

  9. [17]

    I. T. Leong, R. Barbosa, Translating natural language requirements to formal specifications: A study on gpt and symbolic nlp, in: 2023 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W), 2023, pp. 259–262. doi:10.1109/DSN-W58399...

    2023

  10. [18]

    Nowakowski, M

    W. Nowakowski, M. ´Smiałek, A. Ambroziewicz, T. Straszak, Requirements-level language and tools for capturing software system essence, Computer Science and Information Systems 10 (2013) 1499–1524

    2013

  11. [19]

    Ghosh, D

    S. Ghosh, D. Elenius, W. Li, P. Lincoln, N. Shankar, W. Steiner, Arsenal: Automatic requirements specification extraction from natural language, in: S. Rayadurgam, O. Tkachuk (Eds.), NASA Formal Methods, Springer International Publishing, Cham, 2016, pp. 41–46

    2016

  12. [20]

    S. J. Greenspan, A. Borgida, J. Mylopoulos, A requirements modeling language and its logic, Information Systems 11 (1986) 9–23. URL: https://www.sciencedirect.com/science/article/pii/ 0306437986900207. doi:https://doi.org/10.1016/0306-4379(86)90020-7

    1986 doi

  13. [21]

    Fazelnia, M

    M. Fazelnia, M. Mirakhorli, H. Bagheri, Translation titans, reasoning challenges: Satisfiability-aided language models for detecting conflicting requirements, in: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE ’24, Association ...

    2024

  14. [22]

    K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, A. Anandkumar, Leandojo: Theorem proving with retrieval-augmented language models, in: A. Oh, T. Naumann, A. Globerson, K. Saenko, M. Hardt, S. Levine (Eds.), Advances in Neural Information Proces...

    2023

  15. [23]

    A. Q. Jiang, W. Li, S. Tworkowski, K. Czechowski, T. Odrzygó´ zd´ z, P. Mił o´s, Y . Wu, M. Jam- nik, Thor: Wielding hammers to integrate language models and automated theorem provers, in: S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, A. Oh (Eds.), Advances in Neural...

    2022

  16. [24]

    Granberry, W

    G. Granberry, W. Ahrendt, M. Johansson, Towards integrating copiloting and formal methods, in: T. Margaria, B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification, Springer Nature Switzerland, Cham, 2025, pp. 144–158

    2025

  17. [25]

    Mugnier, E

    E. Mugnier, E. A. Gonzalez, R. Jhala, N. Polikarpova, Y . Zhou, Laurel: Generating dafny assertions using large language models, 2024. URL: https://arxiv.org/abs/2405.16792. arXiv:2405.16792

    2024 arXiv

  18. [26]

    Kojima, S

    T. Kojima, S. S. Gu, M. Reid, Y . Matsuo, Y . Iwasawa, Large language models are zero-shot reasoners, in: S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, A. Oh (Eds.), Advances in Neural Information Processing Systems, volume 35, Curran Associates, Inc., 2022, pp. 22199–22213

    2022

  19. [27]

    Y . Li, B. Hui, X. Xia, J. Yang, M. Yang, L. Zhang, S. Si, L.-H. Chen, J. Liu, T. Liu, F. Huang, Y . Li, One-shot learning as instruction data prospector for large language models (2024). URL: https://arxiv.org/abs/2312.10302. arXiv:2312.10302

    2024 arXiv

  20. [28]

    Zhang, M

    H. Zhang, M. Cai, X. Zhang, C. J. Zhang, R. Mao, K. Wu, Self-convinced prompting: Few-shot question answering with repeated introspection (2023). URL: https://arxiv.org/abs/2310.05035. arXiv:2310.05035

    2023 arXiv

  21. [29]

    J. Wei, X. Wang, D. Schuurmans, M. Bosma, b. ichter, F. Xia, E. Chi, Q. V . Le, D. Zhou, Chain- of-thought prompting elicits reasoning in large language models, in: S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, A. Oh (Eds.), Advances in Neural Information Processing ...

    2022

  22. [30]

    J. Li, G. Li, Y . Li, Z. Jin, Structured chain-of-thought prompting for code generation, ACM Trans. Softw. Eng. Methodol. 34 (2025). URL: https://doi.org/10.1145/3690635. doi:10.1145/ 3690635

    2025 doi

  23. [31]

    Hsieh, Y

    C. Hsieh, Y . Chuang, C. Li, Z. Wang, L. T. Le, A. Kumar, J. R. Glass, A. Ratner, C. Lee, R. Krishna, T. Pfister, Found in the middle: Calibrating positional attention bias improves long context utilization, in: L. Ku, A. Martins, V . Srikumar (Eds.), Findings of the Associati...

    2024 doi

  24. [32]

    X. Ye, G. Durrett, The unreliability of explanations in few-shot prompting for textual reasoning, in: S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, A. Oh (Eds.), Advances in Neural Information Processing Systems, volume 35, Curran Associates, Inc., 2022, pp. 30378–30392

    2022

  25. [33]

    K. Shum, S. Diao, T. Zhang, Automatic prompt augmentation and selection with chain-of-thought from labeled data, in: H. Bouamor, J. Pino, K. Bali (Eds.), Findings of the Association for Computa- tional Linguistics: EMNLP 2023, Singapore, December 6-10, 2023, Association for Co...

    2023 doi

  26. [34]

    W. Xu, A. Banburski-Fahey, N. Jojic, Reprompting: Automated chain-of-thought prompt inference through gibbs sampling, CoRR abs/2305.09993 (2023). URL: https://doi.org/10.48550/arXiv.2305. 09993. doi:10.48550/ARXIV.2305.09993. arXiv:2305.09993

    2023 doi arXiv

  27. [35]

    Besta, F

    M. Besta, F. Memedi, Z. Zhang, R. Gerstenberger, N. Blach, P. Nyczyk, M. Copik, G. Kwasniewski, J. Müller, L. Gianinazzi, A. Kubicek, H. Niewiadomski, O. Mutlu, T. Hoefler, Topologies of reasoning: Demystifying chains, trees, and graphs of thoughts, CoRR abs/2401.14295 (2024)....

    2024 doi

  28. [36]

    Lewis, E

    P. Lewis, E. Perez, A. Piktus, F. Petroni, V . Karpukhin, N. Goyal, H. Küttler, M. Lewis, W. Yih, T. Rocktäschel, S. Riedel, D. Kiela, Retrieval-augmented generation for knowledge-intensive NLP tasks, in: H. Larochelle, M. Ranzato, R. Hadsell, M. Balcan, H. Lin (Eds.), Advance...

    2020

  29. [37]

    Sahoo, A

    P. Sahoo, A. K. Singh, S. Saha, V . Jain, S. Mondal, A. Chadha, A systematic survey of prompt engineering in large language models: Techniques and applications (2025). URL: https://arxiv.org/ abs/2402.07927. arXiv:2402.07927

    2025 arXiv

  30. [38]

    E. J. Hu, Y . Shen, P. Wallis, Z. Allen-Zhu, Y . Li, S. Wang, L. Wang, W. Chen, Lora: Low- rank adaptation of large language models, in: The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022, OpenReview.net, 2022. URL: http...

    2022

  31. [39]

    K. R. M. Leino, Dafny: An automatic program verifier for functional correctness, in: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 6355 of Lecture Notes in Computer Science, Springer, 2010, pp. ...

    2010 doi

  32. [40]

    D. R. Cok, Openjml: Software verification for java 7 using jml, openjdk, and eclipse, in: NASA Formal Methods (NFM 2011), volume 6617 of Lecture Notes in Computer Science , Springer, 2011, pp. 472–479. URL: https://doi.org/10.1007/978-3-642-20398-5_35. doi:10.1007/ 978-3-642-2...

    2011 doi

  33. [41]

    M. R. H. Misu, C. V . Lopes, I. Ma, J. Noble, Towards ai-assisted synthesis of verified dafny methods, Proc. ACM Softw. Eng. 1 (2024). URL: https://doi.org/10.1145/3643763. doi:10.1145/ 3643763

    2024 doi

  34. [42]

    J. Yao, Y . Liu, Z. Dong, M. Guo, H. Hu, K. Keutzer, L. Du, D. Zhou, S. Zhang, Promptcot: Align prompt distribution via adapted chain-of-thought, in: 2024 IEEE/CVF Conference on Computer Vi- sion and Pattern Recognition (CVPR), 2024, pp. 7027–7037. doi:10.1109/CVPR52733.2024. 00671

    2024

  35. [43]

    Porshnev, et al., Modelling implicit bias in gender–career associations: A systematic comparison of language models, PsyArXiv (2025)

    A. Porshnev, et al., Modelling implicit bias in gender–career associations: A systematic comparison of language models, PsyArXiv (2025). doi: 10.31234/osf.io/p7hvw\_v1, preprint, 22 May 2025

    2025 doi

  36. [44]

    Tahir, H

    T. Tahir, H. Jahankhani, K. Tasleem, B. Hassan, Cross-project multiclass classification of ears- based functional requirements utilizing natural language processing, machine learning, and deep learning, Systems 13 (2025). URL: https://www.mdpi.com/2079-8954/13/7/567. doi:10.33...

    2025

  37. [45]

    Gregory, A dataset describing data discovery and reuse practices in research, Sci- entific Data 7 (2020) 232

    K. Gregory, A dataset describing data discovery and reuse practices in research, Sci- entific Data 7 (2020) 232. URL: https://doi.org/10.1038/s41597-020-0569-5. doi: 10.1038/ s41597-020-0569-5

    2020 doi

  38. [46]

    Boetticher, T

    G. Boetticher, T. Menzies, T. Ostrand, {PROMISE} repository of empirical software engineering data (2007)

    2007

  39. [47]

    unknown

    J. H. Hayes, J. Payne, A. Dekhtyar, The requirements tracing on target (retro).net dataset (2018). URL: https://arxiv.org/abs/1807.11344. arXiv:1807.11344. A. Work in progress and initial experiment setup As initial experiment setup, we re-simulated the methodology presented i...

    2018 arXiv

Pith tools

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