Neural Circuit Synthesis from Specification Patterns
Year: 2021

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.

heading: 1 Introduction
text: In reactive synthesis, a circuit is automatically constructed from a logical specification given as a formula in linear-time temporal logic (LTL). LTL is widely used by the verification community and is the basis for industrial specification languages like the IEEE standard PSL [24]. Efficient synthesis tools for LTL would simplify the hardware design process: a hardware designer could focus on specifying what the circuit is supposed to compute, instead of implementing how the computation is 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 to push this form of hardware construction process closer to practice (see, for example, the synthesis of the AMBA protocol [5]). The high computational complexity of the general problem (2-EXPTIME-complete), however, is so far a barrier that seems insurmountable with classical, e.g., automaton-based, approaches. Recent successful applications of machine learning for logical tasks, such as SAT solving [45, 46], higher-order theorem proving [36, 3], and the LTL trace generation problem [22] encourage new approaches to the LTL 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 (NeurIPS 2021).
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 a severe 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 show that hierarchical Transformers [33] can be trained on the circuit synthesis problem using the generated data and that the models can solve a significant portion of problems from the annual synthesis competition. In practice, logical hardware specifications follow specific design patterns [12]. 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→ g). The formula describes a response property, stating that at every point in time ( ), a request rmust be eventually ( ) followed by a grant g. 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 describe how the circuit has to react to 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 ϕG. The implication ϕA → ϕG 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 1 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 specifications and circuits as 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 predictions1, i.e., the model constructs a different, yet correct solution. When using a 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 out-of-distribution formulas, taken from a 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) specifications. We demonstrate that our approach achieves similar results on both realizable and unrealizable specifications.
1Note that verifying the solutions, i.e., model-checking, is a by-far easier problem (PSPACE vs 2-EXPTIME) and can typically be done in a 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 is described in Section 3. The experimental setup and the experimental evaluation are presented in Section 4 and Section 5, respectively. We conclude the paper in Section 6.

heading: 2 Related Work
text: 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 in this work. In addition, we consider both realizable and unrealizable specifications while for the LTL trace generation problem the satisfiability of LTL formulas was assumed. Lample and Charton trained Transformers on symbolic integration and solving differential equations and were able to outperform commercial systems on a synthetic dataset [31]. Similar to our findings Lample and Charton observed significant improvements in the Transformer’s accuracy when using a beam search. Rabe et al. applied Transformers to formal mathematical statements and demonstrated the Transformer’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 satisfiability problem [46]. In subsequent work Selsam and Bjørner applied the same architecture to the unsat-core prediction problem and demonstrated that their model can be used as a heuristic to speed up SAT solvers [45]. Lederman et al. applied graph neural networks to quantified Boolean formulas to learn heuristics 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-art performance for higherorder proof search. Similar, Balunović 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-of-the-art SMT solvers. Earlier works on applying learning to mathematics, has focused on ranking premises or clauses Cairns [8], Urban [48, 49], Urban et al. [50], Meng and Paulson [34], Schulz [44], Kaliszyk and Urban [28].
Classic synthesis tools. The hardware synthesis problem traces back to the definition of the problem by Alonzo Church in 1957 [11], 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 a quasi-polynomial algorithm for parity games [9], conceptually with distributed [40] 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, 15, 35]). The first synthesis competition (SYNTCOMP) [26] was held in 2014, as 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 a general hierarchical specification pattern system containing 55 patterns that are mapped to formal specification languages such as LTL and CTL. More patterns for temporal logical formulas are identified by Etessami and Holzmann [13], Holeč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 [19] presented a specification pattern system for probabilistic properties formulated in probabilistic temporal logic and a structured English grammar.

heading: 3 Datasets
text: 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].
→ r
g
[0,0,0,0,0,0]
[1,0,0,0,0,0]
[1,0,1,0,0,0] [0,1,1,0,0,0]
[1,0,0,1,1,0]
Figure 2: Example tree positional encoding for the LTL request pattern (r→ g).

