Automated Formalization of Probabilistic Requirements from Structured Natural Language

• URL: http://arxiv.org/abs/2512.15788v1
• Date: Mon, 15 Dec 2025 20:20:27 GMT
• Title: Automated Formalization of Probabilistic Requirements from Structured Natural Language
• Authors: Anastasia Mavridou, Marie Farrell, Gricel Vázquez, Tom Pressburger, Timothy E. Wang, Radu Calinescu, Michael Fisher,
• Abstract summary: We extend NASA's Formal Requirement Elicitation Tool (FRET) with support for the specification of unambiguous and correct probabilistic requirements.<n>We propose and develop a formal, compositional, and automated approach for translating structured natural-language requirements into formulas in probabilistic temporal logic.
• Score: 2.8065951726067726
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Integrating autonomous and adaptive behavior into software-intensive systems presents significant challenges for software development, as uncertainties in the environment or decision-making processes must be explicitly captured. These challenges are amplified in safety- and mission-critical systems, which must undergo rigorous scrutiny during design and development. Key among these challenges is the difficulty of specifying requirements that use probabilistic constructs to capture the uncertainty affecting these systems. To enable formal analysis, such requirements must be expressed in precise mathematical notations such as probabilistic logics. However, expecting developers to write requirements directly in complex formalisms is unrealistic and highly error-prone. We extend the structured natural language used by NASA's Formal Requirement Elicitation Tool (FRET) with support for the specification of unambiguous and correct probabilistic requirements, and develop an automated approach for translating these requirements into logical formulas. We propose and develop a formal, compositional, and automated approach for translating structured natural-language requirements into formulas in probabilistic temporal logic. To increase trust in our formalizations, we provide assurance that the generated formulas are well-formed and conform to the intended semantics through an automated validation framework and a formal proof. The extended FRET tool enables developers to specify probabilistic requirements in structured natural language, and to automatically translate them into probabilistic temporal logic, making the formal analysis of autonomous and adaptive systems more practical and less error-prone.

Related papers

• Towards Worst-Case Guarantees with Scale-Aware Interpretability [58.519943565092724]
  Neural networks organize information according to the hierarchical, multi-scale structure of natural data.<n>We propose a unifying research agenda -- emphscale-aware interpretability -- to develop formal machinery and interpretability tools.
  arXiv  Detail & Related papers  (2026-02-05T01:22:31Z)
• Multi-Agent Procedural Graph Extraction with Structural and Logical Refinement [66.51979814832332]
  model formulates procedural graph extraction as a multi-round reasoning process with dedicated structural and logical refinement.<n>Experiments demonstrate that model achieves substantial improvements in both structural correctness and logical consistency over strong baselines.
  arXiv  Detail & Related papers  (2026-01-27T04:00:48Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• Agentic System with Modal Logic for Autonomous Diagnostics [0.3437656066916039]
  We argue that scaling the structure, fidelity, and logical consistency of agent reasoning is a crucial, yet underexplored, dimension of AI research.<n>This paper introduces a neuro-symbolic multi-agent architecture where the belief states of individual agents are formally represented as Kripke models.<n>In this work, we use immutable, domain-specific knowledge to make an informed root cause diagnosis, which is encoded as logical constraints essential for proper, reliable, and explainable diagnosis.
  arXiv  Detail & Related papers  (2025-09-15T14:03:06Z)
• Formalizing Operational Design Domains with the Pkl Language [0.4349640169711269]
  The deployment of automated functions that can operate without direct human supervision has changed safety evaluation in domains seeking higher levels of automation.<n>To make a convincing safety claim, the developer must present a thorough justification argument, supported by evidence, that a function is free from unreasonable risk when operated in its intended context.<n>This paper presents a way to formalize an Operational Design Domain specification (ODD) in the Pkl language.
  arXiv  Detail & Related papers  (2025-09-02T11:41:27Z)
• Data Dependency-Aware Code Generation from Enhanced UML Sequence Diagrams [54.528185120850274]
  We propose a novel step-by-step code generation framework named API2Dep.<n>First, we introduce an enhanced Unified Modeling Language (UML) API diagram tailored for service-oriented architectures.<n>Second, recognizing the critical role of data flow, we introduce a dedicated data dependency inference task.
  arXiv  Detail & Related papers  (2025-08-05T12:28:23Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• 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)
• Foundation Models for Logistics: Toward Certifiable, Conversational Planning Interfaces [59.80143393787701]
  Large language models (LLMs) can handle uncertainty and promise to accelerate replanning while lowering the barrier to entry.<n>We introduce a neurosymbolic framework that pairs the accessibility of natural-language dialogue with verifiable guarantees on goal interpretation.<n>A lightweight model, fine-tuned on just 100 uncertainty-filtered examples, surpasses the zero-shot performance of GPT-4.1 while cutting inference latency by nearly 50%.
  arXiv  Detail & Related papers  (2025-07-15T14:24:01Z)
• Un marco conceptual para la generación de requerimientos de software de calidad [0.0]
  Large language models (LLMs) have emerged to enhance natural language processing tasks.<n>This work aims to use these models to improve the quality of software requirements written in natural language.
  arXiv  Detail & Related papers  (2025-04-14T19:12:18Z)
• Technical Report on Neural Language Models and Few-Shot Learning for Systematic Requirements Processing in MDSE [1.6286277560322266]
  This paper is based on the analysis of an open-source set of automotive requirements. We derive domain-specific language constructs helping us to avoid ambiguities in requirements and increase the level of formality.
  arXiv  Detail & Related papers  (2022-11-16T18:06:25Z)
• Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
  We study the problem of learning to satisfy temporal logic specifications with a group of agents in an unknown environment. We develop the first multi-agent reinforcement learning technique for temporal logic specifications. We provide correctness and convergence guarantees for our main algorithm.
  arXiv  Detail & Related papers  (2021-02-01T01:13:03Z)

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.