How to Make Neural Networks Talk: Register Automata as Their Unexpected Interpreters

Prices move. Sensors drift. Users click, pause, return, disappear, and sometimes behave exactly like a Markov chain with a caffeine problem.

Modern sequence models are good at turning such streams into decisions. A recurrent network or transformer can look at a run of numbers and say: buy, flag, reject, approve, alert. What it usually cannot do is explain the rule it has learned in a form that a risk team, engineer, or auditor can actually inspect.

This is the familiar problem. The less familiar problem is nastier: even when a model gives the right label, we may not know whether that label is stable. A time-series model might classify two price paths as “uptrend,” while one signal survives a modest last-value movement and the other collapses after a tiny perturbation. Same label. Very different operational meaning. Lovely. The machine smiles; the margin disappears.

The paper Extracting Robust Register Automata from Neural Networks over Data Sequences tackles exactly this gap.¹ Its central move is not to make neural networks more transparent internally. Instead, it extracts a symbolic surrogate — a deterministic register automaton — from the black-box model, then uses formal methods to ask whether the surrogate’s decision is locally robust. If robustness fails, the method can return a nearby counterexample sequence.

That sounds like interpretability, but it is more specific than the usual “attention heatmap with vibes” genre. The paper’s contribution is a pipeline:

1. extend automata extraction from finite alphabets to numeric data sequences using deterministic register automata;
2. verify local robustness of those automata by reducing the question to coverability and then to shortest paths;
3. combine this checker with active and passive automata learning so black-box neural networks can be approximated by interpretable, statistically supported, robustness-checkable surrogates.

The mechanism matters because the business interpretation depends on it. This is not global proof that a neural network is safe. It is a way to extract a structured approximation, verify that approximation exactly, and connect the approximation back to the original model with statistical guarantees under a sampling distribution. That distinction is not pedantry. It is the difference between a useful model-risk workflow and a compliance fairy tale.

Why ordinary automata fail once the alphabet becomes numbers

Classic automata extraction usually assumes that inputs come from a finite alphabet. That works nicely when a model reads strings made of a small set of symbols. A deterministic finite automaton can represent rules like “no three identical symbols in a row” or “the number of zeros is even.”

But business data often does not arrive as neat finite symbols. It arrives as numbers.

A fraud model may see transaction amounts. A maintenance model may see vibration readings. A trading model may see prices. A logistics model may see travel-time sequences. These are not just symbols; their relative values matter. “Higher than the previous peak” and “below the last trough” are numeric comparisons, not alphabetic tokens.

Discretising the values into bins is the obvious escape hatch. It is also where precision quietly goes to die. If the rule depends on whether today’s value exceeds a stored previous value, a fixed binning scheme can distort the boundary. It may produce an automaton that looks interpretable but has forgotten the actual comparison the model was using.

Register automata solve this by adding a small amount of memory. A deterministic register automaton has states, but it also has registers that can store observed values. Transitions can then use guards such as “current value is greater than register 1” or “current value equals a constant.” The automaton does not merely read a symbol. It reads a value, compares it to stored values, updates registers, and moves to the next state.

That is why the paper’s motivating example uses a “higher highs and higher lows” pattern. A finite automaton over a fixed alphabet can count and switch states. A register automaton can remember the last peak, the last trough, and the previous value. It can then express a rule like:

• keep descending until a trough is found;
• keep ascending until a peak is found;
• accept only if later troughs and peaks satisfy the right ordering constraints.

This is not neural interpretability by metaphor. It is interpretability by executable structure. The extracted object is a small symbolic machine whose decision procedure can be inspected.

Registers turn hidden sequence rules into stored comparisons

The paper’s first important idea is that many learned numeric sequence rules can be represented as regular data languages. In plain terms, the model may be acting as if it follows a finite control logic plus a bounded number of remembered numeric values.

That matters because a deterministic register automaton can express rules of the following kind:

This is the right level of abstraction for many operational systems. Business users rarely need to know which hidden dimension of a transformer encoded a rising trend. They need to know whether the model’s decision depends on a stable pattern or a brittle accident.

