(2021) Neural Circuit Synthesis from Specification Patterns.
|
Text
Neural Circuit Synthesis from Specification Patterns.pdf Download (844kB) | Preview |
Abstract
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Conference: | NeurIPS Conference on Neural Information Processing Systems |
| Depositing User: | Frederik Schmitt |
| Date Deposited: | 06 May 2022 07:01 |
| Last Modified: | 06 May 2022 07:01 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3653 |
Actions
Actions (login required)
 |
View Item |