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

summary

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

In short

The framework extracts interpretable Deterministic Register Automata (DRAs) from complex black-box neural networks. It combines polynomial-time robustness checking with learning algorithms to synthesize surrogates that guarantee both statistical accuracy and formal robustness against small perturbations in the input data.

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 used across episodes

Reinforcement Learning (RL) — explained in 26 episodes
Flow Matching — explained in 22 episodes
Quantum Fisher Information (QFI) — explained in 21 episodes
Retrieval-Augmented Generation (RAG) — explained in 21 episodes
Sample Complexity — explained in 20 episodes
Federated Learning — explained in 18 episodes

This episode discusses

The paper

Synthesis and Verification of Register Automata over Data Sequences (Technical Report) · Read on arXiv

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

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

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.

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>).

More episodes

← Home