# Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 14 of its 32 references that are in the map.
- First posted on arXiv 20 Apr 2026.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Specification Patterns for Robotic Missions](https://mlsanity.com/paper/1901.02077/) (2019)
- [Lessons from the Use of Natural Language Inference (NLI) in Requirements Engineering Tasks](https://mlsanity.com/paper/2405.05135/) (2024)
- [Improving Requirements Completeness: Automated Assistance through Large Language Models](https://mlsanity.com/paper/2308.03784/) (2023)
- [Large Language Models (LLMs) for Requirements Engineering (RE): A Systematic Literature Review](https://mlsanity.com/paper/2509.11446/) (2025)
- [Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs](https://mlsanity.com/paper/2512.17334/) (2025)
- [Formal Consistency Checking over Specifications in Natural Languages](https://mlsanity.com/paper/1405.5003/) (2014)
- [Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects](https://mlsanity.com/paper/2507.14330/) (2025)
- [Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles](https://mlsanity.com/paper/2601.12845/) (2026)
- [LLM-based Satisfiability Checking of String Requirements by Consistent Data and Checker Generation](https://mlsanity.com/paper/2506.16639/) (2025)

## Abstract (arXiv)

Early-stage specifications of safety-critical systems are typically expressed in natural language, making it difficult to derive formal properties suitable for verification and needed to guarantee safety. While recent Large Language Model (LLM)-based approaches can generate formal artifacts from text, they mainly focus on syntactic correctness and do not ensure semantic alignment between informal requirements and formally verifiable properties. We propose an agentic methodology that automatically extracts verification-ready properties from unstructured specifications. The modular pipeline combines requirement extraction, compatibility filtering with respect to a target formalism, and translation into formal properties. Experimental results across three scenarios show that the pipeline generates syntactically and semantically aligned formal properties with a 77.8% accuracy. By explicitly accounting for modeling and verification constraints, the approach is a paving step towards exploiting Artificial Intelligence (AI) to bridge the gap between informal descriptions and semantically meaningful formal verification.