Repairing LLM-Generated Specifications with Deterministic Diagnosis
Large language models (LLMs) are increasingly used as formalizers: given a reasoning problem expressed in natural language, they produce a formal specification that a symbolic solver can then solve, with guarantees relative to that specification. Many specifications are runnable yet semantically wrong, encoding incorrect constraints, domains, objectives, predicates, or goals, and solver-error feedback dries up once execution succeeds. Purely LLM-based diagnosis, lacking a formal ground truth, often fails to spot these errors, and its ungrounded critiques cause regressions in 11.8% of initially correct specifications in our experiments. We propose DRAGO, a repair framework that replaces th...
| Authors | Giovanni Vaccarino, Emanuele La Malfa, Dehai Min et al. |
|---|---|
| Primary category | cs.AI |
| Published | 15 October 2026 |
| Last updated at source | 15 October 2026 |
Popularity, last 6 days
0 now. Counts as reported by the source, snapshotted daily by Silytics.
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 24 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.