Neural Circuit Synthesis from Specification Patterns
Frederik Schmitt,Christopher Hahn,Markus N Rabe,Bernd Finkbeiner
We train hierarchical Transformers on the task of synthesizing hardware circuits directly out of high-level logical speciufb01cations 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 sufufb01cient amounts of training data. In this paper, we consider a method to generate large amounts of additional training data, i.e., pairs of speciufb01cations and circuits implementing them. We ensure that this synthetic data is sufufb01ciently close to human-written speciufb01cations by mining common patterns from the speciufb01cations used in the synthesis competitions. We show that hierarchical Transformers trained on this synthetic data solve a signiufb01cant portion of problems from the synthesis competitions, and even out-of-distribution examples from a recent case study.
