✗ Failed on benchmark 2026

PAC-IMDP Safety Monitor for Neural State Dynamics

Implementation & benchmark of arXiv:2607.27908 — Data-Driven Formal Methods for Complex Dynamical Systems: A Survey

Usefulness8/10

Difficulty6/10

Novelty7/10

Dynamics Stability Generalization Accuracy Rnn Ssm World model Rl Training dynamics Control theory Dynamical systems Probability Statistics

Source paper: Data-Driven Formal Methods for Complex Dynamical Systems: A Survey arXiv:2607.27908 ⓘ · analyzed Aug 31, 2026

AI-generated research hypothesis, automatically tested. Not peer-reviewed.

Idea description

Discretize the hidden state of an RNN, state-space model, or neural world model into cells and estimate a transition interval for every source-cell/action/target-cell triple from trajectory data. Use robust Bellman recursion on the resulting interval MDP to penalize actions or parameter updates whose worst-case probability of reaching an unsafe cell exceeds a prescribed threshold.

Formulas

$$h_{t+1}=f_{\theta}(h_t,u_t,\xi_t),\qquad n_{iaj}=\sum_{s=1}^{N_{ia}}\mathbf 1\{h_s\in C_i,u_s=a,h_{s+1}\in C_j\},\qquad \widehat p_{iaj}=\frac{n_{iaj}}{N_{ia}}.$$

$$\ell_{iaj}=\mathsf I^{-1}\!\left(\frac{\alpha}{2M^2A};\,n_{iaj},N_{ia}-n_{iaj}+1\right),\qquad r_{iaj}=\mathsf I^{-1}\!\left(1-\frac{\alpha}{2M^2A};\,n_{iaj}+1,N_{ia}-n_{iaj}\right),$$

$$\mathcal P_{ia}=\left\{p\in[0,1]^M:\sum_{j=1}^{M}p_j=1,\ \ell_{iaj}\le p_j\le r_{iaj}\right\},\qquad V_{t+1}(i)=\max_{a}\max_{p\in\mathcal P_{ia}}\sum_{j=1}^{M}p_jV_t(j).$$

$$\Pr_{\mathrm{data}}\left(\forall i,a,j:\ p_{iaj}\in[\ell_{iaj},r_{iaj}]\right)\ge 1-\alpha,\qquad \text{certificate: }\max_{i\in C_{\mathrm{safe}}}V_H(i)\le\varepsilon.$$

Mathematical statement

Let the neural hidden dynamics be $h_{t+1}=f_{\theta}(h_t,u_t,\xi_t)$, let $\{C_1,\ldots,C_M\}$ partition the relevant hidden-state region, and let $a$ denote a discrete action or input bin. From $N_{ia}$ visits to source cell $C_i$ under action $a$, let $n_{iaj}$ transitions enter target cell $C_j$. The unknown transition probability is $p_{iaj}=\Pr(h_{t+1}\in C_j\mid h_t\in C_i,u_t=a)$. Construct confidence intervals $[\ell_{iaj},r_{iaj}]$ using a binomial confidence interval with per-entry failure probability $\alpha/(M^2A)$, where $A$ is the number of actions. The admissible transition set is $\mathcal P_{ia}=\{p:\ell_{iaj}\le p_j\le r_{iaj},\sum_jp_j=1\}$. For a finite-horizon unsafe-reachability property, initialize $V_0(i)=1$ if $C_i$ is unsafe and $0$ otherwise, then compute the worst-case recursion $V_{t+1}(i)=1$ for unsafe cells and $V_{t+1}(i)=\max_a\max_{p\in\mathcal P_{ia}}\sum_jp_jV_t(j)$ for controllable systems. The certificate is valid with probability at least $1-\alpha$ over the collected data, subject to representative sampling and a valid Markov abstraction.

Implementation notes

1. Integration point: begin with a GRU or small neural state-space model whose hidden state has dimension 8-16. Freeze or periodically snapshot the encoder, cluster hidden states into $M=32$-256 cells using k-means, and define a discrete action set from the policy's action bins. Add a training penalty when the robust $H$-step unsafe-reachability value from the current cell exceeds $\varepsilon$. For continuous actions, discretize actions or maximize over sampled action candidates. 2. Pseudocode: collect trajectories; assign each pair $(h_t,u_t)$ to $(i,a)$ and $h_{t+1}$ to $j$; count $n_{iaj}$; compute beta or Clopper-Pearson bounds using the displayed formulas; for each Bellman step, solve the inner linear program by placing as much probability as possible on the largest $V_t(j)$ while respecting interval bounds; backpropagate through a differentiable soft approximation of the maximum, or use the certificate for action masking, rejection sampling, and checkpoint selection. 3. Computed from the paper's mechanism: finite abstraction, interval transition model, robust Bellman verification, and confidence accounting. Estimated empirically: hidden-state partition, transition counts, coverage, and whether the Markov approximation is adequate. Unvisited transitions should receive $[0,1]$ bounds or trigger additional data collection rather than being treated as zero. 4. First cheap experiment: train a GRU on sequential MNIST or a 2-D navigation task with unsafe regions, comparing ordinary cross-entropy or RL training against the IMDP penalty. Use $M=64$, horizon $H=20$, and $\alpha=0.05$. The primary falsifiable prediction is that each interval width scales approximately as $O(\sqrt{\log(2M^2A/\alpha)/N_{ia}})$; doubling visits should reduce median width by about $1/\sqrt{2}$. The certified unsafe probability should decrease monotonically as data accumulate, and the empirical violation rate on fresh trajectories should remain below the certified bound except for prescribed confidence failures. Vary the penalty until the robust certificate crosses $\varepsilon=0.1$; this crossing should coincide with a sharp reduction in empirical unsafe reachability. Overly coarse partitions should instead produce a measurable conservatism gap.

