Which Regular Languages Admit Provably Correct RNN Implementations? A Lattice-Theoretic Characterisation via Forward-Invariant Sets

Motivation

• Known: Weiss et al. (2018)는 finite-precision RNN이 정확히 regular language를 인식할 수 있음을 보였으나, 이는 유한 길이에서의 분류일 뿐 임의 길이에서의 length generalisation을 보장하지 않는다. Switched dynamical system 및 Lyapunov 이론에서 forward-invariant set이 안정성 증명에 사용되어 왔으나 RNN의 formal language 인식 문제와 연결된 바는 제한적이었다.
• Gap: 어떤 regular language가 forward-invariant certificate를 통해 provably length-generalising RNN으로 구현 가능한지에 대한 automata-theoretic 특성화가 부재했으며, expressibility(학습 가능성)와 verifiability(검증 가능성) 사이의 경계가 명확히 규명되지 않았다.
• Why: 이 경계를 규명하면 어떤 언어 클래스에 대해 신경망 기반 시퀀스 모델이 임의 길이에서 수학적으로 검증 가능한 정확성을 보장할 수 있는지 사전에 판별할 수 있어, formal verification과 neural network 해석 가능성 연구에 실질적 지침을 제공한다.
• Approach: Elman RNN을 switched dynamical system으로 정식화하고 forward-invariant positive-margin set의 존재가 length generalisation과 동치임을 증명(Theorem 2.1)한 뒤, 이 존재성을 DFA의 absorbing accept state 유무와 연결하는 필요조건(Theorem 3.1)을 제시하고 42개 absorbing 패턴과 12개 non-absorbing 패턴에 대해 대규모 실험으로 그 역방향(충분조건)을 경험적으로 뒷받침한다.

Achievement

Figure 2. CQLF contraction rate γ across hidden sizes. All certified models satisfy γ < 1, with tighter contraction at s

1. 동치성 정리(Theorem 2.1): forward-invariant set Ck의 존재가 length generalisation과 if-and-only-if 관계임을 증명.
2. Absorbing 특성화(Theorem 3.1): forward-invariant RNN 구현이 가능하려면 minimal DFA가 absorbing accept state를 가져야 함을 증명(필요조건), non-absorbing language(modular counting, last-k, alternating)는 이러한 구현이 불가능함을 증명.
3. Lattice 닫힘 성질: absorbing-state language 클래스가 union과 intersection에 닫혀 있음을 증명(단, complement에는 닫혀있지 않음), block-diagonal 구성을 통한 AND/OR/NOT 조합이 30/30 성공.
4. 경험적 검증: 350/350 absorbing 패턴 성공 vs 12개 non-absorbing 패턴에서 0–7% 성공(baseline 63–100%와 대비), 350/350 vs baseline 간 거의 완벽한 분리 확인.
5. 세 가지 검증 도구: Kleene iteration(axis-aligned box lattice, ~14회 반복 수렴), CQLF(Common Quadratic Lyapunov Function) via LMI(109/110 모델을 H=70까지 검증), gap suppression formula(gapd ≈ sech²(z̄d)·|Δzd|, r=+0.743, F1=0.872)로 349/350(99.7%) 모델 인증, 0 false positive.

How

Figure 1. Kleene-iteration invariant boxes. Left: Absorbing-state model (k=3, recipe): tight invariant box with positive

• Elman RNN의 hidden state 업데이트 h_{t+1} = tanh(W_hh h_t + u_{x_t})를 f0, f1 두 개의 switching map으로 정의하고, forward-invariant set Ck가 f0(Ck)∪f1(Ck)⊆Ck 및 양의 margin 조건을 만족하는지를 검증 대상으로 설정.
• minimal DFA의 accept state가 absorbing(δ(qa,σ)=qa for all σ)인지 여부로 language를 absorbing/non-absorbing으로 분류하고, product DFA 구성을 통해 union·intersection에 대한 닫힘성을 증명.
• Gap suppression mechanism을 mean value theorem 기반으로 유도하여, pre-activation이 특정 조건을 만족할 때 tanh의 sech² 항으로 인해 hidden dimension이 input-invariant해짐을 분석(Proposition 4.1, 4.2).
• Kleene iteration: axis-aligned box의 complete lattice 위에서 least fixed point를 interval arithmetic으로 계산(Tarski's theorem 기반), 수렴 시 forward-invariant box로 인증.
• CQLF (Common Quadratic Lyapunov Function): LMI(linear matrix inequality) feasibility로 f0, f1에 대해 공통 Lyapunov function이 존재하는지 검증.
• 42개 absorbing 패턴(substring detection, pattern occurrence 등)과 12개 non-absorbing 패턴(modular counting, last-k, alternating)에 대해 학습 프로토콜(recipe)과 baseline을 비교하는 대규모 실험 수행.

Originality

• Formal language theory(automata의 absorbing state)와 dynamical system 이론(forward-invariant set, Lyapunov function)을 직접적으로 연결하는 최초의 lattice-theoretic 특성화 제시.
• Length generalisation을 "certificate가 존재하는가"라는 검증 가능성 문제로 재정의하고, 이를 automata 구조(DFA의 absorbing 성질)와 연결한 최초의 시도.
• Kleene iteration, CQLF/LMI, gap suppression formula라는 세 가지 독립적 수학적 도구를 결합해 하나의 특성화를 다각도로 검증하는 방법론적 독창성.
• absorbing-state language 클래스가 Boolean lattice의 sublattice를 이룬다는 대수적 구조를 규명하고 이를 block-diagonal RNN 조합과 연결.

Limitation & Further Study

• 논문에서 명시하듯 특성화는 one-directional(필요조건만 증명)이며, 역방향(모든 absorbing-state language가 forward-invariant RNN을 갖는다는 것)은 42개 패턴에 대한 경험적 근거만 있을 뿐 일반적으로 증명되지 않음.
• 테스트된 언어 패턴 수(absorbing 42개, non-absorbing 12개)가 제한적이어서 일반화 가능성에 한계가 있으며, 더 복잡하거나 고차원적인 regular language에 대한 검증이 부족함.
• forward-invariant certificate 외의 다른 형태의 length-generalising RNN 구현 가능성(예: 비-forward-invariant 방식)은 다루지 않아 특성화가 이 특정 certificate 형태에 국한됨.
• Elman RNN과 tanh 활성화 함수에 특화된 분석으로, LSTM, GRU, Transformer 등 다른 아키텍처로의 일반화 가능성은 논의되지 않음.
• 후속 연구로 absorbing-state language의 충분조건에 대한 완전한 증명, 더 넓은 언어 클래스 및 아키텍처로의 확장이 필요.

Evaluation

총평: Automata 이론과 dynamical system/lattice 이론을 정교하게 결합하여 RNN의 provable length generalisation 경계를 규명한 독창적이고 기술적으로 탄탄한 연구이나, 특성화가 필요조건에 국한되고 검증 패턴 수가 제한적이라는 점에서 완전한 이론적 폐쇄에는 이르지 못했다.