NeuroSynTheos: Learning to accelerate counterexample-guided reactive synthesis modulo theories

Reactive synthesis from temporal logic modulo theories (LTLt) automatically con- structs correct-by-construction controllers for systems with arithmetic constraints— elevators, thermostats, robotic patrols—but the state-of-the-art CEGRES algorithm times out on 77% of existing benchmarks due to a fundamental bottleneck: it discovers the universally valid theory tautologies needed to refine its Boolean abstraction one at a time, through expensive counterexample analysis. We present NEUROSYNTHEOS, a neural augmentation of the CEGRES loop that predicts batches of tautologies at each refinement step. We formalize template invariance for parametric specification families, showing that the prediction problem reduces to constant re-instantiation when specifications share algebraic structure. We train a GNN over formula abstract syntax trees and an autoregressive transformer on tautology traces from 104 solved benchmarks. NEUROSYNTHEOS establishes a new state of the art for LTLt synthesis: on 83 standard benchmarks, it solves 60 ±1.2 specifications (vs. 19 for the previous best), resolving 41 that no prior method could handle within a 5-minute budget, while reducing the median itera- tion count by 5.2×with under 3 seconds of neural overhead. All predictions are SMT-verified before injection, preserving full soundness guarantees.