From Natural Language to Formal Specifications: A Metamodel-Driven LLM Pipeline
TL;DR
This case study assesses the feasibility of combining LLM-based extraction, metamodel-guided refinement, automated validation, and human correction for requirements formalization and evaluates the approach on the ten published ACAS Xu safety properties.
Abstract
Formal verification relies on machine-processable specifications, whereas requirements are commonly documented in natural language, whose contextual and implicit interpretation complicates automated formalization. Existing approaches either impose a controlled or structured language on the user, or rely on large language models to formalize requirements directly, without structural guarantees on the output. We propose a metamodel-driven pipeline that transforms unrestricted natural-language requirements into verifiable formal specifications. An LLM first extracts the requirement semantics into a target-independent intermediate model, which is subsequently refined through target-specific and domain-enriched representations before generation of the concrete formal syntax. Each intermediate artifact is checked for schema conformance and cross-element consistency, with detected errors used to guide automatic correction or presented to the user for semantic review. We evaluate the approach on the ten published ACAS Xu safety properties, using WhyML as the target formalism and comparing the proposed multi-step strategy with direct single-call formalization. The case study assesses the feasibility of combining LLM-based extraction, metamodel-guided refinement, automated validation, and human correction for requirements formalization.