heading: 3.1 LTL and And-Inverter Graphs
text: 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 ( P ). By combining these operators, one can specify that P must occur infinitely often ( P ). The propositions are usually partitioned into inputs and outputs. In the following, we provide a small example. For inputs r1, r2 and outputs g1, g2 the LTL formula
¬(g1 ∧ g2) ∧ (r1→ g1) ∧ (r2→ g2)
specifies a simple arbiter using a mutual exclusion property for grant g1 and grant g2 and two response properties that guarantee that always request r1 is eventually answered by grant g1 and always request r2 is eventually answered by grant g2. Given an LTL specification ϕ, i.e., an LTL formula ϕ over atomic propositions AP and a partition of AP in inputs I and outputs O, the LTL synthesis problem is to determine whether a circuit over inputs I 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 to 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 LTL has only unary and binary operations, this is encoded by appending either 1, 0, representing the left child or 0, 1, representing the right child, in front of the encoding. Figure 2 shows an example tree positional encoding for the response pattern (r→ g).
The AIGER format became an established format for benchmarks, competitions, and tool implementations in both computer-aided verification and reactive synthesis. The AIGER format represents sequential circuits as and-inverter graphs in both ASCII and binary format. In this work, we refer to the original version 20071012 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 I , the number latches L, the number of outputs O, and the number of AND gates A. The header is followed by I lines defining the inputs, L 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 1 it corresponds to the negated variable and if the literal modulo 2 equals 0 it corresponds to the unnegated variable. Further literal 0 represents the Boolean constant ⊥ and literal 1 represents the Boolean constant >. 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 a circuit (left) and its AIGER representation (right), which is actually a prediction of a hierarchical Transformer.
aag 3 2 1 2 0 header 2 r1 4 r2 6 7 latch 6 g1 7 g2
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 implementation ignores the inputs I0 and I1, which represent both requests r1 and r2 (except for unnecessarily assigning them to variables 2 and 4). The circuit implementation satisfies the specification by alternating indefinitely between both outputs O0 and O1, which represent both grants g1 and g2, 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 a certain request).

heading: 3.2 Data Generation
text: From the LTL track of SYNTCOMP 2020 [26] we collected 346 benchmarks in Temporal Logic Synthesis Format (TLSF) [27]. Using SyFCo [27] we translated the TLSF specifications to the BoSy input format [14]. The BoSy input format is a JSON-based format representing specifications as a 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 1 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 a restriction that is comparable with most SYNTCOMP specs: 242 of 346 have ≤ 5 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 a uniform random choice from input atomic propositions i0, i1, i2, i3, i4 and a uniform random choice from output atomic propositions o0, o1, o2, o3, o4, respectively. The table below, shows three random examples of assumption patterns and three random examples of guarantee patterns.
assumption patterns guarantee patterns (i0 ∧ (¬o0 ∧¬o1)→ i0) (o2 U i3) ∨ o2 i0 (i0→ (o3 ∨ i3 ∨ (o3 ∨ i3 ∨ (o3 ∨ i3))))
(¬i0 ∨ o3 ∨ o2 ∨ o1 ∨ o0 ∨ i0) (¬o2 ∨¬o4)
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 a suitable assumption is limited to 5. Further, we implemented stopping criteria that limit the maximal number of guarantees to 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 i0, i1, i2, i3, i4 and all five outputs o0, o1, o2, o3, o4 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 a maximum variable index of 50, 2) we filter AIGER circuits with k AND gates if the number of circuits in the dataset with k AND gates exceeds 20% of the dataset size. This filtering especially reduces the number of circuits that have a low amount of AND gates.
The data generation method allows to 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, we constructed a dataset containing 250 000 unique samples split into 200 000 training samples, 25 000 validation samples, and 25 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 1 shows an example of a realizable specification in the test data.

heading: 4 Experimental Setup
text: Based on the code base of DeepLTL [21] (MIT license), we implemented a hierarchical Transformer [33] and augment it with a tree-positional encoding [47].2 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 can combine the representations of tokens across all assumptions and all guarantees. With this hierarchical encoding, we 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 our setting.
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 30 000 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.

