Realisability-Driven Repair of Natural-Language Requirements via Neuro-Symbolic Reasoning

Constructing realisable natural-language (NL) requirements for reactive systems is challenging due to ambiguity, informality, and missing assumptions, which often lead to inconsistencies that only emerge during system integration. We propose SpecRepair, a neuro-symbolic framework that integrates Large Language Models (LLMs) with reactive synthesis to support the construction of such requirements. NL requirements are translated into intent models using LLMs and analysed for realisability using temporal logic. When unrealisability is detected, the resulting counterstrategies are used to generate human-readable explanations and suggest candidate repairs using LLMs. This establishes an iterative loop from NL requirements to formal analysis and back to refinement. The process can be repeated until a realisable specification is obtained, while preserving interpretability by mapping repaired models back to NL. Preliminary results on 40 benchmark specifications show that SpecRepair repairs 16 of the 25 originally unrealisable specifications, compared with 7 for a direct LLM-to-LTL baseline. End-to-end, SpecRepair successfully completes 28 specifications, compared to 11 for the baseline. ... mehrA paired comparison indicates a statistically significant improvement. These gains come at the cost of additional tokens and runtime.