Circuit Transformer: A Transformer That Preserves Logical Equivalence

## Abstract

Abstract. Language, a prominent human ability to express through sequential symbols, has been computationally mastered by recent advances of large language models (LLMs). By predicting the next word recurrently with huge neural models, LLMs have shown unprecedented capabilities in understanding and reasoning. Circuit, as the “language” of electronic design, specifies the functionality of an electronic device by cascade connections of logic gates. Then, can circuits also be mastered by a a sufficiently large “circuit model”, which can conquer electronic design tasks by simply predicting the next logic gate? In this work, we take the first step to explore such possibilities. Two primary barriers impede the straightforward application of LLMs to circuits: their complex, non-sequential structure, and the intolerance of hallucination due to strict constraints (e.g., equivalence). For the first barrier, we encode a circuit as a memory-less, depth-first traversal trajectory, which allows Transformer-based neural models to better leverage its structural information, and predict the next gate on the trajectory as a circuit model. For the second barrier, we introduce an equivalence-preserving decoding process, which ensures that every token in the generated trajectory adheres to the specified equivalence constraints. Moreover, the circuit model can also be regarded as a stochastic policy to tackle optimization-oriented circuit design tasks. Experimentally, we trained a Transformer-based model of 88M parameters, named “Circuit Transformer”, which demonstrates impressive performance in end-to-end logic synthesis. With Monte-Carlo tree search, Circuit Transformer significantly improves over resyn2 while retaining strict equivalence, showcasing the potential of generative AI in conquering electronic design challenges.

## 1. Introduction

Figure: Figure 1. The logic synthesis pipeline with Circuit Transformer. From left to right, the number of AND ($\wedge$) nodes in the toy AIG network is reduced by one, while the logical functionality remains equivalent.
Refer to caption: x1.png

Recent years have witnessed the tremendous success of large language models (LLMs) through world-changing products like ChatGPT and Gemini (OpenAI, ; Team et al., ). While they mastered the art of human languages in an unprecedented way from storytelling to conversation, their overall workflow is surprisingly simple: “just adding one word at a time” (Wolfram, ). That is, given the text so far, a LLM will recurrently predict the next word via a huge neural model trained on large-scale corpora, and append it at the end of the text.

In the world of electronics, there is another fundamental “language”, circuits, that specifies the functionality of an electronic device by cascade connections of logic gates. Thus, it is appealing to wonder whether it is possible to master circuit design by a similar manner. That is, can we train a “circuit model” of substantial size, then design circuits via simply predicting the next logic gate? For instance, logic synthesis, which is to find a compact representation of a circuit, is analogous to text summarization that creates a concise summary of a long text. Then can we employ the same methodology to conquer both tasks, by recurrently predicting the next gate or word?

However, the essential differences between circuits and human languages formed a wide gap to such methodology sharing. The first gap arises from their inherently different natural structures. While all human languages are born to be sequential as people need to speak it word-by-word, circuits are not likely to be represented gate-by-gate, but rather in a cascade structure, given that logic gates typically involve two or more inputs. Such complex cascade structure brings significant difficulty for existing language models to predict gates and generate circuits, as they are designed for leveraging sequential information. Even if the circuits can be serialized in some standard text formats (e.g., AIGER (Biere, ) for And-Inverter Graph), such compact, storage-oriented formats are not sufficiently intuitive for neural models to decode, resulting in poor empirical performance in terms of scalability and accuracy.

The second gap, which might be more intractable, lies in the conflict between the precision demanded by circuits and the inherently approximate nature of neural models. While human languages are already much more tolerant to ambiguity and inaccuracy, LLMs still suffer from hallucination (i.e., the model-generated content may be false or misleading (Ji et al., ; Yu, )), not to mention that circuit design usually requires strict constraint satisfaction. In logic synthesis, for example, the synthesized circuit is typically mandated to be precisely equivalent to the original. A single bit of difference in truth table can result in a complete failure. Even if we can add a term in the loss function of neural models to penalise such circumstance, it will still only mitigate, if possible, rather than eliminating non-equivalence that is easily achievable in existing synthesis tools.

In this work, we take the first step to bridge the two gaps, aiming to design circuits through a fully generative approach supported by a large neural model. For the first gap, our emphasis is on devising an intuitive and efficient circuit encoding scheme tailored for neural models. Instead of tokenizing standard text formats, we propose a memory-less, depth-first traversal trajectory of circuits as the encoding. That is, we traverse through a circuit from its primary output in a depth-first manner, without labeling visited gates. The resulting full traversal trajectory serves as a serialized encoding to be tokenized. In this way, Transformer-based models are allowed to efficiently exploit the structural information via tree-based positional encodings, while retaining the complete circuit information. Given the above serialized encoding, we are able to define the circuit model probabilistically as $P(g_{n}|g_{1:n-1},e_{1:n-1})$, the probability distribution of the $n$-th gate (or input) $g_{n}$ in the traversal trajectory given the previous elements $g_{1},\dots,g_{n-1}$ with their positional encoding $e_{1},\dots,e_{n-1}$, facilitating a gate-by-gate generation of circuits.

