We present a passive automata learning algorithm that can extract automata from recurrent networks with very large or even infinite alphabets. Our method combines overapproximations from the field of Abstract Interpretation and passive automata learning from the field of Grammatical Inference. We evaluate our algorithm by first comparing it with the state-of-the-art automata extraction algorithm from Recurrent Neural Networks trained on Tomita grammars. Then, we extend these experiments to regular languages with infinite alphabets, which we propose as a novel benchmark.
Multiple techniques relying on clustering were proposed for learning DFA [
processing an input vector is then in the following form: (, ℎ− →1−− )−− −
Elman Networks A category of simple RNN architectures, defined by a function (, ℎ− 1)
that computes the hidden state ℎ, followed by a classifier function (ℎ) that computes the
output . and are non linear functions parameterized by their weights and . For
readability purposes, we assume that both the input vector and the hidden state ℎ− 1 are
vectors in R, at any time step = 1, 2 . . . 1. In our paper, for simplicity, we consider only
binary classification networks, i.e. ∈ B. The computation carried out by the RNN after
ℎ
→−− −− −
.
• A relation ⊑ on a set Λ is a partial order if:
1. ∀ ∈ Λ, ⊑
2. ∀ 1, 2 ∈ Λ, ( 1 ⊑ 2) ∧ ( 2 ⊑ 1) ⇒ 1 = 2
3. ∀ 1, 2, 3 ∈ Λ, ( 1 ⊑ 2) ∧ ( 2 ⊑ 3) ⇒ 1 ⊑ 3
• (Λ, ⊑) is a complete lattice if:
1. ⊑ is a partial order on a set Λ
2. any subset of Ω ⊆ Λ has a greatest lower bound ⊓Ω (i.e. the set { ∈ Λ | ∀ ∈ Ω, ⊒ }
has a greatest element), and a least upper bound ⊔Ω (i.e. the set { ∈ Λ | ∀ ∈ Ω, ⊑ }
has a smallest element)
• Then we define:
· ⊥ = ⊔∅ = ⊓Λ
· ⊤ = ⊓∅ = ⊔Λ
· Atoms(Λ) as the set of the minimal elements of Λ ∖ ⊥; in other words, ∈ Λ is an
atom if ∀ ∈ , ⊑ ⇒ = ∨ = ⊥
Atomistic Lattice A lattice (Λ, ⊑) is atomistic if: ∀ ∈ Λ : = ⊔{ ∈ Atoms(Λ) | ⊑ }.
Therefore, we can define a finite partition of Atoms(Λ) either as we did previously, or as a
function Π : {1 . . . } → Λ satisfying the following property: ∀ ∈ Atoms(Λ) there exists a
unique ∈ {1 . . . } such that ⊑ Π(). In this paper, and for the sake of simplicity, (Λ, ⊑) is
defined by the box abstraction.
1if the dimensions are not the same, we can always resize them to the highest dimension
The Box Abstraction Any set Ω ⊆ R can be abstracted by a box (-uple of intervals)
(Ω) = ⟨1 . . . ⟩, such that each is an interval bounding the projection of Ω on the
dimension . It is a classical abstract domain, and there is a Galois connection [
Partition A finite partition on Atoms(Λ) is a function Π : {1 . . . } → (Atoms(Λ)) such that ⋃︀
=1 Π() = Atoms(Λ) and ̸= ⇒ Π() ∩ Π() = ∅. Since Λ is atomistic, for any ∈ {1 . . . },
we can identify the set of atoms Π() with ⊔{| ∈ Π()} which defines the "maximal element"
(also noted Π() by abuse of notation) of this class. We have the property that classes of the
partition are stable for the operation ⊔ : ∀ 1, 2 : 1 ⊑ Π() ∧ 2 ⊑ Π() ⇒ 1 ⊔ 2 ⊑ Π().
Partitions are needed to properly define Lattice Automata, see [
J−∞ , 0J start 0
J0, +∞K J−∞ , 0J
J−∞ , 0J 1
J0, +∞K 2
J0, +∞K
J−∞ , +∞K 3
We also require the following two properties to ensure that the number of transitions is finite, even if the alphabet is infinite: 1. For any transition (, , ′) ∈ , there is ∈ {1 . . . }, such that: ∀ ∈ Atoms(Λ), ⊑ ⇒ ∈ Π(). In other words, a transition shall not mix atoms belonging to diefrent classes of the partition. Thus, we can define a function Π− 1 : Λ → {1 . . . } that associates a label of a transition to its class of the partition. 2. For any couple of states (, ′) and any class of the partition ∈ {1 . . . }, there is at most one transition (, , ) ∈ such that Π− 1( ) = .
In this work, since in our examples and experiments (Λ, ⊑) we rely on the box abstraction, we will simply call them Interval Lattice Automata (ILA). sequence 0 →− 1 1 →− 2 . . . →− such that: Language recognition Like a DFA, an ILA recognizes a language, i.e. a set of words on the input alphabet Atoms(Λ) ≡ R. A word 1 . . . ( ∈ R for all ) is accepted by if there is a • ∀ = {1 . . . }, (− 1, , ) ∈ and ⊑ • 0 ∈ I and ∈ F 5: if ∃(, ′, ′) ∈ such that Π− 1( ′) = then ← ∖ {(, ′, ′)} ∪ {(, ⊔ ′, ′)}; ← ∪ {(, , ′)}; has a role in the learning algorithm.
The function Γ does not play any role in the definition of the language recognized by an ILA. Its purpose is to associate any state of the automaton with a set of hidden states of the RNN, abstracted by an element of Λ. Unlike the elements labelling the transitions, we do not require Γ() to belong to a single class of the partition Π, it can be anything (including ⊤). We included this function in the definition of the automaton since it
Algorithms on ILA are similar to the ones on DFA. However, one must ensure that the two properties stated above remain true. For example, when we want to add a transition (, , ′) to an ILA, we must first check if there already exists a transition between the two states and ′, labelled by ′ belonging to the same class as . If so, that transition is replaced by ⊔ ′, as written in Algorithm 1.
Algorithm 1 Add Transition that ∃ ∈ {1 . . . } ⊑ Π() = ⟨Λ, Π, , I, F, , Γ⟩
An automaton = ⟨Λ, Π, , I, F, , Γ⟩ and (, , ′) ∈ × Λ × such
← I ← I F ← F ← Γ ← Γ Π− 1( ) 4: ← 6: 8:
9: end if 10: return ;
The proposed algorithm is an extension of Gold’s algorithm for the case of ILA. We first create
an Interval Prefix Tree Automaton (IPTA) from a set of traces of the RNN. Then, we launch the
merging phase in which we merge states according to a similarity score inspired by [
Let us consider a finite set of RNN execution traces = { = are of varying lengths .
︁(
() 1 , ℎ () 1 , ())︁ . . . ︁(
() 1 , ℎ () , ())︁
| ≥ 1}, where sequences
We build the IPTA starting with an automaton with a single adds transitions and states to the automaton in the following way:
We consider the initial state 0 and the first triplet (1, ℎ1, 1) of the sequence: initial state 0 and applying the function Add Sequence(, ) for every sequence ∈ . The function Add Sequence(, ) takes a sequence = (1, ℎ1, 1) , (2, ℎ2, 2) . . . (, ℎ, ) and • If there exists already in a state 1 and a transition (0, 1, 1) such that Π− 1( 1) = Π− 1(1), then we modify the transition (0, ′1, 1); with ′ = function to Γ(1) ← Γ(1) ⊔ Jℎ1, ℎ1K; moreover, 1 becomes a final state if 1 = 1 ⊔ J1, 1K, and the Γ • otherwise, we create a new state 1 and a transition (0, 1, 1), with Γ(1) ← being a final state if 1 = 1 The process is then repeated with 1 and the second triplet (2, ℎ2, 2), and so on, until the end of the sequence. This construction ensures that any word = (1, ℎ1, 1) , (2, ℎ2, 2) . . . (, ℎ, ) such that = 1 will also be accepted by the IPTA, and that Jℎ, ℎK ⊑ Γ(). For an example, Figure 2 shows the resulting IPTA from the set of traces : ⎧ 1 = (1.4, ℎ11, 1), (− 1.07, ℎ21, 1), (1.08, ℎ31, 1), (− 7.06, ℎ41, 1), (9.03, ℎ51, 1), . . . ⎪ ⎪ ⎪⎪ 2 = (3.39, ℎ12, 1), (− 3.2, ℎ22, 1), (7.91, ℎ32, 1), (− 3.45, ℎ42, 1), (2.1, ℎ52, 1), . . . = ⎨ 3 = (1.9, ℎ13, 1), (3.56, ℎ23, 1), (3.14, ℎ33, 0), (− 33.2, ℎ43, 0), . . .
⎪⎪ 4 = (2.3, ℎ14, 1), (2.29, ℎ24, 1), (2.06, ℎ34, 0), (− 0.51, ℎ44, 0) ⎪ ⎪⎩ . . .
1
J2.29, 3.56K 20
J2.06, 3.14K 21 J− 33.2, − 0.51K . . .
J1.4, 3.39K
As shown in the example, there are already some merging involved when building the IPTA, since, for each state of the IPTA, there are at most outgoing transitions (one for each class of the partition). Consequently, the language accepted by the IPTA is larger than the set of traces , and there is the implicit assumption that the set of traces is coherent w.r.t. the chosen partition Π. It can be checked by verifying that there cannot be two sequences = (1, ℎ1, 1) . . . (, ℎ, ) and ′ = (′1, ℎ′1, 1′) . . . (′, ℎ′, ′) such that: and ′ are prefixes of sequences of , ∀ 1 ≤ ≤ , Π− 1() = Π− 1(′), and ̸= ′.
If that property does not hold, it means the partition is too coarse to even build the IPTA, and that our method cannot yield a faithful representation of the behavior of the RNN. In that case, we can try again with a finer partition.
Merging the states The second step of the algorithm is to merge states according to their similarity score (a real number between 0 and 2), as long as it is possible. A description of our method is described in algorithm 2.
In our examples and experiments, the similarity score of two states 1 and 2 is defined as follows: • If only one of the two states 1 and 2 belongs to F, then the score is 2 • If both states (or none) belong(s) to F, then the score is: Similarity score(, ) = 1 − cos ((Γ()), (Γ())) = 1 − where (Γ()) denotes the center of the box Γ().
(Γ()) · (Γ()) ‖(Γ())‖2 ‖(Γ())‖2 Therefore, while there is at least one couple of states 1 ̸= 2 such that their similarity score is lower than a hyperparameter , the two states are merged. It means that any transition that goes to (or originates from) 1 or 2 will go to (or originate from) the merged state. In this process, if . . . two transitions (, , ′) and (, ′, ′) belong to the same partition class, they will be merged. For example, when we merge the two states 0 and 2 of the IPTA depicted in Figure 2, we obtain the ILA depicted in Figure 3.
At the end of the algorithm, we obtain an ILA that recognizes a language larger than the set of traces given as its input. Indeed, if = (1, ℎ1, 1) . . . (, ℎ, ) is a trace in , then there exists a sequence of states and transitions 0 →− 1 1 →− 2 . . . →− in such that: 0 ∈ I; ∀ = 1 . . . we have (− 1, , ) ∈ , ⊑ , if = 1 then ∈ F, and ℎ ⊑ Γ().
However, this ILA may also accept words that are not accepted by the original RNN, and if the set of traces is too small, it may also reject words that are accepted by the original RNN. It is why we need experimental results to assess the faithfulness of the resulting automaton w.r.t the original RNN.
Experimental setting Our experiments were run on a Dell Inc. Precision 3591 computer,
equipped with an Intel® Core™ Ultra 7 165H × 22 CPU. Python 3.12.3 was used for algorithms
implementation and data synthesis tasks. We also used PyRAT [
We evaluated our algorithm on two benchmarks. First we run experiments with RNNs trained
on Tomita languages, to compare our findings with [
Tomita 2.0 language Language description 4312 ((NNJJ0oo0,,so11ud00bdKKs)JJt⋆−r−in11g00,,c00oJJn)t⋆aafteirnainngo3dcdonJs0ec,u10tiKvestlreitntgers ∈ J− 10, 0J 5 Even number of letters ∈ J− 10, 0J and even number of letters ∈ J0, 10K 6 7
JD− ife1r0e,n0cJe⋆oJ0f,th10eKn⋆uJ−m1b0e,r0oJf⋆lJe0t,te1r0sK⋆ ∈ J0, 10K and letters ∈ J− 10, 0J is a multiple of 3
Tables 2 and 3 summarize our results. Our implementation takes roughly few seconds to infer an automaton from a set of execution traces. The fidelity score is measured as follows Fidelity(ℛ, , ) = ∑︀
=1 |ℛ() − ()| for a given RNN ℛ, ILA and sequence of inputs .
We also analyze type I and type II errors to evaluate our algorithm: • A type I error would occur because of abstractions imprecision, when a word is rejected by the RNN and accepted by its automaton (also known as false alarms). • A type II error reflects failure to capture RNN semantics, which can be due to insuficient sample size used to build the IPTA.
RNN accuracy ILA size ILA Fidelity Type I error Type II error
RNN accuracy ILA size ILA Fidelity Type I error Type II error
The scores of extracted ILA from a Tomita 2.0 RNN are roughly 80%, which is acceptable
at this stage. The distribution of error scores suggests that our interval abstraction is precise
enough (except for language 4, where it can reach 7.72%); however, type II error reflects an
insuficient sample size, especially for language 2. Increasing the size of our sequences (which
was set to 1000 sequences of maximum length 20 for each) will likely lead to improving the
scores. Our preliminary results can be improved by further benchmarking the merge parameter
and analyzing errors. Also by experimenting with diefrent state merging algorithms that
perform better than Gold’s algorithm, such as RPNI or EDSM [
We presented in this paper a passive learning algorithm that is capable of inferring an automaton from a set of traces of an RNN. Unlike previous methods, we do not require the inputs of the RNN to belong to a finite alphabet. Our algorithm ensures that we obtain an overapproximation of the set of traces. Our experiments demonstrate a capacity to infer ILA from an RNN trained on possibly infinite regular language, while also indicating that there remains significant potential for further improvements (increase fidelity and reduce ILA size), and to extend our benchmarks.
In future work, we aim to extend this proof of concept, especially for the verification and the explainability of RNNs trained for practical real-world applications, e.g. time series forecasting, where the robustness of the RNN is of paramount importance. The automata-based approach is a generalizable formal method oefring a synergy between the interpretability and the verification for recurrent networks. While properties that can be formulated and verified are beyond adversarial robustness, the explanation can also be regarded as a property we seek to verify.
This work was supported by the French Agence Nationale de la Recherche (ANR) through SAIF (ANR-23-PEIA-0006) as part of the France 2030 programme.
During the preparation of this work, the authors used Grammarly in order to: Grammar and spelling check. After using this tool/service, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.