Verification

Failed on benchmark

Stage 1 · Toy mechanism gate: Passed ✓

Stage 2 · Mechanism transferred to benchmark: Not reproduced ✗

Stage 2 · Practical benchmark result: No measurable effect

Methodology: 8 paired seeds, permutation test (p<0.05) against a learning-rate-tuned baseline. How verification works

Stage 1 — Mechanism check agent confidence 8/10

Built a PAC-IMDP safety monitor with exact Clopper–Pearson intervals, interval-simplex worst-case Bellman recursion, and plug-in versus robust policy evaluation. The mechanism manifested clearly: median interval width fitted an exponent of -0.498 versus the predicted -0.5, simultaneous coverage was 0.980–0.985 versus the 0.95 target, and robust certificates decreased from 0.984 to 0.853 while remaining above the true optimal value 0.728. The robust policy had slightly lower fresh unsafe reachability than the empirical plug-in baseline, but the certificate remained highly conservative and did not approach the 0.1 target.

Agent confidence: 8/10

Baseline: Fresh unsafe reachability for n=[100,200,400,800,1600]: [0.237, 0.247, 0.234, 0.239, 0.237].
Idea: Median interval widths=[0.174,0.120,0.086,0.061,0.043], observed ratios=[1.000,0.690,0.498,0.351,0.250] versus predicted sqrt-scaling ratios=[1.000,0.707,0.500,0.354,0.250]; simultaneous coverage=[0.985,0.980,0.985]; robust certificates=[0.984,0.954,0.909,0.897,0.853]; robust-policy unsafe reachability=[0.228,0.230,0.231,0.229,0.217].

Limitations: This is a finite toy Markov chain rather than a GRU or neural hidden-state system. Representation learning, training penalties, continuous actions, clustering error, nonstationarity, and Markov-abstraction misspecification were not tested. Coverage used 200 independent trials per reported sample size after runtime reduction, and certificate contraction was observed for one fixed-seed sequence rather than guaranteed for arbitrary newly collected datasets.

How to run: python3 pac_imdp_experiment.py

Stage 2 — Benchmark vs. tuned baseline (arXiv:2607.27908) Sep 2, 2026

Ahead of the baseline (−0.0%) but not statistically significant (p=1, wins 1 / 8 paired seeds).

Benchmark: Dynamics forecasting
Model: rnn_small
Paired seeds: 8
Baseline mean: 0.8055
Idea mean: 0.8055
Effect (Δ): -0 (−0.0%; negative = idea better)
Wins: 1 / 8 paired seeds
p-value: 1 (permutation test, 20 000 shuffles)
Smallest detectable effect: n/a
Mechanism: Not confirmed ✗
Practical effect: No effect
Baseline tuning: swept over 3 configs

Limitations:

The final run used the reduced benchmark budget of 400 training examples, 200 test examples, and 2 epochs after the nominal configuration exceeded 40 minutes. It tested only the built-in actuated-pendulum dynamics track, a single safety-penalty coefficient, coarse M=8 cells, and a short horizon H=3; no representation snapshotting, action masking, rollout violation-rate certificate, or larger-scale GRU training was tested.

How to run: python3 pac_imdp_bench.py

Verdict computed by deterministic test code from paired-seed statistics — not by the language model.

Stage 2 — Benchmark Aug 31, 2026 latest Failed ✗

Agent confidence: 9/10

Implemented PAC-IMDP interval estimation, worst-case Bellman recursion, and a training-time hidden-state safety penalty on the structurally matched dynamics track with a shared GRU/rnn_small architecture. The corrected 8-seed paired benchmark found no measurable task-metric effect: baseline MSE was 0.8055282905697823 and idea MSE was 0.8055282831192017, with paired delta -7.450580596923828e-09 and permutation p=1.0. The toy sanity check confirmed the theoretical -0.5 interval-width exponent, but trained hidden-state trajectories did not confirm it quantitatively, so the transfer is not a win.

Baseline: 8-seed mean test MSE 0.8055282905697823 (std 0.054040680527913894), best lr 0.0015; sweep means: 0.8369893431663513 at lr=0.0015, 1.014923483133316 at lr=0.003, 2.1336912512779236 at lr=0.006.
Idea: 8-seed mean test MSE 0.8055282831192017 (std 0.054040683770032884), best lr 0.0015; paired delta -7.450580596923828e-09, p=1.0, 1/8 paired wins, verdict no measurable effect.
Mechanism signature: map[prediction:Interval width scales as visits^-1/2 on trained GRU hidden trajectories. toy_sanity:map[confirmed:true expected:-0.5 fitted_exponent:-0.5026184327588654 median_width:[0.2873438408207492 0.14197919797868155 0.07131633132628293] n:[100 400 1600]] trained_confirmed:false trained_observed_exponents:[-0.8790135070455792 -0.8537251774108979 -0.8900873138500266 -0.795808084458392 -0.8452905428771581 -0.5056333577487622 -0.5725026332394434 -0.9192598456420297]]

Benchmark result