Neural Circuit Synthesis from Specification Patterns
Authors: Frederik Schmitt
Christopher Hahn
Markus Norman Rabe
Bernd Finkbeiner
Venue: NeurIPS 2021 Poster (2021)
Keywords: Transformer
Temporal Logic
Synthesis
Circuits

Abstract: We train hierarchical Transformers on the task of synthesizing hardware circuits directly out of high-level logical speciﬁcations 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 sufﬁcient amounts of training data. In this paper, we consider a method to generate large amounts of additional training data, i.e., pairs of speciﬁcations and circuits implementing them. We ensure that this synthetic data is sufﬁciently close to human-written speciﬁcations by mining common patterns from the speciﬁcations used in the synthesis competitions. We show that hierarchical Transformers trained on this synthetic data solve a signiﬁcant portion of problems from the synthesis competitions, and even out-of-distribution examples from a recent case study.

Neural Circuit Synthesis from Specification Patterns
Frederik Schmitt
CISPA Helmholtz Center for Information Security
Saarbrücken, Germany
sreederiksshhifee www.ittttssspaeeeeee
Christopher Hahn
Markus N. Rabe
CISPA Helmholtz Center for Information Security
Google Research
Saarbrücken, Germany christopher hawn@cissa.ddeeeeeee
Mountain View, California, USA
mrabe@google.com
Bernd Finkbeiner
CISPA Helmholtz Center for Information Security
Saarbrücken, Germany f finkbeinee@Cispa..d
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 algo- rithms and tooling over time. New approaches using machine learning might open 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 additional training data, i.c. pairs of specifications and circuits implementing them. We ensure that this synthetic data sufficiently close to cations by mining common patterns from the specifications used in the synthesis competitions. We show that hierarchical Transformers trained on this synthetic data solve significant portion of problems from the synthesis competitions, and even oul-of-distribution examples from a recent case study.
specifi-
Introduction
In reactive synthesis, a circuit is automatically constructed from a logical specification given as formula in linear-time temporal logic (LTTL).. LTL is widely used by the verification community and the basis for industrial specification languages like the IÉEE standard PSL. 24]. Efficient synthesis tools for LTL would simplify the hardware design process: hardware designer could focus on specifying what the circuit is supposed to compute, instead of implementing how the computation done. LTL synthesis procedures, however, have to invoke involved reasoning engines, which turn often out to be infeasible when facing real-world problem instances. Much research has been conducted push this form of hardware construction process closer practice (see, for example, the synthesis of the AMBA protocol (5)). The high computational complexity of the general problem 2-EEXPIMEE-compleee
however, is far a barrier that seems insurmountable with classical, e.g.. automaton-basedd approaches. Recent successful applications of machine learning for logical tasks, such as SAT solving 45 46). hidher-order theorem proving [36]]] 3), and the LTT. trace generation problem [22] encourage new approaches to the I.TL. synthesis problem using machine learning. Similar to the success of machine learning for program synthesis, e.g., [37 20 42). machine learning approaches might open a lot of possibilities in hardware synthesis. For example, secondary design
35th Conference on Neural Information Processing Systems (NcurIPS 2021).

---

