# Neural Circuit Synthesis from Specification Patterns

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

## Key facts

- Cited by 17 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 53 references that are in the map.
- First posted on arXiv 25 Jul 2021.

## Builds on (most cited first, 13 of 13)

- [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)
- [Neural Message Passing for Quantum Chemistry](https://mlsanity.com/paper/1704.01212/) (2017)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [Unsupervised Translation of Programming Languages](https://mlsanity.com/paper/2006.03511/) (2020)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Neuro-Symbolic Program Synthesis](https://mlsanity.com/paper/1611.01855/) (2016)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [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)
- [Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning](https://mlsanity.com/paper/1807.08058/) (2018)
- [BoSy: An Experimentation Framework for Bounded Synthesis](https://mlsanity.com/paper/1803.09566/) (2018)
- [A High-Level LTL Synthesis Format: TLSF v1.1](https://mlsanity.com/paper/1604.02284/) (2016)

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

- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Retrieval-Guided Reinforcement Learning for Boolean Circuit Minimization](https://mlsanity.com/paper/2401.12205/) (2024)
- [Iterative Circuit Repair Against Formal Specifications](https://mlsanity.com/paper/2303.01158/) (2023)
- [SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning](https://mlsanity.com/paper/2501.17496/) (2025)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)
- [Circuit Transformer: A Transformer That Preserves Logical Equivalence](https://mlsanity.com/paper/2403.13838/) (2024)
- [Guessing Winning Policies in LTL Synthesis by Semantic Learning](https://mlsanity.com/paper/2305.15109/) (2023)
- [INVICTUS: Optimizing Boolean Logic Circuit Synthesis via Synergistic Learning and Search](https://mlsanity.com/paper/2305.13164/) (2023)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [Attention Flows for General Transformers](https://mlsanity.com/paper/2205.15389/) (2022)
- [Neural Combinatorial Logic Circuit Synthesis from Input-Output Examples](https://mlsanity.com/paper/2210.16606/) (2022)
- [Learning Better Representations From Less Data For Propositional Satisfiability](https://mlsanity.com/paper/2402.08365/) (2024)
- [RNN Generalization to Omega-Regular Languages](https://mlsanity.com/paper/2509.02491/) (2025)
- [Learning Representations Through Contrastive Neural Model Checking](https://mlsanity.com/paper/2510.01853/) (2025)
- [Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models](https://mlsanity.com/paper/2605.15131/) (2026)

## Abstract (arXiv)

We train hierarchical Transformers on the task of synthesizing hardware circuits directly out of high-level logical specifications in linear-time temporal logic (LTL). The LTL synthesis problem is a well-known algorithmic challenge with a long history and an annual competition is organized to track the improvement of algorithms and tooling over time. New approaches using machine learning might open a lot of possibilities in this area, but suffer from the lack of sufficient amounts of training data. In this paper, we consider a method to generate large amounts of additional training data, i.e., pairs of specifications and circuits implementing them. We ensure that this synthetic data is sufficiently close to human-written specifications by mining common patterns from the specifications used in the synthesis competitions. We show that hierarchical Transformers trained on this synthetic data solve a significant portion of problems from the synthesis competitions, and even out-of-distribution examples from a recent case study.