Venue: NeurIPS 2021 Conference

Reviews:

final_score: rating: 6: Marginally above the acceptance threshold
review_content: 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. 

main_review: Strengths:
- Circuit synthesis is a new and interesting application for deep learning approaches. 
- The paper presents a method to generate synthetic data for this application (which solves the issue of lack of training data).
- An implementation using hierarchical transformers that has decent performance and that can be used as a baseline for future work in this domain.
- Evaluation is extensive (includes comparing  transformers vs hierarchical transformers), multiple different kinds of datasets, and a detailed analysis of results

Weakness:

My 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)
- Are the numbers in section 4 the average of multiple (ideally 5) separately trained models?
- Was the hyper-parameter search done? In a new benchmark paper, hyper-parameter search is very important to establish a good and robust baseline. 
- It will be interesting to see other variations of the model architecture (for e.g. different kinds of encodings on the inputs and outputs) 

Another significant concern is the lack of a discussion on the limitations to the approach
- 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. 
- What fraction of the original SyntComp dataset satisfies the filtering conditions imposed in this paper?
- 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?

Minor:
- Explain the meaning of latches
- How do the results in table 2 look for the other datasets?

limitations_and_societal_impact: Yes.
review_title: null

final_score: rating: 8: Top 50% of accepted NeurIPS papers, clear accept
review_content: 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.

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.

main_review: [page 2]:* When using a beam search, models achieve an accuracy of up to

- Accuracy of correctness or recovering the label? Top accuracy? The mention of beam search might hint is top-k

-----

[page 2]:* Furthermore, the models can solve generated test instances on which classical LTL synthesis tools timed ou

- We’re the solutions correct?

-----

[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

- Most likely all assumptions and guarantees will occur in the validation and test sets.

-----

[page 7]:* when using a beam search algorithm only one of the predictions needs to match

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

-----

[page 7]: * Experiments section

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

-----

[page 8]:* We consistently observed in all experiments that the beam search signiﬁcantly increases the accuracy.

- It’s been observed that decoding with language models with a larger beam size can decrease the quality, so this is not obvious.


limitations_and_societal_impact: N/A
review_title: null

final_score: rating: 5: Marginally below the acceptance threshold
review_content: 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.
main_review: ### Contribution and Significance
Transformers 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. 

### Clarity and Quality
This 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.

The 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. 

### Questions
Q1: 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? 

Q2: 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?

Q3: From the shared GitHub repo, Smart Home seems to be part of the SYNTCOMP benchmarks, instead of independent one. Can you clarify that?

Q4: What is the guarantee on unrealizable specifications? Does the model always produce a counter strategy? 

Q5: 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 ? 
limitations_and_societal_impact: The authors do not explicitly discuss their limitations or potential negative societal impact. There is no concern about the latter. 

Dataset 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_title: null

final_score: rating: 6: Marginally above the acceptance threshold
review_content: 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).

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.
main_review: ## Originality
The 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.

## Quality
The presented work is technically sound, however, there is limited attention given to some of the core limitations:

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

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

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

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

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


## Clarity
The paper is written very well, and the only suggestions I have are to address key questions that came to mind while reading:

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

- What is the time spent on each of the beam sizes in computing a solution?

- Judging by the table, the smart home dataset continually improves. Does this trend continue for beam size = 32 or higher?

- Why do unrealizable benchmarks become easier with larger beam sizes?

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


## Significance
The 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?

I 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.

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

Finally, 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?
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_title: null

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)