Эксперимент: CEGAR-certified latent-state abstraction (#774)

{ "worked": true, "confidence": 8, "verdict": "Built a conservative axis-aligned latent-state abstraction with exact interval propagation for a 2D affine damped oscillator, plus uniform refinement, CEGAR refinement, sampled soundness checks, and parameter sweeps. The mechanism manifested: in-domain sampled transition omissions were 0/19,215 for every tested margin, reachable unsafe area decreased from 2.0 at 2×2 to 0.40625 at 16×16, and the interval margin increased edges from 256 to 354. CEGAR reached unsafe area 0.390625 with 160 cells versus 0.40625 with 256 uniformly refined cells, providing a promising focused-refinement signal, though not evidence for a neural RNN at scale.", "metrics": { "baseline": "Uniform partitions: n=2/4/8/16 gave reachable unsafe areas 2.0/0.75/0.625/0.40625 with 4/16/64/256 cells.", "idea": "CEGAR: at 48 refinement rounds used 160 cells and gave unsafe area 0.390625; sampled soundness had 0 omissions among 19,215 in-domain transitions. Margin sweep: edges 256,256,256,354 for margins 0,0.001,0.01,0.05." }, "how_to_run": "/home/maxwelhelp/main/bin/python3 cegar_abstraction.py", "files": [ "cegar_abstraction.py", "results.json" ], "limitations": "The experiment uses an affine 2D state-space map rather than a trained GRU/RNN, and interval propagation is exact only for this affine rectangular case. Soundness was additionally checked by finite random sampling and conditioned on successors remaining inside the declared bounded domain; no temporal-logic parser, constrained optimizer, learned model, or high-dimensional scalability test was included." }