(assumptions)
(((((())))
(C((())
(guarantees:)
R
((6) (((((
((a))( 0n
(1)))(((m))
(((a))))
(14))
o ((-(2))))
(o) (O((h) R(((() -022) (((-(h)) (oo))))
(O(os)) (is))
Figure 1: A specification in our test set, consisting of assumption patterns and guarantee patterns (left). A circuit, predicted by a hierarchical Transformer, satisfying the specification (right).
goals, which cannot be easily formalized, might be incorporated into the process using natural language. Applying machine learning to the area of hardware synthesis, however, suffers from severe lack of sufficient amounts of training data.
In this paper, we consider method generate large amounts of additional training data, i.e., pairs of specifications and circuits implementing them. We show that hierarchical Transformers [33] can be trained on the circuit synthesis problem using the generated data and that the models can solve significant portion of problems from the annual synthesis competition. In practice, logical hardware specifications follow specific design patterns [2] To cope with the data scarcity of this problem, we propose a method that makes use of specification patterns, from which data for a successful training can be derived.
For example, a common LTL specification pattern looks as follows: -(r The formula describes response property, stating that at every point time (O), request must be eventually (O) followed by grant We obtain these patterns from the annual reactive synthesis competition [25].
We mined 2099 specification patterns from 346 benchmarks, which we split into assumption patterns and guarantee patterns. Assumption patterns restrict the space of possible inputs (environment behavior), and guarantee patterns deseribe how the circuit has to react the environment. From these specification patterns, we generate larger specifications by conjoining assumption patterns to a specification A and by conjoining guarantee patterns to a specification yçg. The implication A - Pa forms the final specification of the circuit. We obtained 200 000 specifications and used classical synthesis tools 14 35 to compute circuits satisfying the specifications. Figure [ shows an example held-out specification constructed in this fashion and a circuit predicted by one of our models (details on the data representation can be found in Section 3). When checking, the predicted circuit indeed satisfies the specification.
To train a machine learning model on the LTL synthesis task, we represent the decomposed speci- fications and circuits sequences and use hierarchical Transformers (33). We show that many of the model's predictions that differ from the circuits in our dataset satisfy the specifications when verifying the predictions i.e., the model constructs different, yet correct solution. When using beam search, models achieve an accuracy of up to 79.9% on our synthetic test data and up to 66.8% on the original formulas from SYNTCOMP. The Transformer can even solve diitr--diittibuttion formulas, taken from recent case study [1] i.e., formulas that were not used for the specification pattern mining. Furthermore, the models can solve generated test instances on which classical LTL synthesis tools timed out. In practice, it is essential to handle both realizable (i.e., when a hardware implementation exists) and unrealizable (i.e., when no hardware implementation exists) specifica- tions. We demonstrate that our approach achieves similar results on both realizable and unrealizable specifications.
Note that verifying the solutions, i.e. model- checkkng,, is by-far easier problem (PSPACE vs 2-EXPTIME) and typically be done in fraction of the time needed to synthesize the circuits classically.

---

The remainder of this paper is structured as follows: Related work is presented in Section 2 The data representation and generation process described in Section
3 The experimental setup and the experimental evaluation are presented in Section 4 and Section respectively. We conclude the paper in Section 6
2 Related Work
Neural architectures for logical reasoning. Neural architectures for logical and mathematical reasoning have been studied recently. The closest work is the application of Transformers to the LTL trace generation problem demonstrating the generalization abilities of Transformers to the semantics of logics [22]. Despite the substantially greater complexity of the LTL synthesis problem, we are able to demonstrate the same generalization realizable and unrealizable specifications while for the LTL trace generation problem the satisfiabilityy of LTL formulas was assumed. Lample and Charton trained Transformers on symbolic integration and solving differential equations and were able outperform commercial systems a synthetic dataset 31. Similar to our findings Lample and Charton observed significant improvements in the Transformer's accuracy when using beam search. Rabe al. applied Transformers formal mathematical statements and demonstrated the Transformer's 's reasoning abilities on tasks such as type inference and completing missing assumptions [41]. In contrast to the supervised setting in this work, Rabe et al. trained Transformers on an unsupervised skip-tree task that outperforms skip-sequence tasks for language modeling. For propositional logic Selsam et al. applied graph neural networks [43] 18] to solve the satisfibiliiyy problem [46]. In subsequent work Selsam and Bjømner applied the same architecture to the unsat-core prediction problem and demonstrated that their model can be used as heuristic to speed up SAT solvers [45]. Lederman et al. applied graph neural networks to quantified Boolean formulas to learn heuristies for QBF solvers through deep reinforcement learning (32.. Paliwal et al. trained graph neural networks on higher-order logic terms to predict tactics for higher-order theorem proving [36]. When integrated with the DeepHOL. (3] neural theorem prover the graph neural networks achieved state-of-the performance for higher- order proof search. Similar, Balunović et al. applied graph neural networks to SMT formulas to predict tactics for SMT solvers [2]. Strategies synthesized from their model demonstrated significant improvements over hand-crafted strategies from state- offte--o--he-arr SMT solvers. Earlier works on applying learning to mathematics, has focused on ranking premises clauses Cairns [8], Urban 48 49),
this work. In addition, we consider both
Urban et al. [50], Meng and Paulson 34] Schulz [44), Kaliszyk and Urban 22
Classic synthesis tools. The hardware synthesis problem traces back to the definition of the problem by Alonzo Church in 1957 [I]] thus also called Church's Problem. With theoretical solutions, already in 1969 by Büchi and Landweber [7]. the field has matured today. From a foundational point of view, advances have been made algorithmically. e.g., with quasi-polynomial algorithm for parity games [9), conceptually with distributed [0) and bounded synthesis [16]. or expressiveness- wise, e.g., GR(1) 39 synthesis, which is an efficient fragment of LTL or synthesis for security properties (17]. From a practical point of view, the field can build on a rich supply of tools (e.g. [6] [5] (5)). The first synthesis competition (SYNTCOMP) (26) was held in 2014, part of the annual international conference on computer-aided verification (CAV).
Property specification patterns. Property specification patterns for temporal logics have already been identified by Dwyer et al. [12). They proposed general hierarchical specification pattern system containing 55 patterns that are mapped to formal specification languages such as L.TL and CTL. More patterns for temporal logical formulas are identified by Etessami and Holzmann [13], Holeček et al. (23) Pelánek [38]. Konrad and Cheng (30) identified real-time specification patterns formulated in different real-time temporal logics and a structured English grammar. Grunske 199 presented
specification pattern system for probabilistic properties formulated in probabilistic temporal logic and a structured English grammar.
3 Datasets
In the following, we will first exemplary describe the specification language LTL and the circuit representation (the interested reader can find the full formalizations in the appendix). We will then describe our dataset, which is generated from specification patterns from the LTL. track of SYNTCOMP 2020 (26).
3

---

[0,0,0,0,0.0]
[100,000,000]
[100,1,0.0.0]
[0.1,1,0,0,0]
g
[1.00011,100]
Figure 2: Example tree positional encoding for the LTL request pattern C(r -
3.1 LTL and And-Inverter Graphs
LTL can specify that some proposition P must hold at every point in time P)) or that P must hold at some future point of time (C P). By combining these operators, one can specify that must occur infinitely often (N P). The propositions are usually partitioned into inputs and outputs. In the following, we provide a small example. For inputs r1, and outputs 91 92 the LTL formula
3 (g) A 92)
(11 + 91)
(r2 92)
specifies a simple arbiter using a mutual exclusion property for grant ạ1 and grant 92 and two response properties that guarantee that always request ri eventually answered by grant 9i and always request r2 is eventually answered by grant g2. Given an LTL specification yo, i.e. an LTL formula şp over atomic propositions AP and partition of AP in inputs / and outputs O the LTL synthesis problem is to determine whether circuit over inputs / and outputs O exists such that the circuit satisfies the specification. If no such circuit exists, we call the specification to be unrealizable. Typically, an LTL specification is decomposed into assumptions, posed on the inputs from the environment, and guarantees, that determine how to react the inputs. For training Transformers, we represent assumptions and guarantees as sequences with a tree positional encoding [47] The basic idea is, to encode the path through the syntax tree for each character. Since L.TL. has only unary and binary operations, this is encoded by appending either 1, O, representing the left child or 0, 1, representing the right child, in front of the encoding. Figure shows an example tree positional encoding for the response pattern O(r g).
The AIGER format became an established format for benchmarks, competitions, and tool implemen- tations in both computer-aide aided verification and reactive synthesis. The AIGER format represents sequential circuits as and-inverter graphs in both ASCII and binary format. In this work, refer to the original version 20071010 in ASCII format [4. The first line in an AIGER file in ASCII format contains the header that is the format identifier string "aag" followed by 5 non-negative integers indicating the maximum variable index M, the number of inputs 7, the number latches L, the number of outputs O, and the number of AND gates A. The header is followed by lines defining the inputs, T, lines defining the latches, O lines defining outputs, and A lines defining the AND gates. An optional symbol table to name inputs, outputs, and latches and a comment section may follow after the definitions. Inputs, latches, outputs, and AND gates are defined using variables and literals represented as non-negative integers. The relationship between literals and variables is that we divide the literal by 2 to obtain the variable and if the literal modulo 2 equals it corresponds to the negated variable and if the literal modulo 2 equals 0 corresponds the unnegated variable. Further literal 0 represents the Boolean constant 1. and literal 1 represents the Boolean constant T. Inputs are defined as unnegated literals. Latches are defined as two literals separated by a space. The first literal provides the current state of the latch and the second literal the next state of the latch. Outputs are defined as arbitrary literals. AND gates are defined as three literals separated by a space. The first literal is the output of the AND gate and the second and third literals are the inputs of the AND gate.

---

For our small arbiter example above, we show below circuit (left) and its AIGER representation (right), which is actually a prediction of a hierarchical Transformer.
aag 3
2
2
header
2
T
2
ON
Oi
4
T2
6 6
latch
6
gi
7
92
The triangles represent inputs and outputs, the rectangles represent variables, the diamond-shaped variables represent latches and the black dots represent inverter (NOT gates). The circuit implementa- tion ignores the inputs /0 and /1, which represent both requests 11 and 72 (except for unnecessarily assigning them to variables and 4), The circuit implementation satisfies the specification by alternating indefinitely between both outputs O0 and O1, which represent both grants ÿ1 and 92. independently of the given inputs. This is, in fact, the smallest solution satisfying the simple arbiter specification above. The hierarchical Transformer also predicts correct circuit implementations for more involved specifications where the circuit has to react to inputs (see, for example, Section 5 for an arbiter that prioritizes certain request).
3.2 Data Generation
From the LTL track of SYNTCOMP 2020 26 we collected 346 benchmarks in Temporal Logic Synthesis Formal (TLSF) (27). Using SyFCo 27 we translated the TLSF specifications to the BoSy input format 14. The BoSy input format is JSON-based format representing specifications list of assumptions and a list of guarantees where assumptions and guarantees can be arbitrary LTL formulas. The LTL specification results from the implication of the conjunction of assumptions to the conjunction of guarantees. An example of the format for a prioritized arbiter specification is shown in Listing in the appendix. From the 346 benchmarks in BoSy input format we collected assumptions and guarantees and filtered LTL formulas with more than five inputs and more than five outputs, which is restriction that is comparable with most SYNTCOMP spees: 242 of 346 have S inputs and 274 have < 5 outputs. Further, we filtered out specifications with an abstract syntax tree of size greater than 25 resulting in 157 instantiated assumption patterns and 1942 instantiated guarantee patterns. In a final step, we renamed inputs and outputs with uniform random choice from input atomic propositions ig, i1, i2, i3, i and a uniform random choice from output atomic propositions oo, 01, 02, 03, 01, respectively. The table below, shows three random examples of assumption patterns and three random examples of guarantce patterns.
assumption patterns
guarantee patterns
[ A On -1n) Oin)
(0 02 ig) V
io
(20 + Olss VOlos Vig Vis)))
-40 V 03 V Vo1 Vo VOio)
(00 V -01)
Given the set of specification patterns, we generate a dataset for supervised learning, i.e., pairs of specifications and systems, by combining randomly instantiated specification patterns. Specifically, we alternate between sampling guarantees until the specification becomes unrealizable and sampling assumptions until the specification becomes realizable where the number of trials to find suitable assumption is limited to 5. Further, we implemented stopping criteria that limit the maximal number of guarantees 10, the maximal number of assumptions to 3, and the runtime for the synthesis tool to 120 seconds. If the resulting specification is unrealizable we also consider its realizable predecessor for our dataset. Apart from that intermediate specifications are discarded. To synthesize specifications, we use the LTL synthesis tool Strix [35]. Systems are represented in the AIGER format. For unrealizable specifications we provide an AIGER circuit representing the winning strategy for the environment, i.e., a counter strategy showing that the specification is unrealizable. When synthesizing specifications, we provide all five inputs ig. i1 iz, is, i4 and all five outputs Og, 01, 02, O3, 04 to the tool such that all AIGER circuits in our datasets have the same five inputs and the same five outputs. Based on the AIGER format, we apply two additional filters when generating data: 1) we filter AIGER circuits exceeding maximum variable index of 50, 2) we filter AIGER circuits with & AND gates if the number of circuits the dataset with & AND gates exceeds 20% of the dataset size. This filtering especially reduces the number of circuits that have a low amount of AND gates.
5

---

Ouanette
Quarertee
Figure 3: A hierarchical Transformer [33 first encodes assumption and guarantee patterns in isolation,
before encoding them globally.
The data generation method allows generate a large number of specifications from a comparatively small set of specification patterns; especially the generation of specifications that include meaningful assumptions and are realized by complex implementations. Following the described method, constructed a dataset containing 250 000 unique samples split into 200 000 training samples, 25 000 validation samples, and 000 test samples. We included the unrealizable specifications met through the first stopping criteria such that half of the dataset consists of unrealizable specifications. Figure shows an example of a realizable specification in the test data.
4 Experimental Setup
Based on the code base of DeepLTL [21] (MIT license), we implemented a hierarchical Trans- former 33 and augment with tree-positional encoding 44 In contrast to a baseline Transformer, the encoder has two types of layers, local and global layers.
The local layers encode individual assumptions and guarantees, and only the global layers combine the representations of tokens across all assumptions and all guarantees. With this hierarchical encoding, gain approximately 10% of accuracy across all models compared to using a standard Transformer (see Figure 6 Figure 3 sketches the use of local and global layers in the encoder for setting.
aag 11
8
10
12
We trained hierarchical Transformers with model dimension 256. The dimension of the feed-forward networks was set to 1024. The encoder employs 4 local layers followed by 4 global layers, and the decoder employs 8 (unmodified) layers. All our attention layers use 4 attention heads. We trained with a batch size of 256 for 30000 steps and saved the model with the best accuracy per sequence on the validation data. We trained on an NVIDIA DGX A100 system for around 10 hours.
14
16
22
16 13 10
18 4
20 19 11
22 21 13
i1
12
13
4.1 Training Details
14 14
10 10
The Transformer architecture is sequence-to-sequeee model trained to predict a sequence of output tokens provided a sequence of input tokens. Similarly, provide multiple sequences of input tokens to an hierarchical Transformer. Assumptions and guarantees LTL formulas and can thus be directly represented sequences of tokens with each atomic proposition, Boolean operator, temporal operator, and Boolean constant being separate token. We omit
o0
al ol
o2
o3 o3
04
Figure 4: AIGER representa-
tion of the circuit in Figure
"The code, our data sets, and data generators are part of the Python library ML2 reactive- systems/mty)))

---

Test Set
SYNTCOMP
Violated
80
Violoted
60
0,60
0.66
0:80
0.75
10
15
20
10
15
25
Number of AUD Gittes
Number of AND Gares
Timeouts
Smart Home
500
Sattefied Violated
Satireed Violated
400
0.25
30
303
0.00
0.23
0.30
0.00
10
10
15
Number AND Giates
Number of AND Galles
Figure 5: Accuracy with respect to the size of the synthesized circuits measured by the number of AND gates for test set (top, left), SYNTCOMP (top, right), timeouts (bottom, left), and smart home benchmarks (bottom, right). Number AND gates are binned into intervals of size 5.
parentheses because we add a tree-positional encoding 47 that identifies each token with its position in the abstract syntax tree of the LTL formula (see Figure 2 To distinguish assumptions from guarantees in the global step we prepend assumptions with special assumption token. Circuits are in AIGER format that we represent as sequence of tokens by representing each integer with a corresponding token and replacing each newline character with a special new line token. Since omit the header and the symbol
all circuits in dataset have the same inputs and outputs table when tokenizing an AIGER circuit. Additionally, we include special realizability token at the beginning of the sequence indicating whether specification is realizable.
We trained all models using the Adam optimizer 29 with 3 = 0.9, 82 = 0.98 and e = 10-9. The optimizer used with learning rate schedule proposed by Vaswani al. [51] that increases the learning rate linear for a given number of warmup steps followed by decreasing learning rate proportionally the inverse square root of the step number. In our experiments, we used 4000 warmup steps as proposed by Vaswani et al. [I].
4.2 Performance Measures
There are infinitely many circuits satisfying a realizable LTL specification. To evaluate the perfor- mance of the trained models thus distinguish between the syntactic accuracy and the semantic accuracy: For a dataset of specifications and systems, the syntactic accuracy measures the percentage of the Transformer's 's predictions that match the circuit in the dataset. Potentially, prediction that does not match the system still satisfies the specification. We thus also measure the semantic accuracy, i.c., the percentage of the Transformer's predictions that satisfy the specification. Note that, when using beam search algorithm only one of the predictions needs to match the system in the dataset or satisfy the specification, respectively. To model check predictions we use the nuXmv model checker [1O]. When training Transformers on the (casier) LTL trace generation problem 222, significant differ- ence between syntactic and semantic accuracy was observed. appears that the Transformers rather generalize to the semantics of the logic than the particularities of the data generator. As we will see the next section, our results are consistent with this observation even for the "harder" problem of predicting circuits.
7

---

accuracy per sequence
0.4
0.2
5.000
10000
15 000
20.000
000
30
step
Figure 6: Accuracy per sequence over the training course shown for the training split (red) and validation split (light red) when training the hierarchical Transformer and for the training split (green) and the validation split (light green) when training the standard Transformer.
Experiments
In this section, report variety of experiments that analyze the performance of hierarchical Transformers on the circuit synthesis task and their generalization behavior. In the following, we will first analyze the overall performance of the models and that they often construct different solutions, yet correct ones, than the classical tool we generated the training data with. For this, we consider four different test sets and group results the size of the predicted circuits. Secondly, compare the training with our data mining method against the ground truth, i.e., against training of hierarchical Transformer performance on realizable and unrealizable specifications, where for the latter the model is supposed construct circuit representing counter strategy. Lastly, we will take deeper look into of the specifications, which, compared to the example in Section 3 is an arbiter that prioritizes certain request.
the raw SYNTCOMP benchmarks. Thirdly, compare the models
Overall results. We tested our models on four different datasets. A Testset consisting of held- out instances generated by our data mining method, the SYNTCOMP set, consisting of the synthesis competition benchmarks, a set Timeouts that consists of generated specifications on which Strix, the classical synthesis tool that used for generating the circuits, timed out (< 120s), and an out-of-distribution (OOD) benchmark set Smart Home consisting of specifications for smart homes. We consistently observed in all experiments that the beam search significantly increases the accuracy. When analyzing the results we found that the beam search often yields several correct circuits. For beam size of 16 and the Testset, average 4.6 of the 16 AIGER circuits satisfy the specification.
In our Testset (see IT, we observe in many cases that the circuit prediction of our model is different from the circuit the tool would synthesize. Since has already shown that this gap between syntactic and semantic accuracy exists for such tasks [22). we concentrate on the semantic accuracy. i.e. the total aceuracy. When analyzing the size of those circuits, we found both smaller and larger
Dataset
Beam Size
Beam Size
Beam Size
Beam Size 16
Testset
53.6(31.1) + 2.4
70.4(39.0) + 2.3
75.8(41.9) + 2.1
79.9(44.5) + 2.0
SYNTCOMP
51.9 + 2.2
60.0 + 1.5
63.6 + 1.9
66.8 + 1.2
Timeouts
11.7 + 1.1
21.1 + 0.9
25.9 + 1.0
30.1 + 1.2
Smart Home
22.9 + 3.6
31.4 + 7.1
44.8 6.5
40.0 6.5
Table 1: Accuracy reported on test data, SYNTCOMP benchmarks, timeouts, and smart home benchmarks for different beam sizes averaged over trainings including standard deviation. For the test data we show the syntactic accuracy in parenthesis.

---

aag 75 1
00
03
(assumptions)
O
(rm)))
10
Lu
14
(guarantees:)
12
(( V(-(g))))
14
((ro) ( ((rm)
12
13
14
0
14
Figure 7: The specification (left), the predicted AIGER eircuit (middle) and the visualization of the circuit (right) for prioritizing arbiter.
circuits, with no significant decrease or increase in average circuit size. In total, the model was able solve 79.9% of the held-out generated test instances with beam size of 16.
While the training data is based on specification patterns extracted from SYNTCOMP benchmarks it unlikely that our data generation process reassembles SYNTCOMP benchmarks. This allows to evaluate the model on them. After filtering out benchmarks with more than 5 inputs/outputs, more than properties, and properties of size greater than 25, the model achieved an accuracy of 66.8% for the resulting 145 benchmarks using beam size of 16.
For timed out specification achieves an accuracy of 30.1% % for beam size 16 demonstrates that our approach can yield performance gains practice. To highlight capabilities of our model we display Figure in the appendix the largest circuit that is predicted for timed out specification and satisfies the specification.
not known whether it is realizable or unrealizable. The model
We constructed the Smart Home set, with the same restriction as for SYNTCOMP, from recently published benchmark set for synthesizing smart home applications [1] The hierarchical Transformer able to solve 44.8% of the provided instances. When compared to the full benchmark (i.c., without the size restrictions), the model solved 11.1% of the formulas. Note that this benchmark set was not used to mine specifications from and the benchmarks include instances with larger assumptions and guarantees than seen during training.
We also analyzed the performance the model depending on the size of the predicted circuit. Results shown in Figure [] As expected, for larger circuit implementations, the model accuracy drops. The size distribution of the training data resembles the size distribution of the test set (top left in Figure 5 and Figure B Meaning that the model has seen significantly lower percentage of large circuits during training. Future experiments have to determine how large the training data and the hierarchical Transformers could be scaled, before the training process breaks down.
Training raw SYNTCOMP benchmarks. We did baseline experiment by training with various batch sizes on the raw SYNTCOMP benchmark. This training (not surprisingly) fails whereas data generation method enables stable training.
Unrealizabile Specifications. The training data contains both realizable and unrealizable specifi- cations. In Table[3ww we analyze the accuracy for realizable and unrealizable specifications separately test data. While the syntactic accuracy is higher for realizable specifications, in terms of the
Beam Size 1
Beam Size 4
Beam Size 8
Beam Size 16
Realizable
50.8 (39.0)
64.3 (48.0)
67.5 (50.0)
70.7 (52.6)
Unrealizable
55.4 (23.0)
74.6 (31.9)
81.0 (35.2)
86.7 (39.0)
Table Accuracy on Testset reported separately for realizable and unrealizable specifications. For different beam sizes we report the semantic accuracy and the syntactic accuracy in parenthesis.

---

semantic accuracy the model solves unrealizable specifications more accurately. Further, we found for a beam size of 1 that the Transformer predicts the correct realizability token for 91.4% of the specifications from the test data.
we show that the model can handle more interesting, real-world specifications. Figure shows the specification, AIGER file and the circuit visualization of arbiter that prioritizes one of the requests whenever access is requested by both processes at the same time; meaning that the implementation can no longer ignore the input as for the example in Section
Prioritizing arbiter. Building the example of Section 3
Conclusion
We proposed a method to address the lack of data for training a neural network on the task of synthesizing circuits out of LTL specifications. We mine specification patterns from the annual reactive synthesis competition (SYNTCOMP) and generate new formulas by combining multiple specification patterns. We showed that this dataset can be used successfully train hierarchical Transformers on the LTL synthesis problem for specifications composed of specification patterns. We also showed that the models generalize unseen specifications, including specifications that are both realizable and unrealizable and specifications that cannot be solved by classical synthesis tool within a time limit of 120 seconds. Furthermore, we performed an -iitt--distriuution test on recently added benchmark set on synthesis problems for smart homes, Experimental results suggest that the Transformer can especially useful for predicting unrealizability.
Acknowledgments and Disclosure of Funding
This work was partially supported by the European Research Council (ERC) Grant OSARES (No. 683300) and the Collaborative Research Center "Foundations Perspicuous Software Systems" (TRR 248, 389792660).
References
[1] V.A.R.V.SS. TSL/TLSF benchmark suite, 2021. URL /ttpps://githii www.smS/TCOOOO
benchmarks http://reeee/eeeeeeeeeeeeeeeeeet hwwt/mmttteeeeeeeeaam http://mattttssstseeeeeeee smart htt__hom___aaaaaaee
[2] M. Balunovic, P. Bielik, and M. T. Vechev. Learning to solve SMT formulas. Advances in Neural Information Processing Systems 31: Annual Conference Neural Information Processing Systems 2018, NeurlPS 2018. December 3-8, 2018, Montréal, Canada, pages 10338-10349 2018.
[3] K. Bansal, S. M. Loos, M. N. Rabe, C. Szegedy, and S. Wilcox. HOList: An environment for machine learning of higher order logic theorem proving. In Proceedings of the 36th International Conference on Machine Learning, ICMI. 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pages 454 463. PMLR, 2019.
[4] A. Biere. The AIGER and-inverter graph (AIG) format version 20071012. FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr, 69: 4040, 2007.
[5] R. Bloem, S. Galler, B. Jobstmann, N. Piterman, A. Pnueli, and M. Weiglhofer. Automatic hardware synthesis from specifications: case study. In 2007 Design, Automation & Test in Europe Conference & Exhibition, pages 1-6. IEEE, 2007.
[6] A. Bohy, V. Bruyere, E. Filiot, N. Jin, and J.-F. Raskin. Acacia+, a tool for LTL synthesis. In International Conference Computer Aided Verification, pages 652 657. Springer, 2012.
[7] J. R. Buchi and L. H. Landweber. Solving sequential conditions by finite-state strategies. In The Collected Works of Richard Büchi, pages 525-541. Springer, 1990.
[8] P. Cairns. Informalising formal mathematics: Searching the mizar library with latent semantics. In International Conference on Mahematical Knowledge Management, pages 58-72. Springer, 2004.
10

---

[9] C. S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasi-port polynomalll time. SIAM Journal on Computing, (0):STCC17-152, 2020.
[10] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta. The nuXmv symbolic model checker. In Computer Aided Verification 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 334-342. Springer, 2014, doi: 10.
[1]] A. Church. Application of recursive arithmetic to the problem of circuit synthesis. 1963.
[12] M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Property specification patterns for finite- state verification. In Proceedings of the Second Workshop on Formal Methods in Software Practice, March 4-5, 1998. Clearwater Beach, Florida, USA, pages 7-15. ACM, 1998. doi: 10.1145/298595.298855
[13] K. Etessami and G. J. Holzmann. Optimizing büchi automata. In C. Palamidessi, editor, CONCUR 2000 Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, volume 1877 of Lecture Notes in Computer Science. pages 153-167. Springer, 2000. 10. 10.11007/3-540-44612
doi: 10. 10.1007/3-540-4441 101188-41111111 13. URI. https:tts://doi. org/
[14] Faymonville, B. Finkbeiner, and Tentrup. BoSy: An experimentation framework for bounded synthesis. In Computer Aided Verification 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 Lecture Notes in Computer Science, pages 325-332. Springer, 2017. doi: 10.10079978-3331--639----
[15] Faymonville, B. Finkbeiner, and L. Tentrup. BoSy: An experimentation framework for bounded synthesis. In International Conference on Computer Aided Verification, pages 325- 332. Springer, 2017.
[16] B. Finkbeiner and S. Schewe. Bounded synthesis. International Journal on Software Tools for Technology Transfer, 15(5):519-523 2013.
[17] B. Finkbeiner, C. Hahn, Lukert, M. Stenger, and L. Tentrup. Synthesis from hyperproperties. Acta informatica, 57(1):137-163, 2020.
[18] J. Gilmer, S. S. Schoenholz, P. F. Riley, O. Vinyals, and G. E. Dahl. Neural message passing for quantum chemistry. In Proceedings of the 34th International Conference on Machine Learning. ICML 2017, Sydney, NSW, Australia, 6-11 August 2017, volume 70 of Proceedings of Machine Learning Research, pages 1263-1272. PMLR, 2017.
[19] L. Grunske. Specification patterns for probabilistic quality properties. In 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008 pages 31-40. ACM, 2008. doi:
1368094.
[20] S. Gulwani, J. Hernández-Orallo, Kitzelmann, S. H. Muggleton, U. Schmid, and B. Zorn. Inductive programming meets the real world. Communications of the ACM, 58( 1):90-99, 2015.
[21] C. Hahn, F. Schmitt, U. Kreber, M. N. Rabe, and B. Finkbeiner. Deepltl, 2020. URL https://github coom:/reactiiee-syttttee////eee
[22] C. Hahn, F. Schmitt, U. Kreber, M. N. Rabe, and B. Finkbeiner. Teaching temporal logics to neural networks. International Conference on Learning Representations, ICLR, 2021.
[23] Holeček, Kratochvíla, kehák, Šafránek, Šimeček, et al. Verification results in Liberouter project, 2004.
[24] IEFF-Commission et al. IEEE standard for property specification language (PSL). IEEE Std 1850-2005, 2005.
[25] S. Jacobs and G. A. Pérez. The reactive synthesis competition. htttp://wwk http://wwwwwttcoopppppp swnssssp.tt..... org

---

[26] S. Jacobs and G. A. Pérez. The 7th reactive synthesis competition: SYNTCOMP 2020. http://www. somptc//ww.syntccompp.. arg/syntcomp w
[27] S. Jacobs, F. Klein, and S. Schirmer. A high-level LTL synthesis format: TLSF v1.1, In Proceedings Fifth Workshop on Synthesis, SYNT@ CAV 2016, Toronto, Canada, July 17-18, 2016, volume 229 of EPTCS, pages 112-132, 2016. doi: 10.4400/EPTCS
[28] C. Kaliszyk and Urban. Learning-assisted assisted automated reasoning with flyspeck. Journal of Automated Reasoning, 53(2):173-211 213, 2014.
[29] D. P. Kingma and J. Ba. Adam: A method for stochastic optimization. In 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings, 2015.
[30] S. Konrad and B. H. C. Cheng. Real-time specification patterns. In 27th International Confer- ence on Software Engineering (ICSE 2005), 15-21 May 2005, St. Louis, Missouri, USA, pages 372-381. ACM, 2005. doi: 10.1145/1022455.0062
[31] G. Lample and F. Charton. Deep learning for symbolic mathematics. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020.
[32] G. Lederman, M. N. Rabe, S. Seshia, and E. A. Lee. Learning heuristics for quantified boolean formulas through reinforcement learning. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.nne, 2020.
[33] W. Li, L. Yu, Y. Wu, and L. C. Paulson. IsarStep: a benchmark for high-level mathematical reasoning. In International Conference on Learning Representations, 2021.
[34] J. Meng and L. C. Paulson. Lightweight relevance filtering for machine seathine-geeratee resolution problems. Journal of Applied Logic, 7(1):41-57, 2009.
[35] P. J. Meyer, S. Sickert, and M. Luttenberger. Strix: Explicit reactive synthesis strikes back! In Computer Aided Verification 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part
I, volume 10981 of Lecture Notes in Computer Science, pages 578-586. Springer, 2018. doi: 1..1077978---31922 3-1999911-994----11111
[36] A. Paliwal, S. M. Loos, M. N. Rabe, K. Bansal, and C. Szegedy. Graph representations for higher-order logic and theorem proving. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, New York, NY, USA, February 7-12, 2020, pages 2967-2974, AAAI Press, 2020.
[37] E. Parisotto, A.r. Mohamed, R. Singh, L. Li, D. Zhou, and P. Kohli. Neuro-symbolic program synthesis. arXiv preprint arXiv:1611.01885. 2016.
[38] R. Pelánck. BEEM:
benchmarks for explicit model checkers. In D. Bosnacki and S. Edelkamp, editors, Model Checking Software, 14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007, Proceedings, volume 4595 of Lecture Notes in Computer Science, pages 263-267. Springer, 2007. doi: 10. 0010778---54---337000 17. URL httpht:/s///oi. org/ 10. 1007/
978-3-540- 73370-6-337
[39] N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of reactive(1) designs. In E. A. Emerson and K. S. Namjoshi, editors, Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, volume 3855 of Lecture Notes in Computer Science, pages 364 380. Springer, 2006. doi: (1000//11097733222 24. /ttppsp:///do 1tt.///00.../1110000/1110077333
1007
[40] A. Pneuli and R. Rosner. Distributed reactive systems are hard to synthesize. In Proceedings [ [1990] 3 Annual Symposium on Foundations of Computer Science, pages 746-757. IEEE, 1990.
[41] M. Rabe, D. Lee, K. Bansal, and C. Szegedy. Mathematical reasoning via self-supervised skip-tree training. 2020.
12

---

[42] B. Rozière, M. Lachaux, L. Chanussot, and G. Lample. Unsupervised translation of programming languages. In H. Larochelle, M. Ranzato, R. Hadsell, M. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems 33: Annual Con-
ference on Neural Information Processing Systems 2020, NeurlPS 2020, December 6-
12, 2020, virtual, 2020. URL
wwwpinnggs..uuiipe nwwrips..rcccm cc. http/ppppe//////aa/eeeee Gue2sf11cccas5f8.1184444488868 ott.:e/eeeeeetcco.oeoobooaaa.a.. Abstract.
[43] Scarselli, M. Gori, A. C. Tsoi, M. Hagenbuchner, and G. Monfardini. The graph neural network model. IEEE Trans. Neural Networks, 20(1):61-80, 2009. doi: 10.1109/....000. 2005605.
[44] S. Schulz. System description: E 1.8. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pages 735-743. Springer, 2013.
[45] D. Selsam and N. Björner. Guiding segh-performance SAT solvers with unsat-core predictions. In Theory and Applications of Satisfiability Testing SAT 2019 22nd International Conference, SAT 2019, Lishon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages
Springer, 2019. doi: 1111000977-30000-24400 24
[46] D. Selsam, M. Lamm, B. Bünz, P. Liang, L. de Moura, and D. L. Dill. Learning SAT solver from single-bit supervision. 7th Interaational Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019.
[47] V. L. Shiv and C. Quirk. Novel positional encodings to enable tree- baseb transformers. In H. M. Wallach, H. Larochelle, A. Beygelzimer, F. d' Alché-Buc, E. B. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurlPS 2019, December 8-14, 2019, Vancouver, BC,
Canada, pages 120688 2019. URL
wwwnrnurrp.... neurips.cc/papeer Abwtractt.ttttee.... html
[48] J. Urban. ing, 33(3-4):319-339) 2004.
implementation. first experiments. Journal of Automated Reason-
[49] J. Urban. Malarea: a metasystem for automated reasoning in large theories. ESARLT, 257, 2007.
[50] J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskoëil. Malarea sgl sgl-machine learner for automated reasoning with semantic guidance. In International Joint Conference on Automated Reasoning, pages 441-456. Springer, 2008
[51] A. Vaswani. N. Shazeer, N. Parmar, Uszkoreit, L. Jones, A. N. Gomez, L. Kaiser, and I. Polo- sukhin. Attention is all you need. In I. Guyon, U. von Luxburg, S. Bengio. H. M. Wallach, R. Fer- gus, V. N. Vishwanathan, and R. Garnett, editors, Advances in Neural Information Processing Systems 30: Anmual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pages 5998 6008, 2017. wttp:0/077...Attss////eeeaiiii1
.neurps
13


Reviews:
[{"review_id": "rmOfnmWhs-v", "reviewer": "Reviewer_fNW6", "summary": "The paper introduces a deep learning approach for converting LTL specifications to circuits, effectively solving the classic LTL synthesis problem. The architecture is based on a pre-existing transformer setup that targets a representation of the circuit that allows for sequential generation of the graphical representation (AIGER).\n\nA key contribution of the work is the dataset generated by the authors for the task of synthesis. While there is a regularly run contest, the benchmarks are limited in size compared to what deep learning approaches would require. The data stems from random recombinations of fragments found in the existing benchmark sets.", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "## Originality\nThe work follows a similar architecture to previous work dealing with similar data. However, this seems to be the first approach using those methods to solve the problem of synthesis.\n\n## Quality\nThe presented work is technically sound, however, there is limited attention given to some of the core limitations:\n\n- The augmentation used for generating the data might make the new LTL fairly meaningless. Without a direct correspondence to LTL that is meaningful (i.e., of the form we would like to synthesize in practice), then the empirical results are less relevant.\n\n- Related, there seems to be quite a bit of overlap between the train/test data sets for much of the results. Even if the precise combination of LTL fragments are not shared, the fragments themselves almost certainly are.\n\n- Much of the analysis hinges on state-of-the-art solvers timing out. At 10 seconds, however, this seems very limited. The low amount should be justified, and the time required for the presented work (i.e., using the hierarchical transformers) should be listed as well.\n\n- The most relevant comparison listed is with the smart home benchmark -- other ones have too much of an overlap between the training and testing sets (see comment above on the fragments). A better analysis might be to train on some SYNTCOMP domains and test on the remainder.\n\n- With only 14% of the smart home solved, compared to 42.9% given the restrictions, demonstrates that the generality of this approach may be a serious limitation.\n\n\n## Clarity\nThe paper is written very well, and the only suggestions I have are to address key questions that came to mind while reading:\n\n- What is the justification for the existing filters on the problems? I.e., circuits > 50vars and the computation on circuit AND gates exceeding 20% of the dataset size.\n\n- What is the time spent on each of the beam sizes in computing a solution?\n\n- Judging by the table, the smart home dataset continually improves. Does this trend continue for beam size = 32 or higher?\n\n- Why do unrealizable benchmarks become easier with larger beam sizes?\n\nA final comment is that it may be worth relating the data processing you do to the traditional data augmentation technique in the ML field (e.g., cropping for image-based data). You have, in essence, introduce a domain-specific form of data augmentation to amplify the amount of available data for the task of LTL synthesis.\n\n\n## Significance\nThe significance of the results is somewhat difficult to ascertain. On the one hand, there seems to be reasonable coverage for both realizable and unrealizable inputs. But, crucially, how does the proposed approach compare with state-of-the-art techniques for LTL synthesis? We have a sense of how long Strix requires, but not for the proposed approach at inference time. Is there some way to use the invalid circuits the proposed approach produces as a seed to a complete algorithm, and would this be competitive?\n\nI understand that the authors point out in the checklist and conclusion that the aim was _not_ to compete with classical tools, but rather just to address the lack of data for ML methods in the space. However, much of the paper is dedicated to the _use_ of the data, rather than the data itself, and if the performance is really poor then the significance is reduced.\n\nThe 88.3% accuracy on realizability classification seems like a really nice result. I would be curious to know if this improves with greater beam sizes (by taking a majority vote, or similar, among those in the beam).\n\nFinally, a major limitation holding back the significance of what's proposed is the size limits placed on things. How might the approach be generalized to arbitrary sizes?", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "I see no negative societal impact of the work, and the limitations that stem from the paper are discussed above.", "review_text": "", "extra_scores": {"ethical_concerns": "I see no ethical concerns with the work presented.", "needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "6"}, "extra_text": {}}, {"review_id": "JtlxrlfYOjz", "reviewer": "Reviewer_iD7H", "summary": "This paper approaches the problem of neural circuit synthesis. To that end, the paper presents a new synthetic dataset of LTL specification and circuits/counter-examples and then, presents evaluation results by training a hierarchical Transformer model on this dataset. The synthetic dataset is generated by mining specification patterns from a real dataset (SyntComp), then artificially combining multiple instantiated patterns. The label (the circuit/counter-example) is generated using an existing classical circuit synthesis tool. The training and the model architecture are straightforward adaptations of prior work. \n", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Strengths:\n- Circuit synthesis is a new and interesting application for deep learning approaches. \n- The paper presents a method to generate synthetic data for this application (which solves the issue of lack of training data).\n- An implementation using hierarchical transformers that has decent performance and that can be used as a baseline for future work in this domain.\n- Evaluation is extensive (includes comparing  transformers vs hierarchical transformers), multiple different kinds of datasets, and a detailed analysis of results\n\nWeakness:\n\nMy main concern is that the lack of clarity on how the experiments are done (I am willing to increase my score if these concerns are answered in the rebuttal)\n- Are the numbers in section 4 the average of multiple (ideally 5) separately trained models?\n- Was the hyper-parameter search done? In a new benchmark paper, hyper-parameter search is very important to establish a good and robust baseline. \n- It will be interesting to see other variations of the model architecture (for e.g. different kinds of encodings on the inputs and outputs) \n\nAnother significant concern is the lack of a discussion on the limitations to the approach\n- Is it not clear how major/minor is it to have the restriction of less than 5 input and output variables?  What motivated this restriction? The limitations of the synthesis solver or the inability of the model to learn with more variables. \n- What fraction of the original SyntComp dataset satisfies the filtering conditions imposed in this paper?\n- Ultimately the data generation process is going to be restricted by what the synthesizer is able to solve. Although there are some cases where the learned model is able to out-beat the synthesizer, it is unlikely that it will outdo on out-of-distribution (significantly longer) specifications. Do the authors have any comments on this and how they might try to address this challenge?\n\nMinor:\n- Explain the meaning of latches\n- How do the results in table 2 look for the other datasets?\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "Yes.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "2"}, "extra_text": {}}, {"review_id": "Hl-gzlLiWp", "reviewer": "Reviewer_jHAd", "summary": "The paper proposes a transformer-based NN methodology for predicting hardware circuits given an LTL specification. This is a well-studied problem in model-checking, so this work represents another attempt of using NNs to solve tasks normally solved using reasoning/symbolic techniques.\n\nThe general idea is to cast the problem as a sequence to sequence problem and use a variation of the widely-used transformer architecture. As in many other cases, data-driven approaches for reasoning tasks produce approximations with no guarantees of correctness. That can be useful in some cases but is solving a different problem. In this case, it is possible to verify that the design satisfies the LTL specification. So, the whole approach is incomplete but sound: a better proper than an approximation.\n\nAnother risk of this kind of work is a naive use of observational data in combinatorial domains like this one that leads to unsupported claims on generalization. A typical methodological error works as follows. The data is split randomly. If results are good in the test set, then it is claimed that the method is solving the problem. The problem is that conclusion. A test set sampled from the original dataset might have many share many constituents with the train set, so the test set might be similar to the training set. That doesn't mean, of course, that the model is not significant; just that the experiments don't support that.\n\nIn this paper, the dataset was build using data from a model-checking competition but combining two parts of the problem (assumptions and guarantees) to get more combinations. That means that almost all assumptions and guarantees will be shared between the training and the test set. However, the evaluation includes a test split from that dataset, as well as three other datasets. These three datasets support the claims of the paper.\n\nThere is an additional risk common in this kind of work: not comparing with the state-of-the-art. While this paper does not compare with them directly, the three extra datasets include one where Strix, a model checking tool, timeout after 10 seconds. The 10s seconds is arbitrary, but it shows that some problems are non-trivial. In all fairness, Strix see those instances for the 1st time, so it might deserve more time.\n\nMain question:\n\n- What if Strix is given, let's say, two hours for attempting to solve the example of Fig 9, of the supplementary material?\n\n- A sequence to sequence model does not have, in principle, limitations in the size of the input and output. However, it's entirely possible -even likely– that a model checking tool might be more robust in a subclass of simpler for larger problems. I noticed that table 1 reports \"68.3%\" accuracy for beam-size 16, SYNTCOMP but *after* \"ﬁltering out benchmarks with more than 5 inputs/outputs, more than 12 properties, and properties of size greater than 25\".  **Did you test in any instance out of this restriction? For instance, what's the accuracy of the rest of the SYNTCOMP formulas? Please provide separated numbers**. I find the absence of this result a bit surprising. If the results were good, please add them to the paper. Otherwise, add this as a limitation of the method.\n\n- I understand this is not introducing a new architecture but using an existing one. While the code is provided, the description of the parameters is extremely brief. For instance, on page 6, what does \"model dimension\" mean? Why this architecture? I think these deserve a better explanation. Additional details and discussions can be added in the supplementary material. If you need more space, compact fig 2 and 6.\n\nThese are the most important issues. Their answer might affect my recommendation.\n\nFor now, I must conclude the contributions of the paper are significant for the task, so I recommend its weak acceptance. If the answers were positive, I'd increase my score.\n\n----\n\nThank you for your response. I'm more convinced now about the merits of the paper. I'm reviewing my scores accordingly. \n\nThere are have been many attempts to solve combinatorial problems using deep learning. In my opinion, some are more famous than they should be like an early one on the TSP. Many of those papers share typical tricks that make the problem easier:\n\n- Change the problem to a softer evaluation. For instance, one thing is getting a tour in a graph, something else getting a good one, it's far harder to get the optimal one.\n- Not being able to scale to bigger problems.\n\nThis paper has issue (2), but it is transparent about it.\n\nNow, for issue (1), they choose a very hard problem: \nsynthesizing the whole circuit. There are no shortcuts there: The circuit do work or doesn't.\n\nSynthetizing circuits for satisfying LTL is a very important problem. Moreover, LTL is being used for safe RL, for offering rewards to RL related to satisfying some conditions. I suggest citing this paper and relevant work:\nFoundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf Restraining Specifications.\nGiuseppe De Giacomo, Marco Favorito, Luca Iocchi and Fabio Patrizi. ICAPS 2019.\nhttps://ojs.aaai.org/index.php/ICAPS/article/view/3549\n\nI was very concerned that the data generating has turned the problem into a memorization problem. The rebuttal was good news. The method is creating new data in a very aggressive way. It's very hard to generalize when mixing assumptions and guarantees. Adjusting the assumption changes very easily the interpretation of the guarantees. Changing the guarantee suddenly matches or mismatch the assumptions. The corresponding circuit can change dramatically. \n\nAfter reading the other reviews, I think the paper should explain better how hard are the instances generated.\nIn this context, I think it'd be enough to show how different the circuits look like when keeping the assumptions and guarantees fixed, and varying the others. In this setting, even editing distance might be informative. A more solid metric would be useful like comparing the circuits per see. Once that is done, I suggest to invite the readers to consider the risk when generating datasets for reasoning tasks.\n", "questions": "", "limitations": "", "rating": 8, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "[page 2]:* When using a beam search, models achieve an accuracy of up to\n\n- Accuracy of correctness or recovering the label? Top accuracy? The mention of beam search might hint is top-k\n\n-----\n\n[page 2]:* Furthermore, the models can solve generated test instances on which classical LTL synthesis tools timed ou\n\n- We’re the solutions correct?\n\n-----\n\n[page 5]:* Following the described method, we constructed a dataset containing 250000 samples split into 200000 training samples, 25000 validation samples, and 25000 test samples\n\n- Most likely all assumptions and guarantees will occur in the validation and test sets.\n\n-----\n\n[page 7]:* when using a beam search algorithm only one of the predictions needs to match\n\n- I think the statements about beam search introduce confusion. In general, using beam size k can return up to k solutions. After that, the accuracy could be measure for top-j, where j <= k. In this case, given designs can be verified afterwards, it makes sense to test all of them.\n- Please, change the wording to emphasize that when using beam search, an answer is considered correct when any of the outputs is correct. That’s not the same as saying “only one of the predictions needs to match”. It’s not needed, is a decision.\n\n-----\n\n[page 7]: * Experiments section\n\n- In table 1, it’s not clear that the accuracy of the last three datasets is semantic. I suggest you use different terms. For instance, “match” for syntactic accuracy, and “correct” for semantic accuracy. I think the term “total accuracy” used below is not convenient.\n\n-----\n\n[page 8]:* We consistently observed in all experiments that the beam search signiﬁcantly increases the accuracy.\n\n- It’s been observed that decoding with language models with a larger beam size can decrease the quality, so this is not obvious.\n\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "N/A", "review_text": "", "extra_scores": {"ethical_concerns": "N/A", "needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "4h"}, "extra_text": {}}, {"review_id": "E252a7697jh", "reviewer": "Reviewer_Z9R3", "summary": "This paper applies hierarchical Transformers to the linear-time logic (LTL) synthesis problem. The contributions are two-fold: 1) data (or LTL specification) generation, which is achieved by conjoining specification patterns from existing SYNTCOMP benchmarks; 2) empirical evaluations of hierarchical Transformer on synthetic specifications as well as the original SYNTCOMP benchmarks.", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "### Contribution and Significance\nTransformers have been applied for the same LTL synthesis problem recently by Hahn et al. 2021 [22]. And this work applies a hierarchical transformer developed by Li et al. 2021 [33].  So both the problem and used techniques are already known. The main contribution of this work is the development of a new LTL synthesis dataset. Specifically, all synthesized LTL specifications share the same form: $A \\rightarrow G$, where $A$ is a set of assumptions and $G$ is a set of guaranttees; $A$ and $G$ are randomly chosen from existing benchmark suite used in the LTL track of SYNTCOMP. This dataset would be useful for evaluating machine learning-based methods for LTL synthesis. \n\n### Clarity and Quality\nThis paper is well-written. It gives a nice introduction to LTL synthesis problem and systemtically summarizes both recent work on using neural architectures for logical reasoning and many classic approaches. The data generation and data format are presented in a very clear manner.  The experimental evalution is also well-done, assuming the success criteria is showing a particular existing method on the newly generated dataset works well, which is something I hesitate to agree with.\n\nThe authors appear to carefully calibrate the data generation process so that hierarchical Transformers perform reasonally well. In terms of dataset generation (the main contribution of this work), I don't see a compelling reason why specifications with more than five inputs or outputs have to be filtered away. Similarly, why circuits with more than 20% k-AND gates should be filtered? Making the dataset easy to solve is not a convincing argument. On the contrary, keeping some challenging instances in a dataset woud make it more valuable. \n\n### Questions\nQ1: Normal LTL specifications encode certain safety or liveness property a system should possess. Could (and how does) randomly combining assumptions with guaranttees end up with \"meaningful\" LTL specifications? \n\nQ2: A LTL specification like $A \\rightarrow G$ will be trivially satisfied when its assumptions $A$ are not met. Such kind of solutions may not be very interesting. Essentially, there are two kinds of solution for a specification $A \\rightarrow G$: first, a solution to $\\neg A$; and second, a solution to $A \\wedge G $.   How often does each situation happens when a solution is found by the neural model?\n\nQ3: From the shared GitHub repo, Smart Home seems to be part of the SYNTCOMP benchmarks, instead of independent one. Can you clarify that?\n\nQ4: What is the guarantee on unrealizable specifications? Does the model always produce a counter strategy? \n\nQ5: Counter strategy sounds really interesting, but the paper only mentions it in two sentences with explaining how it is achieved. How is it fundamentally different (e.g. requiring a different method or training process) from a winning strategy ? ", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "The authors do not explicitly discuss their limitations or potential negative societal impact. There is no concern about the latter. \n\nDataset could be more challenging without artificial filters, which would thus be more useful to inspire future ML-based methods for LTL synthesis. It is also great to see the performance of more one than ML methods on this newly created dataset.", "review_text": "", "extra_scores": {"ethical_concerns": "There are no ethical issues since this paper concerns a technical circuit synthesis problem.", "needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "7.5"}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper elicited significant discussion. On the one hand, circuit synthesis is a significant and interesting application for DL, and the technical approach is reasonable. On the other hand, there were some concerns about the level of rigor in the experiments (see the reviews for more details), and scalability of the approach. At the end, the additional clarifications/results that the authors provided during the author feedback period persuaded the reviewers and me. I am therefore recommending acceptance. Please make sure to incorporate the new results presented in your author response into the final paper. 
Decision: Accept (Poster)