Spaces:
Sleeping
Sleeping
Update app.py
Browse files
app.py
CHANGED
|
@@ -1,14 +1,42 @@
|
|
| 1 |
#!/usr/bin/env python3
|
| 2 |
"""
|
| 3 |
-
PRACTICALITY SYSTEM
|
| 4 |
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 5 |
-
|
| 6 |
-
|
| 7 |
-
|
| 8 |
-
|
| 9 |
-
|
| 10 |
-
|
| 11 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 12 |
"""
|
| 13 |
|
| 14 |
import time, random, math, threading, warnings
|
|
@@ -26,7 +54,7 @@ import gradio as gr
|
|
| 26 |
warnings.filterwarnings("ignore")
|
| 27 |
USE_GPU = torch.cuda.is_available()
|
| 28 |
DEVICE = torch.device("cuda" if USE_GPU else "cpu")
|
| 29 |
-
print(f"[SYSTEM
|
| 30 |
|
| 31 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 32 |
# SECTION 1: CONSTANTS
|
|
@@ -34,15 +62,16 @@ print(f"[SYSTEM 18.0] Compute: {DEVICE.type.upper()} | Engine: Masked Deduction
|
|
| 34 |
SOLVE_THRESHOLD = 0.05
|
| 35 |
VERIFY_G1_THRESHOLD = 0.08
|
| 36 |
VERIFY_G2_TOLERANCE = 1e-3
|
| 37 |
-
|
| 38 |
-
DEDUCE_ADAM_STEPS = 30 # GPU variable-filling steps (strictly masked)
|
| 39 |
N_MPRT_EXPLORE = 1000 # Initial bounding box sampling only
|
| 40 |
PROJECTION_CACHE: Dict = {}
|
| 41 |
-
|
| 42 |
-
|
|
|
|
|
|
|
| 43 |
CE_EARN_RATIO = 0.90
|
| 44 |
SCOUT_CE_THRESHOLD = 0.5
|
| 45 |
-
BRANCH_WIDTH =
|
| 46 |
|
| 47 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 48 |
# SECTION 2: INTERVAL ARITHMETIC (HC4)
|
|
@@ -118,7 +147,7 @@ def _hc4(box,constraints):
|
|
| 118 |
return cur
|
| 119 |
|
| 120 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 121 |
-
# SECTION 3: PSL 2.0 PARSER & COMPILER
|
| 122 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 123 |
@dataclass
|
| 124 |
class PSLVar: name:str; lo:float; hi:float
|
|
@@ -299,27 +328,6 @@ class Problem:
|
|
| 299 |
self.compiled_constraints=[compile_mc(c.kind,c.expr,c.direction,self.variables,c.weight,c.scope,c.branches) for c in self.constraints]
|
| 300 |
self.var_idx = {v: i for i, v in enumerate(self.variables)}
|
| 301 |
|
| 302 |
-
def constraint_energy(self,b:Dict[str,float]) -> float:
|
| 303 |
-
total=0.0
|
| 304 |
-
for mc in self.compiled_constraints:
|
| 305 |
-
if getattr(mc,'weight',1.0)==0.0: continue
|
| 306 |
-
if mc.kind=="or_eq":
|
| 307 |
-
vals=[]
|
| 308 |
-
for bmc in mc.branches:
|
| 309 |
-
if bmc.fast_pt:
|
| 310 |
-
try: vals.append(abs(float(bmc.fast_pt(*[b.get(v,0.0) for v in bmc.syms_used]))))
|
| 311 |
-
except: pass
|
| 312 |
-
total+=(min(vals)*mc.weight) if vals else 1.0
|
| 313 |
-
else:
|
| 314 |
-
if mc.fast_pt is None: total+=1.0; continue
|
| 315 |
-
try:
|
| 316 |
-
val=float(mc.fast_pt(*[b.get(v,0.0) for v in mc.syms_used]))
|
| 317 |
-
total+=(abs(val) if mc.kind=="equality" else max(0.0,-val) if mc.direction=="geq" else max(0.0,val))*mc.weight
|
| 318 |
-
except: total+=1.0
|
| 319 |
-
for v,(lo,hi) in self.bounds.items():
|
| 320 |
-
bv=b.get(v,0.0); total+=max(0.0,lo-bv)+max(0.0,bv-hi)
|
| 321 |
-
return total
|
| 322 |
-
|
| 323 |
def tensor_energy(self, X: torch.Tensor) -> torch.Tensor:
|
| 324 |
is_batched = (X.dim() == 2)
|
| 325 |
total = torch.zeros(X.shape[0] if is_batched else 1, device=DEVICE, dtype=torch.float32)
|
|
@@ -356,10 +364,8 @@ class L9Certificate: residual_ce:float; dominant_vars:List[str]; dominant_exprs:
|
|
| 356 |
|
| 357 |
def _batched_deduce_and_evaluate(problem: Problem, hyps: List['Hypothesis']) -> List[Tuple[Dict, float, List[str]]]:
|
| 358 |
"""
|
| 359 |
-
|
| 360 |
-
|
| 361 |
-
Uses PyTorch to fill in unpinned continuous variables (variable filling).
|
| 362 |
-
Uses loss.backward() to find the exact structural tensions (Oracle).
|
| 363 |
"""
|
| 364 |
if not hyps: return []
|
| 365 |
B = len(hyps); V = len(problem.variables)
|
|
@@ -410,7 +416,6 @@ def _batched_deduce_and_evaluate(problem: Problem, hyps: List['Hypothesis']) ->
|
|
| 410 |
results = []
|
| 411 |
for i in range(B):
|
| 412 |
final_b = {problem.variables[j]: float(X_vals[i, j]) for j in range(V)}
|
| 413 |
-
# Oracle: which variables have the most structural tension right now?
|
| 414 |
var_tensions = {problem.variables[j]: float(grads[i, j]) for j in range(V)}
|
| 415 |
dom_vars = sorted(var_tensions.keys(), key=lambda v: -var_tensions[v])[:3]
|
| 416 |
results.append((final_b, float(ce_vals[i]), dom_vars))
|
|
@@ -484,10 +489,9 @@ class StructuralModel: best_binding:Dict[str,float]; best_ce:float; failure_patt
|
|
| 484 |
|
| 485 |
def _make_hyp(hid,binding,h_type,claim,derivation,pinned,free,conf): return Hypothesis(hid=hid,binding=binding,h_type=h_type,claim=claim,derivation=derivation,pinned_vars=pinned,free_vars=free,confidence=conf)
|
| 486 |
|
| 487 |
-
#
|
| 488 |
def _hyp_continuous(p,bt,a,m): return [_make_hyp("cnt",bt.binding,"continuous","Manifold",[],{},p.variables,0.45)]
|
| 489 |
def _hyp_discrete(p,bt,a,m):
|
| 490 |
-
# Use internal HC4 deduction specifically on scope boundaries
|
| 491 |
b = dict(bt.binding); pinned = {}
|
| 492 |
for sn in p.scope_order:
|
| 493 |
svars = p.scope_vars.get(sn, [])
|
|
@@ -505,7 +509,6 @@ def _hyp_quadratic(p,bt,a,m):
|
|
| 505 |
hyps=[]; b=dict(bt.binding)
|
| 506 |
if bt.l9 and bt.l9.dominant_vars:
|
| 507 |
for v in bt.l9.dominant_vars[:2]:
|
| 508 |
-
# Pin the exact dominant variable to its current spot to force others to align around it
|
| 509 |
hyps.append(_make_hyp(f"qua_{v}",b,"quadratic",f"Root({v})",[],{v:b[v]},p.variables,0.70))
|
| 510 |
return hyps
|
| 511 |
|
|
@@ -576,7 +579,6 @@ def _hyp_atomic(p,bt,a,m):
|
|
| 576 |
if hyps: break
|
| 577 |
return hyps
|
| 578 |
|
| 579 |
-
# Pass-through exploratory/diagnostic axioms (empty pinned_vars)
|
| 580 |
def _hyp_metric(p,bt,a,m): return [_make_hyp("met",bt.binding,"metric","Radial",[],{},p.variables,0.75)]
|
| 581 |
def _hyp_ordered(p,bt,a,m): return [_make_hyp("ord",bt.binding,"ordered","OrderBal",[],{},p.variables,0.67)]
|
| 582 |
def _hyp_monotone(p,bt,a,m): return [_make_hyp("mon",bt.binding,"monotone","MonoPath",[],{},p.variables,0.67)]
|
|
@@ -610,10 +612,58 @@ AXIOM_CONSTRUCTORS={
|
|
| 610 |
}
|
| 611 |
|
| 612 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 613 |
-
# SECTION 6: TRACER + SEEDER (
|
| 614 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 615 |
class CreativeSeeder:
|
| 616 |
-
def
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 617 |
results=[]
|
| 618 |
for (a,c) in ADJACENT_CONTRADICTIONS:
|
| 619 |
for b1 in ALL_AXIOMS:
|
|
@@ -661,16 +711,20 @@ class CreativeSeeder:
|
|
| 661 |
if child: child.ray_id=f"RES_{child.ray_id}"; results.append(child)
|
| 662 |
return results
|
| 663 |
|
|
|
|
|
|
|
| 664 |
class SequenceRayTracer:
|
| 665 |
def trace(self, axl_def, base_problem):
|
| 666 |
-
|
|
|
|
|
|
|
| 667 |
init_b, init_ce = _mprt_sample(base_problem, {v:IV(*base_problem.bounds[v]) for v in base_problem.variables}, N_MPRT_EXPLORE)
|
| 668 |
seed_baton = Baton(binding=init_b, ce=init_ce, ray_id="SEED", l9=L9Certificate(init_ce, base_problem.variables[:3], []))
|
| 669 |
|
| 670 |
queues={
|
| 671 |
"core": [AxiomRay([a], f"S{i}", "seed", ce_prior=init_ce) for i,a in enumerate(ALL_AXIOMS)],
|
| 672 |
-
"explore":
|
| 673 |
-
"genetic":
|
| 674 |
}
|
| 675 |
for q in queues.values(): random.shuffle(q)
|
| 676 |
queue_order = ["core", "explore", "genetic"]; q_idx = 0
|
|
@@ -693,26 +747,22 @@ class SequenceRayTracer:
|
|
| 693 |
|
| 694 |
t0 = time.time(); historical_batons = list(baton_registry.values())
|
| 695 |
|
| 696 |
-
# Step 1: Constructors generate naked hypotheses + masks
|
| 697 |
batch_hyps = []
|
| 698 |
for i, ray in enumerate(batch_rays):
|
| 699 |
p_baton = ray.baton or seed_baton
|
| 700 |
hyps = AXIOM_CONSTRUCTORS[ray.sequence[-1]](base_problem, p_baton, historical_batons, model)
|
| 701 |
if not hyps: hyps = [_make_hyp("fb", p_baton.binding, "fallback", "Pass", [], {}, base_problem.variables, 0.1)]
|
| 702 |
-
batch_hyps.append((i, hyps[0]))
|
| 703 |
|
| 704 |
-
# Step 2: Masked Deduction + Diagnostic Oracle
|
| 705 |
evaluated_results = _batched_deduce_and_evaluate(base_problem, [h for _, h in batch_hyps])
|
| 706 |
|
| 707 |
solved = False
|
| 708 |
elapsed_ms = (time.time() - t0) * 1000 / len(batch_rays)
|
| 709 |
|
| 710 |
-
# Step 3: Verify and Route
|
| 711 |
for (ray_idx, hyp), (final_b, final_ce, dom_vars) in zip(batch_hyps, evaluated_results):
|
| 712 |
ray = batch_rays[ray_idx]
|
| 713 |
parent_ce_val = (ray.baton or seed_baton).ce
|
| 714 |
|
| 715 |
-
# Verify Gate (For anchors)
|
| 716 |
g1_pass = final_ce < VERIFY_G1_THRESHOLD
|
| 717 |
g2_pass = True
|
| 718 |
for inv in axl_def.anchors:
|
|
@@ -725,11 +775,13 @@ class SequenceRayTracer:
|
|
| 725 |
except: g2_pass=False
|
| 726 |
|
| 727 |
overall_pass = g1_pass and g2_pass
|
| 728 |
-
|
|
|
|
|
|
|
|
|
|
| 729 |
|
| 730 |
out_baton = Baton(binding=final_b, ce=final_ce, l9=L9Certificate(final_ce, dom_vars, []))
|
| 731 |
|
| 732 |
-
improved = final_ce < best_ce
|
| 733 |
if improved:
|
| 734 |
best_ce=final_ce; best_binding=final_b; stall_counter=0
|
| 735 |
baton_registry[ray.ray_id] = out_baton; successful_rays.append(ray)
|
|
@@ -740,25 +792,28 @@ class SequenceRayTracer:
|
|
| 740 |
scout_earned = (ray.ray_type == "scout" and final_ce < SCOUT_CE_THRESHOLD)
|
| 741 |
|
| 742 |
if earned or scout_earned:
|
| 743 |
-
new_children = []
|
| 744 |
-
|
| 745 |
-
|
| 746 |
-
|
| 747 |
-
|
|
|
|
|
|
|
|
|
|
| 748 |
|
| 749 |
-
inv =
|
| 750 |
if inv: new_children.append(inv)
|
| 751 |
|
| 752 |
if len(successful_rays) >= 2:
|
| 753 |
candidates = [r for r in successful_rays if r.ray_id != ray.ray_id]
|
| 754 |
if candidates:
|
| 755 |
partner = random.choice(candidates); ba = baton_registry.get(ray.ray_id, out_baton); bb = baton_registry.get(partner.ray_id, out_baton)
|
| 756 |
-
new_children.extend(
|
| 757 |
|
| 758 |
-
new_children.extend(
|
| 759 |
|
| 760 |
for child in new_children:
|
| 761 |
-
if child.ray_type in ("seed", "branch"): queues["core"].append(child)
|
| 762 |
elif child.ray_type in ("scout", "tension"): queues["explore"].append(child)
|
| 763 |
elif child.ray_type in ("recombine", "invert"): queues["genetic"].append(child)
|
| 764 |
|
|
@@ -766,7 +821,7 @@ class SequenceRayTracer:
|
|
| 766 |
|
| 767 |
if solved: break
|
| 768 |
|
| 769 |
-
return best_binding, best_ce,
|
| 770 |
|
| 771 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 772 |
# SECTION 7: AXL PROBLEMS
|
|
@@ -813,7 +868,7 @@ def background_worker():
|
|
| 813 |
base_prob = build_base_problem(axl_def)
|
| 814 |
|
| 815 |
t0 = time.time()
|
| 816 |
-
binding, ce, history = tracer.trace(axl_def, base_prob)
|
| 817 |
ms = round((time.time() - t0) * 1000)
|
| 818 |
|
| 819 |
with STATE_LOCK:
|
|
@@ -822,7 +877,8 @@ def background_worker():
|
|
| 822 |
"ce": ce,
|
| 823 |
"solved": ce < SOLVE_THRESHOLD,
|
| 824 |
"ms": ms,
|
| 825 |
-
"
|
|
|
|
| 826 |
})
|
| 827 |
if len(RUN_LOG) > 30: RUN_LOG.pop()
|
| 828 |
|
|
@@ -830,13 +886,13 @@ def toggle_engine():
|
|
| 830 |
global IS_RUNNING
|
| 831 |
IS_RUNNING = not IS_RUNNING
|
| 832 |
if IS_RUNNING: threading.Thread(target=background_worker, daemon=True).start()
|
| 833 |
-
return "βΉ STOP
|
| 834 |
|
| 835 |
def refresh_dashboard():
|
| 836 |
with STATE_LOCK:
|
| 837 |
if not RUN_LOG: return "<i>No runs yet. Click Start Engine.</i>"
|
| 838 |
html = "<table style='width:100%; border-collapse:collapse; text-align:left;'>"
|
| 839 |
-
html += "<tr style='border-bottom:1px solid #444'><th>Problem</th><th>CE</th><th>Status</th><th>Speed</th><th>
|
| 840 |
for r in RUN_LOG:
|
| 841 |
color = "#4CAF50" if r["solved"] else "#FF9800"
|
| 842 |
html += f"<tr style='border-bottom:1px solid #222'>"
|
|
@@ -844,14 +900,14 @@ def refresh_dashboard():
|
|
| 844 |
html += f"<td style='padding:5px; color:{color}; font-weight:bold'>{r['ce']:.5f}</td>"
|
| 845 |
html += f"<td style='padding:5px; color:{color}'>{'SOLVED' if r['solved'] else 'SEARCHING'}</td>"
|
| 846 |
html += f"<td style='padding:5px; color:#888'>{r['ms']}ms</td>"
|
| 847 |
-
html += f"<td style='padding:5px; color:#888'>{r['
|
| 848 |
html += "</table>"
|
| 849 |
return html
|
| 850 |
|
| 851 |
with gr.Blocks(theme=gr.themes.Monochrome(text_size="sm")) as demo:
|
| 852 |
-
gr.Markdown(f"# β Practicality
|
| 853 |
-
gr.Markdown(f"**Compute Node:** `{DEVICE.type.upper()}` | **Engine:** `
|
| 854 |
-
btn_toggle = gr.Button("βΆ START
|
| 855 |
html_output = gr.HTML(refresh_dashboard())
|
| 856 |
|
| 857 |
btn_toggle.click(toggle_engine, inputs=None, outputs=btn_toggle)
|
|
|
|
| 1 |
#!/usr/bin/env python3
|
| 2 |
"""
|
| 3 |
+
PRACTICALITY SYSTEM 19.1 β THE NEURO-SYMBOLIC ENZYME
|
| 4 |
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 5 |
+
AIM:
|
| 6 |
+
To extract a true, LLM-readable structural isomorphism of a mathematical problem.
|
| 7 |
+
Previous iterations suffered from the "Clever Hans" effect: a powerful continuous
|
| 8 |
+
optimizer (Adam) was quietly solving the problem and letting irrelevant discrete
|
| 9 |
+
logic (Axioms) take the credit.
|
| 10 |
+
|
| 11 |
+
The goal of 19.1 is strict credit assignment. If the sequence trace says
|
| 12 |
+
[SYMMETRIC β MONOTONE_PRODUCT β COMPOSITE] solved the problem, it must be a
|
| 13 |
+
mathematical guarantee that those geometric manipulations isolated the exact
|
| 14 |
+
basin of attraction.
|
| 15 |
+
|
| 16 |
+
THE CURRENT SYSTEM (1.5M Scale):
|
| 17 |
+
We stripped the safety nets and replaced them with a "Naked Evaluation" framework,
|
| 18 |
+
augmented by biological design patterns (Enzyme catalysis & Allosteric feedback).
|
| 19 |
+
|
| 20 |
+
IMPLEMENTATION AT A GLANCE:
|
| 21 |
+
1. NAKED EVALUATION (The Masked Compiler):
|
| 22 |
+
Axioms no longer output fuzzy suggestions. They compile into strict mathematical
|
| 23 |
+
masks (`pinned_vars`). PyTorch is allowed to fill in the continuous blanks using
|
| 24 |
+
Adam, but the gradients for pinned variables are strictly zeroed (`X.grad *= mask`).
|
| 25 |
+
PyTorch is locked in a cage; it cannot undo the Axiom's structural claim.
|
| 26 |
+
|
| 27 |
+
2. BIDIRECTIONAL SEARCH (The Active Site):
|
| 28 |
+
Instead of just forward-chaining, we spawn `RAY_TARGET` seeds by parsing the
|
| 29 |
+
target PSL anchors (the final goal state). The system builds the logical chain
|
| 30 |
+
from both the substrate (initial variables) and the product (anchor states),
|
| 31 |
+
meeting in the middle.
|
| 32 |
+
|
| 33 |
+
3. INTELLIGENT CHAINING (Allosteric Feedback):
|
| 34 |
+
We use PyTorch's `loss.backward()` NOT as an optimizer, but as a Diagnostic Oracle.
|
| 35 |
+
If a hypothesis fails, the gradients reveal exact structural tension.
|
| 36 |
+
- 1 variable in tension = Isolated failure β Chain heavily biases Point Axioms (ATOMIC)
|
| 37 |
+
- 2 variables in tension= Relational failureβ Chain heavily biases Pair Axioms (SYMMETRIC)
|
| 38 |
+
- 3+ variables in tension= Systemic failure β Chain heavily biases Global Axioms (CONSERVED)
|
| 39 |
+
The continuous math directly biases the discrete Markov transition matrix.
|
| 40 |
"""
|
| 41 |
|
| 42 |
import time, random, math, threading, warnings
|
|
|
|
| 54 |
warnings.filterwarnings("ignore")
|
| 55 |
USE_GPU = torch.cuda.is_available()
|
| 56 |
DEVICE = torch.device("cuda" if USE_GPU else "cpu")
|
| 57 |
+
print(f"[SYSTEM 19.1] Compute: {DEVICE.type.upper()} | Engine: Neuro-Symbolic Enzyme (1.5M Scale)")
|
| 58 |
|
| 59 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 60 |
# SECTION 1: CONSTANTS
|
|
|
|
| 62 |
SOLVE_THRESHOLD = 0.05
|
| 63 |
VERIFY_G1_THRESHOLD = 0.08
|
| 64 |
VERIFY_G2_TOLERANCE = 1e-3
|
| 65 |
+
DEDUCE_ADAM_STEPS = 25 # Masked variable filling only
|
|
|
|
| 66 |
N_MPRT_EXPLORE = 1000 # Initial bounding box sampling only
|
| 67 |
PROJECTION_CACHE: Dict = {}
|
| 68 |
+
|
| 69 |
+
# MASSIVE SCALE PARAMETERS
|
| 70 |
+
MAX_TOTAL_RAYS = 1_500_000
|
| 71 |
+
RAY_BATCH_SIZE = 4096
|
| 72 |
CE_EARN_RATIO = 0.90
|
| 73 |
SCOUT_CE_THRESHOLD = 0.5
|
| 74 |
+
BRANCH_WIDTH = 4
|
| 75 |
|
| 76 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 77 |
# SECTION 2: INTERVAL ARITHMETIC (HC4)
|
|
|
|
| 147 |
return cur
|
| 148 |
|
| 149 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 150 |
+
# SECTION 3: PSL 2.0 PARSER & COMPILER
|
| 151 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 152 |
@dataclass
|
| 153 |
class PSLVar: name:str; lo:float; hi:float
|
|
|
|
| 328 |
self.compiled_constraints=[compile_mc(c.kind,c.expr,c.direction,self.variables,c.weight,c.scope,c.branches) for c in self.constraints]
|
| 329 |
self.var_idx = {v: i for i, v in enumerate(self.variables)}
|
| 330 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 331 |
def tensor_energy(self, X: torch.Tensor) -> torch.Tensor:
|
| 332 |
is_batched = (X.dim() == 2)
|
| 333 |
total = torch.zeros(X.shape[0] if is_batched else 1, device=DEVICE, dtype=torch.float32)
|
|
|
|
| 364 |
|
| 365 |
def _batched_deduce_and_evaluate(problem: Problem, hyps: List['Hypothesis']) -> List[Tuple[Dict, float, List[str]]]:
|
| 366 |
"""
|
| 367 |
+
Naked Evaluation: Axioms map masks. HC4 bounds. Adam fills ONLY continuous gaps.
|
| 368 |
+
PyTorch loss.backward() acts purely as a gradient oracle to feed the Markov Chain.
|
|
|
|
|
|
|
| 369 |
"""
|
| 370 |
if not hyps: return []
|
| 371 |
B = len(hyps); V = len(problem.variables)
|
|
|
|
| 416 |
results = []
|
| 417 |
for i in range(B):
|
| 418 |
final_b = {problem.variables[j]: float(X_vals[i, j]) for j in range(V)}
|
|
|
|
| 419 |
var_tensions = {problem.variables[j]: float(grads[i, j]) for j in range(V)}
|
| 420 |
dom_vars = sorted(var_tensions.keys(), key=lambda v: -var_tensions[v])[:3]
|
| 421 |
results.append((final_b, float(ce_vals[i]), dom_vars))
|
|
|
|
| 489 |
|
| 490 |
def _make_hyp(hid,binding,h_type,claim,derivation,pinned,free,conf): return Hypothesis(hid=hid,binding=binding,h_type=h_type,claim=claim,derivation=derivation,pinned_vars=pinned,free_vars=free,confidence=conf)
|
| 491 |
|
| 492 |
+
# Strict Axiomatic Structural Compilers
|
| 493 |
def _hyp_continuous(p,bt,a,m): return [_make_hyp("cnt",bt.binding,"continuous","Manifold",[],{},p.variables,0.45)]
|
| 494 |
def _hyp_discrete(p,bt,a,m):
|
|
|
|
| 495 |
b = dict(bt.binding); pinned = {}
|
| 496 |
for sn in p.scope_order:
|
| 497 |
svars = p.scope_vars.get(sn, [])
|
|
|
|
| 509 |
hyps=[]; b=dict(bt.binding)
|
| 510 |
if bt.l9 and bt.l9.dominant_vars:
|
| 511 |
for v in bt.l9.dominant_vars[:2]:
|
|
|
|
| 512 |
hyps.append(_make_hyp(f"qua_{v}",b,"quadratic",f"Root({v})",[],{v:b[v]},p.variables,0.70))
|
| 513 |
return hyps
|
| 514 |
|
|
|
|
| 579 |
if hyps: break
|
| 580 |
return hyps
|
| 581 |
|
|
|
|
| 582 |
def _hyp_metric(p,bt,a,m): return [_make_hyp("met",bt.binding,"metric","Radial",[],{},p.variables,0.75)]
|
| 583 |
def _hyp_ordered(p,bt,a,m): return [_make_hyp("ord",bt.binding,"ordered","OrderBal",[],{},p.variables,0.67)]
|
| 584 |
def _hyp_monotone(p,bt,a,m): return [_make_hyp("mon",bt.binding,"monotone","MonoPath",[],{},p.variables,0.67)]
|
|
|
|
| 612 |
}
|
| 613 |
|
| 614 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 615 |
+
# SECTION 6: TRACER + SEEDER (Intelligent & Bidirectional Search)
|
| 616 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 617 |
class CreativeSeeder:
|
| 618 |
+
def target_seeds(self, anchors: List[AXLInvariant]) -> List[AxiomRay]:
|
| 619 |
+
"""BIDIRECTIONAL SEARCH: Spawn Axioms based explicitly on the PSL goal state."""
|
| 620 |
+
seeds = []
|
| 621 |
+
for a in anchors:
|
| 622 |
+
if "*" in a.expr and "**" not in a.expr:
|
| 623 |
+
seeds.append(AxiomRay([Axiom.BILINEAR], f"TGT_BIL_{a.name}", "target"))
|
| 624 |
+
seeds.append(AxiomRay([Axiom.MONOTONE_PRODUCT], f"TGT_MPR_{a.name}", "target"))
|
| 625 |
+
elif "**2" in a.expr:
|
| 626 |
+
seeds.append(AxiomRay([Axiom.QUADRATIC], f"TGT_QUA_{a.name}", "target"))
|
| 627 |
+
seeds.append(AxiomRay([Axiom.METRIC], f"TGT_MET_{a.name}", "target"))
|
| 628 |
+
elif "+" in a.expr:
|
| 629 |
+
seeds.append(AxiomRay([Axiom.CONSERVED], f"TGT_CSV_{a.name}", "target"))
|
| 630 |
+
return seeds
|
| 631 |
+
|
| 632 |
+
def intelligent_branch(self, ray, out_baton, remaining_axioms, branch_width):
|
| 633 |
+
"""
|
| 634 |
+
ALLOSTERIC FEEDBACK: Uses the PyTorch Gradient Oracle (dominant_vars)
|
| 635 |
+
to bias the discrete Markov transition matrix.
|
| 636 |
+
"""
|
| 637 |
+
dom_vars = out_baton.l9.dominant_vars if out_baton.l9 else []
|
| 638 |
+
n_dom = len(dom_vars)
|
| 639 |
+
|
| 640 |
+
# Map Axioms to the type of structural tension they resolve
|
| 641 |
+
isolated = {Axiom.ATOMIC, Axiom.EXTREMAL, Axiom.MUTABLE, Axiom.DUALITY, Axiom.LOCALITY}
|
| 642 |
+
relational = {Axiom.SYMMETRIC, Axiom.BILINEAR, Axiom.MONOTONE_PRODUCT, Axiom.ORDERED, Axiom.METRIC, Axiom.INJECTIVE}
|
| 643 |
+
systemic = {Axiom.CONSERVED, Axiom.NETWORK, Axiom.HOLISM, Axiom.COMPOSITE, Axiom.ENTROPY}
|
| 644 |
+
|
| 645 |
+
scored_axioms = []
|
| 646 |
+
for ax in remaining_axioms:
|
| 647 |
+
weight = 1.0 # Base probability
|
| 648 |
+
# Boost probability heavily if the Axiom class matches the Gradient topology
|
| 649 |
+
if n_dom == 1 and ax in isolated: weight += 5.0
|
| 650 |
+
elif n_dom == 2 and ax in relational: weight += 5.0
|
| 651 |
+
elif n_dom >= 3 and ax in systemic: weight += 5.0
|
| 652 |
+
|
| 653 |
+
scored_axioms.append((weight, ax))
|
| 654 |
+
|
| 655 |
+
# Weighted stochastic selection
|
| 656 |
+
scored_axioms.sort(key=lambda x: x[0] * random.random(), reverse=True)
|
| 657 |
+
|
| 658 |
+
children = []
|
| 659 |
+
for _, axiom in scored_axioms[:branch_width]:
|
| 660 |
+
child = ray.extend(axiom, "branch", new_prior=out_baton.ce)
|
| 661 |
+
if child:
|
| 662 |
+
child.baton = out_baton
|
| 663 |
+
children.append(child)
|
| 664 |
+
return children
|
| 665 |
+
|
| 666 |
+
def tension_seeds(self, max_n:int=1000):
|
| 667 |
results=[]
|
| 668 |
for (a,c) in ADJACENT_CONTRADICTIONS:
|
| 669 |
for b1 in ALL_AXIOMS:
|
|
|
|
| 711 |
if child: child.ray_id=f"RES_{child.ray_id}"; results.append(child)
|
| 712 |
return results
|
| 713 |
|
| 714 |
+
CREATIVE_SEEDER = CreativeSeeder()
|
| 715 |
+
|
| 716 |
class SequenceRayTracer:
|
| 717 |
def trace(self, axl_def, base_problem):
|
| 718 |
+
hero_traces = [] # Memory protection: only store important traces
|
| 719 |
+
baton_registry={}; successful_rays=[]
|
| 720 |
+
|
| 721 |
init_b, init_ce = _mprt_sample(base_problem, {v:IV(*base_problem.bounds[v]) for v in base_problem.variables}, N_MPRT_EXPLORE)
|
| 722 |
seed_baton = Baton(binding=init_b, ce=init_ce, ray_id="SEED", l9=L9Certificate(init_ce, base_problem.variables[:3], []))
|
| 723 |
|
| 724 |
queues={
|
| 725 |
"core": [AxiomRay([a], f"S{i}", "seed", ce_prior=init_ce) for i,a in enumerate(ALL_AXIOMS)],
|
| 726 |
+
"explore": CREATIVE_SEEDER.tension_seeds(200) + CREATIVE_SEEDER.random_scouts(100),
|
| 727 |
+
"genetic": CREATIVE_SEEDER.target_seeds(axl_def.anchors) # Inverse chain seeds
|
| 728 |
}
|
| 729 |
for q in queues.values(): random.shuffle(q)
|
| 730 |
queue_order = ["core", "explore", "genetic"]; q_idx = 0
|
|
|
|
| 747 |
|
| 748 |
t0 = time.time(); historical_batons = list(baton_registry.values())
|
| 749 |
|
|
|
|
| 750 |
batch_hyps = []
|
| 751 |
for i, ray in enumerate(batch_rays):
|
| 752 |
p_baton = ray.baton or seed_baton
|
| 753 |
hyps = AXIOM_CONSTRUCTORS[ray.sequence[-1]](base_problem, p_baton, historical_batons, model)
|
| 754 |
if not hyps: hyps = [_make_hyp("fb", p_baton.binding, "fallback", "Pass", [], {}, base_problem.variables, 0.1)]
|
| 755 |
+
batch_hyps.append((i, hyps[0]))
|
| 756 |
|
|
|
|
| 757 |
evaluated_results = _batched_deduce_and_evaluate(base_problem, [h for _, h in batch_hyps])
|
| 758 |
|
| 759 |
solved = False
|
| 760 |
elapsed_ms = (time.time() - t0) * 1000 / len(batch_rays)
|
| 761 |
|
|
|
|
| 762 |
for (ray_idx, hyp), (final_b, final_ce, dom_vars) in zip(batch_hyps, evaluated_results):
|
| 763 |
ray = batch_rays[ray_idx]
|
| 764 |
parent_ce_val = (ray.baton or seed_baton).ce
|
| 765 |
|
|
|
|
| 766 |
g1_pass = final_ce < VERIFY_G1_THRESHOLD
|
| 767 |
g2_pass = True
|
| 768 |
for inv in axl_def.anchors:
|
|
|
|
| 775 |
except: g2_pass=False
|
| 776 |
|
| 777 |
overall_pass = g1_pass and g2_pass
|
| 778 |
+
|
| 779 |
+
improved = final_ce < best_ce
|
| 780 |
+
if improved or overall_pass or (random.random() < 0.001): # Save heroes + tiny sample
|
| 781 |
+
hero_traces.append(HypothesisTrace(ray.ray_id, total_fired-len(batch_rays)+ray_idx, ray.name, ray.ray_type, "Eval", parent_ce_val, final_ce, None, overall_pass, elapsed_ms))
|
| 782 |
|
| 783 |
out_baton = Baton(binding=final_b, ce=final_ce, l9=L9Certificate(final_ce, dom_vars, []))
|
| 784 |
|
|
|
|
| 785 |
if improved:
|
| 786 |
best_ce=final_ce; best_binding=final_b; stall_counter=0
|
| 787 |
baton_registry[ray.ray_id] = out_baton; successful_rays.append(ray)
|
|
|
|
| 792 |
scout_earned = (ray.ray_type == "scout" and final_ce < SCOUT_CE_THRESHOLD)
|
| 793 |
|
| 794 |
if earned or scout_earned:
|
| 795 |
+
new_children = []
|
| 796 |
+
remaining = [a for a in ALL_AXIOMS if a != ray.sequence[-1] and frozenset([ray.sequence[-1], a]) not in _CONTRA_SET and a not in ray.sequence]
|
| 797 |
+
|
| 798 |
+
# ββββ INTELLIGENT CHAINING (ALLOSTERIC FEEDBACK) ββββ
|
| 799 |
+
# The gradient oracle biases the next structural move
|
| 800 |
+
new_children.extend(
|
| 801 |
+
CREATIVE_SEEDER.intelligent_branch(ray, out_baton, remaining, BRANCH_WIDTH)
|
| 802 |
+
)
|
| 803 |
|
| 804 |
+
inv = CREATIVE_SEEDER.invert(ray, final_ce)
|
| 805 |
if inv: new_children.append(inv)
|
| 806 |
|
| 807 |
if len(successful_rays) >= 2:
|
| 808 |
candidates = [r for r in successful_rays if r.ray_id != ray.ray_id]
|
| 809 |
if candidates:
|
| 810 |
partner = random.choice(candidates); ba = baton_registry.get(ray.ray_id, out_baton); bb = baton_registry.get(partner.ray_id, out_baton)
|
| 811 |
+
new_children.extend(CREATIVE_SEEDER.recombine(ray, partner, ba, bb)[:3])
|
| 812 |
|
| 813 |
+
new_children.extend(CREATIVE_SEEDER.resonance_extensions(ray, final_ce, model.resonant_pairs))
|
| 814 |
|
| 815 |
for child in new_children:
|
| 816 |
+
if child.ray_type in ("seed", "branch", "target"): queues["core"].append(child)
|
| 817 |
elif child.ray_type in ("scout", "tension"): queues["explore"].append(child)
|
| 818 |
elif child.ray_type in ("recombine", "invert"): queues["genetic"].append(child)
|
| 819 |
|
|
|
|
| 821 |
|
| 822 |
if solved: break
|
| 823 |
|
| 824 |
+
return best_binding, best_ce, hero_traces, total_fired
|
| 825 |
|
| 826 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 827 |
# SECTION 7: AXL PROBLEMS
|
|
|
|
| 868 |
base_prob = build_base_problem(axl_def)
|
| 869 |
|
| 870 |
t0 = time.time()
|
| 871 |
+
binding, ce, history, total_fired = tracer.trace(axl_def, base_prob)
|
| 872 |
ms = round((time.time() - t0) * 1000)
|
| 873 |
|
| 874 |
with STATE_LOCK:
|
|
|
|
| 877 |
"ce": ce,
|
| 878 |
"solved": ce < SOLVE_THRESHOLD,
|
| 879 |
"ms": ms,
|
| 880 |
+
"traces_saved": len(history),
|
| 881 |
+
"total_fired": total_fired
|
| 882 |
})
|
| 883 |
if len(RUN_LOG) > 30: RUN_LOG.pop()
|
| 884 |
|
|
|
|
| 886 |
global IS_RUNNING
|
| 887 |
IS_RUNNING = not IS_RUNNING
|
| 888 |
if IS_RUNNING: threading.Thread(target=background_worker, daemon=True).start()
|
| 889 |
+
return "βΉ STOP 19.1" if IS_RUNNING else "βΆ START 19.1"
|
| 890 |
|
| 891 |
def refresh_dashboard():
|
| 892 |
with STATE_LOCK:
|
| 893 |
if not RUN_LOG: return "<i>No runs yet. Click Start Engine.</i>"
|
| 894 |
html = "<table style='width:100%; border-collapse:collapse; text-align:left;'>"
|
| 895 |
+
html += "<tr style='border-bottom:1px solid #444'><th>Problem</th><th>CE</th><th>Status</th><th>Speed</th><th>Total Rays Fired</th></tr>"
|
| 896 |
for r in RUN_LOG:
|
| 897 |
color = "#4CAF50" if r["solved"] else "#FF9800"
|
| 898 |
html += f"<tr style='border-bottom:1px solid #222'>"
|
|
|
|
| 900 |
html += f"<td style='padding:5px; color:{color}; font-weight:bold'>{r['ce']:.5f}</td>"
|
| 901 |
html += f"<td style='padding:5px; color:{color}'>{'SOLVED' if r['solved'] else 'SEARCHING'}</td>"
|
| 902 |
html += f"<td style='padding:5px; color:#888'>{r['ms']}ms</td>"
|
| 903 |
+
html += f"<td style='padding:5px; color:#888'>{r['total_fired']:,}</td></tr>"
|
| 904 |
html += "</table>"
|
| 905 |
return html
|
| 906 |
|
| 907 |
with gr.Blocks(theme=gr.themes.Monochrome(text_size="sm")) as demo:
|
| 908 |
+
gr.Markdown(f"# β Practicality 19.1 β Neuro-Symbolic Enzyme")
|
| 909 |
+
gr.Markdown(f"**Compute Node:** `{DEVICE.type.upper()}` | **Engine:** `Allosteric Feedback + Bidirectional Search (1.5M Scale)`")
|
| 910 |
+
btn_toggle = gr.Button("βΆ START 19.1", variant="primary")
|
| 911 |
html_output = gr.HTML(refresh_dashboard())
|
| 912 |
|
| 913 |
btn_toggle.click(toggle_engine, inputs=None, outputs=btn_toggle)
|