# NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis

arXiv: https://arxiv.org/abs/2401.12131 · HTML: https://mlsanity.com/paper/2401.12131/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 31 of its 62 references that are in the map.
- First posted on arXiv 22 Jan 2024.

## Builds on (most cited first, 30 of 31)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Efficient Estimation of Word Representations in Vector Space](https://mlsanity.com/paper/1301.3781/) (2013)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [DreamCoder: Growing generalizable, interpretable knowledge with wake-sleep Bayesian program learning](https://mlsanity.com/paper/2006.08381/) (2020)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [A Neural Network Solves, Explains, and Generates University Math Problems by Program Synthesis and Few-Shot Learning at Human Level](https://mlsanity.com/paper/2112.15594/) (2021)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Teaching Temporal Logics to Neural Networks](https://mlsanity.com/paper/2003.04218/) (2020)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [Learning to Reason in Large Theories without Imitation](https://mlsanity.com/paper/1905.10501/) (2019)
- [From Spot 2.0 to Spot 2.10: What's New?](https://mlsanity.com/paper/2206.11366/) (2022)
- [CLN2INV: Learning Loop Invariants with Continuous Logic Networks](https://mlsanity.com/paper/1909.11542/) (2019)
- [HOList: An Environment for Machine Learning of Higher-Order Theorem Proving](https://mlsanity.com/paper/1904.03241/) (2019)
- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [Iterative Circuit Repair Against Formal Specifications](https://mlsanity.com/paper/2303.01158/) (2023)
- [BoSy: An Experimentation Framework for Bounded Synthesis](https://mlsanity.com/paper/1803.09566/) (2018)
- [The Reactive Synthesis Competition (SYNTCOMP): 2018-2021](https://mlsanity.com/paper/2206.00251/) (2022)
- [Scaling Neural Program Synthesis with Distribution-based Search](https://mlsanity.com/paper/2110.12485/) (2021)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)
- [A High-Level LTL Synthesis Format: TLSF v1.1](https://mlsanity.com/paper/1604.02284/) (2016)
- [Guessing Winning Policies in LTL Synthesis by Semantic Learning](https://mlsanity.com/paper/2305.15109/) (2023)
- [Data Generation for Neural Programming by Example](https://mlsanity.com/paper/1911.02624/) (2019)
- [Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability](https://mlsanity.com/paper/2204.06079/) (2022)

## Built on by (most cited first, 3 of 3)

- [SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning](https://mlsanity.com/paper/2501.17496/) (2025)
- [SemML 2.0: Synthesizing Controllers for LTL](https://mlsanity.com/paper/2604.24102/) (2026)
- [Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models](https://mlsanity.com/paper/2605.15131/) (2026)

## Abstract (arXiv)

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.