# Working Document -- Formalising Software Requirements with Large Language Models

arXiv: https://arxiv.org/abs/2506.14627 · HTML: https://mlsanity.com/paper/2506.14627/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 29 of its 90 references that are in the map.
- First posted on arXiv 17 Jun 2025.

## Builds on (most cited first, 29 of 29)

- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [A Prompt Pattern Catalog to Enhance Prompt Engineering with ChatGPT](https://mlsanity.com/paper/2302.11382/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [The Unreliability of Explanations in Few-shot Prompting for Textual Reasoning](https://mlsanity.com/paper/2205.03401/) (2022)
- [Structured Chain-of-Thought Prompting for Code Generation](https://mlsanity.com/paper/2305.06599/) (2023)
- [Automatic Prompt Augmentation and Selection with Chain-of-Thought from Labeled Data](https://mlsanity.com/paper/2302.12822/) (2023)
- [Found in the Middle: Calibrating Positional Attention Bias Improves Long Context Utilization](https://mlsanity.com/paper/2406.16008/) (2024)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [Iteratively Prompt Pre-trained Language Models for Chain of Thought](https://mlsanity.com/paper/2203.08383/) (2022)
- [Demystifying Chains, Trees, and Graphs of Thoughts](https://mlsanity.com/paper/2401.14295/) (2024)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [Reprompting: Automated Chain-of-Thought Prompt Inference Through Gibbs Sampling](https://mlsanity.com/paper/2305.09993/) (2023)
- [Prompt Design and Engineering: Introduction and Advanced Methods](https://mlsanity.com/paper/2401.14423/) (2024)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving](https://mlsanity.com/paper/2405.01379/) (2024)
- [AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2411.14436/) (2024)
- [Semantically Enhanced Software Traceability Using Deep Learning Techniques](https://mlsanity.com/paper/1804.02438/) (2018)
- [Engineering Safety Requirements for Autonomous Driving with Large Language Models](https://mlsanity.com/paper/2403.16289/) (2024)
- [Large Language Models Based Automatic Synthesis of Software Specifications](https://mlsanity.com/paper/2304.09181/) (2023)
- [Formal Consistency Checking over Specifications in Natural Languages](https://mlsanity.com/paper/1405.5003/) (2014)
- [Exploring LLMs for Verifying Technical System Specifications Against Requirements](https://mlsanity.com/paper/2411.11582/) (2024)
- [Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast](https://mlsanity.com/paper/2411.02318/) (2024)
- [Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP](https://mlsanity.com/paper/1905.05500/) (2019)
- [A Short Survey on Formalising Software Requirements using Large Language Models](https://mlsanity.com/paper/2506.11874/) (2025)
- [Formal Methods: From Academia to Industrial Practice. A Travel Guide](https://mlsanity.com/paper/2002.07279/) (2020)
- [BIS: NL2SQL Service Evaluation Benchmark for Business Intelligence Scenarios](https://mlsanity.com/paper/2410.22925/) (2024)
- [Formalising Software Requirements using Large Language Models](https://mlsanity.com/paper/2506.10704/) (2025)

## Abstract (arXiv)

This draft is a working document, having a summary of nighty-four (94) papers with additional sections on Traceability of Software Requirements (Section 4), Formal Methods and Its Tools (Section 5), Unifying Theories of Programming (UTP) and Theory of Institutions (Section 6). Please refer to abstract of [7,8]. Key difference of this draft from our recently anticipated ones with similar titles, i.e. AACS 2025 [7] and SAIV 2025 [8] is: [7] is a two page submission to ADAPT Annual Conference, Ireland. Submitted on 18th of March, 2025, it went through the light-weight blind review and accepted for poster presentation. Conference was held on 15th of May, 2025; [8] is a nine page paper with additional nine pages of references and summary tables, submitted to Symposium on AI Verification (SAIV 2025) on 24th of April, 2025. It went through rigorous review process. The uploaded version on arXiv.org [8] is the improved one of the submission, after addressing the specific suggestions to improve the paper.