For the second gap, we focus on one of the most common constraints in circuits — the equivalence constraint, which means the output of the generated circuit must be equal to specific values when given specific inputs. Our insight is that, instead of adding an expensive post-process to fix the equivalence issue, a more efficient direction is to ensure that every step remains within the feasible region. To achieve this, we propose an equivalence-preserving decoding process that detects potential conflicts at each step given current circuit encoding. A conflict masking layer is appended to the output of the probabilistic circuit model, assigning a probability of zero to conflict-causing tokens, so as to eliminate any risk of non-equivalence.

Moreover, circuit design is commonly associated with optimization, and the proposed circuit generation process can be also viewed as a sequential decision-making process in optimization tasks. In this context, we show that a trained probabilistic circuit model can serve as a policy to be integrated into Monte-Carlo Tree Search (MCTS), to improve the optimality of the generated circuit.

To validate our proposed approaches, we trained a Transformer model with 88 million parameters, named “Circuit Transformer”, to perform end-to-end logic synthesis on 8-input, 2-output circuits. The model is trained on 20 million random generated circuits, accepting the original circuit as input and the synthesized circuit as output. Experimental results show that Circuit Transformer performs impressively in end-to-end logic synthesis. With the aid of Monte-Carlo tree search, it significantly outperforms resyn2 in ABC, showcasing the potential of generative AI in conquering electronic design challenges.

## 2. Related Work

While machine learning (ML) for electronic design automation (EDA) have been one of the trending topics with lots of studies, most of them focus on addressing ML-friendly subtasks, such as classification, regression and Markov decision process, to enhance the performance of existing EDA algorithms. For example, in logic synthesis, recent ML-based studies focus on scheduling existing traditional optimization strategies (Neto et al., ) and operators within the synthesis flow (Yu et al., ; Hosny et al., ; Grosnit et al., ; Zhu et al., ). Graph Convolution Networks are utilized in some studies to capture information from circuits (Haaswijk et al., ). None of them directly generates logic synthesis solutions, primarily due to the complicated constraints (Huang et al., ).

Recently, there are a few new ML researches (Rai et al., ; Schmitt et al., , ) attempting to tackle circuits in a more generative way, including the employment of Transformer models (Vaswani et al., ) and pre-trained language models. However, since they have not fully addressed the aforementioned issues about circuit representation and constraint satisfaction, their application is currently confined to small-scale, approximated scenarios that permit constraint violation.

Along with the recent wave of LLM applications, there are emerging works on the integration of LLMs in EDA, including ChipGPT (Chang et al., ), Chip-Chat (Blocklove et al., ) and ChipNeMo (Liu et al., ). Similar to LLMs’ integration in other fields, these works focus on natural language interaction in hardware design. They generate hardware description programs, EDA scripts and analyses in response to user prompts, rather than performing the actual EDA tasks (synthesis, verification, etc.) themselves.

## 3. Methods

### 3.1. Neural Encoding of Circuits

Figure: Figure 2. A comparison between standard AIG encoding format (AIGER) and our proposed trajectory-based encoding.
Refer to caption: x2.png

In this section, we focus on finding an encoding scheme of logic circuits that is natural for neural models to process, not only for information capture, but also for transformation and generation. Unless otherwise specified, all the circuits are represented in And-Inverter Graph (AIG) format.

Traditionally, for encoding scheme design, what matters a lot is compactness, i.e., whether it makes efficient use of the memory or storage. The ease of decoding is usually of secondary importance once it can be programmed in advance. However, when entering the realm of neural models, data encodings are deliberately redundant to facilitate neural decoding. For example, for a categorical label $l$ with $N$ possible values, most neural models will employ one-hot encoding $\mathbf{I}_{l}$, i.e., a vector of $N$ binary element whose values are all 0 except the $l$-th element which equals to 1. Such an encoding of $N$ bits (or $N$ floats) is far more redundant from a regular one of $\lceil\log N\rceil$ bits (or a single float), but it “unfold” every possible value with a dedicated input, which allows neural models to simply process each input separately, without the need to learn a decode rule from value ranges to labels.

