Natural Language based Specification and Verification

• URL: http://arxiv.org/abs/2605.11315v1
• Date: Mon, 11 May 2026 23:07:22 GMT
• Title: Natural Language based Specification and Verification
• Abstract summary: Large language models (LLMs) have shown strong performance in identifying security vulnerabilities in large, mature open-source systems.<n>In this paper, we investigate a different approach: using LLMs both to generate specifications and to verify implementations compositionally when the specifications are expressed in natural language.
• Score: 7.776617933367878
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent frontier large language models (LLMs) have shown strong performance in identifying security vulnerabilities in large, mature open-source systems. As LLM-generated code becomes increasingly common, a natural goal is to prevent such models from producing vulnerable implementations in the first place. Formal verification offers a principled route to this objective, but existing verification pipelines typically require specifications written in rigid formal languages. Prior work has explored using LLMs to synthesize such specifications, with limited success. In this paper, we investigate a different approach: using LLMs both to generate specifications and to verify implementations compositionally when the specifications are expressed in natural language. Our preliminary results suggest that this approach is promising.

Related papers

• The Language of Security: How Prompt Syntax Shapes Secure Code Generation in Open LLMs [12.213106649470973]
  Large Language Models (LLMs) are increasingly used for source code generation despite their outputs often exhibiting security vulnerabilities.<n>We show that specific syntactic elements, such as constraints, guards, and concept bindings, and their position within the prompt consistently affect the likelihood of generating insecure code.<n>These findings identify prompt syntax as a concrete security control surface and provide actionable guidance for reducing vulnerability risk in LLM-assisted development.
  arXiv  Detail & Related papers  (2026-07-17T13:20:21Z)
• KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base [9.796586560498026]
  We propose KBSpec, which augments large language models (LLMs) with dual-source knowledge of formal specification language corpora.<n>Results show that KBSpec improves verification pass rates by 10-25% over state-of-the-art LLM-based approaches.
  arXiv  Detail & Related papers  (2026-06-19T11:37:00Z)
• Assessing the Impact of Requirement Ambiguity on LLM-based Function-Level Code Generation [14.755517753769837]
  We introduce Orchid, the first code generation benchmark specifically designed with ambiguous requirements.<n>It comprises 1,304 function-level tasks covering four distinct types of ambiguity: lexical, syntactic, semantic, and vagueness.<n>Our results demonstrate that ambiguity consistently degrades the performance of all evaluated LLMs, with the most pronounced negative effects observed in highly advanced models.
  arXiv  Detail & Related papers  (2026-04-23T10:07:33Z)
• Towards Autoformalization of LLM-generated Outputs for Requirement Verification [0.6015898117103068]
  Autoformalization, the process of translating informal statements into formal logic, has gained renewed interest with the emergence of powerful Large Language Models.<n>This paper explores the use of a simple LLM-based autoformalizer to verify LLM-generated outputs against a small set of natural language requirements.<n>Our findings, while limited, suggest that autoformalization holds significant potential for ensuring the fidelity and logical consistency of LLM-generated outputs.
  arXiv  Detail & Related papers  (2025-11-14T19:45:17Z)
• Verifying Memoryless Sequential Decision-making of Large Language Models [4.570003973862485]
  We introduce a tool for rigorous and automated verification of large language model (LLM)-based policies in sequential decision-making tasks.<n>Given a Markov decision process (MDP) representing the sequential decision-making task, an LLM policy, and a safety requirement expressed as a PCTL formula, our approach incrementally constructs only the reachable portion of the MDP.<n>The resulting formal model is checked with Storm to determine whether the policy satisfies the specified safety property.
  arXiv  Detail & Related papers  (2025-10-08T08:31:48Z)
• How Good LLM-Generated Password Policies Are? [0.1747820331822631]
  We study the application of Large Language Models within the context of Cybersecurity Access Control Systems.<n>Specifically, we investigate the consistency and accuracy of LLM-generated password policies, translating natural language prompts into executable pwquality.conf configuration files.<n>Our findings underscore significant challenges in the current generation of LLMs and contribute valuable insights into refining the deployment of LLMs in Access Control Systems.
  arXiv  Detail & Related papers  (2025-06-10T01:12:31Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  We introduce a type-constrained decoding approach that leverages type systems to guide code generation.<n>For this purpose, we develop novel prefix automata and a search over inhabitable types, forming a sound approach to enforce well-typedness on LLM-generated code.<n>Our approach reduces compilation errors by more than half and significantly increases functional correctness in code synthesis, translation, and repair tasks.
  arXiv  Detail & Related papers  (2025-04-12T15:03:00Z)
• Unnatural Languages Are Not Bugs but Features for LLMs [92.8332103170009]
  Large Language Models (LLMs) have been observed to process non-human-readable text sequences, such as jailbreak prompts.<n>We present a systematic investigation challenging this perception, demonstrating that unnatural languages contain latent features usable by models.
  arXiv  Detail & Related papers  (2025-03-02T12:10:17Z)
• RuAG: Learned-rule-augmented Generation for Large Language Models [62.64389390179651]
  We propose a novel framework, RuAG, to automatically distill large volumes of offline data into interpretable first-order logic rules. We evaluate our framework on public and private industrial tasks, including natural language processing, time-series, decision-making, and industrial tasks.
  arXiv  Detail & Related papers  (2024-11-04T00:01:34Z)
• DECIDER: A Dual-System Rule-Controllable Decoding Framework for Language Generation [57.07295906718989]
  Constrained decoding approaches aim to control the meaning or style of text generated by pre-trained large language (Ms also PLMs) for various tasks at inference time.<n>These methods often guide plausible continuations by greedily and explicitly selecting targets.<n>Inspired by cognitive dual-process theory, we propose a novel decoding framework DECIDER.
  arXiv  Detail & Related papers  (2024-03-04T11:49:08Z)
• 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)
• LMPriors: Pre-Trained Language Models as Task-Specific Priors [78.97143833642971]
  We develop principled techniques for augmenting our models with suitable priors. This is to encourage them to learn in ways that are compatible with our understanding of the world. We draw inspiration from the recent successes of large-scale language models (LMs) to construct task-specific priors distilled from the rich knowledge of LMs.
  arXiv  Detail & Related papers  (2022-10-22T19:09:18Z)
• Exploring Software Naturalness through Neural Language Models [56.1315223210742]
  The Software Naturalness hypothesis argues that programming languages can be understood through the same techniques used in natural language processing. We explore this hypothesis through the use of a pre-trained transformer-based language model to perform code analysis tasks.
  arXiv  Detail & Related papers  (2020-06-22T21:56:14Z)

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.