Venue: ICLR 2023 Conference

Reviews:

final_score: rating: 5: marginally below the acceptance threshold
review_content: summary_of_the_paper: Given a formal specification in LTL, this paper introduces a transformer architecture that aims to transform a defective circuit into a repaired one, in accordance to the spec.   The primary contribution is in the transformer neural architecture, which they call the separated hierarchical transformer since it has separate local layers that do not share model parameters. 

In addition, they introduce a data generation procedure that models human errors to encourage generalization to more complex specifications.
strength_and_weaknesses: ### Main strengths:

- Well motivated problem
- Mostly well written and easy to follow
- Comprehensive experimental analysis (with some caveats)

### Main weaknesses:

- Most of the value of this contribution rests upon whether the following causal claims are true and well-justified: the new architecture and/or the data-augmentation procedure caused the improvements in performance of state of the art.  Despite a number of different experimental analyses in the paper, determining this is not straightforward.  In particular, I cannot see where if anywhere the number of parameters are controlled for.  The paper does say that using separated heads leads to an increase in the number of parameters, but I do not see any evidence in this paper to suggest that performance increases over previous methods is not attributed simply to this network being larger.  Also, the experimental results do not allow us to distinguish whether improvements are from the model changes or from the data changes.
- I have some reservations about the use of Levenshtein distance as a metric for the quality of a synthesized circuit.  Obviously there is no “right” metric, and Levenshtein may be used in prior work, but a more semantic property could be used in addition to convey improvement.  For instance, one could try to look at (some approximation of) the increase or decrease in the number of satisfying traces
clarity,_quality,_novelty_and_reproducibility: The paper is mostly well written and straightforward to follow.  The exception are the figures, which would benefit from more information in the captions.

The novelty of this paper is limited.  The main contributions are a modest variant on an existing hierarchical transformer architecture, and a straightforward data augmentation procedure.  Individually or together these do not seem substantially novel, but that by itself is not necessarily a problem.

The description is precise enough to attempt to reproduce this work.  The authors state in several places that they will produce the source code for this work, which will improve reproducitibility further.

### Questions

- Clarify “filtered out samples that exceed our model restrictions”
- It’s not clear whether “after last iteration” in Table 1 means after exactly 2 iterations of after some arbitrary number.
- In Figure 4 has an “error” label purple, but I do not see any corresponding purple in the graph itself.  Is this just too small to see on the graph?
- Clarify “accuracy” in Figures as semantic accuracy and provide explicit meaning to [0, 1] range.
summary_of_the_review: - Well written paper with comprehensive experimental analysis
- Limited novelty
- Would like to see much more evidence that claimed contributions are responsible for improved performance
review_title: null

final_score: rating: 5: marginally below the acceptance threshold
review_content: summary_of_the_paper: The paper extends hierarchical transformers (neural network models for
synthesising circuits from linear time specifications)  to build models  for
the repair of circuits so that they satisfy a certain linear time property. The
models, which are also used in an iterative procedure to do reactive synthesis,
are trained on a novel algorithm for introducing faults to a dataset.
strength_and_weaknesses: + Good empirical analysis that shows the efficacy of the proposed method in
circuit repair and its superior performance in reactive synthesis when compared
with the state-of-the-art.

- Highly incremental to previous work (the model proposed is a variation of the
  work from Li et al. (2021) and the data generation algorithm is a standard
  fault injection algorithm).

- Some comparisons with related work are shallow. For instance, the
  advantages/disadvantages of the present method to symbolic synthesis are not
  discussed.
clarity,_quality,_novelty_and_reproducibility: The paper  is not entirely self contained with many of the details given in the
Appendix. Though it would be impossible to fit everything in the page limit, I
think that some additional details on major concepts could be given; for
instance, the reactive synthesis problem is never defined and the term
'attention' is used a number of times but never explained. The novelty of the
paper is not particularly strong as it is highly incremental to Le at al.
(2021).
summary_of_the_review: The paper introduces neural models for circuit synthesis which exhibit gains
over the state-of-the-art, albeit being highly incremental to previous work.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: The paper investigates the application of transformer models to repairing circuits given formal specifications. The transformer takes a faulty circuit represented in AIGER format and a specification in LTL, and outputs a circuit that hopefully satisfies the specification. The paper also comes with a detailed description of the generation process of datasets.
strength_and_weaknesses: Strength:

+ The approach is technically sound. While there have been a variety of work on generating logical formulas, formal specifications, or formal proofs with language models these days, the problem this paper is targeting (with language models) looks novel to me.

+ The empirical evaluation is extensive, and validates the proposed framework. The difficulty measures and Levenshtein distance help better understand the capability of language models on the task.

Weakness:

- The specifications are restricted to 5 inputs and 5 outputs, no more than 12 properties. Did you observe a degradation in performance as the size of specifications increases?

