NeuroFORM: Neuro-Symbolic Formalization of Legal Rules with Counterexample-Guided Refinement

A generated formal specification can execute and be satisfiable while still misrepresenting its source rule—for example, by omitting an exception or an applicability condition. We study whether such behavioural errors can be detected and used to repair specifications at test time. NeuroFORM treats a language model as an untrusted proposal generator: given a legal clause and an expert-verified structured representation, it generates a candidate specification, compares its solver outcomes with expected outcomes on source-conditioned scenarios, and feeds failures back for bounded repair. The method operates on propositional encodings of obligations, permissions, prohibitions, exceptions, and boundary conditions. We evaluate it on 238 provisions from GDPR, CCPA, DPDP, and PIPL, with 2,322 span-level annotations and six behavioural scenario categories per provision. Across three independent runs, the full system achieves mean held-out behavioural accuracies of 78.43% with an LLM generator and 75.07% with an SLM generator, exceeding the strongest corresponding functional baselines by 14.77 and 20.33 percentage points, respectively. Among cases eventually repaired, 99.5% succeed by the second attempt within the successful repair invocation in both model tiers. These findings show how behavioural verifier failures can provide effective test-time feedback for generated symbolic specifications.