Binary Circuit Models

Today, evaluating a neural network means interpreting it. The trained weights sit in memory as inert numbers, and a general-purpose machine walks a fetch-decode-execute loop that pushes billions of floating-point multiply-accumulates through its arithmetic units to emit each token. That layer of mediation is where inference spends its energy and its latency, and for a model defined over the reals there is no escaping it. A binary model is a different object. Its alphabet is finite, its weights and activations sit at a fixed low precision, and every operation it performs is an exact integer or logical step. Such a model is a total function from finitely many input bits to finitely many output bits, and Shannon's 1937 switching theorem says any such function is Boolean, so it can be laid out as a network of gates -- a circuit.

The paper does not merely note this reduction; it carries it out and measures the result. Earlier work tends to go one of two ways: quantize a model so it runs cheaply on stock hardware, or train a logic-gate network to imitate a task. This work runs in the opposite direction. It takes a finite-alphabet language-model head that has already been trained and compiles it into a gate-level netlist computing the identical function bit for bit, verifies each block against its integer specification, and tallies precisely how many gates that takes. The framing shifts from asking how closely logic can imitate a network to asking, given that a binary model already is a Boolean function, what circuit it corresponds to and how large it is.

Each layer is an integer multiply-accumulate followed by a nonlinearity. Once binarized, with weights and activations held in one bit as plus-or-minus one, the product of two values is +1 precisely when the two agree, which is precisely when their XNOR is 1. The inner product thus collapses to the celebrated XNOR-and-population-count: an array of XNOR gates emits the agreement bits, a balanced adder tree of full adders counts them, and a gate-free affine relabel recovers the signed dot product as 2*popcount(xnor) - n. The threshold nonlinearity is just the high bit of a comparison, and next-token selection is an arg-max tree of comparators. A binarized model, in the end, is built entirely from these three primitives.

A gate-level compiler assembles each block from primitive AND, OR, NOT, XOR and XNOR gates, evaluates the netlist on concrete inputs, and checks it bit-for-bit against the integer specification. The binarized inner product synthesizes at roughly eleven gates per input bit, climbing gently with width as the popcount tree deepens: 146 gates at n=16, 664 at n=64, and 5,577 at n=512, about 10.9 gates per bit across three orders of magnitude of width. The full adder is verified exhaustively on all eight of its inputs; the wider blocks on random inputs, 500 draws each and exact every time. The equivalence is not approximate.

Composing the verified blocks at real dimensions yields the size of a model's next-token head directly. For embedding width D=512 over a 258-symbol alphabet, the head is 258 binarized inner products of width 512 followed by a 258-way arg-max, totaling about 1.47 million verified gates; at D=768 it is roughly 2.2 million. These are figures a single field-programmable gate array holds comfortably and a modest application-specific integrated circuit realizes with room to spare. On its own, the head of a binary language model is, quite literally, a chip.

Two properties make the whole model, not just its head, a well-posed circuit. Autoregression is handled as state: the emitted symbol shifts into a context register and the combinational core re-evaluates on each clock, turning the loop into an ordinary finite-state machine with no instruction stream. And the alphabet is finite and small -- 258 symbols fit in nine bits -- so there is no analog-to-digital boundary to cross; the model's inputs and outputs are already the bits the circuit carries. Composed at the dimensions of a real trained model, with embedding width 512 over the 258-symbol byte-level alphabet, the head sits near one and a half million gates across the span of embedding widths the paper sweeps.

The one continuous operation in a transformer is the soft-max of its attention, and it is the natural objection to the thesis. The objection dissolves at its own limit. As the temperature goes to zero, the soft-max collapses to a one-hot arg-max over the scores, and arg-max is purely combinational. The query-key similarities are the same XNOR-popcount inner products, monotone in the signed dot product, so the arg-max over popcounts equals the arg-max over true scores; the winning key is chosen by a comparator tree, and the value vector is read out by a one-hot multiplexer. The paper compiles this hard-attention circuit end to end and verifies it bit-exact against a reference arg-max: at 16 keys and head width 64 it is 300 of 300 exact and costs 12,906 gates, growing linearly at about 800 gates per key.

Full soft-max is recovered as the approximate extension. At any fixed numeric precision it too is a finite Boolean function, since its only transcendental piece, exp, is a finite integer look-up table -- the paper realizes a seven-bit-to-twelve-bit exp ROM in 684 gates, exhaustively verified over all 128 inputs -- followed by an integer normalize-and-compare. The claim is stated carefully and not overstated: hard attention is exact, and fixed-point soft-max is a finite Boolean approximation of bounded, precision-controlled error. Either way, attention is a comparator-multiplexer tree over XNOR-popcount scores, optionally preceded by an integer exp table.

Compiling a float-trained model gives a circuit that computes an approximation of it. The remedy is to train the model natively binary, so the circuit computes the model itself. The paper does this for the feed-forward sub-layers, which carry most of a transformer's parameters: each linear map is pushed to plus-or-minus one by sign in the forward pass, with a per-output magnitude scale and a straight-through estimator for the gradient, so the layer is not a model to be compiled but a gate netlist that was trained. On a compiled-bytecode corpus a small native model -- six layers of width 192, some three million parameters -- reaches 0.57 held-out bits per token against the 8.01-bit uniform baseline, at full opcode validity, and at the end of training every feed-forward weight is machine-verified to be sign-valued. Native binarization costs bits -- the companion floating-point model reaches 0.43 -- but it buys exactness.

The result is a trend, not a single point. Across five native-binary models spanning some thirty-fold in size, from half a million to eighteen million parameters, held-out bits per token falls from 0.71 to 0.59, and at every size the entire feed-forward weight set is verified sign-valued. The paper bounds this claim with two honesty caveats stated plainly: it reports the median of the late-training evaluations rather than the noise-mined running minimum, and the points share a fixed wall-clock budget rather than a fixed token budget, so the smaller models in fact saw more data. The honest reading is that native binarization succeeds and improves with size under a fixed budget -- larger size helps despite, not because of, more training -- and a controlled iso-token scaling law is future work.

Composing the verified blocks at the dimensions of a real sub-million-parameter model -- four layers of width 128 -- gives an end-to-end gate budget for one autoregressive step. The feed-forward datapath of all layers is 5.6 million exact gates read straight off the trained plus-or-minus-one weights, the next-token head a further 0.38 million, and the embedding a read-only memory of half a million. The remaining term is attention, and here the compilation exposes a real design fact: a full context of 512 keys reaches 12.5 million gates and dominates the model, while a local window of 128 keys holds it to 3.1 million. The whole model is therefore roughly ten million gates at a local context and nineteen at a global one, both comfortably within a single contemporary FPGA. The lever that matters for a fabricated model is not the arithmetic, which binarization has made cheap, but the attention window.

Simulation checks a circuit on the inputs one thinks to try; a proof checks it on all of them. The paper formalizes the compiler's core in the Lean 4 proof assistant: six theorems compile with no sorry and no added axioms. They prove the full adder correct for all inputs, the n-bit ripple adder by induction, the identity at the heart of the paper that the signed inner product of two sign vectors equals 2*popcount(xnor) - n, that the comparator-tree maximum dominates every element, and -- the formal statement of the thesis -- that every total Boolean function is realized by a circuit over AND, OR and NOT, proved by Shannon expansion. The one thing the paper has not done, and states plainly among its open problems, is synthesize a complete trained model onto silicon; what remains genuinely open is that physical realization.