The paper’s method therefore treats the neural network as an oracle. The learner queries the model or samples labelled sequences, then synthesises a candidate deterministic register automaton that agrees with the model. The surrogate becomes the object we can reason about.

The trick is that once the surrogate is symbolic, robustness becomes a formal question.

Robustness becomes a shortest-path problem, not a slogan

Local robustness asks whether the label remains unchanged inside a neighbourhood of a sequence. If the original sequence is $x$, a distance metric is $d$, and the perturbation radius is $\epsilon$, the neighbourhood is:

A classifier is locally stable at $x$ if all sequences inside that neighbourhood receive the same label.

For a neural network over continuous sequences, exact global robustness checking is generally hard or unavailable, especially under black-box access. The paper avoids pretending otherwise. It shifts the exact symbolic verification step to the extracted deterministic register automaton.

The verification mechanism is elegant. The authors introduce register automata with accumulators, which can compute perturbation costs between two sequences. The accumulator records how much it costs to transform or perturb one sequence into another. Different accumulator constructions support different distance metrics, including last-letter distance, Hamming distance, edit distance, and Manhattan distance. The appendix also discusses metrics such as dynamic time warping and threshold Hamming distance.

The robustness question then becomes:

Is there any sequence inside the perturbation radius that flips the automaton’s label?

The paper reduces this to a coverability problem for a bounded projected register automaton with accumulator. Then it reduces coverability to a single-source shortest-path problem. For a fixed number of registers, the robustness check is polynomial-time. If robustness fails, the procedure can construct a concrete witness — a closest label-flipping sequence under the chosen metric.

That last part is operationally important. A robustness failure is not just a red light. It is a counterexample.

In model governance language, the system can say: “Here is the nearby input that changes the decision.” That is much more useful than “the model may be unstable,” which is the kind of sentence that causes meetings without causing understanding.

There is one boundary to keep in mind. The polynomial-time guarantee holds when the number of registers is fixed. The paper is explicit that the complexity becomes exponential in the number of registers, and this is not a minor engineering inconvenience. It reflects the underlying hardness of the automata problem.

So the mechanism is powerful, but it is not magic. It works best when the relevant decision rule can be captured by a compact symbolic structure with a small number of registers.

Learning the automaton: three routes, three trade-offs

The paper does not rely on one extraction method. It implements three learners inside a prototype called RAExc.

The first is SMT-based synthesis. Given labelled samples, the method encodes the existence of a deterministic register automaton as a satisfiability problem. If the solver finds a model, that model yields an automaton consistent with the sample set. This route is principled and useful for exploring whether a configuration is feasible, but it can become slow.

The second is local search. It starts from a candidate automaton and mutates its accepting states and transitions to improve sample accuracy. This is less exact in spirit, because local search can get stuck in local optima, but the experiments show it often gives a much better practical speed-quality balance.

The third is active learning through RALib. Here the learner asks membership-style queries, using the neural network as an oracle. It incrementally refines its hypothesis when counterexamples appear. This can be very fast when the target structure fits the learner’s assumptions, but the paper also notes a limitation: the active learner cannot synthesise transition guards with uninterpreted constants, while the passive methods can.

The three methods should not be read as “winner takes all.” They are different tools for the same extraction problem.

The paper’s robust synthesis algorithm then wraps these learners with a statistical equivalence and robustness-checking loop. It samples sequences from a distribution, checks whether the DRA and neural network agree, and tests local stability of agreed samples using the symbolic robustness checker. If a counterexample is spurious for the neural network, it refines the surrogate. If the counterexample genuinely flips the neural network’s label, it reports non-robustness of the network.

This is the pipeline’s most important conceptual move: the DRA is not treated as automatically trustworthy. It must remain tied to the black-box model through sampling-based agreement.

The guarantee is statistical for the neural network, exact for the surrogate

A likely misconception deserves killing early, preferably before it breeds in a PowerPoint deck.

This paper does not give a global exact verification procedure for arbitrary neural networks over numeric sequences. The exact symbolic robustness guarantee applies to the extracted deterministic register automaton. The connection between that automaton and the neural network is statistical, based on sampled inputs and PAC-style confidence.