For the neural encoding of circuits, we follow the same methodologies: by allowing “unfolding” with additional redundancy, we free the neural models from learning complicated decode rules. More specifically, we employ a memory-less, depth-first traversal trajectory to serialize the circuit, as illustrated in Figure 2. Given a circuit, we start the traversal from each of its primary outputs (PO), and visit each connected gate in a depth-first, recursive manner. Backtracking occurs when a primary input (PI) is reached. The path from the PO to the current node will also be recorded. Importantly, such a traversal is memory-less, i.e., visited nodes will not be labelled during the traversal, thus a node will appear multiple times in the trajectory if its fan-out is larger than one.

Specifically, for Transformer models, a tokenized sequence with positional encodings is required to represent a sequence with each element’s position. To tokenize the traversal trajectory mentioned above for an $N$-input circuit, we use a vocabulary of $2N+4$ tokens: EOS (end of sequence), PAD (padding token to align sequences of different length), $N$ primary inputs $x_{1},\dots,x_{N}$ with their inverses $\overline{x_{1}},\dots,\overline{x_{N}}$, and AND gate $\wedge$ with its inverse $\overline{\wedge}$. By doubling the PO and AND gate tokens to include their inverses, we avoid the occurrence of individual inverter tokens, which effectively shorten the tokenized trajectory. Also note that all AND gates in a circuit correspond to the same token “$\wedge$”, which is very different from the AIGER format.

For the positional encoding, instead of regular sequential encoding, we utilize the recorded path from the PO as a node’s position, and encode it as a stack of one-hot encodings (“10” for the 1st input and “01” for the 2nd input). For example, in Figure 2, the position of the 2nd node $a_{1}$ in the trajectory can be represented as $e_{2}=[10]$ (push “10” in the encoding stack of $o_{1}$ which is empty, as it is $o_{1}$’s first input), and the position of the 4th node $x_{2}$ in the trajectory can be represented as $e_{4}=[01;e_{2}]=[0110]$ (push “01” in $e_{2}$ as $x_{2}$ is $a_{1}$’s second input) and $e_{6}=[10;e_{5}]=[1001]$ when $x_{2}$ is secondly visited as $a_{2}$’s first input. Such a technique was initially proposed in (Shiv and Quirk, ) to handle tree-based structures. For circuits with multiple POs, we initialize the encoding stack of the $k$th PO $o_{k}$ with a unique one-hot encoding $\mathbf{I}_{k}$.

While such an encoding introduces apparent redundancies, it allows Transformer-based models to manipulate the circuit with ease. For a gate in the circuit, the position encoding of all its transitive fanins and fanouts can be accessed from its own positional encoding by linear transformations, which is easy to be learned by neural models. In contrast, the standard AIGER format shown in Figure 2 requires the model to extract the cascade structure from groups of triples defining AND gates, demanding a more advanced level of semantic understanding.

To provide a more accessible example, we sketch in Figure 3 how a simplified Transformer model may compute the truth table of a circuit with our proposed circuit encoding.(^1^11Note that the following results are for illustration only. An actual training may not lead to such a result due to the more complex model structure and the randomness in training.) In this example, the Transformer only need to learn 1) the embedding of each PO as its own truth table (e.g., “01010101” for $x_{1}$ and “00110011” for $x_{2}$) 2) the query and value vectors to be identical to the corresponding positional encoding and the token embedding, while the key vectors equals to its position encodings left shifted by 2 (its fanout gate’s position). In such a way, a gate will have high attention score with its two inputs, with its attention value equals to the weighted sum of its inputs’ value vectors. 3) a feedforward neural network approximating non-linear functions such as $\text{sgn}(x)$ and $1-\text{sgn}(-x)$ to output a valid truth table. By passing one attention layer, the truth table of AND gates $a_{1}$ and $a_{2}$ are computed, and the truth table of $a_{1}$ can also be computed with an additional layer.

Figure: Figure 3. A simplified, hypothetical Transformer model to compute the truth table of the AIG in Figure 2.
Refer to caption: x3.png

### 3.2. Circuit Model: Predict the Next Logic Gate

Utilizing the efficient neural encoding of circuits proposed above, in conjunction with Transformer models and supervised learning, we can successfully address various circuit-related classification and regression tasks. However, in contrast to standard neural techniques for extracting graph information, such as graph neural networks, what distinguishes the proposed encoding is its generative capability. Now, let’s revisit our initial question: can we train a “circuit model” that design (generate) circuits via simply predicting the next logic gate, just like what large language models do to master human languages? In this section, we show the feasibility of such an generative approach based on our proposed neural encoding of circuits.

Similar to language models, we define a circuit model as one that computes the probability of a logic gate or PI, $g_{n}$, to be appeared as the $n$-th token in the traverse trajectory of a circuit. This probability is conditioned on the previous nodes $g_{1},\dots,g_{n-1}$ with their positional encodings $e_{1},\dots,e_{n-1}$ in the trajectory, denoted as

