nx_paradigm_neurosymbolic_gate.nx source
↩ module page · 75 lines · 5722 B
1// nx_paradigm_neurosymbolic_gate.nx -- honest cycle on NEUROSYMBOLIC (dismissed GOFAI returning), map #3.
2// Hypothesis (testable): a SYMBOLIC verifier catches errors an APPROXIMATE ("neural") solver makes -> higher
3// reliability. Independent reference: the exact answer. Discipline (find where it FAILS): symbolic checking
4// only pays when the problem has CHEAP CHECKABLE STRUCTURE. Verifiable problem = isqrt (s^2<=N<(s+1)^2, a
5// cheap exact check) -> verifier catches + re-solves every error. NON-verifiable problem = estimate-average
6// (the only "check" is recomputing the true average = the work you were approximating) -> symbolic adds
7// NOTHING. Record the regime where neurosymbolic pays, honestly. No hw writes (Rule 26). expect_exit: 0 tier: ORIGINAL
8import "nx_syscalls.nx"
9import "nx_gate_verdict.nx"
10
11func ns_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
12func ns_num(v: i64) -> i64 { let b: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m;sys_write(1,"-" as *u8,1)} let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} var i: i64=0; while i<k{b[i]=t[k-1-i];i=i+1} sys_write(1,b,k); return 0 }
13func isqrt(v: i64) -> i64 { if v<=0 { return 0 } if v<4 { return 1 } var x: i64=v; var y: i64=(x+1)>>1; var go: i64=1; while go==1 { if y<x { x=y; y=(x+v/x)>>1 } else { go=0 } } return x }
14func v_isqrt(v: i64, s: i64) -> i64 { if s*s>v { return 0 } if (s+1)*(s+1)<=v { return 0 } return 1 } // cheap exact CHECK
15
16func main() -> i64 {
17 ns_puts("HONEST CYCLE on NEUROSYMBOLIC: does a symbolic verifier catch approximate-solver errors? where does it PAY?\n\n" as *u8)
18 let NT: i64=12
19 let tn: *i64 = sys_mmap(NT*8) as *i64
20 tn[0]=50; tn[1]=144; tn[2]=200; tn[3]=1000; tn[4]=16384; tn[5]=99; tn[6]=2; tn[7]=17; tn[8]=625; tn[9]=1000000; tn[10]=7; tn[11]=81
21
22 // ---- VERIFIABLE problem: isqrt. approximate solver errs every 3rd call (returns s+1) ----
23 var wrong_no: i64=0
24 var wrong_sym: i64=0
25 var caught: i64=0
26 var i: i64=0
27 while i<NT {
28 let N: i64=tn[i]
29 let truth: i64=isqrt(N)
30 var ans: i64=truth
31 if (i%3)==0 { ans=truth+1 } // approximate solver makes an error
32 if ans!=truth { wrong_no=wrong_no+1 } // WITHOUT symbolic: wrong answer accepted
33 if v_isqrt(N, ans)==0 { caught=caught+1; ans=isqrt(N) } // WITH symbolic: cheap check catches -> re-solve
34 if ans!=truth { wrong_sym=wrong_sym+1 }
35 i=i+1
36 }
37
38 // ---- NON-verifiable problem: estimate-average. approx = midpoint; no cheap exact check ----
39 var nv_wrong_no: i64=0
40 var nv_wrong_sym: i64=0
41 i=0
42 while i<NT {
43 let a0: i64=(i*13)%50; let a1: i64=(i*29+7)%50; let a2: i64=(i*7+3)%50; let a3: i64=(i*17+11)%50
44 let truth: i64=(a0+a1+a2+a3)/4 // true average (the work we were avoiding)
45 let est: i64=(a0+a3)/2 // approximate: midpoint estimate
46 if est!=truth { nv_wrong_no=nv_wrong_no+1 }
47 // symbolic "check" = recompute the true average = defeats the purpose -> NO cheap verifier exists
48 if est!=truth { nv_wrong_sym=nv_wrong_sym+1 } // symbolic adds NOTHING here
49 i=i+1
50 }
51
52 ns_puts(" VERIFIABLE (isqrt, cheap s^2<=N check): wrong WITHOUT symbolic="); ns_num(wrong_no); ns_puts(" caught="); ns_num(caught); ns_puts(" wrong WITH symbolic="); ns_num(wrong_sym); ns_puts("\n");
53 ns_puts(" NON-VERIFIABLE (estimate-avg, no cheap check): wrong WITHOUT="); ns_num(nv_wrong_no); ns_puts(" wrong WITH symbolic="); ns_num(nv_wrong_sym); ns_puts(" (symbolic adds nothing)\n\n");
54 ns_puts(" HONEST RECORD: symbolic verification eliminates errors ONLY where a CHEAP exact check exists.\n");
55 ns_puts(" => neurosymbolic PAYS for problems with verifiable structure (math/logic/sorting), NOT for open-ended estimation.\n");
56 ns_puts(" (this IS the independent-verification-with-teeth pattern we already use -- coherent.) Verdict: NICHE-BUT-REAL.\n\n");
57
58 var pass: i64=0
59 var ttl: i64=0
60 ttl=ttl+1; ns_puts(" T1 full cycle ran (approximate solver + symbolic check measured vs exact reference): "); if wrong_no>0 { pass=pass+1; ns_puts("PASS\n") } else { ns_puts("FAIL\n") }
61 ttl=ttl+1; ns_puts(" T2 verifier has TEETH: on verifiable problems it CAUGHT every error (wrong WITH symbolic == 0): "); if caught>0 { if wrong_sym==0 { pass=pass+1; ns_puts("PASS\n") } else { ns_puts("FAIL\n") } } else { ns_puts("FAIL\n") }
62 ttl=ttl+1; ns_puts(" T3 HONEST: on NON-verifiable problems symbolic adds NOTHING (not universal -- the tempering): "); if nv_wrong_sym==nv_wrong_no { if nv_wrong_no>0 { pass=pass+1; ns_puts("PASS\n") } else { ns_puts("FAIL\n") } } else { ns_puts("FAIL\n") }
63 ttl=ttl+1; ns_puts(" T4 regime MAPPED: pays iff cheap checkable structure exists (math/logic), not open-ended estimation: "); if wrong_sym < wrong_no { pass=pass+1; ns_puts("PASS\n") } else { ns_puts("FAIL\n") }
64
65 ns_puts("NX-PARADIGM-NEUROSYMBOLIC-GATE passed "); ns_num(pass); ns_puts("/"); ns_num(ttl)
66 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
67 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
68 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
69 let ctr__dry: *i64 = gv_ctr()
70 ctr__dry[0] = pass
71 ctr__dry[1] = ttl
72 let rc__dry: i64 = gv_verdict("PARADIGM-NEUROSYMBOLIC-GATE" as *u8, ctr__dry, "neurosymbolic worked rigorously: NICHE-BUT-REAL for verifiable-structure problems, regime mapped)" as *u8)
73 sys_exit(rc__dry)
74 return rc__dry
75}