That does not make the result weak. It makes it usable.

In black-box settings, exact equivalence against a neural network over an infinite input domain is usually unavailable. The paper therefore uses random samples from an input distribution and applies Hoeffding-style bounds. If the robust synthesis procedure accepts, it gives high-confidence statements about agreement and local stability under that sampling distribution.

For business use, the correct interpretation is:

This distinction is not a footnote; it is the product boundary. A bank, manufacturer, or trading desk could use this as a diagnostic and certification layer for recurring sequence patterns. It should not be sold as divine access to the neural soul. The soul, regrettably, remains unavailable.

The experiments test extraction, robustness checking, and failure modes

The experimental section uses 18 benchmark languages. Some are symbolic Tomita-style languages; others are real-valued data languages involving monotonicity, peaks, valleys, and higher-high/lower-low patterns. The authors generate balanced datasets using Markov chains, with 50,000 positive and 50,000 negative samples per benchmark and maximum sequence length 50.

This benchmark design has a clear purpose. It is not meant to prove that every messy industrial time series can be captured by a small DRA. It tests whether neural models can learn regular data languages, whether DRA learners can recover suitable symbolic surrogates, and whether the robustness checker can produce useful certificates or witnesses across different distance metrics.

The neural models are LSTMs and transformers trained as black-box targets. The LSTM models reach near-perfect accuracy across the benchmark suite. The transformer models perform strongly in most cases but struggle on some languages associated with precise counting, matching prior concerns that transformers can be brittle on exact algorithmic structure.

For extraction, the results are fairly clear:

• passive learners generally synthesise adequate automata across the benchmark suite;
• SMT synthesis is reliable but can take substantially longer on harder cases;
• local search often reaches comparable accuracy with much lower synthesis time;
• active learning can be very fast on compatible targets but fails to converge on more complex data-dependency cases within the timeout.

The robustness experiments are more interesting because they show the pipeline behaving as a diagnostic tool rather than a success theatre.

Across 144 active-learning robustness experiments, the method finds 19 robustness witnesses, 73 non-robustness witnesses, and 52 inconclusive outcomes due to synthesis limitations. The total computation time is reported as about 15.37 hours.

For the SMT-based learner, the paper reports 34 robustness witnesses and 102 non-robustness witnesses, with total computation time about 80.27 hours. Some cases remain unknown or time out. This is the expensive but systematic route.

For local search, the paper reports 32 robustness witnesses, 104 non-robustness witnesses, and 8 failed experiments caused by transformer learning failures, with total robustness verification time about 36.83 hours. The authors interpret this as a practical balance between synthesis quality and computational efficiency.

A useful reading of the experiment tables is:

One result should not be misread: many non-robustness witnesses are not a failure of the method. They are the method doing its job. If a model’s decision changes under a nearby sequence, discovering that fact is valuable. In production risk analysis, a concrete counterexample is often more useful than a clean certificate, because it tells engineers where the margin disappears.

The business value is cheaper diagnosis, not automatic trust

The direct technical result is about deterministic register automata, robustness verification, and statistical extraction from black-box sequence models. The business inference is narrower but meaningful.

For organisations using sequence models, the paper suggests a model-risk workflow:

1. Train or obtain a black-box sequence model.
2. Extract a DRA surrogate from representative data or membership queries.
3. Check agreement between the surrogate and the neural model under a relevant input distribution.
4. Define perturbation metrics that match business risk: last-value movement, edit operations, Hamming-like symbolic changes, Manhattan distance, or other suitable sequence costs.
5. Use the DRA verifier to certify local robustness or return nearby label-flipping counterexamples.
6. Feed the result into model debugging, governance, monitoring, or threshold design.

This is especially relevant where decisions depend on recurring numeric patterns: time-series classification, sensor monitoring, financial signal generation, industrial anomaly detection, or sequential user-behavior models. The point is not that every model becomes perfectly explainable. The point is that a class of hidden sequence rules can be translated into small symbolic machines that support formal robustness questions.

For a business team, the operational consequence looks like this:

