Circuit Transformer: A Transformer That Preserves Logical Equivalence
Authors: Xihan Li
Xing Li
Lei Chen
Xing Zhang
Mingxuan Yuan
Jun Wang
Venue: ICLR 2025 Poster (2025)
Keywords: Transformer
Logic
EDA
Circuit
Logic Synthesis
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: An end-to-end Transformer model that efficiently produces logic circuits strictly equivalent to given Boolean functions.

Abstract: Implementing Boolean functions with circuits consisting of logic gates is fundamental in digital computer design. However, the implemented circuit must be exactly equivalent, which hinders generative neural approaches on this task due to their occasionally wrong predictions. In this study, we introduce a generative neural model, the “Circuit Transformer”, which eliminates such wrong predictions and produces logic circuits strictly equivalent to given Boolean functions. The main idea is a carefully designed decoding mechanism that builds a circuit step-by-step by generating tokens, which has beneficial “cutoff properties” that block a candidate token once it invalidate equivalence. In such a way, the proposed model works similar to typical LLMs while logical equivalence is strictly preserved. A Markov decision process formulation is also proposed for optimizing certain objectives of circuits. Experimentally, we trained an 88-million-parameter Circuit Transformer to generate equivalent yet more compact forms of input circuits, outperforming existing neural approaches on both synthetic and real world benchmarks, without any violation of equivalence constraints.

Code: https://github.com/snowkylin/circuit-transformer

