Counterexample-Guided Discovery of Executable Semantic State Abstractions

A semantic representation in a neural network may predict outputs without containing enough information to determine how it evolves through subsequent computation, and therefore need not define an independently executable high-level model. We study how to select the necessary state from given semantic variables and candidate auxiliary variables, and how to synthesize a high-level program that reproduces the transitions and specified outputs of a fixed computational system. Selecting an auxiliary variable also requires determining its successor, so additional features can destroy closure. We give a verifiable sufficient condition under which a dependency graph yields the unique least admissible state. Without this condition, minimum auxiliary-state selection is NP-complete for explicit finite tables even with an involutive transition and a constant response, and remains NP-hard on a rational box with quadratic supplied functions. State-pair and single-state counterexamples separate state insufficiency from program inexpressibility; for a fixed template affine in its $p$ unknown coefficients, exact synthesis needs at most $p+1$ verification calls. Cost-ordered search is optimal within the prescribed finite program class. With a positive verification margin, numerical synthesis terminates and yields finite-execution error bounds under certified domain invariance. Experiments on polynomial instances and ten trained networks demonstrate exact discovery, infeasibility certification, and a separation between greatest and minimum selections. Tests on $120$ finite-table systems isolate the auxiliary-update requirements behind minimum-state selection, while alternative feature libraries on the same frozen networks separate state sufficiency from program expressibility and exhibit multiple minimal selectors without a least one.