$$ (1) $P(g_{n}|g_{1:n-1},e_{1:n-1})$ $$

Most of the time, we design circuits under specific contexts that specify the characteristics of desired circuits, such as an original circuit to be equivalently simplified, a sentence “please generate a 2-bit adder” to be followed, or a picture of circuit to be interpreted. Generally, we denote such a context as $c$, and the circuit model should condition on the context, denoted as

$$ (2) $P(g_{n}|g_{1:n-1},e_{1:n-1},c)$ $$

In such a way, once we obtained a conditional circuit model, we can construct a circuit by recurrently sampling a gate or PI $g_{n}$ from the distribution $P(\cdot|g_{1:n-1},e_{1:n-1},c)$, computing $e_{n}$, adding $g_{n}$ as the input of a previous gate, and updating the path from $g_{t}$ to the current PO. Note that the nature of depth-first traversal determines the position of $g_{t}$, thus no additional position selection mechanism is required. Since a node may appear multiple times in the memery-less traversal trajectory, a set of non-isomorphic gates is also maintained so that all isomorphic gates will be merged during the construction. More details are shown in Algorithm 1. With such a generative routine, we can tackle circuit-related tasks in a very similar way to language models. An example is shown in Figure 4 how text summarization and logic synthesis can be solved with the same generative methodology.

Figure: Algorithm 1 Circuit generation by predicting the next gate

Figure: (a) Text summarization
Refer to caption: x4.png

### 3.3. Equivalence-preserving Generation of Circuits

The demand for accuracy, particularly in the form of strict equivalence preservation, is a fundamental aspect of circuit design, yet it poses a challenge for neural models. However, by leveraging the property of Boolean computation and our proposed circuit encoding, we demonstrate the feasibility of designing an equivalence-preserving decoding process, ensuring that every $g_{t}$ predicted by the circuit model conforms with the provided equivalence constraints.

The key to the equivalent-preserving decoding is that, we can still infer part of the truth table for a Boolean function even when the function is not fully specified. For example, consider a 3-input Boolean function $f_{0}(x_{3},x_{2},x_{1})=x_{1}\wedge?$ (“$?$” represents any valid Boolean expression), even if $f_{0}$ is not fully specified, we can still deduce part of the truth table as “0?0?0?0?”, due to the property of the AND operator that $0\wedge?=0$. In this case, if we have an equivalence constraint $f(0,0,0)=1$, then we already know that $f_{0}$ violates this constraint even if only two elements (an AND gate and a PI) are specified. Therefore, if we have a chance to re-choose the first input of the AND gate in $f_{0}$, we should mask the choice of $x_{1}$ (as well as $x_{2}$ and $x_{3}$) out of the available choices.

Given the insight above, our equivalence-preserving approach will try all possible gates and PIs before predicting a gate via a circuit model, and identify choices that would result in a violation of equivalence constraints. Then, we add a masking layer with softmax at the end of the circuit model, to assign probability zero to these violation-causing choices. Benefitted from the depth-first nature, the current choice of node will not change the truth table of past generated circuit components, thus the non-violated status will persist if every generated node does not cause a violation. Once the construction process is completed, the truth table of the circuit is determined, and a non-violated status ensures equivalence. The algorithmic detail is shown in Algorithm 2 and an example is given in Figure 5.

Figure: Algorithm 2 Get valid choices of $g_{t}$ to be inserted to a trajectory

Figure: Figure 5. An example of the equivalence-preserving decoding process. During the whole depth-first construction process, the choice of tokens are restricted to conform with the truth table of the original logic function $(x_{1}\wedge x_{2})\wedge(x_{2}\wedge x_{3})$, which is “00000001”. For step 5, all tokens except $x_{3}$ are masked, as $x_{3}$ directly leads to a completed state.
Refer to caption: x6.png

### 3.4. Circuit Generation as a Sequential Decision Process

Until now, we regard circuits as similar to languages, in which the circuit model try to “decode” a circuit as an “answer” that conforms with the context. However, compared with language tasks, circuit design are usually more directly involved to optimization, in which we aim to obtain a circuit with better metrics (e.g., less gates in logic synthesis). From such a perspective, since we successfully developed a sequential generation process, we can also interpret this process as a decisional one, in which we can define states, actions and rewards for each step to match a specific optimization objective. And the circuit model, which maps the current circuit encoding to a distribution of nodes, can be regarded as a policy to be leveraged and improved.

For example, in logic synthesis, we can define the state, action and reward for each step $t$ as follows:

- •
State: the previous trajectory $g_{1},\dots,g_{t-1}$ with positional encodings.
- •
Action: the valid choices of $g_{t}$ from Algorithm 2.
- •
Reward: -1 if $g_{t}$ is a gate, or 0 if $g_{t}$ is a PI. If there are one or more gates that is merged with previous ones in Algorithm 1, then the reward should also plus the number of merged gates.

In such a way, any optimization method for sequential decision processes, including heuristics search and reinforcement learning, can be employed to maximize the cumulative reward. To illustrate, we applied Monte-Carlo Tree Search (MCTS) to further minimize the total number of gates of the generated circuit. It bears a resemblance to AlphaGo Zero (Silver et al., ) but incorporates several adaptations: 1) the branch with the maximum cumulative reward appeared is selected as the final action, instead of the most visited branch. This is done as we aim to identify the extreme value without the presence of an opponent. 2) we also use the circuit model $P(\cdot|g_{1:n-1},e_{1:n-1},c)$ as a rollout policy, rather than training another action-value function. 3) no further training for policy improvement is done yet, which is leaved as a future work.

## 4. Experiments

### 4.1. Truth Table Computation with Tiny Models

To empirically demonstrate the ease of neural manipulation with our proposed circuit encoding in subsection 3.1, we show the feasibility to compute the truth table of a circuit (see Figure 3) with absurdly tiny Transformer models of $\sim 10^{3}$ parameters based on our proposed encoding. The truth table computation problem of $N$-input, 1-output circuits is modelled as a multi-label classification task with $2^{N}$ binary labels corresponding to the truth table, and we use a supervised learning approach with loss function set to be the cross entropy between predicted and true truth tables. 4-input, 1-output AIGs are randomly generated with a maximum depth of 3 to train and test the models. We employ an encoder-only Transformer architecture, setting the embedding width and intermediate size of the Transformer models to be 16, aligned with the length of the truth table. Four models are trained with different number of layers.

The result is shown in Table 1. A single-layer Transformer model with only 1,840 parameters can already reach initial capability with 87.2% accuracy, while a 4-layer model with 6,736 parameters can almost perfectly compute truth tables with over 99.9% accuracy. Actually, to the best of our knowledge, this is the smallest trained Transformer model in literature that can tackle a reasonably challenging task. This indicate the advantage of our encoding scheme that it can be easily understood and manipulated by Transformer models without millions of parameters.

**Table 1. Performance of computing the truth table of random 4-input AIGs with tiny Transformer models.**
| #(layers) | 1 layer | 2 layers | 3 layers | 4 layers |
| --- | --- | --- | --- | --- |
| #(parameters) | 1,840 | 3,472 | 5,104 | 6,736 |
| accuracy | 0.8721 | 0.9776 | 0.9796 | 0.9993 |

### 4.2. Logic Synthesis

In this section, we select logic synthesis as a representative, comprehensive circuit design task covering all our proposed techniques. A Transformer model is trained with the traversal trajectory encoding of original AIGs as input (context $c$ in the conditional circuit model described in subsection 3.2), and the encoding of synthesized AIGs as output, shown in 3(b).

To train the Transformer model, we build a large dataset containing 20 million randomly generated 8-input, 2-output AIGs. The supervised signal (i.e., the synthesized circuits) are generated by the resyn2 command in ABC (Brayton and Mishchenko, ). We restrict that the length of the traversal trajectory for each AIG should be no more than 200, all the 8 inputs should appear in the AIG, and each AIG has an unique truth table. The average number of AND gates are 24.10 for the original AIGs and 9.57 for the synthesized AIGs.

The details of the Transformer model are as follows. We employed an encoder-decoder architecture, each with 12 attention layers. The embedding width and the size of feedforward layer are set to 512 and 2048, leading to 88,225,800 total parameters. The vocabulary size is 20 (8 POs and AND gate with their inverse, plus [EOS] and [PAD]). Batch size and learning rate are set to 96 and $10^{-3}$ respectively. We trained the model for 1 million batches.

To evaluate our trained model, we randomly sampled 960 AIGs that does not appear in the training set, and compare the result of each method on these AIGs to resyn2 in ABC. The maximum allowed trajectory encoding length of the synthesized circuit is set to 100. The result is shown in Table 2. Except for direct applying Circuit Transformer by which 7 AIGs failed to be synthesized within the length limit, all other methods succeeded in generating strictly equivalent, synthesized AIGs. The result shows that Circuit Transformer performs very closely to resyn2, even slightly better(^2^22We hypothesise that Circuit Transformer may manipulate the circuit in a more globalized manner due to the nature of the Transformer model, while resyn2 consists of local operators.). Also, Monte-carlo Tree Search boosted the performance significantly. Generally, the more steps and rollouts it takes, the better performance it achieves.