heading: 4.1 Training Details
text: The Transformer architecture is a sequence-to-sequence model trained to predict a sequence of output tokens provided a sequence of input tokens. Similarly, we provide multiple sequences of input tokens to an hierarchical Transformer. Assumptions and guarantees are LTL formulas and can thus be directly represented as sequences of tokens with each atomic proposition, Boolean operator, temporal operator, and Boolean constant being a separate token. We omit
2The code, our data sets, and data generators are part of the Python library ML2 (https://github.com/ reactive-systems/ml2).
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 a special assumption token. Circuits are in AIGER format that we represent as a sequence of tokens by representing each integer with a corresponding token and replacing each newline character with a special new line token. Since all circuits in our dataset have the same inputs and outputs we can omit the header and the symbol table when tokenizing an AIGER circuit. Additionally, we include a special realizability token at the beginning of the sequence indicating whether a specification is realizable.
We trained all models using the Adam optimizer [29] with β1 = 0.9, β2 = 0.98 and = 10−9. The optimizer was used with a learning rate schedule proposed by Vaswani et al. [51] that increases the learning rate linear for a given number of warmup steps followed by a decreasing learning rate proportionally to the inverse square root of the step number. In our experiments, we used 4000 warmup steps as proposed by Vaswani et al. [51].

heading: 4.2 Performance Measures
text: There are infinitely many circuits satisfying a realizable LTL specification. To evaluate the performance of the trained models we 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 predictions that match the circuit in the dataset. Potentially, a prediction that does not match the system still satisfies the specification. We thus also measure the semantic accuracy, i.e., the percentage of the Transformer’s predictions that satisfy the specification. Note that, when using a 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 [10]. When training Transformers on the (easier) LTL trace generation problem [22], a significant difference between syntactic and semantic accuracy was observed. It appears that the Transformers rather generalize to the semantics of the logic than the particularities of the data generator. As we will see in the next section, our results are consistent with this observation even for the “harder” problem of predicting circuits.

heading: 5 Experiments
text: In this section, we report on a 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 see 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 on the size of the predicted circuits. Secondly, we compare the training with our data mining method against the ground truth, i.e., against a training of a hierarchical Transformer on the raw SYNTCOMP benchmarks. Thirdly, we compare the models performance on realizable and unrealizable specifications, where for the latter the model is supposed to construct a circuit representing a counter strategy. Lastly, we will take a deeper look into one of the specifications, which, compared to the example in Section 3 is an arbiter that prioritizes a certain request.
Overall results. We tested our models on four different datasets. A Testset consisting of heldout 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 we 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 a beam size of 16 and the Testset, on average 4.6 of the 16 AIGER circuits satisfy the specification.
In our Testset (see Table 1), we observe in many cases that the circuit prediction of our model is different from the circuit the tool would synthesize. Since it 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 accuracy. When analyzing the size of those circuits, we found both smaller and larger
circuits, with no significant decrease or increase in average circuit size. In total, the model was able to solve 79.9% of the held-out generated test instances with a beam size of 16.
While the training data is based on specification patterns extracted from SYNTCOMP benchmarks it is 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 12 properties, and properties of size greater than 25, the model achieved an accuracy of 66.8% for the resulting 145 benchmarks using a beam size of 16.
For a timed out specification it is not known whether it is realizable or unrealizable. The model achieves an accuracy of 30.1% for beam size 16 demonstrates that our approach can yield performance gains in practice. To highlight the capabilities of our model we display in Figure 9 in the appendix the largest circuit that is predicted for a timed out specification and satisfies the specification.
We constructed the Smart Home set, with the same restriction as for SYNTCOMP, from a recently published benchmark set for synthesizing smart home applications [1]. The hierarchical Transformer is able to solve 44.8% of the provided instances. When compared to the full benchmark (i.e., 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 of the model depending on the size of the predicted circuit. Results are shown in Figure 5. 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 8). Meaning that the model has seen a 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 on raw SYNTCOMP benchmarks. We did a baseline experiment by training with various batch sizes on the raw SYNTCOMP benchmark. This training (not surprisingly) fails whereas our data generation method enables a stable training.
Unrealizabile Specifications. The training data contains both realizable and unrealizable specifications. In Table 3 we analyze the accuracy for realizable and unrealizable specifications separately on our test data. While the syntactic accuracy is higher for realizable specifications, in terms of the
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.
Prioritizing arbiter. Building on the example of Section 3, we show that the model can handle more interesting, real-world specifications. Figure 7 shows the specification, AIGER file and the circuit visualization of an 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 3.

heading: 6 Conclusion
text: 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 to successfully train hierarchical Transformers on the LTL synthesis problem for specifications composed of specification patterns. We also showed that the models generalize to unseen specifications, including specifications that are both realizable and unrealizable and specifications that cannot be solved by a classical synthesis tool within a time limit of 120 seconds. Furthermore, we performed an out-of-distribution test on a recently added benchmark set on synthesis problems for smart homes. Experimental results suggest that the Transformer can be 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 of Perspicuous Software Systems” (TRR 248, 389792660).

Review summaries:
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.  The 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.  Another 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.  In 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.  There 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.  Main question:  - What if Strix is given, let's say, two hours for attempting to solve the example of Fig 9, of the supplementary material?  - 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.  - 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.  These are the most important issues. Their answer might affect my recommendation.  For 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.  ----  Thank you for your response. I'm more convinced now about the merits of the paper. I'm reviewing my scores accordingly.   There 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:  - 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. - Not being able to scale to bigger problems.  This paper has issue (2), but it is transparent about it.  Now, for issue (1), they choose a very hard problem:  synthesizing the whole circuit. There are no shortcuts there: The circuit do work or doesn't.  Synthetizing 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: Foundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf Restraining Specifications. Giuseppe De Giacomo, Marco Favorito, Luca Iocchi and Fabio Patrizi. ICAPS 2019. https://ojs.aaai.org/index.php/ICAPS/article/view/3549  I 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.   After reading the other reviews, I think the paper should explain better how hard are the instances generated. In 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. 

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.  

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).  A 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.