SATISFIABILITY IS NOT ENOUGH: FIDELITY-GATED REPAIR OF LLM-EXTRACTED HYBRID AUTOMATA

Large language models can translate technical manuals into symbolic models, but verifier-guided correction creates a distinct failure mode: a proposer can make a model satisfiable by deleting the obligations that made it unsatisfiable. We call this solver gaming. We present a source-traced pipeline that extracts partially observ- able hybrid-automaton (POHA) graphs, checks discrete and algebraic constraints with an SMT (Satisfiability Modulo Theories) Solver, and places a deterministic fidelity gate before repaired graphs can become active. The gate preserves source traces, declarations, guards, effects, evidence, minimum durations, sensor status, epistemology scope, and safety classifications; source support for additions remains a separate evidence-review obligation. In a natural pre-gate run, an unconstrained loop reached Satisfiability (SAT) through ten unsupported safety downgrades; the gate rejected both affected edits. In a controlled 20-case benchmark, all 15 valid additive candidates were accepted and all 5 solver-satisfying effect deletions were rejected. Separately, we test the utility of raw, not fidelity-gated, graphs for down- stream decision support. Across a chosen dataset of 100 cyber-physical scenarios and five trials per scenario, graph augmentation improved exact decision accuracy from 77.33% to 87.33% on a challenge set and from 78.00% to 87.00% on a repre- sentative set. These results establish repair-integrity behavior and raw-graph utility as separate findings: they do not establish physical completeness or downstream benefit from repaired graphs. However, we note that formal graph structures can occasionally over-constrain valid actions, increasing False Rejection Rate (FRR) in exchange for strict safety compliance.