NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis

TL;DR

NeuroSynt addresses reactive synthesis by integrating a Transformer-based neural solver with model-checking verification and parallel symbolic solvers to ensure soundness and completeness. The framework is designed as an extensible, Dockerized portfolio that translates TLSF inputs to $LTL$ assumptions/guarantees, then combines neural and symbolic results to produce $AIGER$ implementations, validated by model checkers. On SYNTCOMP 2022, NeuroSynt delivers novel solves and faster solving times, achieving additional solvable instances when combined with symbolic tools and yielding smaller circuits. The work demonstrates strong generalization to larger and out-of-distribution specifications and provides an open-source platform for further neuro-symbolic exploration in reactive synthesis.

Abstract

We introduce NeuroSynt, a neuro-symbolic portfolio solver framework for reactive synthesis. At the core of the solver lies a seamless integration of neural and symbolic approaches to solving the reactive synthesis problem. To ensure soundness, the neural engine is coupled with model checkers verifying the predictions of the underlying neural models. The open-source implementation of NeuroSynt provides an integration framework for reactive synthesis in which new neural and state-of-the-art symbolic approaches can be seamlessly integrated. Extensive experiments demonstrate its efficacy in handling challenging specifications, enhancing the state-of-the-art reactive synthesis solvers, with NeuroSynt contributing novel solves in the current SYNTCOMP benchmarks.

Figures (19)

• Figure 1: An overview of NeuroSynt.
• Figure 2: Communication diagram of gRPC calls for a run of NeuroSynt, calling the Symbolic Solver and the neural solver, including model-checking.
• Figure 3: The protobuf definition for a SynSolution, SynProblem, and decomposed LTL specification. Slightly simplified for easier comprehension. We refer the reader to the artifact and our repository for the full definitions.
• Figure 4: Previous datasetschmittNeuralCircuitSynthesis2021, compared with the new final dataset. Comparing the number of atomic propositions in a sample, the largest variable id in the AIGER circuit, and the average size of properties.
• Figure 5: Schematic view of the Hierarchical Transformer, with illustrated inputs/outputs of the reactive synthesis application. The encoder shows the hierarchical self-attention with separation into local and global layers. For simplicity, we show one local and global layer and only two assumptions and guarantees with two tokens each.