## 5. Conclusion and Future Work

In this work, we proposed Circuit Transformer, a comprehensive pipeline including encoding, modeling, decoding and optimization, to design circuits in a fully generative way that is analogous to large language models. We demonstrated its high capability on logic synthesis, which improves over resyn2 in ABC while retaining strict equivalence. This work opens up an ambitious yet challenging direction: is it possible to train an even larger and more generic Circuit Transformer, to master the field of circuit design in a fully generative way, just like what LLMs did to the field of natural language processing? Time will tell.

**Table 2. Experimental result of logic synthesis on 960 random generated 8-input, 2-output AIGs, compared with resyn2 in ABC on #(AND) (the number of AND gates). MCTS-CT = Circuit Transformer with MCTS (S is the number of steps with MCTS enabled, and R is number of MCTS rollouts in each step). ${}^{*}$: 7 AIGs failed to complete construction in 100 steps. ${}^{**}$: The aforementioned 7 AIGs are not counted in this average.**
| Methods | Better<br>than<br>resyn2 | Equal<br>to<br>resyn2 | Worse<br>than<br>resyn2 | Average<br>#(AND) |
| --- | --- | --- | --- | --- |
| Circuit Transformer | 111 | 758 | 91${}^{*}$ | 9.519${}^{**}$ |
| MCTS-CT (S=1, R=5) | 178 | 740 | 42 | 9.352 |
| MCTS-CT (S=1, R=10) | 207 | 722 | 31 | 9.265 |
| MCTS-CT (S=1, R=20) | 221 | 719 | 20 | 9.216 |
| MCTS-CT (S=3, R=10) | 226 | 716 | 18 | 9.196 |
| MCTS-CT (S=3, R=20) | 238 | 713 | 9 | 9.161 |
| MCTS-CT (S=5, R=10) | 235 | 713 | 12 | 9.173 |
| MCTS-CT (S=5, R=20) | 243 | 710 | 7 | 9.145 |
| MCTS-CT (S=10, R=10) | 249 | 703 | 8 | 9.148 |
| MCTS-CT (S=10, R=20) | 251 | 703 | 6 | 9.127 |
| resyn2 | 0 | 960 | 0 | 9.578 |

## Peer Reviews

confidence: 4
contribution: 3
initial_rating: 8
presentation: 2
questions: Please address the weaknesses highlighted.
soundness: 2
strengths: a.	A decoding mechanism that builds circuits step-by-step using tokens with "cutoff properties" to block invalid tokens. 
b.	A "Circuit Transformer" model incorporates this mechanism as a masking layer. 
c.	Formulation of equivalence-preserving circuit optimization as a Markov decision process
summary: Summary:
This paper introduces an approach called "Circuit Transformer" for generating logically equivalent circuits while preserving strict equivalence constraints. Existing neural approaches often make occasional errors, violating the equivalence.
weaknesses: 1.  It is not clear why we need circuit transformer. What does this approach buy compared to existing commercial tools for performing logic synthesis from truth tables? There are methods like the Quine-McCluskey method and its many optimized variants built into commercial logic synthesis tools that can handle Boolean functions of a much larger scale than what this paper proposes. Without a comparative analysis with logic synthesis, this paper's motivation is unclear.
2.	Scalability: While the paper demonstrates effectiveness on 8-input, 2-output circuits, it's unclear how well the approach scales to much larger circuits with hundreds or thousands of inputs/outputs. In any modern digital design, there are likely to be billions of logic gates. What is the point of illustrating on an 8-input 2-output circuit?
3.	Computational: The paper does not provide a detailed analysis of the computational complexity of the proposed approach, especially for larger circuits. This information would be valuable for assessing practical applicability.

---

