Spaces:
Sleeping
Sleeping
Update app.py
Browse files
app.py
CHANGED
|
@@ -1,36 +1,23 @@
|
|
| 1 |
-
|
| 2 |
#!/usr/bin/env python3
|
| 3 |
"""
|
| 4 |
-
PRACTICALITY SYSTEM 27.
|
| 5 |
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 6 |
-
REGRESSIONS FIXED FROM 27.
|
| 7 |
|
| 8 |
-
1.
|
| 9 |
-
|
| 10 |
-
|
| 11 |
-
|
| 12 |
-
2. DYNAMIC BATON REGISTRY
|
| 13 |
-
The registry threshold dynamically scales with the problem's CE
|
| 14 |
-
(max(2.0, best_ce * 1.5, init_ce * 0.1)). High-CE spaces like GLV
|
| 15 |
-
will now successfully save intermediate recombinations.
|
| 16 |
-
|
| 17 |
-
3. DECOUPLED MINIMIZE DIRECTIVE
|
| 18 |
-
The MINIMIZE penalty is strictly isolated to the Adam gradient
|
| 19 |
-
backward pass (is_optimizing=True). scalar_energy (Gate 1) evaluates
|
| 20 |
-
absolute structural truth (CE = 0), unpoisoned by soft objectives.
|
| 21 |
-
|
| 22 |
-
4. FLOAT32 OVERFLOW SHIELD
|
| 23 |
-
t_func_raw now intercepts OverflowError natively. Astronomical
|
| 24 |
-
variables (e.g., 2^1000000 in GHZ) clamp to 1e38 instead of returning
|
| 25 |
-
Infinity and destroying the constraint graph.
|
| 26 |
|
| 27 |
-
|
| 28 |
-
|
| 29 |
-
|
|
|
|
|
|
|
| 30 |
|
| 31 |
HERITAGE MAINTAINED:
|
| 32 |
-
|
| 33 |
-
|
| 34 |
"""
|
| 35 |
|
| 36 |
import os, time, random, math, threading, warnings, json, textwrap, itertools, copy
|
|
@@ -61,7 +48,7 @@ GEMINI_MODEL = "gemini-3.5-flash"
|
|
| 61 |
warnings.filterwarnings("ignore")
|
| 62 |
USE_GPU = torch.cuda.is_available()
|
| 63 |
DEVICE = torch.device("cuda" if USE_GPU else "cpu")
|
| 64 |
-
print(f"[SYSTEM 27.
|
| 65 |
|
| 66 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 67 |
# SECTION 1: CONSTANTS & SAFE HELPERS
|
|
@@ -97,7 +84,6 @@ def safe_round(val, ndigits=8):
|
|
| 97 |
except: return val
|
| 98 |
|
| 99 |
def _c38(v):
|
| 100 |
-
"""Clamps giant floats (like 1e301) to 1e38 so PyTorch float32 doesn't trigger inf."""
|
| 101 |
try:
|
| 102 |
if not math.isfinite(v): return 1e38 if v > 0 else -1e38
|
| 103 |
return max(-1e38, min(1e38, float(v)))
|
|
@@ -417,9 +403,7 @@ def compile_mc(kind,expr_str,direction,variables,weight=1.0,scope="root",branche
|
|
| 417 |
if not isinstance(val, torch.Tensor):
|
| 418 |
val = torch.tensor(float(val), device=DEVICE, dtype=torch.float32)
|
| 419 |
except Exception:
|
| 420 |
-
# Catch math.OverflowError natively (e.g. 2**1000000)
|
| 421 |
val = torch.tensor(1e38, device=DEVICE, dtype=torch.float32)
|
| 422 |
-
# Guarantee no posinf/neginf ruins the CE summation
|
| 423 |
return torch.nan_to_num(val, posinf=1e38, neginf=-1e38)
|
| 424 |
|
| 425 |
mc.torch_func=_t_wrapper
|
|
@@ -547,7 +531,7 @@ class Problem:
|
|
| 547 |
out_of_bounds=torch.relu(lo-margin-col)+torch.relu(col-(hi+margin))
|
| 548 |
total+=(out_of_bounds**2)*10.0
|
| 549 |
|
| 550 |
-
# DECOUPLED MINIMIZE DIRECTIVE
|
| 551 |
if is_optimizing and self.minimize_var and self.minimize_var in self.var_idx:
|
| 552 |
midx = self.var_idx[self.minimize_var]
|
| 553 |
lo,hi = _c38(self.bounds[self.minimize_var][0]), _c38(self.bounds[self.minimize_var][1])
|
|
@@ -562,7 +546,6 @@ class Problem:
|
|
| 562 |
x_arr=[b.get(v,(_c38(self.bounds.get(v,(-1,1))[0])+_c38(self.bounds.get(v,(-1,1))[1]))/2) for v in self.variables]
|
| 563 |
X_t=torch.tensor(x_arr,device=DEVICE,dtype=torch.float32).unsqueeze(0)
|
| 564 |
with torch.no_grad():
|
| 565 |
-
# Gate 1 verification explicitly requires is_optimizing=False
|
| 566 |
return float(self.tensor_energy(X_t, step_ratio=1.0, is_optimizing=False).item())
|
| 567 |
|
| 568 |
def build_base_problem(axl_def:AXLProblemDef) -> Problem:
|
|
@@ -743,7 +726,7 @@ def _global_hc4_tighten_bounds(problem:Problem) -> Dict[str,Tuple[float,float]]:
|
|
| 743 |
for v in problem.bounds if v in c}
|
| 744 |
|
| 745 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 746 |
-
# SECTION 5.10: DIRECT TEMPLATE PARSER
|
| 747 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 748 |
_VAR_RE = re.compile(r'^\s*([a-zA-Z_][a-zA-Z0-9_]*(?:,\s*[a-zA-Z_][a-zA-Z0-9_]*)*)\s+in\s+\[([^\]]+)\]\s*(INT)?\s*',re.IGNORECASE)
|
| 749 |
_CON_RE = re.compile(r'^\s*(EQ|GEQ|LEQ)(?:\s+weight\s*=\s*([0-9.]+))?\s*:\s*(.+)$',re.IGNORECASE)
|
|
@@ -1212,7 +1195,7 @@ def detect_divergence(problem_name):
|
|
| 1212 |
return False,f"ATTRACTOR-STABLE: {len(good)} runs converged."
|
| 1213 |
|
| 1214 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1215 |
-
# SECTION 6.7: HYPOTHESIS TEMPLATES
|
| 1216 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1217 |
STRUCTURAL_HYPOTHESIS_TEMPLATES = {
|
| 1218 |
|
|
@@ -1295,6 +1278,95 @@ Anchor: gap - 1.0 = 0 (tolerance 0.01).
|
|
| 1295 |
Anchor: energy_per_site + 1.0 = 0 (tolerance 0.05).
|
| 1296 |
""",
|
| 1297 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1298 |
"secp256k1 Optimal Window: MINIMIZE total operations": """\
|
| 1299 |
CONCRETE HYPOTHESIS: secp256k1 wNAF Optimal Window via Integer Minimization
|
| 1300 |
============================================================================
|
|
@@ -1344,6 +1416,70 @@ Anchor: k1 + k2*77 - (314 - m*1000) = 0 (tolerance 0.01).
|
|
| 1344 |
Observation: k_target = 314.
|
| 1345 |
""",
|
| 1346 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1347 |
"1024-Qubit Shor: Concrete Full Gate Audit": """\
|
| 1348 |
CONCRETE HYPOTHESIS: Shor RSA-1024 at 1024 Logical Qubits
|
| 1349 |
==========================================================
|
|
@@ -1368,6 +1504,137 @@ Constraints:
|
|
| 1368 |
|
| 1369 |
Anchor: n_log_qubits - 1027 = 0 (tolerance 2.0).
|
| 1370 |
Observation: n_bits = 512.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1371 |
"""
|
| 1372 |
}
|
| 1373 |
|
|
@@ -1425,9 +1692,7 @@ def _batched_deduce_and_evaluate(problem, hyps: List['Hypothesis']) -> List[Tupl
|
|
| 1425 |
optimizer.zero_grad()
|
| 1426 |
step_ratio = min(1.0, step / (DEDUCE_ADAM_STEPS * 0.8))
|
| 1427 |
|
| 1428 |
-
# DECOUPLED MINIMIZE FIX: Apply soft objective strictly in optimization loop
|
| 1429 |
ce = problem.tensor_energy(X, step_ratio, is_optimizing=True)
|
| 1430 |
-
|
| 1431 |
if isinstance(ce, torch.Tensor) and (ce < SOLVE_THRESHOLD).all() and step_ratio == 1.0:
|
| 1432 |
break
|
| 1433 |
ce.sum().backward()
|
|
@@ -1443,7 +1708,6 @@ def _batched_deduce_and_evaluate(problem, hyps: List['Hypothesis']) -> List[Tupl
|
|
| 1443 |
X.data[:, j] = torch.clamp(X.data[:, j], lo - margin, hi + margin)
|
| 1444 |
|
| 1445 |
optimizer.zero_grad()
|
| 1446 |
-
# Evaluate final energy WITHOUT optimization penalties for accurate verification
|
| 1447 |
final_ce = problem.tensor_energy(X, 1.0, is_optimizing=False).view(-1)
|
| 1448 |
final_ce.sum().backward()
|
| 1449 |
|
|
@@ -1555,14 +1819,11 @@ def _make_hyp(hid, binding, h_type, claim, derivation, pinned, free, conf, is_fd
|
|
| 1555 |
derivation=derivation, pinned_vars=pinned, free_vars=free,
|
| 1556 |
confidence=conf, is_fully_determined=is_fd)
|
| 1557 |
|
| 1558 |
-
def _hyp_continuous(p,bt,a,m):
|
| 1559 |
-
return [_make_hyp("cnt",bt.binding,"continuous","Manifold",[],{},p.variables,0.45)]
|
| 1560 |
-
|
| 1561 |
def _hyp_discrete(p,bt,a,m):
|
| 1562 |
b=dict(bt.binding); pinned={}
|
| 1563 |
for sn in p.scope_order:
|
| 1564 |
-
svars=p.scope_vars.get(sn,[])
|
| 1565 |
-
smcs=[p.compiled_constraints[i] for i in p.scope_groups.get(sn,[])]
|
| 1566 |
if svars and smcs:
|
| 1567 |
box={v:IV(b.get(v,0)-max(0.05*(p.bounds[v][1]-p.bounds[v][0]),1e-4),
|
| 1568 |
b.get(v,0)+max(0.05*(p.bounds[v][1]-p.bounds[v][0]),1e-4))
|
|
@@ -1573,35 +1834,26 @@ def _hyp_discrete(p,bt,a,m):
|
|
| 1573 |
b[v]=iv.mid()
|
| 1574 |
if iv.width()<1e-2: pinned[v]=b[v]
|
| 1575 |
return [_make_hyp("dis",b,"discrete","TopoScope",[],pinned,p.variables,0.80)]
|
| 1576 |
-
|
| 1577 |
def _hyp_quadratic(p,bt,a,m):
|
| 1578 |
hyps=[]; b=dict(bt.binding)
|
| 1579 |
if bt.l9 and bt.l9.dominant_vars:
|
| 1580 |
-
for v in bt.l9.dominant_vars[:2]:
|
| 1581 |
-
hyps.append(_make_hyp(f"qua_{v}",b,"quadratic",f"Root({v})",[],{v:b[v]},p.variables,0.70))
|
| 1582 |
return hyps if hyps else [_make_hyp("qua",b,"quadratic","Root",[],{},p.variables,0.55)]
|
| 1583 |
-
|
| 1584 |
def _hyp_bilinear(p,bt,a,m):
|
| 1585 |
hyps=[]; b=dict(bt.binding)
|
| 1586 |
for vi,vj in p.bilinear_pairs:
|
| 1587 |
-
lo_i,hi_i=p.bounds.get(vi,(0,10)); lo_j,hi_j=p.bounds.get(vj,(0,10))
|
| 1588 |
-
product=abs(b.get(vi,1)*b.get(vj,1))
|
| 1589 |
if product<=0: continue
|
| 1590 |
gm=math.sqrt(product)
|
| 1591 |
if lo_i<=gm<=hi_i and lo_j<=gm<=hi_j:
|
| 1592 |
nb=dict(b); nb[vi]=nb[vj]=gm
|
| 1593 |
-
hyps.append(_make_hyp(f"bil_eq_{vi}_{vj}",nb,"bilinear",
|
| 1594 |
-
f"GeoMean({vi}={vj}={gm:.3f})",["bilinear"],{vi:gm,vj:gm},
|
| 1595 |
-
[v for v in p.variables if v not in [vi,vj]],0.70))
|
| 1596 |
for ratio in [0.4,0.7071,0.9]:
|
| 1597 |
vs=gm*ratio; vl=product/(vs+1e-9)
|
| 1598 |
if lo_i<=vs<=hi_i and lo_j<=vl<=hi_j and vs<vl:
|
| 1599 |
nb2=dict(b); nb2[vi]=vs; nb2[vj]=vl
|
| 1600 |
-
hyps.append(_make_hyp(f"bil_asc_{int(ratio*100)}_{vi}_{vj}",nb2,"bilinear",
|
| 1601 |
-
f"BilAsc({vi}={vs:.3f}<{vj}={vl:.3f})",["bilinear"],{vi:vs,vj:vl},
|
| 1602 |
-
[v for v in p.variables if v not in [vi,vj]],0.75))
|
| 1603 |
return hyps
|
| 1604 |
-
|
| 1605 |
def _hyp_monotone_product(p,bt,a,m):
|
| 1606 |
hyps=[]; b=dict(bt.binding)
|
| 1607 |
if not p.monotone_targets: return hyps
|
|
@@ -1615,24 +1867,18 @@ def _hyp_monotone_product(p,bt,a,m):
|
|
| 1615 |
vs=math.sqrt(vs_sq); vl=k/vs
|
| 1616 |
if not(lo_s<=vs<=hi_s and lo_l<=vl<=hi_l and vs<=vl): continue
|
| 1617 |
nb=dict(b); nb[v_small]=vs; nb[v_large]=vl
|
| 1618 |
-
box={u:IV(*tb.get(u,p.bounds.get(u,(-10,10)))) for u in p.variables}
|
| 1619 |
-
|
| 1620 |
-
cont=_hc4(box,p.compiled_constraints)
|
| 1621 |
-
pinned={v_small:vs,v_large:vl}
|
| 1622 |
if cont:
|
| 1623 |
for u,iv in cont.items():
|
| 1624 |
if u in p.bounds: nb[u]=iv.mid()
|
| 1625 |
pinned={u:nb[u] for u in p.variables if cont[u].width()<1e-2}
|
| 1626 |
-
hyps.append(_make_hyp(f"mpr_{v_small}_{v_large}_r{int(ratio*100)}",nb,"monotone_product",
|
| 1627 |
-
f"MonoProd({v_small}={vs:.4f}<={v_large}={vl:.4f})",["ordered","hc4"],pinned,
|
| 1628 |
-
[u for u in p.variables if u not in pinned],0.88))
|
| 1629 |
return hyps
|
| 1630 |
-
|
| 1631 |
def _hyp_metric(p,bt,a,m):
|
| 1632 |
hyps=[]; b=dict(bt.binding)
|
| 1633 |
for mc in p.compiled_constraints:
|
| 1634 |
-
if mc.kind!="equality" or not mc.parsed: continue
|
| 1635 |
-
if not mc.parsed.is_Add: continue
|
| 1636 |
sq_terms=[t for t in mc.parsed.args if t.is_Pow and t.args[1]==2]
|
| 1637 |
if len(sq_terms)<1: continue
|
| 1638 |
vars_in=[str(s) for s in mc.parsed.free_symbols if str(s) in p.variables]
|
|
@@ -1646,14 +1892,10 @@ def _hyp_metric(p,bt,a,m):
|
|
| 1646 |
scale=math.sqrt(target/curr_val); nb=dict(b)
|
| 1647 |
for v in vars_in:
|
| 1648 |
lo,hi=p.bounds.get(v,(-10,10)); nb[v]=max(lo,min(hi,b.get(v,0)*scale))
|
| 1649 |
-
hyps.append(_make_hyp(f"met_{hash(mc.expr_str)%9999}",nb,"metric",
|
| 1650 |
-
f"RadialProject(scale={scale:.4f},dim={len(vars_in)})",["metric",mc.expr_str],
|
| 1651 |
-
{},list(p.variables),0.75))
|
| 1652 |
return hyps
|
| 1653 |
-
|
| 1654 |
def _hyp_symmetric(p,bt,a,m):
|
| 1655 |
-
hyps=[]; b=dict(bt.binding)
|
| 1656 |
-
groups_to_check=list(p.scope_vars.values()) if p.scope_vars else [p.variables]
|
| 1657 |
if not any(p.scope_vars.values()): groups_to_check=[p.variables]
|
| 1658 |
seen_pairs=set()
|
| 1659 |
for grp in groups_to_check:
|
|
@@ -1663,80 +1905,42 @@ def _hyp_symmetric(p,bt,a,m):
|
|
| 1663 |
for j in range(i+1,min(len(vl),8)):
|
| 1664 |
vi,vj=vl[i],vl[j]
|
| 1665 |
if (vi,vj) in seen_pairs: continue
|
| 1666 |
-
seen_pairs.add((vi,vj))
|
| 1667 |
-
lo_i,hi_i=p.bounds.get(vi,(-1e9,1e9)); lo_j,hi_j=p.bounds.get(vj,(-1e9,1e9))
|
| 1668 |
-
bvi,bvj=b.get(vi,0),b.get(vj,0)
|
| 1669 |
if lo_i<=bvj<=hi_i and lo_j<=bvi<=hi_j:
|
| 1670 |
nb=dict(b); nb[vi],nb[vj]=bvj,bvi
|
| 1671 |
-
hyps.append(_make_hyp(f"sym_{vi}_{vj}",nb,"symmetric",
|
| 1672 |
-
f"Swap({vi}<->{vj})",["symmetric"],{vi:nb[vi],vj:nb[vj]},
|
| 1673 |
-
[v for v in p.variables if v not in [vi,vj]],0.60))
|
| 1674 |
avg=(bvi+bvj)/2
|
| 1675 |
if lo_i<=avg<=hi_i and lo_j<=avg<=hi_j:
|
| 1676 |
nb2=dict(b); nb2[vi]=avg; nb2[vj]=avg
|
| 1677 |
-
hyps.append(_make_hyp(f"sym_avg_{vi}_{vj}",nb2,"symmetric",
|
| 1678 |
-
f"Average({vi}={vj}={avg:.4f})",["symmetric"],{vi:avg,vj:avg},
|
| 1679 |
-
[v for v in p.variables if v not in [vi,vj]],0.55))
|
| 1680 |
return hyps[:10]
|
| 1681 |
-
|
| 1682 |
-
def
|
| 1683 |
-
|
| 1684 |
-
|
| 1685 |
-
def _hyp_monotone(p,bt,a,m):
|
| 1686 |
-
return [_make_hyp("mon",bt.binding,"monotone","MonoPath",[],{},p.variables,0.67)]
|
| 1687 |
-
|
| 1688 |
-
def _hyp_convex(p,bt,a,m):
|
| 1689 |
-
return [_make_hyp("cvx",bt.binding,"convex","ConvMix",[],{},p.variables,0.63)]
|
| 1690 |
-
|
| 1691 |
-
def _hyp_conserved(p,bt,a,m):
|
| 1692 |
-
return [_make_hyp("csv",bt.binding,"conserved","Conserve",[],{},p.variables,0.82)]
|
| 1693 |
-
|
| 1694 |
def _hyp_mutable(p,bt,a,m):
|
| 1695 |
b=dict(bt.binding); pinned={}
|
| 1696 |
if bt.l9 and bt.l9.dominant_vars:
|
| 1697 |
-
v=bt.l9.dominant_vars[0]; lo,hi=p.bounds.get(v,(-10,10))
|
| 1698 |
-
b[v]=max(lo,min(hi,b.get(v,0)+random.gauss(0,(hi-lo)*0.05))); pinned={v:b[v]}
|
| 1699 |
return [_make_hyp("mut",b,"mutable","Perturb",[],pinned,p.variables,0.40)]
|
| 1700 |
-
|
| 1701 |
-
def
|
| 1702 |
-
return [_make_hyp("net",bt.binding,"network","HubProp",[],{},p.variables,0.65)]
|
| 1703 |
-
|
| 1704 |
-
def _hyp_equilibrium(p,bt,a,m):
|
| 1705 |
-
return [_make_hyp("eql",bt.binding,"equilibrium","GradBal",[],{},p.variables,0.72)]
|
| 1706 |
-
|
| 1707 |
def _hyp_superposition(p,bt,a,m):
|
| 1708 |
if a and len(a)>0:
|
| 1709 |
-
other=random.choice(a); lam=0.5
|
| 1710 |
-
nb={v:lam*bt.binding.get(v,0)+(1-lam)*other.binding.get(v,0) for v in p.variables}
|
| 1711 |
return [_make_hyp("sup",nb,"superposition","Superpose",[],{},p.variables,0.58)]
|
| 1712 |
return []
|
| 1713 |
-
|
| 1714 |
-
def _hyp_locality(p,bt,a,m):
|
| 1715 |
-
return [_make_hyp("loc",bt.binding,"locality","LocalFirst",[],{},p.variables,0.72)]
|
| 1716 |
-
|
| 1717 |
def _hyp_extremal(p,bt,a,m):
|
| 1718 |
hyps=[]; b=dict(bt.binding)
|
| 1719 |
if bt.l9 and bt.l9.dominant_vars:
|
| 1720 |
v=bt.l9.dominant_vars[0]; lo,hi=p.bounds.get(v,(0,1))
|
| 1721 |
-
for val in [lo,hi]:
|
| 1722 |
-
nb=dict(b); nb[v]=val
|
| 1723 |
-
hyps.append(_make_hyp(f"ext_{v}_{val:.3f}",nb,"extremal",
|
| 1724 |
-
f"PinBound({v}={val:.3f})",[],{v:val},p.variables,0.65))
|
| 1725 |
return hyps
|
| 1726 |
-
|
| 1727 |
-
def
|
| 1728 |
-
|
| 1729 |
-
|
| 1730 |
-
|
| 1731 |
-
def _hyp_injective(p,bt,a,m):
|
| 1732 |
-
return [_make_hyp("inj",bt.binding,"injective","Distinct",[],{},p.variables,0.50)]
|
| 1733 |
-
|
| 1734 |
-
def _hyp_surjective(p,bt,a,m):
|
| 1735 |
-
return [_make_hyp("sur",bt.binding,"surjective","Sweep",[],{},p.variables,0.45)]
|
| 1736 |
-
|
| 1737 |
-
def _hyp_transitive(p,bt,a,m):
|
| 1738 |
-
return [_make_hyp("tra",bt.binding,"transitive","TransSnap",[],{},p.variables,0.77)]
|
| 1739 |
-
|
| 1740 |
def _hyp_atomic(p,bt,a,m):
|
| 1741 |
hyps=[]; b=dict(bt.binding)
|
| 1742 |
for mc in p.compiled_constraints:
|
|
@@ -1744,62 +1948,37 @@ def _hyp_atomic(p,bt,a,m):
|
|
| 1744 |
for v,projs in mc.projections.items():
|
| 1745 |
for proj in projs:
|
| 1746 |
try:
|
| 1747 |
-
val=float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]]))
|
| 1748 |
-
lo,hi=p.bounds.get(v,(-1e9,1e9))
|
| 1749 |
if math.isfinite(val) and lo<=val<=hi:
|
| 1750 |
-
nb=dict(b); nb[v]=val
|
| 1751 |
-
hyps.append(_make_hyp(f"ato_{v}",nb,"atomic",
|
| 1752 |
-
f"Solve({v})",[],{v:val},p.variables,0.70))
|
| 1753 |
-
break
|
| 1754 |
except: pass
|
| 1755 |
if hyps: break
|
| 1756 |
return hyps
|
| 1757 |
-
|
| 1758 |
-
def _hyp_implication(p,bt,a,m):
|
| 1759 |
-
return [_make_hyp("imp",bt.binding,"implication","Imply",[],{},p.variables,0.78)]
|
| 1760 |
-
|
| 1761 |
def _hyp_negation(p,bt,a,m):
|
| 1762 |
-
nb={v:max(p.bounds[v][0],min(p.bounds[v][1],
|
| 1763 |
-
(p.bounds[v][0]+p.bounds[v][1])-bt.binding.get(v,(p.bounds[v][0]+p.bounds[v][1])/2)))
|
| 1764 |
-
for v in p.variables}
|
| 1765 |
return [_make_hyp("neg",nb,"negation","Mirror",[],{},p.variables,0.42)]
|
| 1766 |
-
|
| 1767 |
-
def
|
| 1768 |
-
return [_make_hyp("cmp",bt.binding,"composite","Enz",[],{},p.variables,0.90)]
|
| 1769 |
-
|
| 1770 |
-
def _hyp_holism(p,bt,a,m):
|
| 1771 |
-
return [_make_hyp("hol",bt.binding,"holism","Global",[],{},p.variables,0.73)]
|
| 1772 |
-
|
| 1773 |
def _hyp_parsimony(p,bt,a,m):
|
| 1774 |
-
b=dict(bt.binding); nb={}
|
| 1775 |
-
max_val=max((abs(v) for v in b.values() if math.isfinite(v)), default=1.0)
|
| 1776 |
for v in p.variables:
|
| 1777 |
val=b[v]; lo,hi=p.bounds[v]
|
| 1778 |
if not math.isfinite(val): nb[v]=0.0; continue
|
| 1779 |
if abs(val)<0.1*max_val and lo<=0.0<=hi: nb[v]=0.0
|
| 1780 |
else:
|
| 1781 |
-
candidates=[round(val*m)/m for m in [1,2,4] if lo<=round(val*m)/m<=hi]
|
| 1782 |
-
nb[v]=min(candidates, key=lambda c:abs(c-val)) if candidates else val
|
| 1783 |
return [_make_hyp("par",nb,"parsimony","Occam",[],{},p.variables,0.58)]
|
| 1784 |
-
|
| 1785 |
-
def _hyp_duality(p,bt,a,m):
|
| 1786 |
-
return [_make_hyp("dua",bt.binding,"duality","Tight",[],{},p.variables,0.68)]
|
| 1787 |
|
| 1788 |
AXIOM_CONSTRUCTORS={
|
| 1789 |
-
Axiom.CONTINUOUS:_hyp_continuous,
|
| 1790 |
-
Axiom.
|
| 1791 |
-
Axiom.
|
| 1792 |
-
Axiom.
|
| 1793 |
-
Axiom.
|
| 1794 |
-
Axiom.
|
| 1795 |
-
Axiom.
|
| 1796 |
-
Axiom.SUPERPOSITION:_hyp_superposition, Axiom.LOCALITY:_hyp_locality,
|
| 1797 |
-
Axiom.EXTREMAL:_hyp_extremal, Axiom.ENTROPY:_hyp_entropy,
|
| 1798 |
-
Axiom.INJECTIVE:_hyp_injective, Axiom.SURJECTIVE:_hyp_surjective,
|
| 1799 |
-
Axiom.TRANSITIVE:_hyp_transitive, Axiom.ATOMIC:_hyp_atomic,
|
| 1800 |
-
Axiom.IMPLICATION:_hyp_implication, Axiom.NEGATION:_hyp_negation,
|
| 1801 |
-
Axiom.COMPOSITE:_hyp_composite, Axiom.HOLISM:_hyp_holism,
|
| 1802 |
-
Axiom.PARSIMONY:_hyp_parsimony, Axiom.DUALITY:_hyp_duality,
|
| 1803 |
}
|
| 1804 |
|
| 1805 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
|
@@ -1995,7 +2174,6 @@ class SequenceRayTracer:
|
|
| 1995 |
out_baton=Baton(binding=final_b,ce=final_ce,ray_id=ray.ray_id,
|
| 1996 |
l9=L9Certificate(final_ce,dom_vars,[],tension_class))
|
| 1997 |
|
| 1998 |
-
# DYNAMIC BATON THRESHOLD FIX: Ensure states are saved relative to the current progress
|
| 1999 |
dynamic_baton_thresh = max(BATON_REGISTRY_THRESHOLD, best_ce * 1.5, init_ce * 0.1)
|
| 2000 |
if final_ce < dynamic_baton_thresh:
|
| 2001 |
baton_registry[ray.ray_id] = out_baton
|
|
@@ -2006,9 +2184,10 @@ class SequenceRayTracer:
|
|
| 2006 |
if improved:
|
| 2007 |
best_ce=final_ce; best_binding=dict(final_b)
|
| 2008 |
model.best_ray=ray.name; best_ray_name=ray.name
|
|
|
|
|
|
|
| 2009 |
if g1_pass and g2_pass and final_ce<SOLVE_THRESHOLD: solved=True
|
| 2010 |
|
| 2011 |
-
# DEPTH-0 BRANCHING FIX: Restore unconditional seed expansion (ray.depth < 1)
|
| 2012 |
if (passed_pruning or improved or ray.depth < 1) and ray.depth < MAX_CHAIN_DEPTH:
|
| 2013 |
remaining=[a for a in ALL_AXIOMS if a not in ray.sequence]
|
| 2014 |
queues["core"].extend(bandit.intelligent_branch(ray,out_baton,remaining,BRANCH_WIDTH,sketch))
|
|
@@ -2067,7 +2246,7 @@ OUTPUT SCHEMA (JSON only, no markdown):
|
|
| 2067 |
RULES: USE ** FOR EXPONENTS. NEVER USE ^. No =, >=, <= inside expressions.
|
| 2068 |
EQ/GEQ/LEQ are expression's relation to zero. Output ONLY the JSON object."""
|
| 2069 |
|
| 2070 |
-
COLLAPSER_SYSTEM_PROMPT = """You are the Grounded Hypothesis Engine for Practicality 27.
|
| 2071 |
|
| 2072 |
Check infeasibility_report first. If non-empty: the system proved infeasibility via
|
| 2073 |
algebraic propagation before firing any rays. Output:
|
|
@@ -2176,7 +2355,7 @@ def collapse_solution(problem_text, axl_def, psl_text, binding, g1_pass, g2_pass
|
|
| 2176 |
# SECTION 15: GLOBAL SOLVE TASK
|
| 2177 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 2178 |
def global_solve_task(original_problem_text, api_key, prebuilt_axl=None,
|
| 2179 |
-
use_proxy_decomp: bool=True
|
| 2180 |
_update_state(
|
| 2181 |
is_running=True, phase="ENCODING", high_level_logs=[], answer="",
|
| 2182 |
best_ce=float('inf'), total_fired=0, best_ray="β",
|
|
@@ -2187,119 +2366,106 @@ def global_solve_task(original_problem_text, api_key, prebuilt_axl=None,
|
|
| 2187 |
minimize_result="",
|
| 2188 |
)
|
| 2189 |
try:
|
| 2190 |
-
|
| 2191 |
used_key=api_key or DEFAULT_GEMINI_API_KEY
|
| 2192 |
sketch_notes=[]; proxy_isos=[]
|
| 2193 |
|
| 2194 |
-
|
| 2195 |
-
|
| 2196 |
-
|
| 2197 |
-
|
| 2198 |
-
|
| 2199 |
-
|
| 2200 |
-
|
| 2201 |
-
|
| 2202 |
-
|
| 2203 |
-
_update_state(phase="ERROR",answer=f"Encoder Failed: {str(e)}"); return
|
| 2204 |
|
| 2205 |
-
|
| 2206 |
-
|
| 2207 |
-
|
| 2208 |
|
| 2209 |
-
|
| 2210 |
-
|
| 2211 |
-
|
| 2212 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 2213 |
|
|
|
|
|
|
|
|
|
|
| 2214 |
try:
|
| 2215 |
-
|
| 2216 |
-
|
| 2217 |
-
|
| 2218 |
-
|
| 2219 |
-
|
| 2220 |
-
|
| 2221 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 2222 |
|
| 2223 |
-
|
| 2224 |
-
|
| 2225 |
-
|
| 2226 |
-
|
| 2227 |
-
binding=q_binding; ce=q_ce
|
| 2228 |
|
| 2229 |
-
|
| 2230 |
-
|
| 2231 |
-
|
| 2232 |
-
|
| 2233 |
-
|
| 2234 |
-
current_infeas=GLOBAL_SOLVE_STATE.get("infeasibility_report","")
|
| 2235 |
-
|
| 2236 |
-
for inv in axl_def.anchors:
|
| 2237 |
-
if not inv.compiled_func:
|
| 2238 |
-
try: inv.compile(base_prob.variables)
|
| 2239 |
-
except: pass
|
| 2240 |
|
| 2241 |
-
|
| 2242 |
-
|
| 2243 |
-
|
| 2244 |
-
|
| 2245 |
-
|
| 2246 |
-
|
| 2247 |
-
|
| 2248 |
-
|
| 2249 |
-
|
| 2250 |
-
|
| 2251 |
-
|
| 2252 |
-
|
| 2253 |
-
|
| 2254 |
-
|
| 2255 |
-
|
| 2256 |
-
|
| 2257 |
-
|
| 2258 |
-
|
| 2259 |
-
|
| 2260 |
-
|
| 2261 |
-
_update_state(raw_results_json=raw_json)
|
| 2262 |
-
if min_var and min_val is not None:
|
| 2263 |
-
_update_state(minimize_result=f"{min_var} = {safe_round(min_val,4)}")
|
| 2264 |
-
|
| 2265 |
-
solved_str=("β SOLVED" if (g1_pass and g2_pass)
|
| 2266 |
-
else "π« INFEASIBLE" if current_infeas
|
| 2267 |
-
else "~ PARTIAL" if g1_pass else "β UNSOLVED")
|
| 2268 |
-
best_ray=traces[-1].ray_name if traces and traces[-1].survived else best_ray_name
|
| 2269 |
-
_add_log(f"π {solved_str} (CE: {safe_round(ce,5)}) | Ray: {best_ray}")
|
| 2270 |
-
|
| 2271 |
-
record_fingerprint(axl_def.name,best_ray,binding,ce)
|
| 2272 |
-
is_div,fp_msg=detect_divergence(axl_def.name)
|
| 2273 |
-
if fp_msg: _update_state(fingerprint_summary=fp_msg)
|
| 2274 |
-
|
| 2275 |
-
if prebuilt_axl is None and allow_retry and not current_infeas:
|
| 2276 |
-
if not g1_pass and attempt<MAX_ATTEMPTS:
|
| 2277 |
-
current_text=(original_problem_text+
|
| 2278 |
-
f"\n\nPREVIOUS ATTEMPT FAILED (CE: {ce}):\nApply ALGEBRAIC REDUCTION.")
|
| 2279 |
-
_add_log("β Geometric failure. Retrying..."); continue
|
| 2280 |
-
if not g2_pass and attempt<MAX_ATTEMPTS:
|
| 2281 |
-
failed={k:v for k,(v,ok) in inv_results.items() if not ok}
|
| 2282 |
-
current_text=(original_problem_text+
|
| 2283 |
-
f"\n\nGate 2 failed:\n{json.dumps(failed,indent=2)}\nRevise constraints.")
|
| 2284 |
-
_add_log("β Gate 2 failure. Retrying..."); continue
|
| 2285 |
-
|
| 2286 |
-
scaling_exponents=empirical_scaling_probe(axl_def,base_prob,binding,best_ray)
|
| 2287 |
-
raw_eqs=[mc.expr_str for mc in base_prob.compiled_constraints if mc.kind=="equality"]
|
| 2288 |
-
|
| 2289 |
-
_add_log("π€ Collapsing β Grounded Hypothesis...")
|
| 2290 |
-
_update_state(phase="COLLAPSING")
|
| 2291 |
-
try:
|
| 2292 |
-
answer=collapse_solution(
|
| 2293 |
-
original_problem_text,axl_def,psl_text,binding,
|
| 2294 |
-
g1_pass,g2_pass,inv_results,best_ray,total_fired,
|
| 2295 |
-
sketch_notes,current_sympy_derivation,proxy_isos,
|
| 2296 |
-
scaling_exponents,raw_eqs,current_prop_log,current_infeas,
|
| 2297 |
-
min_var,min_val,used_key)
|
| 2298 |
-
_update_state(answer=answer,phase="DONE"); _add_log("β Done.")
|
| 2299 |
-
except Exception as e:
|
| 2300 |
-
_update_state(answer=f"Collapse error: {e}\n\nRAW:\n{raw_json}",phase="ERROR")
|
| 2301 |
-
_add_log("β Collapse failed β raw results available.")
|
| 2302 |
-
break
|
| 2303 |
|
| 2304 |
except Exception as e:
|
| 2305 |
import traceback; traceback.print_exc()
|
|
@@ -2340,11 +2506,11 @@ def trigger_hypothesis_solve(template_name, api_key):
|
|
| 2340 |
axl_def=None
|
| 2341 |
if axl_def is not None:
|
| 2342 |
threading.Thread(target=global_solve_task,args=(problem_text,api_key),
|
| 2343 |
-
kwargs={"prebuilt_axl":axl_def,"use_proxy_decomp":True
|
| 2344 |
daemon=True).start()
|
| 2345 |
else:
|
| 2346 |
threading.Thread(target=global_solve_task,args=(problem_text,api_key),
|
| 2347 |
-
kwargs={"use_proxy_decomp":True
|
| 2348 |
daemon=True).start()
|
| 2349 |
|
| 2350 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
|
@@ -2486,10 +2652,10 @@ def _reset_ans_cache(a_cache):
|
|
| 2486 |
return a_cache
|
| 2487 |
|
| 2488 |
# ββ Gradio App ββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 2489 |
-
with gr.Blocks(css=CSS, title="Practicality 27.
|
| 2490 |
gr.Markdown(
|
| 2491 |
-
"## β Practicality 27.
|
| 2492 |
-
"`[Direct Parser] -> [INT Grid] -> [
|
| 2493 |
)
|
| 2494 |
|
| 2495 |
dash_cache = gr.State({"html": ""})
|
|
@@ -2536,18 +2702,17 @@ with gr.Blocks(css=CSS, title="Practicality 27.2") as demo:
|
|
| 2536 |
value=(f"Compute: {DEVICE.type.upper()}\n"
|
| 2537 |
f"Axioms: {len(ALL_AXIOMS)}\n"
|
| 2538 |
f"Templates: {len(STRUCTURAL_HYPOTHESIS_TEMPLATES)}\n"
|
| 2539 |
-
f"\n27.
|
| 2540 |
-
f" β
|
| 2541 |
-
f"
|
| 2542 |
-
f" β
|
| 2543 |
-
f"
|
| 2544 |
-
f" β
|
| 2545 |
-
f"
|
| 2546 |
-
f"
|
| 2547 |
-
f" MINIMIZE Soft Objectives (
|
| 2548 |
-
f"
|
| 2549 |
-
f"
|
| 2550 |
-
f" Proxy Decomposition (w/ full graph skip)\n"
|
| 2551 |
f"\n MAX_RAYS={MAX_RAYS_PER_ATTEMPT:,}\n"
|
| 2552 |
f" MAX_CHAIN_DEPTH={MAX_CHAIN_DEPTH}"),
|
| 2553 |
lines=35,interactive=False,elem_classes=["solver-log"])
|
|
@@ -2576,15 +2741,15 @@ with gr.Blocks(css=CSS, title="Practicality 27.2") as demo:
|
|
| 2576 |
outputs=[live_html,dash_cache,ans_cache],
|
| 2577 |
js="""
|
| 2578 |
function() {
|
| 2579 |
-
if (!window.
|
| 2580 |
-
window.
|
| 2581 |
const el = document.getElementById('dash_poll_btn');
|
| 2582 |
if (!el) return;
|
| 2583 |
(el.tagName === 'BUTTON' ? el : el.querySelector('button'))?.click();
|
| 2584 |
}, 1000);
|
| 2585 |
}
|
| 2586 |
-
if (!window.
|
| 2587 |
-
window.
|
| 2588 |
const el = document.getElementById('ans_poll_btn');
|
| 2589 |
if (!el) return;
|
| 2590 |
(el.tagName === 'BUTTON' ? el : el.querySelector('button'))?.click();
|
|
@@ -2622,13 +2787,11 @@ with gr.Blocks(css=CSS, title="Practicality 27.2") as demo:
|
|
| 2622 |
outputs=[ans_cache])
|
| 2623 |
|
| 2624 |
gr.Markdown(
|
| 2625 |
-
f"Practicality 27.
|
| 2626 |
elem_classes=["status-bar"])
|
| 2627 |
|
| 2628 |
if __name__ == "__main__":
|
| 2629 |
-
print(f"[SYSTEM 27.
|
| 2630 |
-
print(f"[SYSTEM 27.
|
| 2631 |
-
print(f"[SYSTEM 27.
|
| 2632 |
-
print(f"[SYSTEM 27.2] Fixes: Float32 Exponent Overflow Native Shield")
|
| 2633 |
-
print(f"[SYSTEM 27.2] Adam logic: Reverted to Original Space bounds tracking")
|
| 2634 |
demo.launch(server_name="0.0.0.0", server_port=7860, share=False)
|
|
|
|
|
|
|
| 1 |
#!/usr/bin/env python3
|
| 2 |
"""
|
| 3 |
+
PRACTICALITY SYSTEM 27.3 β THE FAIL-FAST RESTORATION
|
| 4 |
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 5 |
+
REGRESSIONS FIXED FROM 27.2:
|
| 6 |
|
| 7 |
+
1. REMOVED LLM AUTO-RETRY LOOP (The "Endless Looping" Bug)
|
| 8 |
+
The system now operates on a strict One-Shot paradigm. If the ray
|
| 9 |
+
budget is exhausted (even if Gate 2 fails), it immediately collapses
|
| 10 |
+
and returns the JSON/Markdown to the user for manual recalibration.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 11 |
|
| 12 |
+
2. EARLY STOPPING CLARITY
|
| 13 |
+
The system will only short-circuit if CE < SOLVE_THRESHOLD AND Gate 2
|
| 14 |
+
(Anchors) pass. If an anchor is mathematically malformed (returns 999.0),
|
| 15 |
+
it will exhaust the search budget trying to satisfy it, then fail-fast
|
| 16 |
+
and report.
|
| 17 |
|
| 18 |
HERITAGE MAINTAINED:
|
| 19 |
+
All 17 domain templates. Original-Space Adam. Depth-0 Ray Expansion.
|
| 20 |
+
Dynamic Baton Registry. Float32 Overflow Shield. Decoupled MINIMIZE.
|
| 21 |
"""
|
| 22 |
|
| 23 |
import os, time, random, math, threading, warnings, json, textwrap, itertools, copy
|
|
|
|
| 48 |
warnings.filterwarnings("ignore")
|
| 49 |
USE_GPU = torch.cuda.is_available()
|
| 50 |
DEVICE = torch.device("cuda" if USE_GPU else "cpu")
|
| 51 |
+
print(f"[SYSTEM 27.3] Compute: {DEVICE.type.upper()} | Fail-Fast Core Active")
|
| 52 |
|
| 53 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 54 |
# SECTION 1: CONSTANTS & SAFE HELPERS
|
|
|
|
| 84 |
except: return val
|
| 85 |
|
| 86 |
def _c38(v):
|
|
|
|
| 87 |
try:
|
| 88 |
if not math.isfinite(v): return 1e38 if v > 0 else -1e38
|
| 89 |
return max(-1e38, min(1e38, float(v)))
|
|
|
|
| 403 |
if not isinstance(val, torch.Tensor):
|
| 404 |
val = torch.tensor(float(val), device=DEVICE, dtype=torch.float32)
|
| 405 |
except Exception:
|
|
|
|
| 406 |
val = torch.tensor(1e38, device=DEVICE, dtype=torch.float32)
|
|
|
|
| 407 |
return torch.nan_to_num(val, posinf=1e38, neginf=-1e38)
|
| 408 |
|
| 409 |
mc.torch_func=_t_wrapper
|
|
|
|
| 531 |
out_of_bounds=torch.relu(lo-margin-col)+torch.relu(col-(hi+margin))
|
| 532 |
total+=(out_of_bounds**2)*10.0
|
| 533 |
|
| 534 |
+
# DECOUPLED MINIMIZE DIRECTIVE
|
| 535 |
if is_optimizing and self.minimize_var and self.minimize_var in self.var_idx:
|
| 536 |
midx = self.var_idx[self.minimize_var]
|
| 537 |
lo,hi = _c38(self.bounds[self.minimize_var][0]), _c38(self.bounds[self.minimize_var][1])
|
|
|
|
| 546 |
x_arr=[b.get(v,(_c38(self.bounds.get(v,(-1,1))[0])+_c38(self.bounds.get(v,(-1,1))[1]))/2) for v in self.variables]
|
| 547 |
X_t=torch.tensor(x_arr,device=DEVICE,dtype=torch.float32).unsqueeze(0)
|
| 548 |
with torch.no_grad():
|
|
|
|
| 549 |
return float(self.tensor_energy(X_t, step_ratio=1.0, is_optimizing=False).item())
|
| 550 |
|
| 551 |
def build_base_problem(axl_def:AXLProblemDef) -> Problem:
|
|
|
|
| 726 |
for v in problem.bounds if v in c}
|
| 727 |
|
| 728 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 729 |
+
# SECTION 5.10: DIRECT TEMPLATE PARSER
|
| 730 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 731 |
_VAR_RE = re.compile(r'^\s*([a-zA-Z_][a-zA-Z0-9_]*(?:,\s*[a-zA-Z_][a-zA-Z0-9_]*)*)\s+in\s+\[([^\]]+)\]\s*(INT)?\s*',re.IGNORECASE)
|
| 732 |
_CON_RE = re.compile(r'^\s*(EQ|GEQ|LEQ)(?:\s+weight\s*=\s*([0-9.]+))?\s*:\s*(.+)$',re.IGNORECASE)
|
|
|
|
| 1195 |
return False,f"ATTRACTOR-STABLE: {len(good)} runs converged."
|
| 1196 |
|
| 1197 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1198 |
+
# SECTION 6.7: HYPOTHESIS TEMPLATES
|
| 1199 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 1200 |
STRUCTURAL_HYPOTHESIS_TEMPLATES = {
|
| 1201 |
|
|
|
|
| 1278 |
Anchor: energy_per_site + 1.0 = 0 (tolerance 0.05).
|
| 1279 |
""",
|
| 1280 |
|
| 1281 |
+
"Heisenberg TFIM Trotter: One Circuit Step Observable Evolution": """\
|
| 1282 |
+
CONCRETE HYPOTHESIS: TFIM Trotterized Circuit One-Step Heisenberg Evolution
|
| 1283 |
+
===========================================================================
|
| 1284 |
+
Variables:
|
| 1285 |
+
z_in in [0.99, 1.01]
|
| 1286 |
+
z_mid in [0.9, 1.0]
|
| 1287 |
+
z_out in [0.9, 1.0]
|
| 1288 |
+
zz_in in [0.99, 1.01]
|
| 1289 |
+
zz_mid in [0.85, 1.0]
|
| 1290 |
+
zz_out in [0.85, 1.0]
|
| 1291 |
+
x_out in [-0.1, 0.1]
|
| 1292 |
+
energy_out in [-2.0, 0.0]
|
| 1293 |
+
|
| 1294 |
+
Constraints:
|
| 1295 |
+
EQ weight=10: z_in - 1.0
|
| 1296 |
+
EQ weight=10: zz_in - 1.0
|
| 1297 |
+
EQ weight=10: z_mid - z_in*0.95534
|
| 1298 |
+
EQ weight=10: zz_mid - zz_in*0.91241
|
| 1299 |
+
EQ weight=10: z_out - z_mid
|
| 1300 |
+
EQ weight=10: zz_out - zz_mid
|
| 1301 |
+
EQ weight=5: x_out
|
| 1302 |
+
EQ weight=5: energy_out + zz_out + 0.5*x_out
|
| 1303 |
+
GEQ: z_out - 0.85
|
| 1304 |
+
GEQ: 1.0 - z_out
|
| 1305 |
+
|
| 1306 |
+
Anchor: z_mid - 0.9553 = 0 (tolerance 0.005).
|
| 1307 |
+
Anchor: zz_out - 0.9124 = 0 (tolerance 0.01).
|
| 1308 |
+
""",
|
| 1309 |
+
|
| 1310 |
+
"Heisenberg Clifford: 4-Qubit Chain Observable Evolution": """\
|
| 1311 |
+
CONCRETE HYPOTHESIS: 4-Qubit 1D Chain Clifford Circuit via Heisenberg Picture
|
| 1312 |
+
=============================================================================
|
| 1313 |
+
Variables:
|
| 1314 |
+
x0, x1, x2, x3 in [-1.0, 1.0]
|
| 1315 |
+
z0, z1, z2, z3 in [-1.0, 1.0]
|
| 1316 |
+
zz01 in [-1.0, 1.0]
|
| 1317 |
+
zz12 in [-1.0, 1.0]
|
| 1318 |
+
zz23 in [-1.0, 1.0]
|
| 1319 |
+
magnetization in [-1.0, 1.0]
|
| 1320 |
+
entanglement_proxy in [0.0, 1.0]
|
| 1321 |
+
|
| 1322 |
+
Constraints:
|
| 1323 |
+
EQ weight=10: z0
|
| 1324 |
+
EQ weight=10: z1
|
| 1325 |
+
EQ weight=10: z2
|
| 1326 |
+
EQ weight=10: z3
|
| 1327 |
+
EQ weight=10: magnetization - (z0 + z1 + z2 + z3)/4.0
|
| 1328 |
+
EQ weight=10: zz01
|
| 1329 |
+
EQ weight=10: zz12
|
| 1330 |
+
EQ weight=10: zz23
|
| 1331 |
+
EQ weight=10: entanglement_proxy - (x0**2 + x1**2 + x2**2 + x3**2)/4.0
|
| 1332 |
+
GEQ: 1.0 - x0**2 - z0**2
|
| 1333 |
+
GEQ: 1.0 - x1**2 - z1**2
|
| 1334 |
+
GEQ: 1.0 - x2**2 - z2**2
|
| 1335 |
+
GEQ: 1.0 - x3**2 - z3**2
|
| 1336 |
+
|
| 1337 |
+
Anchor: magnetization = 0 (tolerance 0.01).
|
| 1338 |
+
Anchor: zz01 = 0 (tolerance 0.01).
|
| 1339 |
+
""",
|
| 1340 |
+
|
| 1341 |
+
"Heisenberg XXZ: Spin-Half Chain Magnetization Plateaus": """\
|
| 1342 |
+
CONCRETE HYPOTHESIS: 1D XXZ Chain Magnetization Plateaus via Observables
|
| 1343 |
+
=========================================================================
|
| 1344 |
+
Variables:
|
| 1345 |
+
mag_z in [-1.0, 1.0]
|
| 1346 |
+
corr_xx in [-1.0, 1.0]
|
| 1347 |
+
corr_zz in [-1.0, 1.0]
|
| 1348 |
+
chirality in [-1.0, 1.0]
|
| 1349 |
+
energy_ps in [-3.0, 0.0]
|
| 1350 |
+
suscept in [0.0, 5.0]
|
| 1351 |
+
plateau in [0.0, 1.0]
|
| 1352 |
+
|
| 1353 |
+
Constraints:
|
| 1354 |
+
EQ weight=10: energy_ps - (-corr_xx - 0.5*corr_zz - 0.3*mag_z)
|
| 1355 |
+
EQ weight=5: corr_xx - (-0.3*mag_z - 0.1)
|
| 1356 |
+
EQ weight=10: corr_zz - mag_z**2 - 0.05*(1.0 - mag_z**2)
|
| 1357 |
+
EQ weight=5: chirality
|
| 1358 |
+
EQ weight=5: suscept - (1.0 - mag_z**2)*2.0
|
| 1359 |
+
GEQ: 1.0 - mag_z**2 - corr_xx**2
|
| 1360 |
+
GEQ: corr_zz - (mag_z**2 - 0.3)
|
| 1361 |
+
GEQ: mag_z + 1.0
|
| 1362 |
+
LEQ: mag_z - 1.0
|
| 1363 |
+
GEQ: plateau
|
| 1364 |
+
LEQ: plateau - 1.0
|
| 1365 |
+
|
| 1366 |
+
Anchor: chirality = 0 (tolerance 0.01).
|
| 1367 |
+
Anchor: energy_ps + 0.75 = 0 (tolerance 0.1).
|
| 1368 |
+
""",
|
| 1369 |
+
|
| 1370 |
"secp256k1 Optimal Window: MINIMIZE total operations": """\
|
| 1371 |
CONCRETE HYPOTHESIS: secp256k1 wNAF Optimal Window via Integer Minimization
|
| 1372 |
============================================================================
|
|
|
|
| 1416 |
Observation: k_target = 314.
|
| 1417 |
""",
|
| 1418 |
|
| 1419 |
+
"secp256k1 Montgomery Ladder vs Double-and-Add": """\
|
| 1420 |
+
CONCRETE HYPOTHESIS: Montgomery Ladder Constant-Time Overhead
|
| 1421 |
+
=============================================================
|
| 1422 |
+
Variables:
|
| 1423 |
+
scalar_bits in [254, 258] INT
|
| 1424 |
+
montgomery_ops in [500, 520] INT
|
| 1425 |
+
dbl_add_doubles in [252, 260] INT
|
| 1426 |
+
dbl_add_adds in [100, 140] INT
|
| 1427 |
+
dbl_add_total in [350, 400] INT
|
| 1428 |
+
ct_overhead in [0.2, 0.5]
|
| 1429 |
+
|
| 1430 |
+
Constraints:
|
| 1431 |
+
EQ weight=10: montgomery_ops - 2*scalar_bits
|
| 1432 |
+
EQ weight=10: dbl_add_doubles - scalar_bits
|
| 1433 |
+
EQ weight=10: dbl_add_adds - scalar_bits/2
|
| 1434 |
+
EQ weight=10: dbl_add_total - dbl_add_doubles - dbl_add_adds
|
| 1435 |
+
EQ weight=10: ct_overhead - (montgomery_ops - dbl_add_total)/dbl_add_total
|
| 1436 |
+
GEQ: ct_overhead - 0.28
|
| 1437 |
+
LEQ: ct_overhead - 0.40
|
| 1438 |
+
|
| 1439 |
+
Anchor: montgomery_ops - 2*scalar_bits = 0 (tolerance 2.0).
|
| 1440 |
+
""",
|
| 1441 |
+
|
| 1442 |
+
"secp256k1 Schnorr Batch Verify: Pippenger Scaling": """\
|
| 1443 |
+
CONCRETE HYPOTHESIS: Schnorr Batch Verification via Pippenger
|
| 1444 |
+
=============================================================
|
| 1445 |
+
Variables:
|
| 1446 |
+
n_sigs in [2, 10000] INT
|
| 1447 |
+
naive_ops in [500, 3000000]
|
| 1448 |
+
pippenger_adds in [100, 500000]
|
| 1449 |
+
bucket_width in [4, 16] INT
|
| 1450 |
+
n_buckets in [16, 65536] INT
|
| 1451 |
+
batch_speedup in [1.0, 1000.0]
|
| 1452 |
+
|
| 1453 |
+
Constraints:
|
| 1454 |
+
EQ weight=10: naive_ops - n_sigs*768
|
| 1455 |
+
EQ weight=10: n_buckets - 2**bucket_width
|
| 1456 |
+
EQ weight=10: pippenger_adds - 256*n_buckets + n_sigs*256/bucket_width
|
| 1457 |
+
EQ weight=10: batch_speedup - naive_ops/pippenger_adds
|
| 1458 |
+
GEQ: batch_speedup - 1.0
|
| 1459 |
+
|
| 1460 |
+
Anchor: batch_speedup - 1.0 >= 0 (mode=geq, tolerance 0.1).
|
| 1461 |
+
""",
|
| 1462 |
+
|
| 1463 |
+
"secp256k1 Group Law Feasibility": """\
|
| 1464 |
+
STRUCTURAL HYPOTHESIS: secp256k1 Elliptic Curve Group Law
|
| 1465 |
+
==========================================================
|
| 1466 |
+
Variables:
|
| 1467 |
+
x1 in [0.1, 3.0]
|
| 1468 |
+
y1 in [0.1, 10.0]
|
| 1469 |
+
m in [-50.0, 50.0]
|
| 1470 |
+
x3 in [-5.0, 15.0]
|
| 1471 |
+
y3 in [-30.0, 30.0]
|
| 1472 |
+
|
| 1473 |
+
Constraints:
|
| 1474 |
+
EQ weight=10: y1**2 - x1**3 - 7
|
| 1475 |
+
EQ weight=10: 2*y1*m - 3*x1**2
|
| 1476 |
+
EQ weight=10: x3 - m**2 + 2*x1
|
| 1477 |
+
EQ weight=10: y3 + m*(x3 - x1) + y1
|
| 1478 |
+
EQ weight=10: y3**2 - x3**3 - 7
|
| 1479 |
+
|
| 1480 |
+
Anchor: y3**2 - x3**3 - 7 = 0 (tolerance 0.001).
|
| 1481 |
+
""",
|
| 1482 |
+
|
| 1483 |
"1024-Qubit Shor: Concrete Full Gate Audit": """\
|
| 1484 |
CONCRETE HYPOTHESIS: Shor RSA-1024 at 1024 Logical Qubits
|
| 1485 |
==========================================================
|
|
|
|
| 1504 |
|
| 1505 |
Anchor: n_log_qubits - 1027 = 0 (tolerance 2.0).
|
| 1506 |
Observation: n_bits = 512.
|
| 1507 |
+
""",
|
| 1508 |
+
|
| 1509 |
+
"2048-Qubit Shor: RSA-2048 Full Resource Certificate": """\
|
| 1510 |
+
CONCRETE HYPOTHESIS: Shor RSA-2048 Resource Certificate
|
| 1511 |
+
========================================================
|
| 1512 |
+
Variables:
|
| 1513 |
+
n_bits in [2046, 2050] INT
|
| 1514 |
+
n_log_qubits in [4096, 4104] INT
|
| 1515 |
+
total_tgates in [1e12, 1e17]
|
| 1516 |
+
total_cnots in [1e12, 1e17]
|
| 1517 |
+
code_dist in [25, 50] INT
|
| 1518 |
+
phys_qubits in [1e6, 1e10]
|
| 1519 |
+
wall_time_days in [1.0, 100000000.0]
|
| 1520 |
+
gate_time_ns in [100.0, 2000.0]
|
| 1521 |
+
|
| 1522 |
+
Constraints:
|
| 1523 |
+
EQ weight=10: n_log_qubits - (2*n_bits + 3)
|
| 1524 |
+
EQ weight=10: total_tgates - 512*n_bits**3
|
| 1525 |
+
EQ weight=10: total_cnots - 256*n_bits**3
|
| 1526 |
+
EQ weight=10: code_dist - 31
|
| 1527 |
+
EQ weight=10: phys_qubits - n_log_qubits*2*code_dist**2
|
| 1528 |
+
EQ weight=5: wall_time_days - total_tgates*code_dist*gate_time_ns*1e-9/86400
|
| 1529 |
+
GEQ: gate_time_ns - 100
|
| 1530 |
+
LEQ: gate_time_ns - 1000
|
| 1531 |
+
|
| 1532 |
+
Anchor: n_log_qubits - 4099 = 0 (tolerance 2.0).
|
| 1533 |
+
Observation: n_bits = 2048.
|
| 1534 |
+
""",
|
| 1535 |
+
|
| 1536 |
+
"Kyber-1024 NTT: Post-Quantum Key Generation Audit": """\
|
| 1537 |
+
CONCRETE HYPOTHESIS: CRYSTALS-Kyber-1024 NTT Operation Count
|
| 1538 |
+
=============================================================
|
| 1539 |
+
Variables:
|
| 1540 |
+
n_poly in [254, 258] INT
|
| 1541 |
+
k_param in [3, 5] INT
|
| 1542 |
+
ntt_butterflies in [900, 1100] INT
|
| 1543 |
+
ntt_mults in [900, 1100] INT
|
| 1544 |
+
ntt_adds in [1800, 2200] INT
|
| 1545 |
+
keygen_ntts in [10, 25] INT
|
| 1546 |
+
total_mults in [5000, 30000] INT
|
| 1547 |
+
total_adds in [10000, 60000] INT
|
| 1548 |
+
|
| 1549 |
+
Constraints:
|
| 1550 |
+
EQ weight=10: ntt_butterflies - n_poly*4
|
| 1551 |
+
EQ weight=10: ntt_mults - ntt_butterflies
|
| 1552 |
+
EQ weight=10: ntt_adds - 2*ntt_butterflies
|
| 1553 |
+
EQ weight=10: keygen_ntts - k_param*(k_param + 1)
|
| 1554 |
+
EQ weight=10: total_mults - keygen_ntts*ntt_mults
|
| 1555 |
+
EQ weight=10: total_adds - keygen_ntts*ntt_adds
|
| 1556 |
+
|
| 1557 |
+
Anchor: total_mults - keygen_ntts*ntt_mults = 0 (tolerance 10.0).
|
| 1558 |
+
Observation: k_param = 4.
|
| 1559 |
+
""",
|
| 1560 |
+
|
| 1561 |
+
"Grover Oracle: SHA256 Preimage Circuit Cost": """\
|
| 1562 |
+
CONCRETE HYPOTHESIS: Grover SHA-256 Preimage Circuit
|
| 1563 |
+
=====================================================
|
| 1564 |
+
Variables:
|
| 1565 |
+
output_bits in [254, 258] INT
|
| 1566 |
+
oracle_toffoli in [1400, 1600] INT
|
| 1567 |
+
oracle_cnots in [2800, 3200] INT
|
| 1568 |
+
grover_iters in [125, 130]
|
| 1569 |
+
total_log2_ops in [128, 132]
|
| 1570 |
+
toffoli_to_t in [6, 8] INT
|
| 1571 |
+
log2_tgates in [135, 145]
|
| 1572 |
+
code_dist in [25, 55] INT
|
| 1573 |
+
|
| 1574 |
+
Constraints:
|
| 1575 |
+
EQ weight=10: oracle_toffoli - 1500
|
| 1576 |
+
EQ weight=10: oracle_cnots - 3000
|
| 1577 |
+
EQ weight=10: grover_iters - output_bits/2
|
| 1578 |
+
EQ weight=10: total_log2_ops - grover_iters + 1
|
| 1579 |
+
EQ weight=10: toffoli_to_t - 7
|
| 1580 |
+
EQ weight=10: log2_tgates - total_log2_ops + 10
|
| 1581 |
+
EQ weight=5: code_dist - 33
|
| 1582 |
+
GEQ: log2_tgates - 135
|
| 1583 |
+
|
| 1584 |
+
Anchor: grover_iters - 128 = 0 (tolerance 1.0).
|
| 1585 |
+
""",
|
| 1586 |
+
|
| 1587 |
+
"LWE Lattice Crypto: Short Vector Feasibility": """\
|
| 1588 |
+
STRUCTURAL HYPOTHESIS: Learning With Errors (n=4 proxy)
|
| 1589 |
+
========================================================
|
| 1590 |
+
Variables:
|
| 1591 |
+
s0 in [-5.0, 5.0] INT
|
| 1592 |
+
s1 in [-5.0, 5.0] INT
|
| 1593 |
+
s2 in [-5.0, 5.0] INT
|
| 1594 |
+
s3 in [-5.0, 5.0] INT
|
| 1595 |
+
e0 in [-1.5, 1.5]
|
| 1596 |
+
e1 in [-1.5, 1.5]
|
| 1597 |
+
e2 in [-1.5, 1.5]
|
| 1598 |
+
e3 in [-1.5, 1.5]
|
| 1599 |
+
|
| 1600 |
+
Constraints:
|
| 1601 |
+
EQ: 3*s0 + s1 + 4*s2 + s3 + e0 - 17
|
| 1602 |
+
EQ: 5*s0 + 9*s1 + 2*s2 + 6*s3 + e1 - 43
|
| 1603 |
+
EQ: 5*s0 + 3*s1 + 5*s2 + 8*s3 + e2 - 31
|
| 1604 |
+
EQ: 9*s0 + 7*s1 + 9*s2 + 3*s3 + e3 - 36
|
| 1605 |
+
GEQ: 1 - e0**2
|
| 1606 |
+
GEQ: 1 - e1**2
|
| 1607 |
+
GEQ: 1 - e2**2
|
| 1608 |
+
GEQ: 1 - e3**2
|
| 1609 |
+
|
| 1610 |
+
Anchor: s0 - 1 = 0 (tolerance 0.1).
|
| 1611 |
+
""",
|
| 1612 |
+
|
| 1613 |
+
"Quantum Bell State Structural Feasibility": """\
|
| 1614 |
+
STRUCTURAL HYPOTHESIS: Bell State Maximal Entanglement
|
| 1615 |
+
======================================================
|
| 1616 |
+
Variables:
|
| 1617 |
+
x0 in [-1.0, 1.0]
|
| 1618 |
+
y0 in [-1.0, 1.0]
|
| 1619 |
+
z0 in [-1.0, 1.0]
|
| 1620 |
+
x1 in [-1.0, 1.0]
|
| 1621 |
+
y1 in [-1.0, 1.0]
|
| 1622 |
+
z1 in [-1.0, 1.0]
|
| 1623 |
+
xx01 in [-1.0, 1.0]
|
| 1624 |
+
zz01 in [-1.0, 1.0]
|
| 1625 |
+
|
| 1626 |
+
Constraints:
|
| 1627 |
+
EQ weight=5: z0
|
| 1628 |
+
EQ weight=5: z1
|
| 1629 |
+
EQ weight=5: x0
|
| 1630 |
+
EQ weight=5: x1
|
| 1631 |
+
EQ weight=10: zz01 - 1
|
| 1632 |
+
EQ weight=10: xx01 - 1
|
| 1633 |
+
GEQ: 1 - x0**2 - y0**2 - z0**2
|
| 1634 |
+
GEQ: 1 - x1**2 - y1**2 - z1**2
|
| 1635 |
+
|
| 1636 |
+
Anchor: zz01 - 1 = 0 (tolerance 0.01).
|
| 1637 |
+
Anchor: xx01 - 1 = 0 (tolerance 0.01).
|
| 1638 |
"""
|
| 1639 |
}
|
| 1640 |
|
|
|
|
| 1692 |
optimizer.zero_grad()
|
| 1693 |
step_ratio = min(1.0, step / (DEDUCE_ADAM_STEPS * 0.8))
|
| 1694 |
|
|
|
|
| 1695 |
ce = problem.tensor_energy(X, step_ratio, is_optimizing=True)
|
|
|
|
| 1696 |
if isinstance(ce, torch.Tensor) and (ce < SOLVE_THRESHOLD).all() and step_ratio == 1.0:
|
| 1697 |
break
|
| 1698 |
ce.sum().backward()
|
|
|
|
| 1708 |
X.data[:, j] = torch.clamp(X.data[:, j], lo - margin, hi + margin)
|
| 1709 |
|
| 1710 |
optimizer.zero_grad()
|
|
|
|
| 1711 |
final_ce = problem.tensor_energy(X, 1.0, is_optimizing=False).view(-1)
|
| 1712 |
final_ce.sum().backward()
|
| 1713 |
|
|
|
|
| 1819 |
derivation=derivation, pinned_vars=pinned, free_vars=free,
|
| 1820 |
confidence=conf, is_fully_determined=is_fd)
|
| 1821 |
|
| 1822 |
+
def _hyp_continuous(p,bt,a,m): return [_make_hyp("cnt",bt.binding,"continuous","Manifold",[],{},p.variables,0.45)]
|
|
|
|
|
|
|
| 1823 |
def _hyp_discrete(p,bt,a,m):
|
| 1824 |
b=dict(bt.binding); pinned={}
|
| 1825 |
for sn in p.scope_order:
|
| 1826 |
+
svars=p.scope_vars.get(sn,[]); smcs=[p.compiled_constraints[i] for i in p.scope_groups.get(sn,[])]
|
|
|
|
| 1827 |
if svars and smcs:
|
| 1828 |
box={v:IV(b.get(v,0)-max(0.05*(p.bounds[v][1]-p.bounds[v][0]),1e-4),
|
| 1829 |
b.get(v,0)+max(0.05*(p.bounds[v][1]-p.bounds[v][0]),1e-4))
|
|
|
|
| 1834 |
b[v]=iv.mid()
|
| 1835 |
if iv.width()<1e-2: pinned[v]=b[v]
|
| 1836 |
return [_make_hyp("dis",b,"discrete","TopoScope",[],pinned,p.variables,0.80)]
|
|
|
|
| 1837 |
def _hyp_quadratic(p,bt,a,m):
|
| 1838 |
hyps=[]; b=dict(bt.binding)
|
| 1839 |
if bt.l9 and bt.l9.dominant_vars:
|
| 1840 |
+
for v in bt.l9.dominant_vars[:2]: hyps.append(_make_hyp(f"qua_{v}",b,"quadratic",f"Root({v})",[],{v:b[v]},p.variables,0.70))
|
|
|
|
| 1841 |
return hyps if hyps else [_make_hyp("qua",b,"quadratic","Root",[],{},p.variables,0.55)]
|
|
|
|
| 1842 |
def _hyp_bilinear(p,bt,a,m):
|
| 1843 |
hyps=[]; b=dict(bt.binding)
|
| 1844 |
for vi,vj in p.bilinear_pairs:
|
| 1845 |
+
lo_i,hi_i=p.bounds.get(vi,(0,10)); lo_j,hi_j=p.bounds.get(vj,(0,10)); product=abs(b.get(vi,1)*b.get(vj,1))
|
|
|
|
| 1846 |
if product<=0: continue
|
| 1847 |
gm=math.sqrt(product)
|
| 1848 |
if lo_i<=gm<=hi_i and lo_j<=gm<=hi_j:
|
| 1849 |
nb=dict(b); nb[vi]=nb[vj]=gm
|
| 1850 |
+
hyps.append(_make_hyp(f"bil_eq_{vi}_{vj}",nb,"bilinear",f"GeoMean({vi}={vj}={gm:.3f})",["bilinear"],{vi:gm,vj:gm},[v for v in p.variables if v not in [vi,vj]],0.70))
|
|
|
|
|
|
|
| 1851 |
for ratio in [0.4,0.7071,0.9]:
|
| 1852 |
vs=gm*ratio; vl=product/(vs+1e-9)
|
| 1853 |
if lo_i<=vs<=hi_i and lo_j<=vl<=hi_j and vs<vl:
|
| 1854 |
nb2=dict(b); nb2[vi]=vs; nb2[vj]=vl
|
| 1855 |
+
hyps.append(_make_hyp(f"bil_asc_{int(ratio*100)}_{vi}_{vj}",nb2,"bilinear",f"BilAsc({vi}={vs:.3f}<{vj}={vl:.3f})",["bilinear"],{vi:vs,vj:vl},[v for v in p.variables if v not in [vi,vj]],0.75))
|
|
|
|
|
|
|
| 1856 |
return hyps
|
|
|
|
| 1857 |
def _hyp_monotone_product(p,bt,a,m):
|
| 1858 |
hyps=[]; b=dict(bt.binding)
|
| 1859 |
if not p.monotone_targets: return hyps
|
|
|
|
| 1867 |
vs=math.sqrt(vs_sq); vl=k/vs
|
| 1868 |
if not(lo_s<=vs<=hi_s and lo_l<=vl<=hi_l and vs<=vl): continue
|
| 1869 |
nb=dict(b); nb[v_small]=vs; nb[v_large]=vl
|
| 1870 |
+
box={u:IV(*tb.get(u,p.bounds.get(u,(-10,10)))) for u in p.variables}; box[v_small]=IV(vs-1e-6,vs+1e-6); box[v_large]=IV(vl-1e-6,vl+1e-6)
|
| 1871 |
+
cont=_hc4(box,p.compiled_constraints); pinned={v_small:vs,v_large:vl}
|
|
|
|
|
|
|
| 1872 |
if cont:
|
| 1873 |
for u,iv in cont.items():
|
| 1874 |
if u in p.bounds: nb[u]=iv.mid()
|
| 1875 |
pinned={u:nb[u] for u in p.variables if cont[u].width()<1e-2}
|
| 1876 |
+
hyps.append(_make_hyp(f"mpr_{v_small}_{v_large}_r{int(ratio*100)}",nb,"monotone_product",f"MonoProd({v_small}={vs:.4f}<={v_large}={vl:.4f})",["ordered","hc4"],pinned,[u for u in p.variables if u not in pinned],0.88))
|
|
|
|
|
|
|
| 1877 |
return hyps
|
|
|
|
| 1878 |
def _hyp_metric(p,bt,a,m):
|
| 1879 |
hyps=[]; b=dict(bt.binding)
|
| 1880 |
for mc in p.compiled_constraints:
|
| 1881 |
+
if mc.kind!="equality" or not mc.parsed or not mc.parsed.is_Add: continue
|
|
|
|
| 1882 |
sq_terms=[t for t in mc.parsed.args if t.is_Pow and t.args[1]==2]
|
| 1883 |
if len(sq_terms)<1: continue
|
| 1884 |
vars_in=[str(s) for s in mc.parsed.free_symbols if str(s) in p.variables]
|
|
|
|
| 1892 |
scale=math.sqrt(target/curr_val); nb=dict(b)
|
| 1893 |
for v in vars_in:
|
| 1894 |
lo,hi=p.bounds.get(v,(-10,10)); nb[v]=max(lo,min(hi,b.get(v,0)*scale))
|
| 1895 |
+
hyps.append(_make_hyp(f"met_{hash(mc.expr_str)%9999}",nb,"metric",f"RadialProject(scale={scale:.4f},dim={len(vars_in)})",["metric",mc.expr_str],{},list(p.variables),0.75))
|
|
|
|
|
|
|
| 1896 |
return hyps
|
|
|
|
| 1897 |
def _hyp_symmetric(p,bt,a,m):
|
| 1898 |
+
hyps=[]; b=dict(bt.binding); groups_to_check=list(p.scope_vars.values()) if p.scope_vars else [p.variables]
|
|
|
|
| 1899 |
if not any(p.scope_vars.values()): groups_to_check=[p.variables]
|
| 1900 |
seen_pairs=set()
|
| 1901 |
for grp in groups_to_check:
|
|
|
|
| 1905 |
for j in range(i+1,min(len(vl),8)):
|
| 1906 |
vi,vj=vl[i],vl[j]
|
| 1907 |
if (vi,vj) in seen_pairs: continue
|
| 1908 |
+
seen_pairs.add((vi,vj)); lo_i,hi_i=p.bounds.get(vi,(-1e9,1e9)); lo_j,hi_j=p.bounds.get(vj,(-1e9,1e9)); bvi,bvj=b.get(vi,0),b.get(vj,0)
|
|
|
|
|
|
|
| 1909 |
if lo_i<=bvj<=hi_i and lo_j<=bvi<=hi_j:
|
| 1910 |
nb=dict(b); nb[vi],nb[vj]=bvj,bvi
|
| 1911 |
+
hyps.append(_make_hyp(f"sym_{vi}_{vj}",nb,"symmetric",f"Swap({vi}<->{vj})",["symmetric"],{vi:nb[vi],vj:nb[vj]},[v for v in p.variables if v not in [vi,vj]],0.60))
|
|
|
|
|
|
|
| 1912 |
avg=(bvi+bvj)/2
|
| 1913 |
if lo_i<=avg<=hi_i and lo_j<=avg<=hi_j:
|
| 1914 |
nb2=dict(b); nb2[vi]=avg; nb2[vj]=avg
|
| 1915 |
+
hyps.append(_make_hyp(f"sym_avg_{vi}_{vj}",nb2,"symmetric",f"Average({vi}={vj}={avg:.4f})",["symmetric"],{vi:avg,vj:avg},[v for v in p.variables if v not in [vi,vj]],0.55))
|
|
|
|
|
|
|
| 1916 |
return hyps[:10]
|
| 1917 |
+
def _hyp_ordered(p,bt,a,m): return [_make_hyp("ord",bt.binding,"ordered","OrderBal",[],{},p.variables,0.67)]
|
| 1918 |
+
def _hyp_monotone(p,bt,a,m): return [_make_hyp("mon",bt.binding,"monotone","MonoPath",[],{},p.variables,0.67)]
|
| 1919 |
+
def _hyp_convex(p,bt,a,m): return [_make_hyp("cvx",bt.binding,"convex","ConvMix",[],{},p.variables,0.63)]
|
| 1920 |
+
def _hyp_conserved(p,bt,a,m): return [_make_hyp("csv",bt.binding,"conserved","Conserve",[],{},p.variables,0.82)]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1921 |
def _hyp_mutable(p,bt,a,m):
|
| 1922 |
b=dict(bt.binding); pinned={}
|
| 1923 |
if bt.l9 and bt.l9.dominant_vars:
|
| 1924 |
+
v=bt.l9.dominant_vars[0]; lo,hi=p.bounds.get(v,(-10,10)); b[v]=max(lo,min(hi,b.get(v,0)+random.gauss(0,(hi-lo)*0.05))); pinned={v:b[v]}
|
|
|
|
| 1925 |
return [_make_hyp("mut",b,"mutable","Perturb",[],pinned,p.variables,0.40)]
|
| 1926 |
+
def _hyp_network(p,bt,a,m): return [_make_hyp("net",bt.binding,"network","HubProp",[],{},p.variables,0.65)]
|
| 1927 |
+
def _hyp_equilibrium(p,bt,a,m): return [_make_hyp("eql",bt.binding,"equilibrium","GradBal",[],{},p.variables,0.72)]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1928 |
def _hyp_superposition(p,bt,a,m):
|
| 1929 |
if a and len(a)>0:
|
| 1930 |
+
other=random.choice(a); lam=0.5; nb={v:lam*bt.binding.get(v,0)+(1-lam)*other.binding.get(v,0) for v in p.variables}
|
|
|
|
| 1931 |
return [_make_hyp("sup",nb,"superposition","Superpose",[],{},p.variables,0.58)]
|
| 1932 |
return []
|
| 1933 |
+
def _hyp_locality(p,bt,a,m): return [_make_hyp("loc",bt.binding,"locality","LocalFirst",[],{},p.variables,0.72)]
|
|
|
|
|
|
|
|
|
|
| 1934 |
def _hyp_extremal(p,bt,a,m):
|
| 1935 |
hyps=[]; b=dict(bt.binding)
|
| 1936 |
if bt.l9 and bt.l9.dominant_vars:
|
| 1937 |
v=bt.l9.dominant_vars[0]; lo,hi=p.bounds.get(v,(0,1))
|
| 1938 |
+
for val in [lo,hi]: nb=dict(b); nb[v]=val; hyps.append(_make_hyp(f"ext_{v}_{val:.3f}",nb,"extremal",f"PinBound({v}={val:.3f})",[],{v:val},p.variables,0.65))
|
|
|
|
|
|
|
|
|
|
| 1939 |
return hyps
|
| 1940 |
+
def _hyp_entropy(p,bt,a,m): return [_make_hyp("ent",{v:random.uniform(*p.bounds[v]) for v in p.variables},"entropy","MaxEnt",[],{},p.variables,0.48)]
|
| 1941 |
+
def _hyp_injective(p,bt,a,m): return [_make_hyp("inj",bt.binding,"injective","Distinct",[],{},p.variables,0.50)]
|
| 1942 |
+
def _hyp_surjective(p,bt,a,m): return [_make_hyp("sur",bt.binding,"surjective","Sweep",[],{},p.variables,0.45)]
|
| 1943 |
+
def _hyp_transitive(p,bt,a,m): return [_make_hyp("tra",bt.binding,"transitive","TransSnap",[],{},p.variables,0.77)]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1944 |
def _hyp_atomic(p,bt,a,m):
|
| 1945 |
hyps=[]; b=dict(bt.binding)
|
| 1946 |
for mc in p.compiled_constraints:
|
|
|
|
| 1948 |
for v,projs in mc.projections.items():
|
| 1949 |
for proj in projs:
|
| 1950 |
try:
|
| 1951 |
+
val=float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])); lo,hi=p.bounds.get(v,(-1e9,1e9))
|
|
|
|
| 1952 |
if math.isfinite(val) and lo<=val<=hi:
|
| 1953 |
+
nb=dict(b); nb[v]=val; hyps.append(_make_hyp(f"ato_{v}",nb,"atomic",f"Solve({v})",[],{v:val},p.variables,0.70)); break
|
|
|
|
|
|
|
|
|
|
| 1954 |
except: pass
|
| 1955 |
if hyps: break
|
| 1956 |
return hyps
|
| 1957 |
+
def _hyp_implication(p,bt,a,m): return [_make_hyp("imp",bt.binding,"implication","Imply",[],{},p.variables,0.78)]
|
|
|
|
|
|
|
|
|
|
| 1958 |
def _hyp_negation(p,bt,a,m):
|
| 1959 |
+
nb={v:max(p.bounds[v][0],min(p.bounds[v][1],(p.bounds[v][0]+p.bounds[v][1])-bt.binding.get(v,(p.bounds[v][0]+p.bounds[v][1])/2))) for v in p.variables}
|
|
|
|
|
|
|
| 1960 |
return [_make_hyp("neg",nb,"negation","Mirror",[],{},p.variables,0.42)]
|
| 1961 |
+
def _hyp_composite(p,bt,a,m): return [_make_hyp("cmp",bt.binding,"composite","Enz",[],{},p.variables,0.90)]
|
| 1962 |
+
def _hyp_holism(p,bt,a,m): return [_make_hyp("hol",bt.binding,"holism","Global",[],{},p.variables,0.73)]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1963 |
def _hyp_parsimony(p,bt,a,m):
|
| 1964 |
+
b=dict(bt.binding); nb={}; max_val=max((abs(v) for v in b.values() if math.isfinite(v)), default=1.0)
|
|
|
|
| 1965 |
for v in p.variables:
|
| 1966 |
val=b[v]; lo,hi=p.bounds[v]
|
| 1967 |
if not math.isfinite(val): nb[v]=0.0; continue
|
| 1968 |
if abs(val)<0.1*max_val and lo<=0.0<=hi: nb[v]=0.0
|
| 1969 |
else:
|
| 1970 |
+
candidates=[round(val*m)/m for m in [1,2,4] if lo<=round(val*m)/m<=hi]; nb[v]=min(candidates, key=lambda c:abs(c-val)) if candidates else val
|
|
|
|
| 1971 |
return [_make_hyp("par",nb,"parsimony","Occam",[],{},p.variables,0.58)]
|
| 1972 |
+
def _hyp_duality(p,bt,a,m): return [_make_hyp("dua",bt.binding,"duality","Tight",[],{},p.variables,0.68)]
|
|
|
|
|
|
|
| 1973 |
|
| 1974 |
AXIOM_CONSTRUCTORS={
|
| 1975 |
+
Axiom.CONTINUOUS:_hyp_continuous, Axiom.DISCRETE:_hyp_discrete, Axiom.QUADRATIC:_hyp_quadratic, Axiom.BILINEAR:_hyp_bilinear,
|
| 1976 |
+
Axiom.METRIC:_hyp_metric, Axiom.SYMMETRIC:_hyp_symmetric, Axiom.ORDERED:_hyp_ordered, Axiom.MONOTONE:_hyp_monotone,
|
| 1977 |
+
Axiom.CONVEX:_hyp_convex, Axiom.MONOTONE_PRODUCT:_hyp_monotone_product, Axiom.CONSERVED:_hyp_conserved, Axiom.MUTABLE:_hyp_mutable,
|
| 1978 |
+
Axiom.NETWORK:_hyp_network, Axiom.EQUILIBRIUM:_hyp_equilibrium, Axiom.SUPERPOSITION:_hyp_superposition, Axiom.LOCALITY:_hyp_locality,
|
| 1979 |
+
Axiom.EXTREMAL:_hyp_extremal, Axiom.ENTROPY:_hyp_entropy, Axiom.INJECTIVE:_hyp_injective, Axiom.SURJECTIVE:_hyp_surjective,
|
| 1980 |
+
Axiom.TRANSITIVE:_hyp_transitive, Axiom.ATOMIC:_hyp_atomic, Axiom.IMPLICATION:_hyp_implication, Axiom.NEGATION:_hyp_negation,
|
| 1981 |
+
Axiom.COMPOSITE:_hyp_composite, Axiom.HOLISM:_hyp_holism, Axiom.PARSIMONY:_hyp_parsimony, Axiom.DUALITY:_hyp_duality,
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1982 |
}
|
| 1983 |
|
| 1984 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
|
|
|
| 2174 |
out_baton=Baton(binding=final_b,ce=final_ce,ray_id=ray.ray_id,
|
| 2175 |
l9=L9Certificate(final_ce,dom_vars,[],tension_class))
|
| 2176 |
|
|
|
|
| 2177 |
dynamic_baton_thresh = max(BATON_REGISTRY_THRESHOLD, best_ce * 1.5, init_ce * 0.1)
|
| 2178 |
if final_ce < dynamic_baton_thresh:
|
| 2179 |
baton_registry[ray.ray_id] = out_baton
|
|
|
|
| 2184 |
if improved:
|
| 2185 |
best_ce=final_ce; best_binding=dict(final_b)
|
| 2186 |
model.best_ray=ray.name; best_ray_name=ray.name
|
| 2187 |
+
|
| 2188 |
+
# STRICT EARLY EXIT: If CE is perfect AND anchors pass, stop everything.
|
| 2189 |
if g1_pass and g2_pass and final_ce<SOLVE_THRESHOLD: solved=True
|
| 2190 |
|
|
|
|
| 2191 |
if (passed_pruning or improved or ray.depth < 1) and ray.depth < MAX_CHAIN_DEPTH:
|
| 2192 |
remaining=[a for a in ALL_AXIOMS if a not in ray.sequence]
|
| 2193 |
queues["core"].extend(bandit.intelligent_branch(ray,out_baton,remaining,BRANCH_WIDTH,sketch))
|
|
|
|
| 2246 |
RULES: USE ** FOR EXPONENTS. NEVER USE ^. No =, >=, <= inside expressions.
|
| 2247 |
EQ/GEQ/LEQ are expression's relation to zero. Output ONLY the JSON object."""
|
| 2248 |
|
| 2249 |
+
COLLAPSER_SYSTEM_PROMPT = """You are the Grounded Hypothesis Engine for Practicality 27.3.
|
| 2250 |
|
| 2251 |
Check infeasibility_report first. If non-empty: the system proved infeasibility via
|
| 2252 |
algebraic propagation before firing any rays. Output:
|
|
|
|
| 2355 |
# SECTION 15: GLOBAL SOLVE TASK
|
| 2356 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 2357 |
def global_solve_task(original_problem_text, api_key, prebuilt_axl=None,
|
| 2358 |
+
use_proxy_decomp: bool=True):
|
| 2359 |
_update_state(
|
| 2360 |
is_running=True, phase="ENCODING", high_level_logs=[], answer="",
|
| 2361 |
best_ce=float('inf'), total_fired=0, best_ray="β",
|
|
|
|
| 2366 |
minimize_result="",
|
| 2367 |
)
|
| 2368 |
try:
|
| 2369 |
+
current_text=original_problem_text
|
| 2370 |
used_key=api_key or DEFAULT_GEMINI_API_KEY
|
| 2371 |
sketch_notes=[]; proxy_isos=[]
|
| 2372 |
|
| 2373 |
+
if prebuilt_axl is not None:
|
| 2374 |
+
_add_log("β‘ Direct AXL (template parser β no LLM encoder)")
|
| 2375 |
+
axl_def=prebuilt_axl
|
| 2376 |
+
else:
|
| 2377 |
+
_add_log(f"π LLM Encoding (One-Shot)...")
|
| 2378 |
+
try: axl_def=encode_problem_to_axl(current_text,used_key)
|
| 2379 |
+
except Exception as e:
|
| 2380 |
+
_add_log(f"β Encode failed: {e}")
|
| 2381 |
+
_update_state(phase="ERROR",answer=f"Encoder Failed: {str(e)}"); return
|
|
|
|
| 2382 |
|
| 2383 |
+
_add_log(f"β `{axl_def.name}` | {len(axl_def.variables)} vars | {len(axl_def.constraints)} constraints")
|
| 2384 |
+
if axl_def.minimize_var: _add_log(f" β³ MINIMIZE Directive: {axl_def.minimize_var}")
|
| 2385 |
+
_update_state(phase="COMPILING")
|
| 2386 |
|
| 2387 |
+
try: psl_text=AXL_COMPILER.compile(axl_def); base_prob=build_base_problem(axl_def)
|
| 2388 |
+
except Exception as e:
|
| 2389 |
+
_add_log(f"β Compile failed: {e}")
|
| 2390 |
+
_update_state(phase="ERROR",answer=f"Compiler Failed: {str(e)}"); return
|
| 2391 |
+
|
| 2392 |
+
try:
|
| 2393 |
+
_add_log("π Ray Tracer...")
|
| 2394 |
+
tracer=SequenceRayTracer()
|
| 2395 |
+
binding,ce,traces,total_fired,best_ray_name=tracer.trace(
|
| 2396 |
+
axl_def,base_prob,use_proxy_decomp=use_proxy_decomp)
|
| 2397 |
+
except Exception as e:
|
| 2398 |
+
_add_log(f"β Solver error: {e}")
|
| 2399 |
+
_update_state(phase="ERROR",answer=f"Ray Tracer Crashed: {str(e)}"); raise e
|
| 2400 |
+
|
| 2401 |
+
_update_state(phase="QUANTIZING")
|
| 2402 |
+
q_binding,q_ce,q_success=quantize_binding(binding,base_prob)
|
| 2403 |
+
if q_success and any(abs(q_binding.get(v,0)-binding.get(v,0))>0.01 for v in base_prob.int_vars):
|
| 2404 |
+
_add_log(f"π§± Quantize+Propagate: CE {ce:.4f} -> {q_ce:.4f}")
|
| 2405 |
+
binding=q_binding; ce=q_ce
|
| 2406 |
+
|
| 2407 |
+
with STATE_LOCK:
|
| 2408 |
+
sketch_notes=GLOBAL_SOLVE_STATE.get("sketch_summary","").split("; ")
|
| 2409 |
+
current_sympy_derivation=GLOBAL_SOLVE_STATE.get("sympy_derivation",[])
|
| 2410 |
+
proxy_isos=GLOBAL_SOLVE_STATE.get("proxy_component_isos",[])
|
| 2411 |
+
current_prop_log=GLOBAL_SOLVE_STATE.get("propagation_log",[])
|
| 2412 |
+
current_infeas=GLOBAL_SOLVE_STATE.get("infeasibility_report","")
|
| 2413 |
+
|
| 2414 |
+
for inv in axl_def.anchors:
|
| 2415 |
+
if not inv.compiled_func:
|
| 2416 |
+
try: inv.compile(base_prob.variables)
|
| 2417 |
+
except: pass
|
| 2418 |
|
| 2419 |
+
g1_ce=base_prob.scalar_energy(binding); g1_pass=g1_ce<VERIFY_G1_THRESHOLD
|
| 2420 |
+
inv_results={}
|
| 2421 |
+
for inv in axl_def.anchors:
|
| 2422 |
try:
|
| 2423 |
+
val=float(inv.compiled_func(*[binding.get(v,0.0) for v in inv.syms_used]))
|
| 2424 |
+
err=abs(val)
|
| 2425 |
+
if inv.mode=="eq": passed=err<inv.tolerance
|
| 2426 |
+
elif inv.mode=="geq": passed=val>=-inv.tolerance
|
| 2427 |
+
else: passed=val<=inv.tolerance
|
| 2428 |
+
inv_results[inv.name]=(safe_round(val,6),passed)
|
| 2429 |
+
except: inv_results[inv.name]=(999.0,False)
|
| 2430 |
+
g2_pass=all(v[1] for v in inv_results.values()) if inv_results else True
|
| 2431 |
+
|
| 2432 |
+
infeas_obj=None
|
| 2433 |
+
if current_infeas: infeas_obj=InfeasibilityReport(True,[],current_infeas,True)
|
| 2434 |
+
|
| 2435 |
+
min_var = base_prob.minimize_var
|
| 2436 |
+
min_val = binding.get(min_var) if min_var else None
|
| 2437 |
|
| 2438 |
+
raw_json=build_raw_results_json(binding,ce,g1_pass,g2_pass,inv_results,current_prop_log,infeas_obj,min_var,min_val)
|
| 2439 |
+
_update_state(raw_results_json=raw_json)
|
| 2440 |
+
if min_var and min_val is not None:
|
| 2441 |
+
_update_state(minimize_result=f"{min_var} = {safe_round(min_val,4)}")
|
|
|
|
| 2442 |
|
| 2443 |
+
solved_str=("β SOLVED" if (g1_pass and g2_pass)
|
| 2444 |
+
else "π« INFEASIBLE" if current_infeas
|
| 2445 |
+
else "~ PARTIAL" if g1_pass else "β UNSOLVED")
|
| 2446 |
+
best_ray=traces[-1].ray_name if traces and traces[-1].survived else best_ray_name
|
| 2447 |
+
_add_log(f"π {solved_str} (CE: {safe_round(ce,5)}) | Ray: {best_ray}")
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 2448 |
|
| 2449 |
+
record_fingerprint(axl_def.name,best_ray,binding,ce)
|
| 2450 |
+
is_div,fp_msg=detect_divergence(axl_def.name)
|
| 2451 |
+
if fp_msg: _update_state(fingerprint_summary=fp_msg)
|
| 2452 |
+
|
| 2453 |
+
scaling_exponents=empirical_scaling_probe(axl_def,base_prob,binding,best_ray)
|
| 2454 |
+
raw_eqs=[mc.expr_str for mc in base_prob.compiled_constraints if mc.kind=="equality"]
|
| 2455 |
+
|
| 2456 |
+
_add_log("π€ Collapsing β Grounded Hypothesis...")
|
| 2457 |
+
_update_state(phase="COLLAPSING")
|
| 2458 |
+
try:
|
| 2459 |
+
answer=collapse_solution(
|
| 2460 |
+
original_problem_text,axl_def,psl_text,binding,
|
| 2461 |
+
g1_pass,g2_pass,inv_results,best_ray,total_fired,
|
| 2462 |
+
sketch_notes,current_sympy_derivation,proxy_isos,
|
| 2463 |
+
scaling_exponents,raw_eqs,current_prop_log,current_infeas,
|
| 2464 |
+
min_var,min_val,used_key)
|
| 2465 |
+
_update_state(answer=answer,phase="DONE"); _add_log("β Done.")
|
| 2466 |
+
except Exception as e:
|
| 2467 |
+
_update_state(answer=f"Collapse error: {e}\n\nRAW:\n{raw_json}",phase="ERROR")
|
| 2468 |
+
_add_log("β Collapse failed β raw results available.")
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 2469 |
|
| 2470 |
except Exception as e:
|
| 2471 |
import traceback; traceback.print_exc()
|
|
|
|
| 2506 |
axl_def=None
|
| 2507 |
if axl_def is not None:
|
| 2508 |
threading.Thread(target=global_solve_task,args=(problem_text,api_key),
|
| 2509 |
+
kwargs={"prebuilt_axl":axl_def,"use_proxy_decomp":True},
|
| 2510 |
daemon=True).start()
|
| 2511 |
else:
|
| 2512 |
threading.Thread(target=global_solve_task,args=(problem_text,api_key),
|
| 2513 |
+
kwargs={"use_proxy_decomp":True},
|
| 2514 |
daemon=True).start()
|
| 2515 |
|
| 2516 |
# ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
|
|
|
| 2652 |
return a_cache
|
| 2653 |
|
| 2654 |
# ββ Gradio App ββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 2655 |
+
with gr.Blocks(css=CSS, title="Practicality 27.3") as demo:
|
| 2656 |
gr.Markdown(
|
| 2657 |
+
"## β Practicality 27.3 β The Fail-Fast Core\n"
|
| 2658 |
+
"`[Direct Parser / LLM] -> [INT Grid] -> [Orig Space Adam] -> [No Retry Loops β Manual Recalibration]`"
|
| 2659 |
)
|
| 2660 |
|
| 2661 |
dash_cache = gr.State({"html": ""})
|
|
|
|
| 2702 |
value=(f"Compute: {DEVICE.type.upper()}\n"
|
| 2703 |
f"Axioms: {len(ALL_AXIOMS)}\n"
|
| 2704 |
f"Templates: {len(STRUCTURAL_HYPOTHESIS_TEMPLATES)}\n"
|
| 2705 |
+
f"\n27.3 UPDATES (Fail-Fast Paradigm):\n"
|
| 2706 |
+
f" β REMOVED auto-retry loop entirely.\n"
|
| 2707 |
+
f" β Stops 'looping from the beginning'.\n"
|
| 2708 |
+
f" β CE=0 with Anchor=999 correctly explores, \n"
|
| 2709 |
+
f" then fails fast to show broken constraint.\n"
|
| 2710 |
+
f" β All 17 templates fully restored.\n"
|
| 2711 |
+
f"\n27.2 FEATURES RETAINED:\n"
|
| 2712 |
+
f" ray.depth < 1 unconditional branching.\n"
|
| 2713 |
+
f" MINIMIZE Soft Objectives (isolated)\n"
|
| 2714 |
+
f" Float32 max overflow native handler.\n"
|
| 2715 |
+
f" Range-normalized Adam reverted to orig space.\n"
|
|
|
|
| 2716 |
f"\n MAX_RAYS={MAX_RAYS_PER_ATTEMPT:,}\n"
|
| 2717 |
f" MAX_CHAIN_DEPTH={MAX_CHAIN_DEPTH}"),
|
| 2718 |
lines=35,interactive=False,elem_classes=["solver-log"])
|
|
|
|
| 2741 |
outputs=[live_html,dash_cache,ans_cache],
|
| 2742 |
js="""
|
| 2743 |
function() {
|
| 2744 |
+
if (!window._p273_dash) {
|
| 2745 |
+
window._p273_dash = setInterval(() => {
|
| 2746 |
const el = document.getElementById('dash_poll_btn');
|
| 2747 |
if (!el) return;
|
| 2748 |
(el.tagName === 'BUTTON' ? el : el.querySelector('button'))?.click();
|
| 2749 |
}, 1000);
|
| 2750 |
}
|
| 2751 |
+
if (!window._p273_ans) {
|
| 2752 |
+
window._p273_ans = setInterval(() => {
|
| 2753 |
const el = document.getElementById('ans_poll_btn');
|
| 2754 |
if (!el) return;
|
| 2755 |
(el.tagName === 'BUTTON' ? el : el.querySelector('button'))?.click();
|
|
|
|
| 2787 |
outputs=[ans_cache])
|
| 2788 |
|
| 2789 |
gr.Markdown(
|
| 2790 |
+
f"Practicality 27.3 Β· Strict One-Shot Paradigm Β· Fail-Fast Core",
|
| 2791 |
elem_classes=["status-bar"])
|
| 2792 |
|
| 2793 |
if __name__ == "__main__":
|
| 2794 |
+
print(f"[SYSTEM 27.3] Compute: {DEVICE.type.upper()} | Quantum={HAS_QUANTUM}")
|
| 2795 |
+
print(f"[SYSTEM 27.3] Templates: {len(STRUCTURAL_HYPOTHESIS_TEMPLATES)}")
|
| 2796 |
+
print(f"[SYSTEM 27.3] Fixes: Removed LLM auto-retry endless loop.")
|
|
|
|
|
|
|
| 2797 |
demo.launch(server_name="0.0.0.0", server_port=7860, share=False)
|