Synthesis and Verification of Register Automata over Data Sequences (Technical Report)

arXiv:2511.19100 · cs.AI, cs.FL, cs.LG · Submitted 2025-11-24 · Read on arXiv

Listen

Transcript

Introduction to the show: ident: AI Radio. Generated commentary on the latest Artificial Intelligence papers.

Tom: We're looking at the paper: "Synthesis and Verification of Register Automata over Data Sequences (Technical Report)".

Jane: Here's the gist of the paper. The gist: A framework for robust Deterministic Register Automata (DRAs) extraction from black-box neural networks, combining polynomial-time robustness checking with learning algorithms, enables synthesising interpretable surrogates with statistical robustness and equivalence guarantees Automata Modeling and Robustness Definition The paper addresses the challenge of extracting automata from data sequences drawn from continuous domains by using Deterministic Register Automata (DRAs), which extend finite automata with registers that store and compare numeric values This approach overcomes the limitations of previous DFA extraction methods that are restricted to finite alphabets The concept of robustness is defined formally as follows: Given a DRA A and a sequence v in L(A), an RAA A D and a constant δ in Q, the language L(A) is robust at v up to δ (w.r.t.

Tom: D), if Bδ (v) ∩ L(Ac) = ∅ This definition unifies one-sided robustness in Definition 1: if A (w) = 1, then Stabδ (A,w) is precisely “L(A) is δ-robust at w,” i.e., Bδ (w) ∩ L(Ac) = ∅ Robustness Verification Procedure The paper develops a decision procedure to verify the robustness of DRAs in polynomial time when the number of registers is fixed Theorem 1 states that for any fixed number of registers k, checking whether a k-DRA is robust at a given sequence is decidable in polynomial time The proof proceeds by reducing robustness to the coverability problem for a restricted class of RAA called bounded projected RAA This reduction further reduces the coverability problem to the single-source shortest path problem via Dijkstra’s algorithm, thereby proving Theorem 1 Automata Synthesis Methods Three complementary methods are presented for synthesising DRAs from black-box models 1.

Jane: SMT-Based Synthesis: This method builds on reducing DFA identification to SMT, where the inclusion of registers and constants adds complexity The process involves encoding guard formulas as interval constraints and register updates symbolically, allowing an SMT solver to check satisfiability for a consistent DRA 2.

Tom: Synthesis Based on Local Search: This heuristic navigates the search space by applying mutation operations like opf and opΔ to refine candidate automata using a score function defined as score(A, S) = S+ ∩ L(A) + S− 3.

Title and authors: Jane: Let's look at the title and who wrote this. "Synthesis and Verification of Register Automata over Data Sequences (Technical Report)." It tells us immediately that they are doing two main things: building these automata, and then checking them.

