cispa_all_3653.pdf (824.69 kB)

Neural Circuit Synthesis from Specification Patterns

Download (824.69 kB)
Version 2 2023-12-11, 20:14
Version 1 2023-11-29, 18:18
conference contribution
posted on 2023-12-11, 20:14 authored by Frederik SchmittFrederik Schmitt, Christopher Hahn, Markus N. Rabe, Bernd FinkbeinerBernd Finkbeiner
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.


Preferred Citation

Frederik Schmitt, Christopher Hahn, Markus Rabe and Bernd Finkbeiner. Neural Circuit Synthesis from Specification Patterns. In: Conference on Neural Information Processing Systems (NeurIPS). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Conference on Neural Information Processing Systems (NeurIPS)

Legacy Posted Date


Open Access Type

  • Gold


@inproceedings{cispa_all_3653, title = "Neural Circuit Synthesis from Specification Patterns", author = "Schmitt, Frederik and Hahn, Christopher and Rabe, Markus N. and Finkbeiner, Bernd", booktitle="{Conference on Neural Information Processing Systems (NeurIPS)}", year="2021", }

Usage metrics


    No categories selected


    Ref. manager