confidence: 3
contribution: 3
initial_rating: 6
presentation: 3
questions: Please address the weakness raised in **Weaknesses**.
soundness: 3
strengths: - A novel transformer-based method to generate a circuit while preserving the semantics of the original Boolean function.
- Experiments show good performance compared with other methods.
summary: This paper presents a generative model to produce circuits while ensuring logical equivalence with the given Boolean function. The key innovation is the "Circuit Transformer", which utilizes a novel decoding mechanism based on cutoff properties that enable token generation in a way that prevents logical errors. This ensures each generated circuit is logically equivalent to its Boolean function. The Circuit Transformer was tested against existing tasks and achieved good performance in terms of both success rate and circuit size.
weaknesses: - The motivation and intuition behind the proposed method are not immediately clear. Including a concrete illustrative example or practical application would significantly aid in understanding the approach.
- The authors provide an example illustrating how a feasible circuit can be constructed using the proposed method, but the process for selecting each token $s_i$ is not explicitly explained in the example. This leaves ambiguity about whether the selection is deterministic or nondeterministic, as I could not locate specific instructions for this process in the paper. More details would be beneficial to help understand the cutoff-property-based method.
- The set $S_i$ is central to ensure the equivalence between Boolean functions and generated circuits, as it necessitates checking that $F(\cdot)$ holds (essentially a semi-equivalence SAT check) after each token selection (line 3 in Alg.1). Given the top-down mechanism, I guess it will become increasingly non-trivial? It is also unclear how this "semi-equivalence checking" is guaranteed within the Transformer model, particularly in terms of maintaining the inference efficiency. Additionally, Table 2 does not include training and inference time, which would provide valuable insight into efficiency.
- Given that the benchmark circuits involve 8-input and 2-output nodes, it seems feasible to represent such boolean functions using a more compact form, such as Binary Decision Diagram (BDD). Existing methods for converting BDDs into circuits while preserving Boolean function semantics could serve as a viable alternative approach. Why were these methods not considered in your comparative experiments?

---

confidence: 4
contribution: 3
initial_rating: 6
presentation: 2
questions: See above.
soundness: 3
strengths: Representing circuits sequentially with cutoff properties is novel and integrates well with sequential generative methods such as Transformers. Formally guaranteeing the correctness of a generative solution is immensely important for circuit design. The authors show that an inherently sound generative process is beneficial compared to validating solutions past generation. 

Integrating symbolic methods into the generative process not only gives formal guarantees on the result but also improves performance, which is an exciting finding and a strength of the paper.

The authors evaluate in-distribution on random circuits and out-of-distribution on circuits extracted from IWLS 2023 benchmarks, showing that their approach is robust.
summary: The paper introduces a generative neural model (based on Transformers), which generates Boolean circuits equivalent to the model’s input. The primary contribution is a novel circuit representation coupled with a decoding mechanism that guarantees logical equivalence.

The sequential representation of circuits is based on a three-valued logic (true, false, unknown) and follows specific characteristics (Inheritability, Incrementality, Backtrack Elimination, Completeness). These characteristics ensure that 1) the model can build circuits incrementally while logical equivalence (under the tree-valued logic) is preserved in each step, and 2) no backtracking is necessary, which is on par with the generative properties of the Transformer. 

A standard Transformer model is trained in a supervised manner to convert randomly constructed circuits to smaller but equivalent circuits (ground truth created by an existing tool). During inference, tokens that would invalidate the circuits (i.e., invalidate equivalence under three-valued logic) are masked and, hence, cannot be predicted. Consequently, every step of the generation produces a circuit equivalent to the input circuit under the three-valued logic, and every generated circuit that does not contain wild-card nodes (“unknown”) is equivalent to the input under boolean logic. 

In addition to greedy decoding, the authors introduce a Monte-Carlo Tree Search (MCTS) to prefer circuits with fewer gates. The MCTS utilizes the next token probabilities of the Transformer and a reward function based on the number of gates in the circuit's DAG representation. 

Experimentally, the authors’ approach outperforms Transformer models on other sequential and non-sequential representations of circuits. Using MCTS during inference also produces smaller circuits than the symbolical tool Resyn2 used for training data.
weaknesses: ## Related Work

I believe the related work (line 155ff, Schmitt et al. d’Ascoli et al.) is relevant because of the similarity in the domains and the usage of Transformers. While I agree that feasibility guarantees are important for tasks requiring correctness, it may be challenging to attribute the failure cases in related works solely to their absence, given the differences in task complexities. Both related works target very different tasks than this work. Because of the incomparability of the tasks and their complexity, it is unclear whether the failure cases are attributed to missing feasibility guarantees (as claimed by the authors) or the different tasks and complexities.

__Q1:__ Since the authors claim that the related work would benefit from feasibility guarantees, it would be interesting to see whether they think their approach also applies to the work of Schmitt et al. and d’Ascoli et al.

## Markov Decision Process and Monte Carlo Tree Search

The explanation of the generation using a Markov Decision Process (MDP) and Monte Carlo Tree Search (MCTS) should be expanded for clarity. Crucial details on how the trained Transformer model interacts with the Monte Carlo Tree Search are left in the Appendix (Algorithm 3). I recommend including MCTS in Section 3.5 and explaining how the Reward, the MCTS, and the Transformer model interact. 

Additionally, algorithm 3 in the appendix could be more precise. E.g., When creating child nodes, the authors refer to $P(s_t|s_1, …, s_{t-1})$; however, $s_1$ to $s_{t-1}$ should be indexed by the MCTS nodes (line 878). Otherwise, P would be constant. Furthermore, the authors should clarify how “visited” and “total value” are updated (line 881). $s_a$ (line 870) has the same notation as a token, although it is a rational number. 

