1import json
 2import time
 3import numpy as np
 4from pruning_mvp import make_net, prune_report, output_interval, forward
 5
 6
 7def run(seed=123, n_cases=32):
 8    rng = np.random.default_rng(seed)
 9    rows = []
10    for case in range(n_cases):
11        W, b = make_net(seed=1000 + case)
12        center = rng.uniform(-0.5, 0.5, 2)
13        eps = 0.30
14        xlo, xhi = center - eps, center + eps
15        hiddenW, hiddenb = W[:-1], b[:-1]
16        base_vars = 2 * sum(len(v) for v in hiddenb)
17        t0 = time.perf_counter()
18        base_lo, base_hi = output_interval(W, b, xlo, xhi)
19        base_time = time.perf_counter() - t0
20        row = {'case': case, 'baseline_variables': base_vars,
21               'baseline_interval_seconds': base_time}
22        for tau, name in [(0.0, 'exact_sign'), (1e-6, 'tau_1e-6'),
23                          (0.1, 'tau_0.1'), (0.3, 'tau_0.3'), (1.0, 'tau_1.0')]:
24            t0 = time.perf_counter()
25            _, reports = prune_report(hiddenW, hiddenb, xlo, xhi, tau)
26            idea_time = time.perf_counter() - t0
27            retained = sum(r.retained for r in reports)
28            fixed = sum(r.active + r.inactive for r in reports)
29            row[name] = {'variables': 2 * retained, 'fixed_sign': fixed,
30                          'contribution_pruned': sum(r.pruned_contribution for r in reports),
31                          'seconds': idea_time,
32                          # Exact sign mode must preserve the interval exactly.
33                          'certificate_equal': bool(tau == 0.0 and np.array_equal(
34                              base_lo, output_interval(W, b, xlo, xhi)[0]) and
35                              np.array_equal(base_hi, output_interval(W, b, xlo, xhi)[1]))}
36        rows.append(row)
37
38    names = ['exact_sign', 'tau_1e-6', 'tau_0.1', 'tau_0.3', 'tau_1.0']
39    summary = {'cases': n_cases, 'baseline_variables_mean': float(np.mean([r['baseline_variables'] for r in rows])),
40               'baseline_seconds_mean': float(np.mean([r['baseline_interval_seconds'] for r in rows]))}
41    for name in names:
42        vals = [r[name] for r in rows]
43        summary[name] = {
44            'variables_mean': float(np.mean([v['variables'] for v in vals])),
45            'reduction_fraction_mean': float(np.mean([(r['baseline_variables'] - v['variables']) / r['baseline_variables'] for r, v in zip(rows, vals)])),
46            'fixed_sign_mean': float(np.mean([v['fixed_sign'] for v in vals])),
47            'contribution_pruned_mean': float(np.mean([v['contribution_pruned'] for v in vals])),
48            'certificate_equal_all': bool(all(v['certificate_equal'] for v in vals)) if name == 'exact_sign' else None,
49        }
50    # Independent point checks on the first case: output intervals remain sound.
51    W, b = make_net(seed=1000)
52    center = rows[0]['case'] * 0.0 + np.array([0.0, 0.0])
53    xlo, xhi = center - .3, center + .3
54    lo, hi = output_interval(W, b, xlo, xhi)
55    points = rng.uniform(xlo, xhi, (5000, 2))
56    violations = sum(np.any((forward(W, b, p) < lo - 1e-10) | (forward(W, b, p) > hi + 1e-10)) for p in points)
57    result = {'summary': summary, 'independent_soundness_points': 5000,
58              'independent_soundness_violations': int(violations)}
59    with open('results.json', 'w') as f:
60        json.dump(result, f, indent=2)
61    print(json.dumps(result, indent=2))
62
63
64if __name__ == '__main__':
65    run()