Tom: The authors are Hong, Jiang, Lin, Markgraf, Parsert, Tan A from various universities in Germany and the United Kingdom > (<ref:2511.19100#pg1>). They’re bringing together folks from different research groups to tackle this specific challenge.

Lu: What’s interesting is that they explicitly state their main contribution right up front: a framework for robust DRA extraction from black-box models > (<ref:2511.19100#pg1>). It sets the stage for everything else they do with this paper.

Meng: So, it’s not just about creating one new model type; it's about building a whole pipeline that starts with a black box and ends up with something we can actually inspect > (<ref:2511.19100#pg3>).

Lalam: They combine polynomial-time robustness checking for DRAs with passive and active automata learning algorithms to synthesize surrogate DRAs that have statistical robustness and equivalence guarantees > (<ref:2511.19100#pg3>).

The paper's summary: Tom: So, the core idea is that you can use a neural network N as an oracle to build these automata, and then check if the automaton A they built actually captures the behavior of N robustly > (<ref:2511.19100#pg3>).

Jane: They define robustness formally as language L(A) being robust at a sequence v up to a constant delta, meaning that within that neighborhood, there are no counterexamples in the automaton's language > (<ref:2511.19100#pg3>).

Lu: The key theoretical win here is their decision procedure: for any fixed number of registers k, checking if a k-DRA is robust at a given sequence is decidable in polynomial time > (<ref:2511.19100#pg3>).

Meng: Polynomial time sounds good on paper, but how does that translate to something that runs on real data sequences we actually see in production? I’m worried about the complexity of those register updates > (<ref:2511.19100#pg3>).

Lalam: They prove this by reducing robustness verification to a single-source shortest-path problem through an intermediate formalism, which is the Register Automata with Accumulators > (<ref:2511.19100#pg3>).

The paper's improvements: Tom: So, the paper lays out three main ways they synthesize these DRAs from a black-box model N. First, SMT-Based Synthesis, which uses satisfiability solvers to check consistency for guards and register updates > (<ref:2511.19100#pg3>).

Jane: Then there's the synthesis based on local search, using mutation operations like opf and opΔ with a specific score function to refine candidate automata incrementally > (<ref:2511.19100#pg3>).

Lu: And finally, they have synthesis based on active learning, where the neural network acts as an oracle to incrementally refine its hypothesis based on counterexamples > (<ref:2511.19100#pg3>).

Meng: I’m interested in the active learning part. Does that mean we can actually use an existing model to teach us a better, more robust surrogate? What are the costs associated with running that process at scale > (<ref:2511.19100#pg3>)?

Lalam: They combine these methods into one pipeline where the neural network N acts as an L-star style learner for register automata, allowing them to synthesize robust DRAs with statistical guarantees > (<ref:2511.19100#pg3>).

Conclusion: Tom: So, to wrap up, this paper gives us a complete procedure for extracting interpretable surrogates from black-box RNNs and transformers while also providing probabilistic robustness certification of the underlying models > (<ref:2511.19100#pg3>).

Jane: The results show that passive learners successfully synthesized adequate automata for all the benchmark languages, and LLS verified most neural networks across all distance metrics > (<ref:2511.19100#pg4>).

Lu: The major bottleneck they identified is actually the automata learners themselves, suggesting that developing better synthesis methods is where the next big effort should be directed > (<ref:2511.19100#pg4>).

Meng: From a deployment standpoint, knowing that you can get a surrogate with statistical robustness guarantees makes deploying these kinds of models much safer than just trusting the raw output > (<ref:2511.19100#pg3>).

Lalam: The framework successfully extracts interpretable automata from black-box RNNs and transformers while enabling probabilistic robustness certification of the underlying models > (<ref:2511.19100#pg3>).

Tom: This work opens up some promising directions for interpretable machine learning and formal verification of neural systems > (<ref:2511.19100#pg3>).

Jane: That’s the gist of it. It moves us from just building big models to being able to formally verify and certify what those models are actually doing, even when they're complex data sequences > (<ref:2511.19100#pg3>).

CHIH-DUO HONG, HONGJIAN JIANG, ANTHONY W. LIN, OLIVER MARKGRAF, JULIAN PARSERT, TONY TAN

National Chengchi University · University of Kaiserslautern-Landau · University of Liverpool

cs.AI, cs.FL, cs.LG

Submitted: 2025-11-24

Updated: 2026-10-21

License: http://creativecommons.org/licenses/by/4.0/

Importance score: 86/100

The gist: The gist: A framework for robust Deterministic Register Automata (DRAs) extraction from black-box neural networks, combining polynomial-time robustness checking with learning algorithms, enables

Key concepts

Deterministic Register Automata (DRA): These are automata that extend standard finite automata by adding registers capable of storing and comparing numeric values. This allows them to process sequences drawn from continuous domains, overcoming limitations found in traditional DFA extraction methods.
Robustness Definition: Robustness is formally defined as whether a DRA's language remains unchanged when the input sequence is slightly perturbed (up to a distance delta). A language is robust if the set of sequences accepted by the original automaton and its perturbed version do not overlap.
SMT-Based Synthesis: This method builds DRAs by translating their logic into Satisfiability Modulo Theories (SMT) problems. Guard formulas are encoded as interval constraints, allowing a solver to symbolically check if a given set of register updates and transitions is logically consistent for a specific DRA.
Active Learning Synthesis: This approach uses an active learning framework where the neural network acts as an oracle. The system iteratively queries the network for counterexamples to refine its hypothesis, ensuring that the resulting synthesized DRA is statistically robust and accurate.

Terminology

Robustness — 5× in this paper · explained in 6 episodes
Active Automata Learning — 1× in this paper · explained in 1 episode
Interpretability — 1× in this paper · explained in 15 episodes
Transformer — 1× in this paper · explained in 2 episodes
Transformer Architecture — 1× in this paper · explained in 4 episodes
Verification — 1× in this paper · explained in 2 episodes

Summary

The gist: A framework for robust Deterministic Register Automata (DRAs) extraction from black-box neural networks, combining polynomial-time robustness checking with learning algorithms, enables synthesising interpretable surrogates with statistical robustness and equivalence guarantees

Automata Modeling and Robustness Definition

The paper addresses the challenge of extracting automata from data sequences drawn from continuous domains by using Deterministic Register Automata (DRAs), which extend finite automata with registers that store and compare numeric values This approach overcomes the limitations of previous DFA extraction methods that are restricted to finite alphabets The concept of robustness is defined formally as follows: Given a DRA A and a sequence v in L(A), an RAA A D and a constant δ in Q, the language L(A) is robust at v up to δ (w.r.t. D), if Bδ (v) ∩ L(Ac) = ∅ This definition unifies one-sided robustness in Definition 1: if A (w) = 1, then Stabδ (A,w) is precisely “L(A) is δ-robust at w,” i.e., Bδ (w) ∩ L(Ac) = ∅

Robustness Verification Procedure

The paper develops a decision procedure to verify the robustness of DRAs in polynomial time when the number of registers is fixed Theorem 1 states that for any fixed number of registers k, checking whether a k-DRA is robust at a given sequence is decidable in polynomial time The proof proceeds by reducing robustness to the coverability problem for a restricted class of RAA called bounded projected RAA This reduction further reduces the coverability problem to the single-source shortest path problem via Dijkstra’s algorithm, thereby proving Theorem 1

Automata Synthesis Methods

Three complementary methods are presented for synthesising DRAs from black-box models

SMT-Based Synthesis: This method builds on reducing DFA identification to SMT, where the inclusion of registers and constants adds complexity The process involves encoding guard formulas as interval constraints and register updates symbolically, allowing an SMT solver to check satisfiability for a consistent DRA
Synthesis Based on Local Search: This heuristic navigates the search space by applying mutation operations like opf and opΔ to refine candidate automata using a score function defined as score(A, S) = S+ ∩ L(A) + S−
Synthesis Based on Active Learning: This method wraps RALib so that the neural network serves as the membership and statistical equivalence oracle It incrementally refines its hypothesis by issuing queries to oracles based on counterexamples necessitating refinement

Robust DRA Extraction Pipeline

The overall framework combines learning procedures with a symbolic robustness checker (Algorithm 2) This checker treats the neural network N as a black box and evaluates the hypothesis through membership queries Algorithm 2 distinguishes between a spurious counterexample (used to refine A) and a genuine robustness violation of N Theorem 8 provides a robustness guarantee stating that if the procedure accepts then with confidence at least 1 − η, it holds that λ ≤ 1 − η1/n

Experimental Evaluation

Experiments evaluate the effectiveness of neural networks and DRA learning algorithms across eighteen benchmark languages Results show that passive learners successfully synthesised adequate automata for all benchmarks LSMT and LLS successfully verified the majority of neural networks across all supported distance metrics The major bottleneck lies in the automata learners rather than the robustness checker

Conclusion

The framework successfully extracts interpretable automata from black-box RNNs and transformers while enabling probabilistic robustness certification of the underlying models These results open promising directions for interpretable machine learning and formal verification of neural systems

How it works

The paper presents a theoretical foundation and practical framework for interpreting and verifying sequential neural networks over data words By reducing robustness verification to computation of shortest paths, it obtains a polynomial-time decision procedure for deterministic register automata with a fixed number of registers It combines this algorithm with the automata synthesis methods to obtain a procedure for verifying the robustness of black-box models

Automata Modeling and Robustness Definition

A k-Register Automaton (k-RA) is defined as a tuple A = (Q, Δ, q0, F) consisting of k registers, a finite set Q of states, the initial state q0 ∈ Q, the set F of accepting states, and a finite transition relation Δ For each transition (p, φ, ψ, q), there is a guard φ given by a conjunction of (in)equalities over the registers r1,..., rk, the currently read data curr and constants from Q The language L(A) consists of all sequences accepted by A

Formal Definition of RAA

A k-RAA is a tuple A = (Q, Δ, q0, F), where Δ is the transition relation with guards φ and assignments ψ The accumulator update τ is of the form acc += a1 ∗ curr1 + a2 ∗ curr2 + b where a1, a2, b ∈ Q

Metric Definitions

The paper defines several distance metrics and their corresponding RAAs

**- Hamming Distance: The RAA for this captures Dham by incrementing acc by one when curr1 and curr2 are different **

**- Manhattan Distance: This RAA captures the metric by incrementing acc by curr2 − curr1 or curr1 − curr2 **

**- Edit Distance: The RAA for this guesses the monotone matching M and computes Dedt(v,w) as the minimum over all possible incremental matchings **

**- Dynamic-Time-Warping (DTW) Distance: This RAA tries to guess the incremental matching M and computes Ddtw(v,w) by summing vi − wj over the matching M **

Robustness for DRA languages

Definition 1 (Robustness) states that L(A) is robust at v up to δ (w.r.t.

Improvements for AI systems

Robustness Verification for Sequence Models: The improved system can certify that a neural network N is robust at a sequence v up to a perturbation distance delta by deciding whether L(A) is delta-robust at v, which checks if B delta (v) intersect L(Ac) = empty.
Interpretable Surrogate Synthesis: The system can synthesize deterministic register automata with statistical robustness guarantees by combining passive and active learning algorithms, yielding surrogates that provide both agreement and stability guarantees.
Automated Robustness Witness Identification: The system can identify genuine non-robustness of a network by distinguishing between a spurious counterexample (used to refine A) and a genuine robustness violation of N, reporting the latter to the user.
Learning from Black-Box Models: The system can learn an interpretable surrogate DRA by wrapping active learning frameworks like RALib, allowing the neural network N to serve as an L∗-style learner for register automata.
Metric-Specific Robustness Analysis: The framework allows for robust verification using various distance metrics, including last-letter distance, edit distance, Manhattan distance, and c threshold Hamming distance by constructing corresponding Register Automata with Accumulators (RAAs).

Abstract

Data sequences, such as time series, traces, and sensor streams, are words over large or infinite data domains. Their properties often depend on comparisons between values at different positions, which finite automata cannot express directly. We study synthesis and verification for Deterministic Register Automata (DRAs) over ordered data sequences. DRAs combine finite control with registers for remembered data values, providing compact symbolic descriptions of quantitative sequence languages. Our technical core is a local-search synthesis procedure and an exact robustness checker for DRAs. We fix the alphabet theory to ordered rationals (;<,=) with rational guard constants and use non-negative affine accumulator costs. For a fixed number of DRA registers, the checker runs in polynomial time; its dependence on that number is exponential. It reduces robustness to coverability and then to a shortest-path problem. Since the search ranges over+, it produces variable-length witnesses and, for RAA-definable alignment costs such as DTW, explores a counterexample space with no a priori length bound. As an application, we use learned DRAs as interpretable surrogates for queried neural sequence classifiers. A probably approximately correct (PAC) validation loop refines rejected candidates, returns genuine non-robustness witnesses for the classifier when found, and accepts a surrogate only with statistical guarantees for fidelity and local stability. We implement the framework in RAExc, enabling the synthesis of interpretable automata and the verification of their robustness. We evaluate the approach on benchmark languages and sequentialized MNIST, demonstrating high accuracy while verifying the robustness of the learned automata.