"""Small, exact interval CEGAR abstraction for a 2-D neural-state-space toy. The affine map is an intentionally transparent surrogate for a saturated RNN cell: h' = A h + b. For axis-aligned boxes, interval propagation is exact for each coordinate's independent extrema. Therefore every edge generated by intersecting the resulting box with partition cells is conservative (up to floating point). """ import json, math, random from dataclasses import dataclass from pathlib import Path import numpy as np A = np.array([[.85, .15], [-.15, .85]], dtype=float) b = np.array([.20, 0.0]) DOMAIN = (-1.0, 1.0, -1.0, 1.0) UNSAFE_X = .72 @dataclass(frozen=True) class Cell: x0: float; x1: float; y0: float; y1: float def bounds(self): return np.array([self.x0,self.x1,self.y0,self.y1]) def center(self): return np.array([(self.x0+self.x1)/2,(self.y0+self.y1)/2]) def width(self): return max(self.x1-self.x0,self.y1-self.y0) def intersects(self, box, eps=1e-12): return (self.x1 >= box[0]-eps and self.x0 <= box[1]+eps and self.y1 >= box[2]-eps and self.y0 <= box[3]+eps) def unsafe(self): return self.x1 >= UNSAFE_X def affine_box(cell, margin=0.0): lo, hi = cell.bounds()[::2], cell.bounds()[1::2] # extrema of each affine coordinate over a rectangle outlo=[]; outhi=[] for row, bias in zip(A,b): mn = bias + sum(c*l if c >= 0 else c*h for c,l,h in zip(row,lo,hi)) mx = bias + sum(c*h if c >= 0 else c*l for c,l,h in zip(row,lo,hi)) outlo.append(mn-margin); outhi.append(mx+margin) return np.array([outlo[0], outhi[0], outlo[1], outhi[1]]) def uniform_partition(n): xs=np.linspace(DOMAIN[0],DOMAIN[1],n+1); ys=np.linspace(DOMAIN[2],DOMAIN[3],n+1) return [Cell(xs[i],xs[i+1],ys[j],ys[j+1]) for i in range(n) for j in range(n)] def split(c): xm=(c.x0+c.x1)/2; ym=(c.y0+c.y1)/2 return [Cell(c.x0,xm,c.y0,ym),Cell(c.x0,xm,ym,c.y1),Cell(xm,c.x1,c.y0,ym),Cell(xm,c.x1,ym,c.y1)] def build_graph(cells, margin=0.0): edges=[] for c in cells: box=affine_box(c,margin) edges.append([j for j,d in enumerate(cells) if d.intersects(box)]) return edges def reachable(cells, edges, initial=(.01,.01), steps=12): # Boundary ownership is immaterial because all intersecting cells are kept. cur={next(i for i,c in enumerate(cells) if c.x0 <= initial[0] <= c.x1 and c.y0 <= initial[1] <= c.y1)} levels=[set(cur)]; parents=[] for _ in range(steps): nxt=set(); par={} for i in cur: for j in edges[i]: nxt.add(j); par.setdefault(j,i) parents.append(par); levels.append(nxt); cur=nxt unsafe=sorted({i for lev in levels for i in lev if cells[i].unsafe()}) return levels, parents, unsafe def path_to_unsafe(levels, parents, target): # recover one shortest-ish abstract counterexample t=next(k for k,lev in enumerate(levels) if target in lev) path=[target] for k in range(t-1,-1,-1): path.append(parents[k][path[-1]]) return list(reversed(path)) def concrete_rollout(h=(.01,.01), steps=30): z=np.array(h,float); out=[z.copy()] for _ in range(steps): z=A@z+b; out.append(z.copy()) return np.array(out) def cegar(initial_n=4, rounds=8, margin=1e-10): cells=uniform_partition(initial_n); refinements=[] for _ in range(rounds): edges=build_graph(cells,margin); levels,parents,unsafe=reachable(cells,edges) if not unsafe: break path=path_to_unsafe(levels,parents,unsafe[0]) # Refine the widest cell on the counterexample, prioritizing its prefix. k=max(range(len(path)), key=lambda q: cells[path[q]].width()) chosen=path[k]; old=cells[chosen]; cells=cells[:chosen]+split(old)+cells[chosen+1:] refinements.append(old.width()) edges=build_graph(cells,margin); levels,parents,unsafe=reachable(cells,edges) return cells, levels, unsafe, refinements def sampled_soundness(n=4, margin=0.0, samples=20000, seed=7): rng=np.random.default_rng(seed); cells=uniform_partition(n); edges=build_graph(cells,margin) failures=0; checked=0 for i,c in enumerate(cells): pts=rng.uniform([c.x0,c.y0],[c.x1,c.y1],size=(max(1,samples//len(cells)),2)) nxt=pts@A.T+b for z in nxt: # The abstraction is over DOMAIN; successors outside it are # intentionally excluded from this conditional soundness check. if not (DOMAIN[0]-1e-12 <= z[0] <= DOMAIN[1]+1e-12 and DOMAIN[2]-1e-12 <= z[1] <= DOMAIN[3]+1e-12): continue js=[j for j,d in enumerate(cells) if d.x0-1e-12<=z[0]<=d.x1+1e-12 and d.y0-1e-12<=z[1]<=d.y1+1e-12] checked+=1 if not any(j in edges[i] for j in js): failures+=1 return checked, failures def run(): np.set_printoptions(precision=4,suppress=True) exact=concrete_rollout(); concrete_unsafe=bool(np.max(exact[:,0])>=UNSAFE_X) sweep=[] for n in [2,4,8,16]: cells=uniform_partition(n); ed=build_graph(cells); lev,_,u=reachable(cells,ed) area=sum((cells[i].x1-cells[i].x0)*(cells[i].y1-cells[i].y0) for i in u) sweep.append({'n':n,'cells':len(cells),'abstract_unsafe_cells':len(u), 'abstract_unsafe_area':area, 'abstract_unsafe_levels':sum(any(cells[i].unsafe() for i in q) for q in lev), 'concrete_unsafe':concrete_unsafe}) ce_cells,ce_lev,ce_u,ref=cegar() ce_area=sum((c.x1-c.x0)*(c.y1-c.y0) for i,c in enumerate(ce_cells) if i in ce_u) margins=[] for m in [0,.001,.01,.05]: checked,fail=sampled_soundness(8,m) edge_count=sum(len(x) for x in build_graph(uniform_partition(8),m)) margins.append({'margin':m,'checked':checked,'failures':fail,'coverage':1-fail/checked,'edges':edge_count}) result={'map_A':A.tolist(),'map_b':b.tolist(),'unsafe_x':UNSAFE_X, 'concrete_max_x':float(np.max(exact[:,0])),'predictions':{ 'P1_soundness': 'conditional in-domain sampled omissions are zero for every nonnegative margin', 'P2_uniform_resolution': 'area of reachable unsafe overapproximation decreases as cell width shrinks', 'P3_margin': 'adding interval margin cannot reduce edge count', 'P4_CEGAR_focus': 'CEGAR reaches comparable unsafe area with fewer cells than uniform n=16'}, 'uniform_sweep':sweep, 'cegar':{'final_cells':len(ce_cells),'unsafe_cells':len(ce_u),'unsafe_area':ce_area, 'unsafe_levels':sum(any(ce_cells[i].unsafe() for i in q) for q in ce_lev), 'refined_widths':ref},'margin_sweep':margins} Path('results.json').write_text(json.dumps(result,indent=2)) print(json.dumps(result,indent=2)) if __name__=='__main__': run()