Эксперимент: Sound active-neuron pruning for SDP verification (#1284)

{ "worked": true, "confidence": 8, "verdict": "Built a readable interval-bound ReLU pruning MVP with exact fixed-sign substitutions and optional contribution pruning. Across 32 seeded networks, exact sign pruning reduced the SDP-variable proxy from 44 to 22 on average (50%), with zero fixed-substitution error and no violations among 5,000 independent sampled outputs; tolerance pruning was monotone, reaching 58.9% average reduction at tau=1.0. The claimed soundness/dimension-reduction phenomenon is real in this toy setting, but no actual SDP solver speedup or CNN verification win was established.", "metrics": { "baseline": "Mean proxy: 44 hidden-neuron variables; mean interval propagation time 0.000136 s; 0/5000 sampled soundness violations.", "idea": "Exact sign: 22 variables mean, 50.0% reduction, 11 fixed-sign neurons, exact certificate equality in all 32 cases. tau=0.1: 21.94 variables, 50.14% reduction; tau=0.3: 21.69, 50.71%; tau=1.0: 18.06, 58.95%. Fixed substitutions had maximum error 0.0 and the 6,561-point grid had 0 interval violations." }, "how_to_run": "/home/maxwelhelp/main/bin/python3 pruning_mvp.py && /home/maxwelhelp/main/bin/python3 mini_experiment.py", "files": [ "pruning_mvp.py", "mini_experiment.py", "results.json" ], "limitations": "This is not an SDP implementation and uses a variable-count proxy rather than constructing or solving SDP constraints. It tests small randomly generated 2D MLPs, not MNIST/CIFAR CNNs; no peak memory, solver failures, certified accuracy, or verification-time speedup was measured. The approximate tau modes report pruning counts but do not compute a relaxed certificate or quantify certificate-quality loss." }