Published as a conference paper at ICLR 2025
CIRCUIT TRANSFORMER: A TRANSFORMER THAT PRESERVES LOGICAL EQUIVALENCE
Xihan Li', Xing Li Lei Chen', Xing Zhang", Mingxuan Yuan", Jun Wangb UCL Centre for Artificial Intelligence 2 Huawei Noah's Ark Lab (xihan. li, jun. wang] (at.g)c0sccccac.. www.ccc.cc.... [li. xing2, 1c. le chen, zhangxing85, Yuan. Wua.. wuan.Mingguan//hhaaeee....
ABSTRACT
Implementing Boolean functions with circuits consisting of logic gates is funda- mental in digital computer design. However, the implemented circuit must be exactly equivalent, which hinders generative neural approaches on this task due their occasionally wrong predictions. this study, we introduce a generative neural model, the "Circuit Transformer", which eliminates such wrong predic- tions and produces logic circuits strictly equivalent to given Boolean functions. The main idea is a carefully designed decoding mechanism that builds circuit step-by-step by generating tokens, which has beneficial "cutoff properties" that block a candidate token once it invalidate equivalence. In such way, the pro- posed model works similar to typical LLMs while logical equivalence is strictly preserved. A Markov decision process formulation is also proposed for optimizing certain objectives of circuits. Experimentally, we trained an 88-million parameter Circuit Transformer generate equivalent yet more compact forms of input cir- cuits, outperforming existing neural approaches on both synthetic and real world benchmarks, without any violation of equivalence constraints.
-8-million-parameter
Code: hhtt:::: /tttps://github www.///oowkyiin//irr....... transforme
INTRODUCTION
In this work, concerned about the feasibility of generative neural models foundational logic problem - circuit realization. Given a Boolean function, is required to produce a directed acyclic graph (DAG) that connects basic logic gates (AND, OR, NOT, etc.), whose output exactly matches the given function. The DAG is also named a circui of theoretical significance in circuit complexity research (Shannon
Circuit realization is not only
1949 Vollmer 1999 Sipser
2013), but also lies in the core of digital design (Wang et al. 2009).
Recently, generative neural models, represented by large language models (LLMs) that recurrently predict next token, excel in multiple domains from natural conversation to code generation (Pei al., 2024 Liu al., (023a). However, their feasibility for circuit realization is questionable. The main barrier is the requirement of strictly preserving logical equivalence. Given a Boolean function of N inputs, there are 2 possible combinations of input values, and the output of the realized circuit must be equal to the given function on exactly all the 2 values. An example is shown in Figure I For generative neural models, due to their predictive and data-driven nature, they occasionally make wrong predictions and fall short in maintaining complex logical relations, which lead researchers to believe that they are less promising in such equivalence presservin circuit realization (Huang et al. (021). Instead, recent machine learning approaches in this topic mainly focus on strengthening traditional symbolic methods, replacing certain modules to learned one to improve the performance.
In this work, we show that a formal guarantee of logical equivalence achievable for generative neural models with next token prediction. novel mechanism is developed to build circuit incre- mentally by predicting sequence of tokens, which is carefully designed to incorporate beneficial
Moor specifically, combinatorial logic circuit, which is referred to as "circuit" in short in this paper unless otherwise stated.

---

Published as a conference paper at ICLR 2025
33
2g
21
Zg
01
33
41
Jo
0
0
1
0
0
1
0
0
0
1
0
1
1
0
1
1
90 81
0
1
0
0
(a) A Boolcan function (V1, (o) = f13, 22, T1)
(b) An initial valid implementation of the Boolean
in which 20, 22, 23, yo; V1 (0. 1).
function f in Figure 1a
with 7 AND/NAND gates.
D
91
21
do
81
50
(c) A valid implementation of f with 5 ANDINAND (d) An invalid implementation. In this circuit go gates, which is optimal in size.
0 o yo when æ = (1, 1, 1, 1).
An example showing how Boolean function can be implemented by circuits, i.e., cascade connections of logic gates. D and Do are the AND gate and NOT gate respectively, and the NAND gate, an AND gate followed by NOT gate. The circuits shown in FFigure 1b and Figure 1c are both valid implementations of f. while the latter is more compact size. The circuit shown in Figure Id invalid, even if the difference is as small one bit.
Figure I:
"cutoff properties". Given partially-defined circuit and candidate token, it is possible to quickly determine whether adding this candidate token will violate the logical equivalence. In such a way, when predicting logical equivalence to be preserved throughout the generation process. The mechanism is also de- signed eliminate "dead ends", which means adding valid new token is always possible until the circuit is completed. Therefore, our proposed mechanism allows smooth generation of circuits without backtracking, analogous typical LLM-based natural language generation.
token, candidates that invalidate equivalence will be blocked, ensuring the
Based on the above mechanism, we propose the Circuit Transformer, which adopts the classical encoder-decoder Transformer architecture (Vaswani et al., 2017). The Boolean function be im- plemented is embedded by the Transformer encoder, and the aforementioned decoding mechanism adopted by inserting masking layer at the end of the Transformer decoder. When predicting the next token 8,4+1 the masking layer blocks candidates that invalidate equivalence, based on the cur- rent "cutoff" circuit partially defined by .1....,8, 8t. Such a Transformer can be trained in a standard supervised way, while the equivalence of produced circuits is guaranteed during the inference stage.
Moreover, our proposed approach enables optimization methods to search freely within the equiva- lence class optimize certain objective. Specifically, equivalent circuit generation with a certain objective can be formulated as a Markov decision process, and an example is provided to minimize circuit size by designating proper reward function.
To demonstrate the effectiveness our proposed techniques, a Circuit Transformer 88 million parameters is trained in supervised way generate strietly equivalent yet more compact implemen- tations of given circuits. Experimental results show that the trained model capable of generating strictly equivalent implementations for all unseen eircuits in the test set, and the size decrease is close to the traditional method that serves as the supervised signal.
To conclude, we make the following main contributions:
A decoding mechanism that builds a circuit by a sequence of tokens, with beneficial cutoff properties that allows logical equivalence to be preserved throughout the decoding process. A generative neural model named "Circuit Transformer" adopting the proposed decoding mechanism as masking layer, which can be trained normally and preserve equivalence during the inference stage.
formulation of squivalence-preservee cireuit optimization as Markov decision process. Extensive experiments on the circuit size minimization problem demonstrating the equivalence-preserving capability of Circuit Transformer.
2

---

Published as a conference paper at ICLR 2025
2
RELATED WORK
While data-driven Al techniques achieve tremendous success in recent years, they are generally based on probabilistic prediction that allows occasional mistakes, thus less promising to be di- rectly applied to domains requiring exact preciseness, such as theorem proving and circuit design. Therefore, the mainstream paradigm of AI for such domains is to aid traditional methods in solv- ing sub-problem, that are more relaxed with respect to exactness. For circuit design, such relaxed sub-problems include SAT solver acceleration (Selsam Björner, 2019. Wang et al. 2023 Zhang
et al., 2020 Guo et a 2023). circuit representation learning (Zhang et al. [019]] Yang et al. 2022b
Li ct al. 2022, Wang et al. 2022), learning based graph optimization (Neto et al. 2021; Li et al,
2023
operator sequence scheduling (Yu et al., 20018 Hosny et al. 2020)] Grosnit et al. 2022 Zhu
ct al.
2020 Yang et al. 2022a), and placement and routing (Mirhoseini et al. 2021 Cheng et al,
2022
Nonetheless, there are a few research works (Schmitt et al., 2021 2023 d' Ascoli et al., 2023 that attempt to generate circuits or logical expressions directly via next token prediction models. How- ever, feasibility guarantee is not considered in these work, resulting different extent of constraint violation in their reported result. In (Schmitt al. (021), 20% 70% generated circuits violate the input specification in different datasets, while a follow-up work (Schmitt et al., (023) mitigates the invalid percentage to 16% 65% with pre-trained language models. In (d Ascoli et al. 2023), 5% 10% cases failed to be fully recovered when the number of operators are between 25 and 50. Apart from the low-level circuit generation, many researchers focus on transferring the software
code generation capability of LLM to high-level hardware code generation, but these methods still
suffer from functional inequivalence (Liu et al. 2023b Thakur et al. 2024 Pei et al., 2024 Liu
et al. 2024).
There are also research works that guarantee the feasibility of solutions via action masking, espe- cially for problems involving routing such maze game, traveling salesman problem, and vehicle routing problem (Nazari et al. 2018 Kool et al., 2019: Duan et al. 2020). However, these prob- lems usually intuitive to be sequentially modelled, allowing action masks to simply filter invalid actions such as wall-hitting directions and already visited cities. Action masking techniques under complicated constraints have yet be explored.
For sequential representation of gate-level circuits, existing formats include graph-hased ones like AIGER (Biere 2007) and BLIF (Berkeley T992), and code-based ones like Verilog (Thomas & Moorby 2008) and VHDL (Skahill, 1996). However, they can only be validated once the content is given in full, lacking the "cutoff properties" that will be discussed in Section
PROBLEM DESCRIPTION
In this work, focus formally guaranteeing a generative neural model produce valid circuits that strictly match given Boolean function. For an N N-input, M M-output Boolean function
= f(x).
(1)
in which æ = (I (zi,..., TN) E {0, 1JN and y = (yI..... VM) E 10, any valid circuit implementing the function must be strictly within the equivalence class of f. That is, for any N- dimensional input æ E 10, (there are 2 of them), the M -iimensioona output of the circuit, denoted as g(z), must be equal to f(x) in element- wise way. This can be formally described as g E C(),, in which
(2) the equivalence class of f. Any violation of the 2 equivalence constraints will disqualify the circuit as valid implementation of f. An example with 4-inpu, 2-output Boolean function is shown in Figure 1 in which the produced circuits must satisfy 24 = 16 equality constraints.
C(f) = (o g(x) = f(x), Vx E 1)
4 METHODS
In this section, we start from a general introduction of constrained sequence generation, highlighting the importance of "cutoff properties" for efficiency. Then we propose sequential representation of
3

---

Published as a conference paper at ICLR 2025
that circuits in Section 4.2 that has such beneficial properties, allowing efficient generation akin natural language generation while strictly adhering to equivalence constraints. It is followed by a postpro- cessing step regarding graph structures in Section 4.3 Given the circuit representation, Section 4.4 how can be integrated into the encoding and decoding process of Transformer model, forming the Circuit Transformer. Finally, we discuss in Section 4.3 how our proposed approach help model pouivaleence-reserviin circuit optimization as Markov decision process.
show in
4.1 CONSTRAINED SEQUENCE GENERATION WITH CUTOFF PROPERTIES
In this section, we briefly introduce how to generate sequences .1..... Sn E D with constraints, i.c.. certain property F(s1......5. Sx) E {0, 1} strictly holds. We use the eight-queen puzzle as an illustrative example, while circuit-specific sequence generation will be followed in the next section. In this puzzle, we place eight chess queens on an x chess- board. The queen positions can be encoded which the i-th queen in the i-th row, and 8; E D = {a, b, c, d. e, S. h} specifies its column index. In this way, queen positions in Figure 2 can be encoded as "dibhegac"". The property F(s1..... S8)
sequence . 88, in
holds when two queens threaten each other. Out of all 8 possible sequences, there are 92 of them that the above property holds.
Figure 2: A valid solu- tion of the eight-queen puzzle, sequentially en- coded "dbhegacf".
Researchers have already found that "cutoff properties" of the sequential encoding are critical for generating such constrained sequences efficiently (Knuth 2020). They are series of properties Fs1,,..., 8x) for 1 n, which have the following two characteristics
Characteristic 4.1 (Inheritability). Characteristic 4.2 (Incrementality). F(s1,..., 8t) ) is fairly eas to test, if F(s1...., 8t-1) holds.
is true whenever F(11,..., true;
Once constrained sequence generation task has such properties, it can be solved step-by-step by selecting proper 81 so that F(11) holds, proper 82 so that F(11,82) holds, proper 83 so that F(s1, 82, $3) holds, etc, until all $1, $1...., Sn are properly selected. In each step, is selected from set
S = (s E F ( holds)
which can be easy to compute given F(si,..., ((81,)...8..1)) already holds, due to ChCraccteeristic 4.2 Such properties admit the concept of "partial (cutoff) candidate solutions" (s1,...,,8)) < < n toward a full solution, which is often much faster than brute-force enumeration of all complete candidates, since it can eliminate many candidates halfway with single test.
For the aforementioned example of eight- queen puzzle, instead of enumerating all g placements to find the attack-free sequences, much more efficient way is to leverage the cutoff properties of the sequence encod- ing, in which F(si....;:8 8t) "the queens located at (1, $1), si),...................... st, will not attack each other,
Algorithm 1 Constrained Sequence Generation with Cutoff properties
Input: Domain D, property F(s1...., 8n), cutoff prop- erties F(s 8t). 1 <
< n.
Output: A sequence with F(s holds.
2:
while S n do Set S; + D[F((s......
< t 8". This is fairly easy to test if F(s 81-1) holds, since we only need to check whether the queen lo- cated at (t, st) can attack any other queens located at (1, (1,81)..... ,. (L 11,+- For ex- ample, when 81 dl and #2 = b, the cut-
3:
holds}
4:
while truc do
5:
if S. + 0 then Select 8, from S, t
7:
8:
break
off property F(d,b, 6, 53) holds when 83 S3 = {e,g, h). Because cutoff properties reject column and diagonal attacks even on incomplete boards, it examines only 15,720
9:
else
The backtrack process
10:
t 1-t-1
11:
S. + --
12:
end if end while
13:
possible queen placements out of g8 16, 777, 216 find all valid sequences.
14:
end while
15: return St.....
This is directly quoted from (Knuth 2020). "Fairly easy" typically means that the test leverages the fact that F(8 8t-1) holds, and only do incremental work to check whether it still holds after adding st-
4

---

Published as a conference paper at ICLR 2025
A.A.
b
0
(a) NOT operator
(b) AND operator
(c) OR operator
(d) SIMEQ operator
Table 1: The truth tables for NOT, AND, OR and SIMEQ operators in three-valued logic.
The full algorithm is shown in Algorithm|] [ Note that St in Equation 3 may be empty, which means a "dead end" at step / that cannot proceed. In this case, we should return back to step / 1, mark St-1 as dead end, and select another one in St-1 if possible (or repeat the following steps if all of them are dead ends).
4.2 A SEQUENTIAL REPRESENTATION CIRCUITS WITH CUTOFF PROPERTIES
The main idea of this work is to find a sequential representation of circuits ......, with aforementioned cutoff properties ((, f), S / n that keep the represented circuit within the equivalence class of f. In such way, we can leverage next-token prediction models to generate tokens step-by-step and validate the logical equivalence each step, corresponding line 6 in Algorithm!! [] In such way, the final completed circuit can be guaranteed to be equivalent to f.
However, Algorithm [ include a "backtrack process" in line and 11, which may lead to back- and-forth and is not desired for efficient circuit generation. We note that such a process can be eliminated by assuring S, * 0 all the time, leading the following desired characteristic for the sequential representation:
Characteristic 4.3 (Backtrack Elimination). St + is always guaranteed in line 5 of Algorithm
With such characteristic, the autoregressive next-token prediction process of circuits can always proceed forward efficiently, analogous to typical natural language generation.
For tasks requiring exploration of feasible regions for circuits, it is important for representation of circuits to cover the widest possible (ideally all) feasible circuits, minimizing the miss of targets due the restriction of representation. For example, while we can always generate a strictly equivalent circuit for Boolean function f via sum-of-product or product-of-sum forms, such forms are too re- stricted for any feasible region exploration. Therefore, we have the following desired characteristic:
Characteristic 4.4 (Completeness). For any g C(f), there exists sequence $1,..., Sn that uniquely represents g.
Now propose sequential representation of circuits with cutoff properties, that has all the afore- mentioned characteristics.
First, while circuits usually built in bottom-up manner from inputs to outputs, we notice that the equivalence constraints are applied on each output of the circuit. That is, given the index of output and input æ, a constraint fx(x)) g)( is only possible to be validated when the corresponding circuit output has been built. Therefore, we adopt a special top-down order, specifying a cir- cuit from outputs to inputs, to allow constraint validation throughout the intermediate construction process. It improves sampling efficiency and equivalence preservation of circuit generation.
Then, to allow for indeterminacy in circuit representation, we include the three-valued logic into the circuit evaluation process. That is, besides (0, 1} which indicate false and true, there is another truth value "U" which means unknown. The truth tables of such logic for NOT, AND and OR operators are shown in Table Additionally, we define binary operator "SIMEQ" (=, is similar or equal to), which equivalent to the equal operator (=) for (0, 1). while accommodating by U ~ 0 and U = 1. During the generation process, we relax the equivalence class of f from Eqqation 2 to
C²(f) = {g g(x)) ~ f(x) Va E (0,
(4)
so that the occurrence of U in the output will not violate the constraint. For simplicity, here we sume M = and leave multi-output cases to be discussed later. The generated circuit g is initialized to be single constant node U. which
call "wildeard node" it can potentially represent any feasible circuits. So initially, (xx) = U no matter what the input æ is. This is within the relaxed feasible region in Inqquattinn 4 but does not provide information about the circuit structure.
5

---

Published as a conference paper at ICLR 2025
D
(a) The initial circuit.
(b) Step I.
(c) Step 2. 82 D.
(d) Step 3. So (20.
(e) Step 4. Se [A. 44
[).
S1 (20. A. R).
40
42 22
8g
(f) Step 5. 85 (20, A)
Step g
(h) Step A,
Step Ss ( X).
The generated cir- cuit.
86 D.
S7 [T0.
Figure 3: An example showing how strictly feasible circuit can be built with our proposed se- quential representation with cutoff properties. f(22, 21. 2o) is Boolean function with 700,0, I(1,1,1) and [ x0) = otherwise. wildcard node. The next wildcard node to be replaced is marked in red. S, = {s E D F( 8; f) holds]. The selection of 8 from St based on masked probability dis- tribution estimated via a trained Circuit Transformer, which will be elaborated in [Section 4.4
A.. {ro, क6. Iı "h, 2T, I2, A2,A, J. U denotes the
Given the initial circuit, the sequential generation process acts refining the circuit g by recursively replacing a wildcard node to a specific one & E D, which can be either a new logic gate or new primary input. For new logic gate, all its inputs will be initialized to wildcard nodes that need further refinement, With the proposed top-down approach, the values of g(x) for all x E {0, 1) )M in Equation 4 can always be evaluated throughout the construction process, following the truth tables Table 1] Note that the introduction of three-valued logic also enables short-circuit evaluation with unknown values. For an AND gate c(z) a(x) A b(æz), if one of the inputs (a(x) or b(x)) is evaluated to be 0 given specific æ, then e(x) = 0 no matter what the other input is evaluated, even if it is U. The same logic applies for the OR gate when one of the inputs evaluated be 1.
Then, the cutoff properties F(sI,..., S;; f) holds if and only if the circuit partially defined by $1...., St, denoted as g( is in the relaxed equivalence class of in|Equation 4 More specifically, for all x E {0, 1 the output of the constructed circuit g(t) is similar or equal to f(x) That is,
11 (o otherwise
if (x) = f(x), Vas 10,
F($1....,$$: =
(5)
For the ending criteria, as a wildcard node can potentially be any circuit, only when all the wildcard nodes are recursively replaced by specific ones, can the sequence uniquely represent circuit, which marks the end of the generation process. For the order of replacement when multiple wildcard nodes exist, we follow fixed order that prioritizes those with the largest distance from the output and the left child of a gate over the right one. For multi-output cases, we generate the circuit for each output separately, and combine them together via node merging which will be discussed in the next section.
For the selection of logic gates (vocabulary list) in the sequential representation, standard setting the combination of AND and NOT gates, which can express all possible truth tables of Boolean functions (termed "functional completeness",, and is also commonly adopted in standard circuit formats such as AIGER (Biere) 2007). Therefore, we adopted this setting. Additional types of gates can be further included to adapt to different circuit settings, which is left as future work. An alteration is that we merged the NOT gate with the AND gate and primary inputs. Instead of assigning the NOT gate individual token, each primary inputs and the AND gate has two versions: the original ones (II,... N,N A) and the inverse ones (TI,..., 7), so the vocabulary list contains 2N + 2 tokens in tota That is.
D {21 TI. IN, A,
This allows to significantly shorten the sequence with moderate increase of vocabulary size.
An example of our proposed representation and cutoff properties are shown in Figure 3. We leave the proof of Characteristic 4.1 4.2 4.3 and 4.4 in /Section A.2 Given Equation 3 Equation 5 and Characteristic 4.2 we can compute St in a time complexity of O(N 2 d). d is the depth of the wildcard node to replace at step f. The detail is leaved in Section A.3
TTiis does not include special tokens such [FOS] and [PAD] in Transformer models.

---

the sequential Published as a conference paper at ICLR 2025
4.3 FROM TREES TO DIRECTED ACYCLIC GRAPHS
In the previous section, we proposed a sequen- tial representation of circuits based on recursive replacement of wildcard nodes in a top-down manner. Such an approach implicitly assumes that a logic gate would always have single outgoing edge, restricting the generated circuits to be highly hierarchical with tree structures. However, multi-fanou gates do commonly ex- ist in real-world logic circuits, which shape cir- cuits as directed acyclic graphs (DAGs).
affid
BAC
Trads)
Figure 4: Transition between a DAG and one or more trees.
In this section, we show how extend our method to generate DAG circuits. We notice that DAG can be "unfolded" to one or more trees once we duplicate every node with outdegree larger than one, so that every node has at most one outgoing edge. For example, the orange node in the left DAG of Figure 4 is duplicated into two individual nodes, where its two outgoing edges are as- signed respectively. Reversely, one more trees can also be transformed to DAG by merging nodes with structural equivalence. For circuits, such a bidirectional transition will not change the Boolean function it represents. Therefore, we generate a DAG circuit by firstly generating its un- folded tree representation, and then merging equivalent nodes in the generated tree representation. In logic circuit design, different nodes can be not only structurally equivalent but also functionally equivalent (Mishchenko et al.) 2005), which means that their outputs represent the same Boolean functionality. Functionally equivalent nodes can thus be merged as a single node even if they have different underlying structures. Our approach mainly leverages the functional equivalence.
4.4 NEURAL ENCODING OF CIRCUITS AND CIRCUIT TRANSFORMER
While we can deserialize our proposed sequential representation to a DAG circuit via node merging, can also serialize a given DAG circuit our proposed sequential representation in similar manner, via a depth-first traversal with node duplication. Given a DAG circuit, we start a traversal from each of its primary outputs, and visit each connected gate in a depth-first and recursive manner. Backtracking occurs when a primary input is reached. 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, corresponding to the node duplication in the previous section. When the process is finished, the traversal trajectory 81,...,8, 8, representation of the unfolded tree version of the original DAG circuit. Note that such an unfolding process may lead to long sequences, especially for nodes with large number of outgoing edges. A more compact representation is left as future work.
For Transformer models to process the sequential representation, it is important to provide an effi- cient positional encoding for each node to indicate its position in the circuit. In this work, we utilize the path from the primary output to a given node to indicate the node's s position. To achieve this, we follow (Shiv & Quirk 2019) that encodes the path as stack of one-hor hot encodings ("10" for the first input and "01" for the second input). More details are left in the appendix.
With all the circuit encoding and generation techniques introduced above, propose the Circuit Transformer, an end-to-end Transformer model that generates a functionally equivalent circuit of a Boolean function. The Transformer adopts the classical encoder-decoder Transformer architecture (Vaswani et al. 2017). The Boolean function to be implemented is specified as a circuit, and encoded by the Transformer encoder with the aforementioned encoding approach. The Transformer decoder adopted the mechanism in [Section 4.2 by inserting masking layer before the final softmax layer, which reflects S,. When predicting the next token 8141, the masking layer blocks candidates that invalidate equivalence, based on the current "cutoff" circuit partially defined by $1...., 8t. The Transformer is trained in standard supervised way, which minimize the cross entropy between the predicted distribution and the ground truth. Moreover, node merging proposed in Secciinn 4.3 is applied to the decoding process on-the-fly to transform the unfolded tree representation to a DAG circuit, whose details can be found in Algorithm 3 in the appendix. The training and inference stage is shown in FFiurr 5! We denote a trained Circuit Transformer as
Per(s| 81, 81,-..,8855
7

---

Published as a conference paper at ICLR 2025
Cround
Predicted Novt Token Fe Distibbution
Maxcad Protuability
Mosking Layer
Apartion Layer
Attendion Layer
Anention
Atwenton
Abtenton Laver
Atterngo Lower
Erazala
Deooder
Degoder
Sequental
Rusroserttion
based
Poutonsl Encodinge
DAG Iveresrtition
(a) Training stage
(b) Inference stage
Figure 5: The training and the inference stage of the Circuit Transformer. In the inference stage, the positional encoding és at step / is computed on-the-fly based on the position of the currett token 8r the partially defined circuit. The mask S for predicting the next token 8t+1 computed based on Equation 3 gigve the previous tokens $1,..... and the cutoff property F(s1,..., St; f). "S" and "E" denote the [START] and [END] tokens in Transformer model.
in which Eeesy1 Per(s $1,..., 8t; f) 1 and Per(s] ,1,..., 815 0, 0, DVS The input cireuit specifying f is omitted for simplicity.
4.5 EQUIVALENCE-
CRUUVALLENC--PRESERVVVN PRESERVING CIRCUIT OPTIMIZATION AS A MARKOV DECISION PROCESS
important application equivalent circuit generation is to optimize circuits with respect to certain objectives. For example, one important problem is to find compact implementation of Boolean function f with minimal number of logic gates (the circuit size minimization problem). That is
min g s.t. E C(f),
(7)
where lgl is the number of logic gates (NOT gates are not counted to align with the mainstream research setting) g. Under our proposed sequential representation, it can achieved by attaching an immediate reward function R(s1..... 8) to the generation of token at step I, that the sum of the reward function throughout the generation reflects the objective. In this way, the generation process can be regarded as a deterministic Markov decision process, in which the state at step t is the generated tokens (s1...., 8t), the set of actions available from the state Sy in [Equattin 3) the immediate reward is R(s),
St, s), and the next state is (S1,..., 8t, s) with probability 1. The process terminates once (.I,..., 8t) represents a unique circuit with all wildcard nodes replaced.
Such formulation has key advantages. First, the feasibility of the generated circuit is guaran- teed once the process terminates. No effort is required to penalize infeasible cases via crafting the reward function. Second, the size of the available action is at most 2N 22 in which N, the num- ber of inputs, is usually moderately small in practice. Other circuit representations typically assign unique ID to each logic gate describe their adjacency, requiring the size of available actions to be proportional to the number of gates, which is usually significantly larger than N.
For the circuit size minimization problem Equation 7 the immediate reward function can be defined as
[1,
== ors=
R(s
(8)
0. otherwise
in which A reflects the refinement due equivalent node merging. Given depth-fire first replace- ment order of wildcard nodes in [Section 4.2, the node merging process in (Section 4.3 can done simultaneously with the generation process, whose details are left in the appendix.
8

---

Published as a conference paper at ICLR 2025
Given the reward function, we can adopt Monte- tree search (MCTS) to maximize the cumu- lative reward Σ; R( R($1....,55: while strictly preserving the equivalence. Each search node will be "simulated" once to obtain value e, which is the estimated cumulative reward when choosing the path from the root node to this node. Each node also stores four values: the average value ((s), the number of visits (s)), the immediate reward R(s) and the prior probability P(s). When selecting a child a for the node s, MCTS make a balance between exploitation and exploration by assigning each child a PUCT score (Silver et al. 2017) as follows
PUCT(a) = Q(a) + cP(a) VN(s) 1+ N(a)
in which is hyperparameter (set to 1 in our case). P(a) is prior probability of selecting a, allowing nodes with larger P(a) obtain higher score. We adopt Circuit Transformer to estimate P(a) as well conducting simulation to get the value The detailed procedure is shown in Algorithm iin the appendix.
5 EXPERIMENTS
In this section, we supervisedly train a Circuit Transformer to solve the circuit size minimization problem in Equation generating equivalent yet more compact forms of input circuits, and conduct extensive experiments on both synthetic and real datasets to evaluate its feasibility and optimality.
We conduct the experiments on 8-input, 2-output circuits, which can specify (2²*)²= = 1.34 - 10154
different Boolean functions. Optimizing circuit while exactly matching one of the functions is challenging. Such size is out of the capacity of current exact solvers and significantly larger than the typical sub-circuit size (4-6 inputs and one output) for traditional divide-and -nd-quqe methods. Effective end-to-end optimization on such a circuit size leads to enhancement of global optimality for large circuit optimization (Li & Dubrova, 2011 Zhu et al. 2023).
The detailed parameter setting of the Circuit Transformer model are as follows. The embedding width and the size of feedforward layer are set to 512 and 2048 following (Vaswani et al.) 2017). while the number of attention layers is set to 12, leading to 88.2 million total parameters, a moderate size that allows efficient training and evaluation on a single, customer-gras gradd GPU. The vocabulary size is 20 (8 inputs and the AND gate, with their inverse, plus [EOS] and [PAD]). Batch size is set to be 128. The maximum length of the input and output sequence is set to be 200. To evaluate the effectiveness of tree positional encoding (TPE) in Section 4.4| we trained Circuit Transformers with and without TPE. The maximal depth of tree positional embeddings is set to be 32. The implemen- tation is based YYu al. 2020). During inference, the prediction of tokens from distributions is deterministic (the token with the largest probability is selected) for reproducibility.
We also trained two baseline Transformer models with exactly the same experimental settings, ex- cept employing different sequential representation of circuits as follows:
Boolean Chain (Knuth 2015): a representation that is extensively applied in SAT-based op- timization techniques. A chain is initialized by all the primary inputs of the circuit, and each gate is represented by two prior indices in the chain, indicating the source of its two inputs. AIGER (Biere) (007): popular representation of logic circuits with AND and NOT gates. We follow the tokenization setting in (Schmitt et al. 2021), representing an AND gate by three tokens followed by a special new line token.
To train and evaluate the Circuit Transformer model, we build a large dataset containing 15 million randomly generated 8-input, 2-output circuits. The supervised signals (i.e., the equivalent circuits that are optimized in size) are generated by the Resyn2 command in ABC (Brayton & Mishchenko 2010), representative optimization flow for circuit size minimization. The detail of random circuit generation is left in the appendix. 89% of the data is for training, 1% is for validation and 10% is reserved for testing. All the Transformer models are trained on the training set sufficiently for epochs on a single NVIDIA GeForce RTX 4090 graphic card for 75 hours.
We employ both synthetic dataset and real EDA benchmarks to evaluate the performance:
Random circuits: 10,240 circuits are randomly sampled from the test set of the aforemen- tioned randomly generated dataset. The average size is 25.83 + 5.38.

---

Published as a conference paper at ICLR 2025
Random circuits
FFWS
Methods
Unsuccessful cases
Avg. size
Unsuccesstul cases
Avg. size
Boolean Chain
5.07% (5.07%)
15.25
11.36% (11.26%)
17.24
Boolean Chain (beam size 16)
2.16% (2.16%)
14.89
6.34% (6.29%)
17.15
Boolean Chain (beam size 128)
1.91% (1.91%)
14.87
5.97% (5.94%)
17.15
AIGER
4.32% (4.32%)
15.14
8.35% (7.77%)
17.19
AIGER (beam size 16)
1.85% (1.85%)
14.87
4.62% (4.37%)
17.12
AIGER (beam size 128)
1.71% (1.71%)
14.86
4.24% (3.99%)
17.12
Circuit Transformer w/o TPE
2.14% (0%)
15.02
6.63% (0%)
17.33
Circuit Transformer
1.14% (0%)
14.79
4.76% (0%)
17.17
Circuit Transformer (K = 10)
0.20% (0%)
14.02
2.83% (0%)
16.92
Circuit Transformer (K 100)
0.17% (0%)
13.73
2.63% (0%)
16.73
Resyn2 (ground truth for training)
14.56
16.82
Table 2: Results on 10,240 randomly generated circuits, and 10,240 fanout-free windows randomly sampled from the IWLS 2023 benchmark. For unsuccessful cases, the percentage the bracket corresponds to failures due to equivalence constraint violation. All results of Circuit Transformers show zero violation of equivalence constraints. denotes the total number of playouts in Monte- Carlo tree search. All the models are supervisedly trained on the Resyn2 optimized circuits.
IWLS FFWs: we transform the IWLS 2023 benchmark (Mishchenko 2023 into circuits represented by AND and NOT gates by the script suggested in (Mishchenko & Chatterjee 2022), and extract 1.5 million 8-input, 2-output fanout-free windows (FFWs), a kind of sub- structure of large circuits (Zhu et al., 2023). Then we randomly sample 10,240 circuits from the extracted FFWs. The average size is 18.01 + 6.47.
To enhance the performance of the Transformer models in comparison, two heuristics search tech- niques are applied. Monte-Carlo tree search in Algorithm 4 is applied for Circuit Transformer to evaluate our proposed MDP formulation Section 4.5| For Transformer models trained on Boolean chain and AIGER, applying MCTS is significantly more inefficient due to the large set of available actions discussed in /Section 4.5) so we adopt Beam search as an alternative, which finds the most probable sequence by maintaining a fixed size (beam size) of candidates.
The results are presented in Table with more detailed version in [Section A.9 On both syn- thetic and real datasets, the Circuit Transformer surpasses two other Transformer models in terms of feasibility (measured by percentage of unsuccessful cases) and optimality (measured by the average circuit size). The two baseline models generate unsuccessful circuits for various reasons, including equivalence constraint violations, cycles in circuits, or incomplete specifications, with the most common issue being that the generated circuit is complete and valid but not strietly equiva- lent to the original. In contrast, the Circuit Transformer's exact precision is empirically shown by zero violation of complex equivalence constraints. The only reason for unsuccessful cases that wildcard nodes are not fully replaced within the given maximum sequence length of 200. Case studies can be found in the appendix. Regarding heuristic search enhancement, while beam search significantly improved feasibility, consistent with findings in (Schmitt et al., 2021). the issue of non- equivalence remained prevalent. Conversely, Monte-Carlo tree search in the Circuit Transformer not only substantially reduced unsuccessful cases but also significantly improved the average circuit size, sometimes producing circuits more compact than the ground truth with moderate number of playouts.
6 CONCLUSION
In this work, we make an important advancement towards achieving precise generative Al for logic tasks, demonstrating that complex hard-constraint satisfaction is attainable for next-token prediction models when a proper formulation of the constrained problem established. Inspired by the cutoff properties, we introduce novel approach to the fundamental problem of equivalent circuit genera- tion, enabling next-token prediction models to generate new logic circuits while strictly adhering to complex equivalence constraints. Future works includes extending such methodology to other fun- damental constrained problems, integrating current models into industrial large circuit optimizers, and exploiting more compact representation of circuits such BDDs.
10

---

Published as a conference paper at ICLR 2025
REFERENCES
UoC Berkeley. Berkeley logic interchange format (blif). Oct Tools Distribution, 2:197-247, 1992.
Armin Biere, The AIGER And-Inverter Graph (AIG) format version 20071012. Technical Report 07/1, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2007.
Robert Brayton and Alan Mishchenko. Abc: An academic industrial-strength verification tool. In Computer Aided Verification, pp. 24-40, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. ISBN 978-3-642-14299-6.
D. Chai and A. Kuchlmann. Building a Better Boolean Matcher and Symmetry Detector. In Pro- ceedings of the Design Automation & Test in Europe Conference, volume 1, pp. 1-6, March 2006.
doi: 10. 10.110900 A..110//ATEE.00..44550 243959. ISSN: 1558-1100 1101.
Ruoyu Cheng, Xianglong Lyu, Yang Li, Junjie Ye, Jianye Hao, and Junchi Yan. The policy-gradient placement and generative routing neural networks for chip design. Advances in Neural Informa- fion Processing Systems, 01226300-23662 2022.
Stéphane d' A'Acolli, Samy Bengio, Josh Susskind, and Emmanuel Abbé. Boolformer: Symbolic Regression Logic Functions with Transformers, September 2023. URL, https://arxiv..
org/abs/ 2309. 12207v1
Lu Duan, Yang Zhan, Haoyuan Hu, Yu Gong, Jiangwen Wei, Xiaodong Zhang, and Yinghui Xu. Efficiently solving the practical vehicle routing problem: novel joint learning approach. In Proceedings of the 26th ACM SIGKDD International Conference Knowledge Discovery & Data Mining. KDD '20. pp. 3054-3063, New York, NY. USA, 2020. Association for Computing Machinery. ISBN 9781 4503799999
doi: 10. 10.1145/39948663403335
URL https://doi.
Antoine Grosmit, Cedric Malherbe, Rasul Tutunov, Xingchen Wan, Jun Wang, and Haitham Bou Ammar. Boils: Bayesian optimisation for logic synthesis. In 2022 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1193-1196, 2022.
Wenxuan Guo, Hui-Ling Zhen, Xijun Li, Wanqian Luo, Mingxuan Yuan, Yaohui Jin, and Junchi Yan. Machine Learning Methods in Solving the Boolean Satisfiability Problem. Ma- chine Intelligence Research, 20(5):640-655, October 2023. ISSN 2731-5398. doi: 10.
1007///1663--22--13962. URL hatts:://inni: springer. com/ wttparrreceee...10000..0 611633-022-1396
Abdelrahman Hosny, Soheil Hashemi, Mohamed Shalan, and Sherief Reda. Drills: Deep rein- forcement learning for logic synthesis. In 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 581-586, 2020.
Guyue Huang, Jingbo Hu, Yifan He, Jialong Liu, Mingyuan Ma, Zhaoyang Shen, Juejian Wu, Yuan- fan Xu, Hengrui Zhang, Kai Zhong, Xuefei Ning, Yuzhe Ma, Haoyu Yang, Bei Yu, Huazhong Yang. and Yu Wang. Machine learning for electronic design automation: A survey. ACM Truns. Des. Autom. Electron. Syst., 26(5), jun 2021. ISSN 1084-4309.
Donald Knuth. The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability. Addison- Wesley Professional, 2015.
Donald E Knuth. The Art of Computer Programming, Volume 4, Fascicle 5: Mathematical Pre- liminaries Redux; Introduction to Backtracking; Dancing Links. Addison- Wesley Professional, 2020.
Wouter Kool, Herke van Hoof, and Max Welling. Attention, learn to solve routing problems! In International Conference on Learning Representations, 2019. URL httt:t://opeeeevieeee
Rm
Min Li, Sadaf Khan, Zhengyuan Shi, Naixing Wang, Huang Yu, and Qiang Xu. Deepgate: Learning neural representations of logic gates. In Proceedings of the 59th ACM/IEEE Design Automation Conference, pp. 667-672, 2022.
11

---

Published as a conference paper at ICLR 2025
Nan Li and Elena Dubrova. AIG Rewriting Using 5-Input Cuts. arXiv:1108.3675 [cs], August 2011. URLptttp:/aaxxit orq/ aba/ /1108.110.... 3675
arXiv: 1108.3675.
Xing Li, Lei Chen, Jiantang Zhang, Shuang Wen, Weihua Sheng, Yu Huang, and Mingxuan Yuan. Efficient logic synthesis with dynamic scoring and pruning. In 2023 IEEE/ACM Interna- tional Conference on Computer Aided Design (ICCAD), pp. 1-9. IEEE, 2023.
Effisyn:
Mingjie Liu, Teo Ene, Robert Kirby, Chris Cheng, Nathaniel Pinckney, Rongjian Liang, Jonah Alben, Himyanshu Anand, Sanmitra Banerjee, Ismet Bayraktaroglu, Bonita Bhaskaran, Bryan Catanzaro, Arjun Chaudhuri, Sharon Clay, Bill Dally, Laura Dang, Parikshit Deshpande, Sid- dhanth Dhodhi, Sameer Halepete, Eric Hill, Jiashang Hu, Sumit Jain, Brucek Khailany, Kishor Kunal, Xiaowei Li, Hao Liu, Stuart Oberman, Suject Omar, Sreedhar Pratty, Ambar Sarkar, Zhengjiang Shao, Hanfei Sun, Pratik P Suthar, Varun Tej, Kaizhe Xu, and Haoxing Ren. Chip- nemo: nomain-adapteds Ilms for chip design, 2023a.
Mingjee Liu, Nathaniel Pinckney, Brucek Khailany, and Haoxing Ren. Verilogeval: Evaluating large language models for verilog code generation. In 2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD), pp. 1-8. IEEE, 2023b.
Shang Liu, Wenji Fang. Yao Lu, Qijun Zhang, Hongce Zhang, and Zhiyao Xie. Rtlcoder: Outper- forming gpt-3.5 in design rtl generation with our open-source dataset and lightweight solution, 2024. URL hattpe///axxxv..org////////122
arxiv.
Azalia Mirhoseini, Anna Goldie, Mustafa Yazgan, Joe Wenjie Jiang, Ebrahim Songhori, Shen Wang, Young-Joon Lee, Eric Johnson, Omkar Pathak, Azade Nazi, et al. A graph placement methodol- ogy for fast chip design. Nature, 594(786))20772222, 2021.
Alan Mishchenko.
alamiinkofills222345conreee
Problems and Results of IWLS httpg//ttht....oaaaaaaee// www../owwaaaaaaaa.aam
2023 Programming Contest, 2023.
URL
i ww1s2023- 1s contest
Alan Mishchenko and Satrajit Chatterjee. IWLS 2022 Programming Contest, 2022. Progg22oograaala1eoo
URL httpp::/
Contest.pd:
Alan Mishchenko, Satrajit Chatterjee, Roland Jiang, and Robert K. Brayton. FRAIGs: unifying representation for logic synthesis and verification. Technical report, ERL Technical Report, 2005.
MohammadReza Nazari, Afshin Oroojlooy, Lawrence Snyder, and Martin Takac. Re- inforcement Learning for Solving the Vehicle Routing Problem. In Advances in Neural Information Processing Systems, volume 31. Curran Associates, Inc.,
URL http:::/prrcceednss...ee neuripp....e....... ctt ccc/paper/201/haahh 02065115122222200000060000055560
2018.
Walter Lau Neto, Matheus T Moreira, Yingjie Li, Luca Amarů, Cunxi Yu, and Earraeemmanuel Gaillardon. Slap: A supervised learning approach for priority cuts technology mapping. In 2021 58th ACM/IEEE Design Automation Conference (DAC), pp. 859-864 IEEE, 2021.
Zehua Pei, Hui-Ling Zhen, Mingxuan Yuan, Yu Huang, and Bei Yu. Betterv: Controlled verilog generation with discriminative guidance. arXiv preprint arXiv:2402.0337. 2024.
Frederik Schmitt, Christopher Hahn, Markus N Rabe, and Bernd Finkbeiner. Neural circuit synthesis from specification patterns. In Advances in Neural Information Processing Systems, volume 34, pp. 15408-15420. Curran Associates, Inc., 2021.
Frederik Schmitt, Matthias Cosler, and Bernd Finkbeiner. Neural circuit synthesis with pre-trained language models. In First International Workshop on Deep Learning-aide Verification, 2023.
Daniel Selsam and Nikolaj Bjørner. Guiding High-Performance SAT Solvers with Unsat-Core Pre- dictions. In Mikoláš Janota and Inés Lynce (eds.), Theory and Applications of Satisfiability Testing SAT 2019, pp. 336-353, Cham, 2019. Springer International Publishing. ISBN 978-3-030- 24.
24258-9. doi: 10. 0007/978-3-030-222000
12

---

Published as a conference paper at ICLR 2025
Claude. E. Shannon. The synthesis of two-terminal switching circuits. The Bell System Technical Journal, 28(1):59-95 98, 1949. doi: 10.1002/j.
Vighnesh Shiv and Chris Quirk. Novel positional encodings to enable tree-based transformers. In Advances in Neural Information Processing Systems, volume 32. Curran Associates, Inc., 2019.
David Silver, Julian Schrittwieser, Karen Simonyan, loannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of go without human knowledge. nature, 550(7676);354-35,, 2017.
Michael Sipser. Introduction the theory of computation. Cengage Learning, Australia Brazil Japan Korea Mexiko Singapore Spain United Kingdom United States, third edition, international edition edition, 2013. ISBN
978-1-133- 13781-8 978-0-357-67058-3
Kevin Skahill. VHDL for programmable logic. Madison-Wesley Longman Publishing Co., Inc., 1996.
Shailja Thakur, Balcegh Ahmad, Hammond Pearce, Benjamin Tan, Brendan Dolan-Gavit, Ramesh Karri, and Siddharth Garg. Verigen: A large language model for verilog code generation. ACM Transactions on Design Automation of Electronic Systems, 29(3):1-31, 2024.
Donald Thomas and Philip Moorby. The Verilog@ hardware description language. Springer Science & Business Media, 2008
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, E ukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in Neural Infor- mation Processing Systems, volume 30. Curran Associates, Inc., 2017.
Heribert Vollmer. Introduction to circuit complexity: uniform approach. Springer Science & Business Media, 1999.
Laung-Terny Wang. Yao Ken Chang, and Kwang-Ting Cheng. Electronic design automation: syn- thesis, verification, and test. The Morgan Kaufmann series in systems on silicon. Morgan Kauf- mann/Elsevier, Amsterdam Boston, 2009. ISBN 777-0-12-374366-
Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth McMillan, and Risto Miikku lainen. NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks, November 2023. (RR:: wwtp://.wwrraba////1100
org
arXiv:2110114053 [es].
Ziyi Wang, Chen Bai, Zhuolun He, Guangliang Zhang, Qiang Xu, Tsung- Yi Ho, Bei Yu, and Yu Huang. Functionality matters netlist representation learning. In Proceedings of the 59th ACM/IEEE Design Automation Conference, pp. 61-66, 2022.
Chenghao Yang, Yinshui Xia, Zhufei Chu, and Xiaojing Zha. Logic synthesis optimization sequence tuning using rl-based Istm and graph isomorphism network. IEEE Transactions Circuits and Systems II: Express Briefs, 69(8)3600-3304 2022a. doi: 10. 2.110///CSII.2222333366
Shuwen Yang, Zhihao Yang, Dong Li. Yingxueff Zhang, Zhanguang Zhang, Guojie Song, and Jianye Hao. Versatile multi-stage graph neural network for circuit representation. Advances in Neural Information Processing Systems,
2022b.
Cunxi Yu, Houping Xiao, and Giovanni De Micheli. Developing synthesis flows without human knowledge. In Proceedings of the 55th Annual Design Automation Conference, DAC '18, New York, NY, USA. 2018. Association for Computing Machinery. ISBN 9781450357005.
Hongkun Yu, Chen Chen, Xianzhi Du, Yeqing Li, Abdullah Rashwan, Le Hou, Pengchong Jin, Fan Yang, Frederick Liu, Jaeyoun Kim, and Jing Li. TensorFlow Model Garden. https: //gi //github. cow/tensorf lowwooode 2020.
Guo Zhang, Hao He, and Dina Katabi. Cireuit-gnn: Graph neural networks for distributed circuit design. In International conference machine learning, pp. 7364-7373. PMLR, 2019.
13

---

Published as a conference paper at ICLR 2025
Wenjie Zhang, Zeyu Sun, Qihao Zhu, Ge Li. Shaowei Cai, Yingfei Xiong, and Lu Zhang. NLocal- SAT: Boosting Local Search with Solution Prediction. In Proceedings of the Twenty-Ninth Inter- national Joint Conference Artificial Intelligence, pp. 1177-1183, Yokohama, Japan, July 2020. International Joint Conferences on Artificial Intelligence Organization. ISBN 978-0-9992411-6
5. doi: 10. 00.24963/ijcai 2020/114. httphttss:///e jeai mgg 164
Keren Zhu, Mingjie Liu, Hao Chen, Zheng Zhao, and David Z. Pan. Exploring logic optimizations with reinforcement learning and graph convolutional network, 2020 ACM/IEEE 2nd Workshop on Machine Learning for CAD (MICAD)), pp. 145-150, 2020.
Xuliang Zhu, Ruofei Tang, Lei Chen, Xing Li, Xin Huang, Mingxuan Yuan, Weihua Sheng, and Jianliang Xu. A database dependent framework for k-input maximum fanout-free window rewrit- ing. In 2023 60th ACM/TEEE Design Automation Conference (DAC), pp- 1-6, 2023. doi: 10.1 20.1099995999992222.. 102.7777777..
14

---

Published as a conference paper at ICLR 2025
A APPENDIX
A.1 DETAIL OF BACKTRACKING FRAMEWORK
The basic backtracking algorithm is follows, extracted from (Knuth 2020):
Given domain D and properties F(s1,...,, 88), this algorithm visites all sequence $1, 82,...; 8n that satisfy :(s1,.......)>
Step [Initialize] Set f- 1, and initialize the data structures needed later. Step 2 [Enter level [] (Now F(s1,.... ((81))..:8t-1) holds.) If n, visit 813--1,84 8n and go Step 5, Otherwise set 8, +- min D, the smallest element of D).
Step [Try st] If F( F'(1,...., St, 1, set 4- & + 1, and go to Step 2.
holds, update the data structures to facilitate testing
Step [Try again] If st o max D, set 8t the next larger element of D and return to Step 3. Step 5 [Backtrack] Set t- t t- 1. If t > O, downdate the data structures by undoing the changes recently made in Step and return to Step (Otherwise stop.)
We refer to Section 7.2.2 of (Knuth 2020) for more details about backtracking.
A.2
PROOF OF CHARACTERISTICS
In this section, we demonstrate that our proposed sequential representation has Characteristic 4.1
4.2
4.3 and 4.4
Characteristic 4.1 When F(s,,..., $t+1; /) is true, the transition from 81,..., 81+1 to 81,- corresponds to reversely replacing a specific node 81+1 with a wildcard node. such a replacement will never break the feasibility, because (1) a wildcard node only represents feasible circuits; (2) the wildcard node at least have a feasible choice to be set $141 $1, ... $r+1 is feasible.
During the generation from step to step t - 1, a cache mechanism can be employed cache the truth table of the constructed nodes. Therefore, when F(s1, , $t-1: f) holds and F(s1..... St-1, $t; f) needs to be evaluate, we simply traverse the generated circuit in bottom-up manner, from the current wildcard node to be replaced to the root, to evaluate g ((t)(=) for all {0, 1 with time complexity of O(N 2 d) in which d is the depth of the node. More details about the cache mechanism can be found in [Section A.3]
Characteristic 4.2,
Characteristic 4.3) Note that the AND gate A and the NAND gate 7. is always in S, in sequential representation, as replacing a wildcard node to an AND or NAND gate with two wildcard nodes will never break the feasibility.
Characteristic 4.4, For all g E C(f), the sequence $1;-.., 8n that represents is demonstrated in Section 4.4]
A.3
THE COMPUTATION OF S.
In Section 4.2
we need to compute
S = E D[F(s s1-1, holds}
in which
f1. = -
if (x) = f(x), Var E 10,1)N
otherwise
Literally, such computation is done by initializing S, as 0, and iterating through all possible sym- bols in D to see whether it should be added to St. For each s, do the following:
1. Append to $1,..., $t-1 (i.e., replace a wildcard node of current partial circuit by s, to form a new partial circuit (*))
2. Iterate through all possible inputs E 10 to see if any equivalence conflict (i.c. and f()) 0) occurs in the new partial cir- (*)
(x) 0 and f(x)
cuit ((t).
3. If we can find any æ that leads to an equivalence conflict, s should not be added to S,, there is equivalence conflict for all E (0, 1) should be added to S..
15

---

Published as a conference paper at ICLR 2025
However, the above process is not very efficient in practice for two reasons. First, many nodes in the current partial circuit are already "fully constructed" or "fixed", which means that their truth table only contains 0 and I, which will no longer change during the generation process. However, in step 2, such nodes with their child nodes still participate in the calculation of (x) for every e
{0, 1 13N, leading to unnecessary repetitiveness. Second, the calculation of g()((r) (ar) for a single æ E {0. 1 is performed on a DAG, which cannot benefit from the acceleration of matrix computation.
In this section, we introduce how to compute S, in d steps of matrix-vector computation (with time complexity of O 2 d)), in which d is the depth of the wildcard node to replace at step t. In such way, the computation will not be a bottleneck when N is reasonably small (in our case N = 8). First, during the construction process, we name a node s in a circuit as "fixed" if the value of is either 0 or 1 (not U) for all possible inputs. Formally,
8 fixed iff s(x:) # U, Va E {0, 13
in which a(x)) is the value of node given input æ. Therefore, an input node is always fixed. An intermediate node must be fixed if its left and right child are both fixed. For example, in the partial sequence [A A 22 the second A is fixed because left and right children are #1 and zg. which are both fixed. The first A is not fixed because its right child is U, its value is U when 21 and 22 both 1 A1 = U).
Recall that during the construction process in Section 4.2 for the order of replacement when multiple wildcard nodes exist, we follow fixed order that prioritizes those with the largest distance from the output, and prioritizes the left child of a gate over the right one if they have the same distance. Therefore, the construction process will only replace a node's ' right wildcard child if there is no wildcard nodes in its left branch. In other words, in the construction process, when the wildcard node to replace is then for any node s on the path from u to the root,
(x))
If u is in the right branch of s, the left child of must be fixed.
Figure 6: When the wildcard to replace is the node U in red, the blue nodes on the left must be fixed, and the red nodes on the right must U.
If u is in the left branch of the right child of must be a wildeard node.
An illustration is shown in Figure 6. Therefore, we can cache the truth table of the fixed nodes (the blue nodes in Figure 6) by main- taining a cache dictionary d during the construction process. When computing g()) (z:) for all s E D and a: E {0. 1) 1 we first initialize the wildcard node as an 2N x x Boolean matrix B, each row storing the truth table of x1, F1, ..N. NNN. Then, we backtrack from NN-
the wildcard node U to the root in Figure 6) and do the following computation in each step
If the current node u is the right child of its parent, query the cache d for the truth table d[]] of the left child (a blue node), and update B[i] + B[i A d[[] for each row of B (can be efficiently done by broadcasting mechanism"
If the current node is the left child of its parent, the right child must be U (a red node), so we simply update < B A U in an element-wise way. If the current node u is A. update B by its inverse. Then update by its parent to start the next step.
When we finished the backtrack process and reached the root, B will store the truth table of n (a) for every s E fI......... NN, E. Then we simply compare each row of B with the truth table of f to see if there is any equivalence conflict, and add tokens without conflict in S.. A and will never cause a conflict, so they will always stay in Sp. The detailed process is shown in Algorithm 2
A.4 DEMONSTRATION OF THE TREE POSITIONAL ENCODING
For example, in Figure 5 the position of the second node in the sequence, i.c., the uppermost AND gate connecting L and 22, can be represented as e2 = [10] (this gate's 's output is the first input of the
www.aaassscc...octtttttacci.aaae html
16

---

Published as a conference paper at ICLR 2025
Algorithm 2 The Computation of S;
Input: The truth table t of the Boolean function f to be realized, the wildcard node to be replaced at time step a cache dictionary d of fixed nodes storing their truth tables.
Output: St
S: f {A,A]
b < the truth tables of imput nodes 21, 2i,..., CNN, NN
while is not root do
if u is the left node of its parent then
Set b[s] + b(s) U
ss (I,, NN
else
Set b[s] + b[s) A d[1
As (~), J....,..... EN ENJ. y. in which is the left node of u's parent
end if
if u
A then
Set b(s) + b[s)
2 EN
end if
end while
for E fI., ZN. ] do
if there
in b[s] = t then
Add to St end if end for rturn S:
rightmost AND gate, so "10" pushed the encoding stack rightmost AND gate, which empty), and the position of the fourth node 22 in the sequence be represented eд [01: eg [0110] (push "01" in E2 as 22 is the second node's s second input) and eg = [10; es] = [1001] when 32 secondly visited the fifth node's first input.
For circuits with multiple primary outputs (M > 1), we initialize the encoding stack of each primary output with unique one-hot encoding, if there is virtual root node of M children, and each primary output corresponds to one of the children.
A.5 IMMEDIATE EQUIVALENT NODE MERGING AND FUNCTIONAL EQUIVALENCE CHECKING
With depth-first replacement order, can follow Algorithm 3 to merge equivalent nodes during the generation process. For functional equivalence checking of two nodes and we check whether p(æ) = ((x), Vi (0, 1) by iterating all ac. If there is such that p(x:) (3x). then p and q are not functionally equivalent.
A.6 CIRCUIT TRANSFORMER WITH MONTE-CARLOO TREE SEARCH
The detailed procedure is shown in Figure
A.7 DATASET GENERATION
The process to generate random circuit is shown in Algorithm 5] We restrict that the length of the encoded sequence for each circuit should fit all the three sequential representations with maximal length of 200, and all the 8 inputs should appear in the circuit. Each circuit has a unique structure, which is realized by canonicalization technique (Chai & Kuchlmann 2006).
A.8 EXPERIMENTS COMPUTE RESOURCES
All the experiments conducted workstation with the following specification:
CPU: AMD RyZenTM 9 7950X Desktop Processor (16 cores, 32 threads) Memory: 192GB (48GB 4) DDR5 5200MHz
GPU: NVIDIA GeForce RTX 4090 x 2
Each Transformer model in the experiments is trained single GPU with 75 hours.
17

---

Published as a conference paper at ICLR 2025
Algorithm 3 Circuit generation with immediate equivalent node merging
Input: The Boolcan function f that the generated circuit should be equivalent to. Next token prediction model P(st 81...... 8t-1).
Output: A feasible circuit g satisfying 9 E C(f).
Initialize path as an empty stack of gates, POs as an empty list.
2: Initialize G @ as a set of non-isomorphic gates
3: for t = 1, 3, do
4: Compute probability distribution of by the next token prediction model
P: +
St
5:
Set St - (
holds}
S. * is guaranteed by Characteristic 4.3
6:
t- arg maX.E8, (s()
7:
Initialize st.impuf1 <- Stirippu +- st gate.
8:
if path is empty then
b the output of s is the primary output of the circuit
9:
Append to POs and push to path
10:
else
8, should be the input of the last gate in path get the last gate added to path
+ path.peek()
12:
s. s.inputt U then s.input1 + St else s. s.input2 + St D replace a wildcard node in 8 to
13:
8, is gate then
14:
path.push(s..
15:
else
is an input node 21, II,..,,,N,, Pop fully constructed gates from path while s.impull * U and s.impu12 of do if E G then
17:
b Compute the truth table of to check functional equivalence Update path and POs to replace with the functional equivalent one in C
18:
19:
else
20:
Add s end
21:
22:
8 t- path.pop()
23:
end while
24:
end if
end
26:
end for
27:
Return the circuit with POs POs
A.9 DETAILED EXPERIMENTAL RESULT
For all unsuccessful cases, the size of optimized circuit is regarded the size of the original circuit (i.e., the model does nothing). For all the results regarding Circuit Transformer, the time cost of masking layer contributes to 6% of the total time cost. Note that the decrease of time cost by removing the masking layer is more significant than 6%, due to the fact that the masking layer "forces" the model to generate longer sequences to satisfy the constraint, which costs more time. Also note that the size of the Transformer model significantly impacts the time cost, and the reported time cost only reflects the current size setting of 88 million parameters. The time cost with heuristics search is generally proportional the beam size / search rounds.
More detailed results are shown Table 3 and Table 4
A. CASE STUDY
To show how the unsuccessful cases looks like for both the baselines and Circuit Transformer, Ta- ble 5 shows three categories of unsuccessful cases for the baseline Transformer model trained AIGER format, and provide an example from the IWLS FFWs dataset for each category. [Table shows the only cireumstance that Circuit Transformer is unsuccessful, which is the exceeding of the pre-set maximal sequence length of 200.
18

---

Published as a conference paper at ICLR 2025
Algorithm Circuit Generation with Circuit Transformer and Monte-Carlo Tree Search
Input:
The Boolean function f to be realized. Circuit Transformer PeT(se)lt......tt Immediate re-
ward function R( 9t). Number of playouts K. Output: An improved sequential representation of circuit
Create root search node initialize Umux small number. BestSeq D.
for ....
Starting from r, iteratively selects a child node with the largest PUCT score, until reaching a leaf node Set v +- R(r) +..4 R(1) if has been simulated before then
holds} as its children Expand by adding all valid tokens {s D F(r,...,4, s,, s;
Compute prior probability P(a) for each child of via P(a) <- Per(a [ ".....l:1]
Initialize (aa) <- 0, (a) <- for each child of
Select the child with the largest PUCT score and set R((e) <-
+ R(c)
else
S
end if
while EOS do
Set c arg max, Per(s r...., f), and then set v R(r,...,..
end while
e Umm then Unax f- v, BestSeq + [r....,c]
for 8 c........ C.... do
Set Q(s) + (Q(s) (()) +)/ 1), N+))++ end for end for Return Best.Sg
Table 3: Detailed results for random circuits.
Random Circuits
Methods
Average circuit
of
circuits strictly smaller
Average
Unsuccessful
Violation cases
circuit
per circuit
cases
than Resyn2
(s)
Boolean Chain
5.07%
5.07%
15.25
4.52
15.49%
0.010
Boolcan Chain (beam sizc=16)
2.16%
2.16%
14.89
3.86
16.42%
0.048
Boolean Chain (beam size= 128)
1.91%
1.91%
14.87
3.82
16.57%
0.369
AIGER
4.32%
4.32%
15.14
6.34
16.22%
0.018
AIGER
1.85%
1.85%
14.87
3.78
16.06%
0.097
AIGER
1.71%
1.71%
14.86
3.73
16.25%
0.734
Circuit Transformer w/o Masking
2.59%
2.59%
14.95
3.83
15.49%
0.010
Circuit Transformer w/o TPE
2.14%
0.00%
15.02
3.83
16.44%
0.018
Circuit Transformer
1.14%
0.00%
14.79
3.48
16.84%
0.018
Circuit Transformer (K=10))
0.20%
0.00%
14.02
2.79
36.15%
0.210
Circuit Transformer (K=100)
0.17%
0.00%
13.73
2.62
46.77%
2.090
Resyn2 (ground truth for training)
0.00%
0.00%
14.56
2.98
0.00%
Table 4: Detailed results for IWLS fanout-free windows.
TWLS FFWss
Methods
Unsuccessful cases
Violation cases
Average circuit
oF
% circuits
Average time
circuit
strictly smaller
per circuit
than Resyn2
(s)
Boolean Chain
11.36%
11.27%
17.24
6.40
7.71%
0.015
Boolcan Chain (beam sizc=16)
6.34%
6.29%
17.15
6.29
8.42%
0.079
Boolean Chain (beam sizem 128)
5.97%
5.94%
17.15
6.29
8.48%
0.539
AIGER
8.35%
7.77%
17.19
6.34
8.46%
0.025
AIGER
4.62%
4.37%
17.12
6.26
8.65%
0.149
AIGER
4.23%
3.98%
17.12
6.25
8,59%
0,906
Circuit Transformer w/o Masking
6.56%
6.54%
17.13
6.20
8.69%
0.012
Circuit Transformer w/o TPE
6.63%
0.00%
17.33
6.46
7.46%
0.019
Circuit Transformer
4,76%
0.00%
17.17
6.29
8.78%
0.018
Circuit Transformer (K=10)
2,83%
0.00%
16.92
6.17
17.42%
0.214
Circuit Transformer (K=1000)
2.63%
0.00%
16.73
6.07
26.68%
2.168
Resyn2 (ground truth for training)
0.00%
0.00%
16.83
5.57
0.00%
19

---

Published as a conference paper at ICLR 2025
Reason to be Unsuc- cessful Equivalence
Encoded Input Circuit Ex- ample
Encoded Output Circuit Ex- ample
Note
189
20
18 6
22
114
24
18 13
25 154
22
18
24.9
No node equiva-
constraint
2022
289
14.5
lent to the first out-
violation
32
34
36
32
3427
3625
35
put of the input cir- cuit.
377-40382
41
44
32
27
42
46
48 16
50
20
4638
16
40
5250 54 10
56
58 56
52 50
[BOS]
15-00583
[BOS]
Not
in
18 20
22 129
24
1892 10 12
22 20
24 15
4 elements rather than 3 in the second last line of the out- put circuit (marked bold type).
valid
12 34
32
36
30
30
32
348
36
143
38
AIGER
139
40
34
38
20
42
format
37
46
48
47
49
7 27
48 47
50
523
54
56
177
58
52 11
54
56
58.7
66 11 68
67
70 69 13
72
66 10
68
56
67
70 69 72
5571
50 12
76
-
80
77 79
82
14
84
13 80
78
11
82
81
37
84
83
86
88 83
99
92
86
76
17
88
76
87
[BOS]
8091 9493
96
95
[EOS]
Exceeding maximal
18
20
29
188 16
20 13
22
24 12
No [EOS] appears in the first 200 to- kens.
30
11 32
34
33
36
35
32 10
34
30
36
35
sequence
length
42 17 46
486
50 40
17
46
44
43
47
50 49
52445
54
56
-2
54
443
568
88
609
62
64
14
60
59
61
64
63
3 66
66
708
66
128
68
14
70
06
8 10
80 79
81 13
84 82
11
80
79
82
76
81
84 74
92 50
94936-
[BOS]
86 68
90 89
90
89
90 68
89
89 89
89
89
89 89 89
89
89
89
89
89
90
Table Example of unsuccessful cases for the baseline Transformer model trained on the AIGER format, taken from the IWLS FFWs dataset. "-" denotes the new line token. Index 2, 3, 16, 17 reserved for zo; 26. 27, 17. For the i-th AND node a, (start from 0), index 2(i + 9) denotes and index 2(i + 9) + denotes d,.
Reason to be Unsuc- cessful Exceeding maximal
Encoded Input Circuit Ex- ample
Encoded Output Circuit Ex- ample
Note
19
18
18
18
189
18
19
18
18
16
18
18
9
While no equiva- lence constraint is violated, no [EOS] appears the first 200 tokens.
18
19
18
18
18
18
14
15
18
19
18
18
18
15
18
7
19
18
18
18
19
19 19
19
18
19
sequence
19
19
12
19
13
15
19
19
19
18 18
13
18
18
18
17
14
18 18
length
19
18
15
18
17
19
18
14
18
6
16
10
18
12 19
10
13
19
19
S
12
19
10
13
19
19
[FOS]
18
10
19
12 19
19
10
19
12
13 19
19
19
10
18
18
19 18
19
19
19 5
19
19
5
19
19
19
19
19
5
5
18
19 5
18
18
19
5
19
5
18
19 18
5.
19.5
Table 6: Example of unsuccessful for the Circuit Transformer, taken from the IWLS FFWs dataset. Index 2, 3...., 16, 17 denote zo, To.-. , I7. Index 18 and 19 denote A and A.
20

---

Published as a conference paper at ICLR 2025
Algorithm Random generation a k-inppt, l-output circuit
Input: Number of input k, number output I, number of steps Output: randomly generated circuit with & inputs and outputs. C + [Lo 4....... 1--1]
for i 1,2, ... Masp do
Create AND node 8; Randomly sample two nodes co 61 E C' without replacement
Set the first input of 8; as co or og randomly
Set the second input of s; as or टт randomly
Append to the end of C end for
Return the circuit with To, J,,... Jn-1 1 as primary inputs and or-1+1, -M.-- ... ar as primary outputs.
21


Reviews:
[{"review_id": "l7rptZRmBZ", "reviewer": "Reviewer_Gw9o", "summary": "Summary:\nThis 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.", "questions": "Please address the weaknesses highlighted.", "limitations": "", "rating": 8, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "a.\tA decoding mechanism that builds circuits step-by-step using tokens with \"cutoff properties\" to block invalid tokens. \nb.\tA \"Circuit Transformer\" model incorporates this mechanism as a masking layer. \nc.\tFormulation of equivalence-preserving circuit optimization as a Markov decision process", "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.\n2.\tScalability: 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?\n3.\tComputational: 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "015j914ItR", "reviewer": "Reviewer_w2Zd", "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.", "questions": "Please address the weakness raised in **Weaknesses**.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- A novel transformer-based method to generate a circuit while preserving the semantics of the original Boolean function.\n- Experiments show good performance compared with other methods.", "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.\n- 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.\n- 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.\n- 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?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "hAD7E4SpO7", "reviewer": "Reviewer_yijD", "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.\n\nThe 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. \n\nA 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. \n\nIn 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. \n\nExperimentally, 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.", "questions": "See above.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 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. \n\nIntegrating 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.\n\nThe authors evaluate in-distribution on random circuits and out-of-distribution on circuits extracted from IWLS 2023 benchmarks, showing that their approach is robust.", "weaknesses": "## Related Work\n\nI 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.\n\n__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.\n\n## Markov Decision Process and Monte Carlo Tree Search\n\nThe 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. \n\nAdditionally, 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. \n\n## Experiments\n\nIt 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.\n\n__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?\n\n__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. \n\n__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? \n\nThe following two questions did not affect my review but would be an interesting addition to the experiment section: \n \n__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. \n\n__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?\n\n## Presentation: \n\nAlthough 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. \n - 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. \n - An introduction before the first subsection of the method section would clarify the structure and guide the reader through the different subsections.\n - 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.\n - 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. \n - Section 3.3 starts with “in the last section”, but this is not the last section.\n - Important information (such as the loss function) is only mentioned in the caption of Figure 5. I recommend moving this to the main text.\n\n## Summary\n\nOverall, 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.\n\nWeighing 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)