A Short Survey on Formalising Software Requirements using Large Language Models

• URL: http://arxiv.org/abs/2506.11874v1
• Date: Fri, 13 Jun 2025 15:26:58 GMT
• Title: A Short Survey on Formalising Software Requirements using Large Language Models
• Authors: Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan,
• Abstract summary: This paper presents a focused literature survey on the use of large language models (LLM) to assist in writing formal specifications for software.<n>A summary of thirty-five key papers is presented, including examples for specifying programs written in Dafny, C and Java.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper presents a focused literature survey on the use of large language models (LLM) to assist in writing formal specifications for software. A summary of thirty-five key papers is presented, including examples for specifying programs written in Dafny, C and Java. This paper arose from the project VERIFAI - Traceability and verification of natural language requirements that addresses the challenges in writing formal specifications from requirements that are expressed in natural language. Our methodology employed multiple academic databases to identify relevant research. The AI-assisted tool Elicit facilitated the initial paper selection, which were manually screened for final selection. The survey provides valuable insights and future directions for utilising LLMs while formalising software requirements.

Related papers

• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1 aims to investigate automated and semi-automated approaches to bridge this gap.<n>This position paper presents a preliminary synthesis of relevant literature to identify recurring challenges and prospective research directions.
  arXiv  Detail & Related papers  (2025-07-18T19:15:50Z)
• Formalising Software Requirements using Large Language Models [0.0]
  The project addresses the challenges in the traceability and verification of formal specifications.<n>It provides support for the automatic generation of the formal specifications and the traceability of the requirements from the initial software design stage through the systems implementation and verification.
  arXiv  Detail & Related papers  (2025-06-12T13:55:01Z)
• TALLMesh: a simple application for performing Thematic Analysis with Large Language Models [0.0]
  Thematic analysis (TA) is a widely used qualitative research method for identifying and interpreting patterns within textual data.<n>Recent research has shown that it is possible to satisfactorily perform TA using Large Language Models (LLMs)<n>This paper presents a novel application using LLMs to assist researchers in conducting TA.
  arXiv  Detail & Related papers  (2025-04-05T15:10:08Z)
• Zero-Shot Keyphrase Generation: Investigating Specialized Instructions and Multi-Sample Aggregation on Large Language Models [52.829293635314194]
  Keyphrase generation is a long-standing NLP task for automatically generating keyphrases for a given document.<n>We focus on the zero-shot capabilities of open-source instruction-tuned LLMs (Phi-3, Llama-3) and the closed-source GPT-4o for this task.
  arXiv  Detail & Related papers  (2025-03-01T19:38:57Z)
• Personalized Multimodal Large Language Models: A Survey [127.9521218125761]
  Multimodal Large Language Models (MLLMs) have become increasingly important due to their state-of-the-art performance and ability to integrate multiple data modalities.<n>This paper presents a comprehensive survey on personalized multimodal large language models, focusing on their architecture, training methods, and applications.
  arXiv  Detail & Related papers  (2024-12-03T03:59:03Z)
• Benchmarking Large Language Models for Conversational Question Answering in Multi-instructional Documents [61.41316121093604]
  We present InsCoQA, a novel benchmark for evaluating large language models (LLMs) in the context of conversational question answering (CQA) Sourced from extensive, encyclopedia-style instructional content, InsCoQA assesses models on their ability to retrieve, interpret, and accurately summarize procedural guidance from multiple documents. We also propose InsEval, an LLM-assisted evaluator that measures the integrity and accuracy of generated responses and procedural instructions.
  arXiv  Detail & Related papers  (2024-10-01T09:10:00Z)
• Eliciting Human Preferences with Language Models [56.68637202313052]
  Language models (LMs) can be directed to perform target tasks by using labeled examples or natural language prompts. We propose to use *LMs themselves* to guide the task specification process. We study GATE in three domains: email validation, content recommendation, and moral reasoning.
  arXiv  Detail & Related papers  (2023-10-17T21:11:21Z)
• How Effective are Large Language Models in Generating Software Specifications? [14.170320751508502]
  Large Language Models (LLMs) have been successfully applied to numerous Software Engineering (SE) tasks.<n>We conduct the first empirical study to evaluate the capabilities of LLMs for generating software specifications from software comments or documentation.
  arXiv  Detail & Related papers  (2023-06-06T00:28:39Z)
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models [3.1143846686797314]
  We present nl2spec, a framework for applying Large Language Models (LLMs) derive formal specifications from unstructured natural language. We introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization.
  arXiv  Detail & Related papers  (2023-03-08T20:08:53Z)
• Recitation-Augmented Language Models [85.30591349383849]
  We show that RECITE is a powerful paradigm for knowledge-intensive NLP tasks. Specifically, we show that by utilizing recitation as the intermediate step, a recite-and-answer scheme can achieve new state-of-the-art performance.
  arXiv  Detail & Related papers  (2022-10-04T00:49:20Z)
• The Use of NLP-Based Text Representation Techniques to Support Requirement Engineering Tasks: A Systematic Mapping Review [1.5469452301122177]
  The research direction has changed from the use of lexical and syntactic features to the use of advanced embedding techniques. We identify four gaps in the existing literature, why they matter, and how future research can begin to address them.
  arXiv  Detail & Related papers  (2022-05-17T02:47:26Z)
• Detecting Text Formality: A Study of Text Classification Approaches [78.11745751651708]
  This work proposes the first to our knowledge systematic study of formality detection methods based on statistical, neural-based, and Transformer-based machine learning methods. We conducted three types of experiments -- monolingual, multilingual, and cross-lingual. The study shows the overcome of Char BiLSTM model over Transformer-based ones for the monolingual and multilingual formality classification task.
  arXiv  Detail & Related papers  (2022-04-19T16:23:07Z)
• SPECTER: Document-level Representation Learning using Citation-informed Transformers [51.048515757909215]
  SPECTER generates document-level embedding of scientific documents based on pretraining a Transformer language model. We introduce SciDocs, a new evaluation benchmark consisting of seven document-level tasks ranging from citation prediction to document classification and recommendation.
  arXiv  Detail & Related papers  (2020-04-15T16:05:51Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.