## Experiments

It is noteworthy that an out-of-distribution real-world dataset has been evaluated. The experiments with different representations (Boolean Chain, AIGER, w/o TPE) show rigor in the evaluations. Providing details on the model’s runtime and scalability would add depth to the empirical results, particularly in comparison to Resyn2. These additions would provide a more comprehensive view of the method's practical implications, although they may not impact the current findings directly.

__Q2:__ The authors only report on average circuit sizes, but it would also be interesting to report the standard deviation. What percentage of circuits is smaller than the ground truth reference?

__Q3:__ How long does inference of the model take? If I understood correctly, the MCTS makes at least K independent calls to the model. Furthermore, how computationally expensive is the token masking in each step? Am I right that it is exponential in the number of inputs, as mentioned in Appendix 2? Generally, some time measurements of the approach would be interesting, especially in comparison with Resyn2. 

__Q4:__ The approach can handle circuits with at most eight inputs and two outputs. Can the authors argue whether this is representative of the problem area? How many inputs/outputs does the IWLS benchmark (before extracting) have? __Q5__: Would the approach scale to larger circuits? 

The following two questions did not affect my review but would be an interesting addition to the experiment section: 
 
__Q6:__ It would be interesting to know how well the Circuit Transformer performs without next-token masking. This would singularize whether performance improvement is mainly based on the representation, the symbolic next-token masking, or the MCTS. 

__Q7:__ The authors compare with other representations and apply beam search in those experiments. The authors acknowledge that this leads to a performance boost. Why is beam search not used in combination with the Circuit Transformer model?

## Presentation: 

Although the paper is well-structured overall, several presentation adjustments could enhance readability, particularly in the methods section. Introducing symbols closer to their relevant subsections, providing an introductory paragraph for Section 3, and clarifying Figure 3 would help guide the reader. Such refinements would further support the clarity of the contributions. However, most of these issues are easy to fix and did not impact my assessment of the technical contribution and its soundness. 
 - Most symbols are defined in the paper's first paragraph. Personally, I would use this space to motivate the paper rather than introduce formal definitions. I recommend moving symbol definitions closer to where they are used in the methods section so the reader does not have to search for those definitions. 
 - An introduction before the first subsection of the method section would clarify the structure and guide the reader through the different subsections.
 - I’m not sure if the eight-queen-puzzle example as a vessel to explain cutoff properties is the right fit, as the reader expects circuits to be the domain of the paper. If the authors think introducing the eight-queen-puzzle is necessary, I would inform the reader before the subsection with a quick introduction that the puzzle is only an illustration to explain constrained sequence generation and that the sequential representation of circuits will follow in 3.2.
 - Figure 3 needs more explanation for easier understanding. That includes an intuitive explanation of $S_t$ and $s_t$. Furthermore, at this point, it is unclear to the reader why the unknowns are explored in this order, as it will be introduced later in 3.4. A note to this fact would help. 
 - Section 3.3 starts with “in the last section”, but this is not the last section.
 - Important information (such as the loss function) is only mentioned in the caption of Figure 5. I recommend moving this to the main text.

## Summary

Overall, the authors present a novel and promising approach. Integrating feasibility guarantees with Transformer-based generative models represents a valuable contribution to the field. The experiment section is exhaustive regarding experiments on different representations and datasets. Comments/experiments about size and scaling would, however, strengthen the empirical results. Most of the issues in the presentation can be fixed by adding small explanations and some structure to guide the reader in the methods section. Section 3.5 should be updated, as crucial information is hidden in the appendix. The authors should be more accurate in the related work.

Weighing the idea, its relevance, and the contribution to the presentation, I am giving a weak acceptance, with the option to raise my rating if the authors address my questions and remarks and improve the presentation and experiments.

Meta-review: This paper introduces “circuit” transformer which generate logical circuits. Furthermore it can ensure the generated circuits’ equivalence with the given boolean function. The main novelty lies on its proposes decoding mechanism based on a cutoff property that prevents logical error. The technical contribution is solid, which is shared across all reviewers. The integration of symbolic methods into the generation process not only gives formal guarantees but also improve performance. This is a big strength. Theory and experiments math each other and it works. Both in-distribution and out-of-distribution results are good and robust. However, this paper is a dense one, which means its presentation can be further improved. Some of the notations can be more consistent, and introduced easier in the manuscript. And another trick that could make this paper even better is that, readers could be overwhelmed by the technical details and in turn forget the big picture and the motivation of this paper. In some sense, the readers could find it difficult to have a feel of the method. An illustrative example, which makes discussion more concrete, would help a lot.

Decision: Accept (Poster)