The uncertainty boundary is equally important. The method is strongest when the business rule is reasonably compact, sequential, and comparison-driven. It is weaker when the model relies on high-dimensional continuous features, large latent interactions, out-of-distribution behavior, or rules requiring many registers. It also depends on choosing a meaningful perturbation metric. A robustness certificate under last-letter distance may be useful for a closing-price signal; it says little about robustness under regime shifts, liquidity shocks, or data-feed corruption.

No metric saves a badly framed question. Sadly, mathematics remains unlicensed for wish fulfilment.

Where the method should sit in an AI governance stack

This paper fits best as a diagnostic layer between black-box model training and deployment approval.

It is not a replacement for standard test sets. It is not a replacement for white-box verification when white-box verification is possible. It is not a substitute for domain validation. Instead, it gives a structured way to ask:

• What symbolic rule seems to approximate this model?
• Does the rule depend on stored numeric comparisons?
• Where is the decision locally stable?
• Where can a small perturbation flip the decision?
• Is the extracted rule sufficiently aligned with the model on representative inputs?

That makes it useful for model cards, internal validation reports, and monitoring design. For example, a trading-signal system might use the extracted automaton to separate robust uptrend signals from fragile near-boundary signals. A sensor-monitoring system might identify sequences where an anomaly alert depends on a small fluctuation. A credit or fraud system using sequential transaction histories might discover that a risk label is stable for some behavioural paths but fragile for others.

The key is to treat the automaton as an interpretable surrogate with bounded authority. It can support decisions, but it should not replace the original performance evaluation or domain-specific stress testing.

The limitations are not decoration; they define the use case

The paper is refreshingly clear about several limits, and those limits matter for adoption.

First, the exact robustness result belongs to the DRA, not directly to the neural network. The neural-network claim comes through statistical equivalence and robustness guarantees under sampling. If the sampling distribution misses important operational regions, the guarantee does not magically cover them.

Second, scalability depends on the number of registers. Fixed-register robustness checking is polynomial-time, but the complexity grows badly when the number of registers is not fixed. If the business logic requires many remembered values, the surrogate may become too costly or too large to be useful.

Third, synthesis is the main bottleneck. The experiments show that the robustness checker itself is often not the dominant cost; learning an adequate DRA is. SMT can be slow, local search can be heuristic, and active learning can fail when the target model or query behavior does not fit the learner.

Fourth, the benchmark suite is controlled. It includes meaningful real-valued data languages, but it is still a formal benchmark environment. Production time series often contain noise, missing data, shifting regimes, multivariate dependencies, and nonstationary behavior. The paper opens a path; it does not eliminate the work of adapting that path to ugly data. And ugly data, as every practitioner knows, is the default setting.

Fifth, the perturbation metric is a modelling choice. Hamming, edit, Manhattan, and last-letter distances correspond to different notions of “nearby.” A certificate under one metric should not be casually reinterpreted under another. This is where domain expertise enters. The formal method can answer a precise question. It cannot choose the right business question on your behalf.

The real contribution: symbolic counterfactuals for numeric sequences

The most useful way to read this paper is not as “automata extraction, but with registers.” That is true, but too small.

The deeper contribution is that it connects three things that are usually separated:

• black-box sequence models;
• symbolic explanations over numeric data;
• local robustness and minimum-change counterexamples.

In formal explainable AI terms, the verifier behaves like a contrastive explanation engine for data sequences. It does not merely list features associated with a decision. It can search for the closest sequence that flips the label, under a chosen cost metric. That is a stronger and more operational form of explanation.

For Cognaptus-style business automation, this points to a practical architecture. Let neural models handle pattern recognition where they are strong. Then extract symbolic surrogates where the pattern has regular structure. Use those surrogates to find brittle regions, document stable regions, and generate counterexamples for retraining or review.

The result is not “trust the neural network.” It is closer to “make the neural network talk, then check whether what it says survives a small push.”

That is a much better deal. Machines do not need to become honest. They just need to become inspectable enough that we can catch them when they are confidently standing on glass.

Cognaptus: Automate the Present, Incubate the Future.