Small universal multiset reaction systems

Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These systems are typically represented using either Mealy machines or AIGER circuits. We present the second version of SemML, which outperforms all state-of-the-art tools for finding either solution. Aside from implementing the classical automata-theoretic approach, our tool utilizes partial exploration and machine-learning guidance for obtaining solutions efficiently, and numerous heuristics and improvements of classic algorithms for extracting small representations of these solutions. We evaluate our tool against the existing state-of-the-art tools (in particular Strix, LtlSynt, and the previous version of SemML) on the dataset of the synthesis competition SYNTCOMP. We show that we solve significantly more instances and do so much faster than other tools, while maintaining state-of-the-art solution quality.

Modern sequence models are increasingly deployed as agents that interleave token generation with calls to external tools. We study when such tool access increases computational expressivity. We model any fixed finite-precision recurrent sequence model, including finite-precision state-space models (SSMs) with $B$ bits of internal state, as a deterministic finite-state controller interacting with an oracle through a finite command/observation interface, and establish a separation between the two regimes analyzed. First, every finite-state bounded-interface tool with memory set $M$ can be internalized at a cost of at most $\lceil\log_2|M|\rceil+O(1)$ recurrent bits, so the combined system remains finite-state. Second, a single unbounded tape with only local $\mathtt{read}$/$\mathtt{write}$/$\mathtt{move}$ commands suffices for Turing completeness: every single-tape Turing machine with state set $Q$ and tape alphabet $Γ$ is simulated by a controller with $O(\log|Q|+\log|Γ|)$ recurrent bits, and $\mathrm{EQ}_n$ requires $2^n$ states without tools but one constant-size controller with the tape. Third, this construction is realized exactly by a one-layer finite-precision selective affine SSM with binary one-hot states, $\{0,1\}$ transition matrices, and zero biases. Under explicitly stated resource conventions, $O(\log B)$ recurrent bits suffice for tape-assisted simulation of any $B$-state Turing machine, whereas directly realizing an arbitrary $B$-state transition map in one exact affine update without external memory requires total recurrent dimension exactly $B-1$. Fixed description size, occupied tape cells, and interaction cost are reported separately from recurrent memory. Our results concern exact expressivity under deterministic semantics, not learnability or empirical performance.

A fixed network of McCulloch-Pitts threshold units with weights in {-1,0,1} can hold other threshold networks in its state and run them: the state is a ring of banks of records, each record a unit of a stored network, and each step evaluates one record. We use such a network to carry out von Neumann's universal construction and self-reproduction exactly. As a cellular automaton keeps its rule, the fixed network keeps its weights, and what reproduces is a stored network. A constructor of 143 records reads the description of a network from its tape, builds that network in the next bank, copies the description onto the next tape and hands control to what it built; started on its own description, it rebuilds itself, weights included, in every generation. The scheme scales to a universal computer. A SUBLEQ computer of 17,598 ternary units, stored as 36,080 records and running a program of 27 instructions, builds any network that fits a bank and reproduces itself in the same way, at every word width from eight bits on; run directly, it emits the serialization of its own weights, memory and tape. Integer pre-activations give every orbit a margin of 1/2, and replicating each unit r times multiplies it by r. That suffices against noise of any size on the pre-activations, but against von Neumann's output flips only below a threshold inversely proportional to the fan-in. These results are proved in Rocq.