- What are the advantages of hierarchical transformers over vanilla ones? Although the experiments are extensive, I can't seem to find this particular dimension of evaluation. Also, would fine-tuning a pre-trained language model be as good as training a hierarchical transformer from scratch?
clarity,_quality,_novelty_and_reproducibility: The paper is clearly written and easy to follow. The approach looks novel to me. The authors promised the release of datasets and code for reproducibility. 
summary_of_the_review: The framework is well-designed and the performance looks good. I lean toward accepting the paper.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: This paper proposes using a neural network to iteratively repair sequential circuits represented as And Inverter Graphs (AIGs) against temporal logic specifications. The architecture is a variation of a transformed that separately takes as input the circuit and the specification. The specification is also separated into its assumptions and its guarantees. The network is then trained by (i) sampling circuits and specifications from well established benchmarks (ii) randomly introducing errors by changing the textual representation of the AIG.

Empirical results suggest that this technique is indeed able to correct incorrectly synthesized specifications and that repeated applications further improve performance. Importantly this can be used in combination with neural network based synthesis of the initial circuit.
strength_and_weaknesses: # Strengths
1. The problem considered is a very important and difficult problem with a wide range of applications. Further, neural approaches make sense since in practice scalable synthesis in electronic design automation involves specializing the synthesis software by hand.

2. The technique empirically improves synthesis on established benchmarks. This is measured as Levenshtein distance in the AIGER format which intuitively captures a degree of close-ness.

# Weakness

1. The technique seems to be limited to incredibly small circuits.
    - To give context, the upper limit on 61 symbols is easily exceed by small adders (a naive adder using the popular py-aiger tool uses 65 symbols.)

2. Unconvinced by human generated error argument.
   - Having worked with AIGER a fair amount, most large circuits I create are done using tools (e.g., py-aiger) and not by hand. Thus, the argument that the introduced errors are natural seems odd.
   - A more common setting is that the specification (or unit tests) used when designing the circuit were slightly wrong, either because:
     1) It was missing assumptions.
     2) It was missing guarantees.
     3) Used bounded time horizon reasoning.
   - I would be much more interested in a neural repair that could fix this more common class of errors.

3. Perhaps I missed something, but there seems to be a missing comparison with non-neural techniques. As the authors point out, this is a very mature field, so it would be have been nice to see a detailed comparison.
clarity,_quality,_novelty_and_reproducibility: The paper is well written and the technique is certainly novel. I believe that the basic architecture and dataset could be reproduced from the description given in the paper.

The clarity of the baseline comparison could be improved (see weakness above).
summary_of_the_review: Overall, I believe the future potential of the propose method out weight the clear limitations on scale and questionable motivation for the error insertion. Circuit repair (and circuit synthesis) are computationally difficult problems in general and the field largely relies on hand tuned heuristics. Supporting data-driven techniques is a natural means to accelerate synthesis in specific target domains.
review_title: null

Meta-review: metareview:_summary,_strengths_and_weaknesses: This paper introduces a way to repair sequential circuits that do not meet a given LTL specification. The overall idea follows closely previous work on synthesis from LTL specifications [1], except that the failing circuit becomes input to the Transformer. The paper also introduces a variant on the hierarchical Transformer architecture and a data augmentation procedure.

The main result is that using deep learning can be effectively used to predict the design of a correct circuit given a failing circuit and its LTL specification, and this results in correctly synthesizing many more circuits. This is indeed an interesting result, and could turn out to be an important next step in a difficult problem.

The architectural and learning innovations here are fairly straightforward, as acknowledged by several of the reviewers, but the main innovation here is in evaluating synthesize+repair versus a synthesize-only neural workflow.

The most serious weaknesses discussed by the reviewers were adequately addressed in the author response. These were: 

   * Controlling for the number of parameters (Y3T4): Additional experiments in the response addressed this.
   * Comparison to symbolic methods (oocom, NdwS): This is well addressed by the Strix comparison, which is impressive.
   * Advantages compared to hierarchical transformers compared to vanilla: This is also addressed in the response to LxSj.

I would emphasize to the authors, however, that many of these results (even ones that were in the original draft) are relegated to appendices. These are important comparisons, as can be seen from the fact that several reviewers asked for them. I would urge the authors to highlight all three of the results above in the main paper. They are more important in my view than (say) Figure 3, which could be safely relegated to an appendix.

A final weakness of the paper is that the specifications here are extremely small, and would not cover many real world circuits. The authors responding by pointing out that the synthesis problem is 2-EXPTIME. That would usually be a good response, but it is not a good response here. The problem is that while the exact problem is indeed intractable, but the neural method does not solve the exact problem, because its output is not guaranteed to meet the specification (of course you can use it to generate-and-test with a verifier afterwards). Part of the point of using a deep learning method for synthesis is to give up the formal guarantees to get scalability.

However, I am persuaded by the fact that: (a) the standard benchmarks are necessarily going to be restricted to those that symbolic methods can solve, and (b) the overall idea of synthesize+repair using Transformers can in principle be applied to much larger circuits (if one resorts to empirically verifying the circuits rather than formal verification). But it would be good if a more nuanced discussion of this point appeared in the paper.

[1] Frederik Schmitt, Christopher Hahn, Markus N. Rabe, and Bernd Finkbeiner. Neural circuit synthesis from specification patterns. NeurIPS 2021.



justification_for_why_not_higher_score: This problem is specialized enough that it might not yet be of interest to a larger subset of the community.
justification_for_why_not_lower_score: The main result makes an interesting advance towards a difficult problem.
Decision: Accept: poster