diff --git "a/app.py" "b/app.py" --- "a/app.py" +++ "b/app.py" @@ -1,27 +1,64 @@ #!/usr/bin/env python3 """ -PRACTICALITY UNIFIED SERVER 23.1 — STABILIZED MANIFOLD & ALGEBRAIC REDUCTION +PRACTICALITY SYSTEM 24.0 — STRUCTURAL SKETCH & WORLD MODEL PRIOR ═══════════════════════════════════════════════════════════════════ ARCHITECTURE: - User Text → [GEMINI 3.1 ENCODER] → AXLProblemDef (Strict Math Representation) - → [WISDOM LAYER] → PyTorch Masked Deduction (with Gradient Clipping) - → Verification (Gate 1 & Gate 2) - → [ALGEBRAIC REDUCTION LOOP] if Geometry Fails - → [GEMINI 3.1 COLLAPSER] → Domain-language explanation - -LATEST UPDATES (23.1): - - UI FIX: Restored the RAY_ICONS dictionary so the live dashboard renders properly. - - PYTORCH STABILIZER: Added X.grad.clamp_() and tightened default fallback bounds - to prevent polynomial volume explosions (CE 10^14). - - ALGEBRAIC PRE-SOLVING: If PyTorch fails to navigate the manifold (Gate 1 fails), - the system feeds back to Gemini to perform Symbolic Variable Elimination. + User Text → [GEMINI ENCODER] → AXLProblemDef + → [STRUCTURAL SKETCH] → Axiom affinity map (derived, not learned) + → [SYMPY PRE-SOLVER] → Exact solutions if system is reducible + → [TEMPLATE ENGINE] → Analytically-derived partial hypotheses + (conservation projections, exact roots, + monotone product splits, symmetry orbits) + → [WISDOM LAYER] → Sketch-weighted rays + template-seeded queue + → PyTorch Masked Deduction + → Verification (Gate 1 & Gate 2) + → [GEMINI COLLAPSER] → Domain-language explanation + +NEW IN 24.0: + + 1. STRUCTURAL SKETCH: + Computed analytically from each problem before any rays fire. + Assigns affinity scores to all 28 axioms based on what the + problem's own algebra reveals: conservation laws → CONSERVED boost, + bilinear pairs → BILINEAR/MPR boost, sum-of-squares → METRIC boost. + No learning. No cross-problem bias. Derived fresh each time. + + 2. SYMPY PRE-SOLVER: + For polynomial systems with n_vars ≤ 5 and n_equalities ≥ n_vars, + attempt symbolic solve before rays fire. If it succeeds, the solution + becomes a perfect anchor template and the ray search validates/refines. + If it fails, the attempt still informs the sketch about solvability. + + 3. HYPOTHESIS TEMPLATES: + The "must happen" map. Analytically-derived partial hypotheses + from provable algebraic facts: + • SymPy exact roots (confidence=0.99) + • Conservation projections (confidence=0.75) + • Monotone product splits at analytical ratios (confidence=0.88) + • Algebraic projection roots from equality constraints (confidence=0.72) + All templates are evaluated in one batch before seeds fire. + The best template result becomes the initial floor that seeds improve on. + + 4. SKETCH-WEIGHTED BRANCHING: + intelligent_branch now multiplies sketch affinities into the allosteric + feedback scores. Both the gradient topology (from masked Adam) AND the + problem's structural fingerprint bias the next axiom choice. + One is local (what does the current residual look like?), + the other is global (what does this problem structurally require?). + + 5. DIMENSION-ADAPTIVE CONSTRUCTOR FIXES: + _hyp_symmetric: now checks all variable pairs within scope groups, + not just variables 0 and 1. + _hyp_discrete: HC4 delta now 5% of bound range, not fixed ±1. + _hyp_metric: robust sum-of-squares detection for arbitrary dimension. """ -import os, time, random, math, threading, warnings, queue, json, textwrap +import os, time, random, math, threading, warnings, json, textwrap from functools import reduce from typing import Optional, Callable, List, Dict, Tuple, Any, Set from dataclasses import dataclass, field from collections import defaultdict, deque +import concurrent.futures import numpy as np import sympy as sp @@ -37,12 +74,12 @@ from google.genai import types # ══════════════════════════════════════════════════════════════════ DEFAULT_GEMINI_API_KEY = os.environ.get("AI_Key", "") GEMINI_MODEL = "gemini-3-flash-preview" -# "gemma-4-26b-a4b-it" # +# "gemma-4-26b-a4b-it" # "gemini-3-flash-preview" # warnings.filterwarnings("ignore") USE_GPU = torch.cuda.is_available() DEVICE = torch.device("cuda" if USE_GPU else "cpu") -print(f"[UNIFIED SERVER] Compute: {DEVICE.type.upper()} | System 23.1 (Algebraic Reduction)") +print(f"[SYSTEM 24.0] Compute: {DEVICE.type.upper()} | Structural Sketch + World Model Prior") # ══════���═══════════════════════════════════════════════════════════════ # SECTION 1: CONSTANTS @@ -54,8 +91,9 @@ DEDUCE_ADAM_STEPS = 25 N_MPRT_EXPLORE = 1000 PROJECTION_CACHE: Dict = {} -MAX_RAYS_PER_ATTEMPT = 1000000 # ~245k rays per cycle before reframing +MAX_RAYS_PER_ATTEMPT = 24576 * 10 RAY_BATCH_SIZE = 24576 +TEMPLATE_BATCH_SIZE = 512 # templates evaluated before any rays fire CE_EARN_RATIO = 0.90 SCOUT_CE_THRESHOLD = 0.5 BRANCH_WIDTH = 12 @@ -63,8 +101,12 @@ BRANCH_WIDTH_SYSTEMIC = 16 BATON_REGISTRY_THRESHOLD = 2.0 BATON_REGISTRY_MAX = 5000 +# SymPy pre-solver gate: only attempt for small polynomial systems +SYMPY_MAX_VARS = 5 +SYMPY_TIMEOUT_SECS = 4.0 + # ══════════════════════════════════════════════════════════════════════ -# SECTION 2: GLOBAL STATE +# SECTION 2: GLOBAL STATE # ══════════════════════════════════════════════════════════════════════ STATE_LOCK = threading.Lock() @@ -77,6 +119,9 @@ GLOBAL_SOLVE_STATE = { "recent_traces": deque(maxlen=25), "high_level_logs": [], "answer": "", + "sketch_summary": "", + "template_count": 0, + "template_best_ce": float('inf'), } def _update_state(**kwargs): @@ -170,7 +215,7 @@ def _global_hc4_tighten_bounds(problem): for v in problem.bounds if v in c} # ══════════════════════════════════════════════════════════════════════ -# SECTION 4: PSL PARSER & PRE-COMPILATION +# SECTION 4: PSL PARSER & AXL LAYER # ══════════════════════════════════════════════════════════════════════ @dataclass class PSLVar: name:str; lo:float; hi:float @@ -260,14 +305,14 @@ def expand_psl(prog:PSLProgram) -> ExpandedProblem: @dataclass class AXLInvariant: name:str; expr:str; tolerance:float=VERIFY_G2_TOLERANCE; mode:str="eq" - compiled_func: Optional[Callable] = field(default=None, repr=False) - syms_used: List[str] = field(default_factory=list) + compiled_func:Optional[Callable]=field(default=None,repr=False) + syms_used:List[str]=field(default_factory=list) - def compile(self, variables: List[str]): - syms = {v: sp.Symbol(v) for v in variables} - parsed = parse_expr(self.expr, local_dict=syms) - self.syms_used = [str(s) for s in parsed.free_symbols if str(s) in variables] - self.compiled_func = sp.lambdify([sp.Symbol(v) for v in self.syms_used], parsed, modules="math") + def compile(self,variables:List[str]): + syms={v:sp.Symbol(v) for v in variables} + parsed=parse_expr(self.expr,local_dict=syms) + self.syms_used=[str(s) for s in parsed.free_symbols if str(s) in variables] + self.compiled_func=sp.lambdify([sp.Symbol(v) for v in self.syms_used],parsed,modules="math") @dataclass class AXLProblemDef: @@ -363,20 +408,16 @@ def compile_mc(kind,expr_str,direction,variables,weight=1.0,scope="root",branche except: pass return mc -def _extract_ordering_pair(mc: MathConstraint, variables: List[str]) -> Optional[Tuple[str,str]]: - if mc.kind != "inequality" or mc.direction != "geq": return None - if mc.parsed is None: return None - parsed = mc.parsed - free = [str(s) for s in parsed.free_symbols if str(s) in variables] - if len(free) != 2: return None - v0, v1 = free[0], free[1] +def _extract_ordering_pair(mc:'MathConstraint',variables:List[str]) -> Optional[Tuple[str,str]]: + if mc.kind!="inequality" or mc.direction!="geq" or mc.parsed is None: return None + free=[str(s) for s in mc.parsed.free_symbols if str(s) in variables] + if len(free)!=2: return None + v0,v1=free[0],free[1] try: - c0 = float(parsed.coeff(sp.Symbol(v0))) - c1 = float(parsed.coeff(sp.Symbol(v1))) - except Exception: - return None - if c0 > 0 and c1 < 0: return (v1, v0) - elif c1 > 0 and c0 < 0: return (v0, v1) + c0=float(mc.parsed.coeff(sp.Symbol(v0))); c1=float(mc.parsed.coeff(sp.Symbol(v1))) + except: return None + if c0>0 and c1<0: return (v1,v0) + elif c1>0 and c0<0: return (v0,v1) return None @dataclass @@ -386,10 +427,9 @@ class Problem: scope_groups:Dict[str,List[int]]=field(default_factory=dict) scope_vars:Dict[str,List[str]]=field(default_factory=dict) scope_order:List[str]=field(default_factory=list) - - bilinear_pairs: List[Tuple[str,str]] = field(default_factory=list) - monotone_targets: List[Tuple[str,str,float]] = field(default_factory=list) - ordering_pairs: List[Tuple[str,str]] = field(default_factory=list) + bilinear_pairs:List[Tuple[str,str]]=field(default_factory=list) + monotone_targets:List[Tuple[str,str,float]]=field(default_factory=list) + ordering_pairs:List[Tuple[str,str]]=field(default_factory=list) def __post_init__(self): self.compiled_constraints=[ @@ -398,36 +438,33 @@ class Problem: self.var_idx={v:i for i,v in enumerate(self.variables)} for mc in self.compiled_constraints: - pair = _extract_ordering_pair(mc, self.variables) - if pair and pair not in self.ordering_pairs: - self.ordering_pairs.append(pair) + pair=_extract_ordering_pair(mc,self.variables) + if pair and pair not in self.ordering_pairs: self.ordering_pairs.append(pair) for mc in self.compiled_constraints: if mc.parsed and mc.parsed.is_Add: for term in mc.parsed.args: if term.is_Mul: - syms_in = [str(s) for s in term.free_symbols if str(s) in self.variables] - if len(syms_in) == 2: - va, vb = syms_in - if (va, vb) not in self.bilinear_pairs and (vb, va) not in self.bilinear_pairs: - self.bilinear_pairs.append((va, vb)) + syms_in=[str(s) for s in term.free_symbols if str(s) in self.variables] + if len(syms_in)==2: + va,vb=syms_in + if (va,vb) not in self.bilinear_pairs and (vb,va) not in self.bilinear_pairs: + self.bilinear_pairs.append((va,vb)) for mc in self.compiled_constraints: - if mc.kind == "equality" and mc.parsed is not None: - for va, vb in self.bilinear_pairs: - sa, sb = sp.Symbol(va), sp.Symbol(vb) + if mc.kind=="equality" and mc.parsed is not None: + for va,vb in self.bilinear_pairs: + sa,sb=sp.Symbol(va),sp.Symbol(vb) if sa in mc.parsed.free_symbols and sb in mc.parsed.free_symbols: try: - k_expr = -(mc.parsed - sa*sb) - k = float(k_expr.evalf()) - if k > 0: - for vs, vl in self.ordering_pairs: - if set([va, vb]) == set([vs, vl]): - target = (vs, vl, k) + k_expr=-(mc.parsed-sa*sb); k=float(k_expr.evalf()) + if k>0: + for vs,vl in self.ordering_pairs: + if set([va,vb])==set([vs,vl]): + target=(vs,vl,k) if target not in self.monotone_targets: self.monotone_targets.append(target) - except Exception: - pass + except: pass def tensor_energy(self,X:torch.Tensor) -> torch.Tensor: is_batched=(X.dim()==2) @@ -486,7 +523,370 @@ def build_base_problem(axl_def:AXLProblemDef) -> Problem: scope_order=ep.scope_order) # ══════════════════════════════════════════════════════════════════════ -# SECTION 6: BATCHED MASKED DEDUCTION & ORACLE +# SECTION 6: STRUCTURAL SKETCH — The World Model Prior +# ══════════════════════════════════════════════════════════════════════ + +@dataclass +class StructuralSketch: + """ + Analytically-derived prior distribution over axiom sequence space. + Computed once per problem from its algebraic structure. + + This is the 'world model' the user described — not learned from + experience, but derived from the problem's own mathematics. + It answers: "What does any valid solution to THIS problem structurally + require?" The rays then explore within that answer. + + axiom_affinities: Dict[axiom -> float] + Higher = this axiom's constructor will generate useful hypotheses + for this problem. Used to weight seed queue and branching. + + exact_solutions: SymPy found the answer before rays fired. + templates: analytically-derived partial hypotheses (the "must happen" map). + """ + axiom_affinities: Dict[str,float] + solvable_by_sympy: bool + exact_solutions: List[Dict[str,float]] + n_free_dof: int + has_conservation: bool + has_bilinear: bool + has_ordering: bool + has_transcendental: bool + dominant_type: str # "linear" | "quadratic" | "transcendental" + sketch_notes: List[str] # human-readable explanation of what was found + +@dataclass +class HypothesisTemplate: + """ + A partial hypothesis derived from provable algebraic facts. + Unlike a random hypothesis, these are grounded in the problem's + own structure. The stochastic component only fills the gaps. + + Source taxonomy: + "sympy_exact" — SymPy found the complete solution + "conservation" — conservation law projects one variable + "monotone_prod" — ordered bilinear split at analytical ratio + "projection" — algebraic root of equality constraint + """ + template_id: str + pinned_vars: Dict[str,float] + free_vars: List[str] + source: str + confidence: float + derivation: str + +def _try_sympy_solve(problem:Problem) -> Tuple[List[Dict[str,float]],bool]: + """ + Attempt symbolic solve for small polynomial systems. + Runs in a thread with timeout to prevent hanging. + Returns (solutions, success). + """ + # Gate: only attempt for small polynomial systems + has_transcendental=any( + mc.parsed is not None and + (mc.parsed.has(sp.sin) or mc.parsed.has(sp.cos) or + mc.parsed.has(sp.exp) or mc.parsed.has(sp.log)) + for mc in problem.compiled_constraints) + if has_transcendental: return [],False + + eq_mcs=[mc for mc in problem.compiled_constraints + if mc.kind=="equality" and mc.parsed is not None and mc.syms_used] + if len(eq_mcs)0 + +def compute_sketch(problem:Problem) -> StructuralSketch: + """ + Analyzes the problem's algebraic structure to build the world model prior. + This runs before any rays fire — it's the map, not the territory. + """ + affinities={a:1.0 for a in _ALL_AXIOMS_PLACEHOLDER} # filled after axiom def + notes:List[str]=[] + + n_vars=len(problem.variables) + n_eq=sum(1 for mc in problem.compiled_constraints if mc.kind=="equality") + n_ineq=sum(1 for mc in problem.compiled_constraints if mc.kind=="inequality") + + # Conservation laws + has_conservation=any(mc.weight>=5.0 for mc in problem.compiled_constraints if mc.kind=="equality") + if has_conservation: + affinities["CONSERVED"]+=3.0; affinities["COMPOSITE"]+=1.5 + notes.append("Conservation laws → CONSERVED/COMPOSITE boosted") + + # Bilinear pairs + if problem.bilinear_pairs: + boost=min(3.0+len(problem.bilinear_pairs)*0.5,6.0) + affinities["BILINEAR"]+=boost + notes.append(f"{len(problem.bilinear_pairs)} bilinear pairs → BILINEAR boosted") + + # Monotone targets (the hardest structural pattern) + if problem.monotone_targets: + affinities["MONOTONE_PRODUCT"]+=5.0; affinities["ORDERED"]+=2.5 + notes.append(f"{len(problem.monotone_targets)} monotone product targets → MPR strongly boosted") + + # Ordering constraints + if problem.ordering_pairs: + affinities["ORDERED"]+=2.0; affinities["DISCRETE"]+=1.0 + notes.append(f"{len(problem.ordering_pairs)} ordering constraints → ORDERED boosted") + + # Scope structure suggests discrete topology + if any(problem.scope_vars.values()): + affinities["DISCRETE"]+=2.0; affinities["LOCALITY"]+=1.0 + notes.append("Scope structure detected → DISCRETE boosted") + + # Projection availability → ATOMIC/IMPLICATION/TRANSITIVE + n_proj=sum(1 for mc in problem.compiled_constraints if mc.projections) + if n_proj>0: + affinities["ATOMIC"]+=2.0+n_proj*0.3 + affinities["IMPLICATION"]+=1.5; affinities["TRANSITIVE"]+=1.5 + notes.append(f"{n_proj} projectable constraints → ATOMIC/IMPLICATION boosted") + + # Sum-of-squares → METRIC/QUADRATIC/CONTINUOUS + has_sos=any( + mc.parsed is not None and mc.parsed.is_Add and + any(t.is_Pow and t.args[1]==2 for t in mc.parsed.args) + for mc in problem.compiled_constraints if mc.kind=="equality") + if has_sos: + affinities["METRIC"]+=2.5; affinities["QUADRATIC"]+=2.0; affinities["CONTINUOUS"]+=1.5 + notes.append("Sum-of-squares pattern → METRIC/QUADRATIC/CONTINUOUS boosted") + + # Tight bounds (integer-ish solutions likely) + tight=sum(1 for v in problem.variables if abs(problem.bounds[v][1]-problem.bounds[v][0])<10) + if tight>n_vars//2: + affinities["PARSIMONY"]+=2.0 + notes.append("Tight bounds → PARSIMONY boosted (integer solutions likely)") + + # High dimensionality → holistic and systemic axioms + if n_vars>=6: + affinities["HOLISM"]+=1.5; affinities["NETWORK"]+=1.5; affinities["LOCALITY"]+=1.0 + notes.append(f"High-D ({n_vars} vars) → HOLISM/NETWORK boosted") + + # Symmetry detection: same bounds for multiple variables + bound_groups=defaultdict(list) + for v in problem.variables: bound_groups[problem.bounds[v]].append(v) + if any(len(g)>=2 for g in bound_groups.values()): + affinities["SYMMETRIC"]+=1.5 + notes.append("Symmetric bounds → SYMMETRIC boosted") + + # Transcendental constraints + has_transcendental=any( + mc.parsed is not None and + (mc.parsed.has(sp.sin) or mc.parsed.has(sp.cos) or + mc.parsed.has(sp.exp)) + for mc in problem.compiled_constraints) + if has_transcendental: + affinities["CONTINUOUS"]+=2.0; affinities["EQUILIBRIUM"]+=1.5 + notes.append("Transcendental constraints → CONTINUOUS/EQUILIBRIUM boosted") + + # Dominant constraint type + max_deg=1 + for mc in problem.compiled_constraints: + if mc.parsed is not None: + try: + for sym in mc.parsed.free_symbols: + d=sp.degree(mc.parsed,sym) + if isinstance(d,int): max_deg=max(max_deg,d) + except: pass + if has_transcendental: dom_type="transcendental" + elif max_deg>=3: dom_type="transcendental" + elif max_deg==2: dom_type="quadratic" + else: dom_type="linear" + + # DOF + n_obs=sum(1 for v in problem.variables if problem.bounds[v][0]==problem.bounds[v][1]) + n_free_dof=max(0,n_vars-n_obs-n_eq) + + # SymPy pre-solve attempt (for small polynomial systems) + exact_solutions=[]; solvable=False + if n_vars<=SYMPY_MAX_VARS and dom_type in ("linear","quadratic") and not has_transcendental: + exact_solutions,solvable=_try_sympy_solve(problem) + if solvable: + notes.append(f"✓ SymPy found {len(exact_solutions)} exact solution(s) — templates loaded") + else: + notes.append("SymPy attempted (no closed form) — proceeding to ray search") + + return StructuralSketch( + axiom_affinities=affinities, + solvable_by_sympy=solvable, + exact_solutions=exact_solutions, + n_free_dof=n_free_dof, + has_conservation=has_conservation, + has_bilinear=bool(problem.bilinear_pairs), + has_ordering=bool(problem.ordering_pairs), + has_transcendental=has_transcendental, + dominant_type=dom_type, + sketch_notes=notes, + ) + +def generate_templates(problem:Problem,sketch:StructuralSketch) -> List[HypothesisTemplate]: + """ + Generates analytically-derived partial hypotheses from the structural sketch. + These are the 'must happen' elements — algebraic facts about what any + valid solution must contain. Stochastic rays fill the remaining gaps. + """ + templates:List[HypothesisTemplate]=[] + b_mid={v:(problem.bounds[v][0]+problem.bounds[v][1])/2 for v in problem.variables} + + # ── Type 1: SymPy exact solutions (highest confidence) ────────── + for i,sol in enumerate(sketch.exact_solutions): + templates.append(HypothesisTemplate( + template_id=f"sympy_{i}", + pinned_vars=sol, + free_vars=[v for v in problem.variables if v not in sol], + source="sympy_exact", + confidence=0.99, + derivation=f"SymPy exact solution #{i+1}")) + + # ── Type 2: Conservation projections ──────────────────────────── + for mc in problem.compiled_constraints: + if mc.kind!="equality" or mc.weight<5.0 or not mc.projections: continue + for v,projs in mc.projections.items(): + lo,hi=problem.bounds.get(v,(-1e9,1e9)) + for proj in projs: + try: + val=float(proj["func"](*[b_mid.get(s,0.0) for s in proj["syms"]])) + if math.isfinite(val) and lo<=val<=hi: + templates.append(HypothesisTemplate( + template_id=f"cons_{v}_{hash(mc.expr_str)%9999}", + pinned_vars={v:val}, + free_vars=[u for u in problem.variables if u!=v], + source="conservation", + confidence=0.75, + derivation=f"Conservation {mc.expr_str} → {v}={val:.4f}")) + except: pass + + # ── Type 3: Monotone product splits (strongest for bilinear) ──── + for v_small,v_large,k in problem.monotone_targets: + lo_s,hi_s=problem.bounds.get(v_small,(-1e9,1e9)) + lo_l,hi_l=problem.bounds.get(v_large,(-1e9,1e9)) + tb=_global_hc4_tighten_bounds(problem) + for ratio in [0.1,0.2,0.25,0.3,0.4,0.5,0.6,0.707,0.8,0.9,0.95]: + vs_sq=k*ratio + if vs_sq<=0: continue + vs=math.sqrt(vs_sq); vl=k/vs + if not(lo_s<=vs<=hi_s and lo_l<=vl<=hi_l and vs<=vl): continue + nb=dict(b_mid); nb[v_small]=vs; nb[v_large]=vl + # HC4 cascade for propagation + box={u:IV(*tb.get(u,problem.bounds.get(u,(-10,10)))) for u in problem.variables} + box[v_small]=IV(vs-1e-6,vs+1e-6); box[v_large]=IV(vl-1e-6,vl+1e-6) + cont=_hc4(box,problem.compiled_constraints) + pinned={v_small:vs,v_large:vl} + if cont: + for u,iv in cont.items(): + if u in problem.bounds: nb[u]=iv.mid() + pinned={u:nb[u] for u in problem.variables if cont[u].width()<1e-2} + templates.append(HypothesisTemplate( + template_id=f"mpr_{v_small}_{v_large}_r{int(ratio*100)}", + pinned_vars=pinned, + free_vars=[u for u in problem.variables if u not in pinned], + source="monotone_prod", + confidence=0.88, + derivation=f"Monotone {v_small}={vs:.4f}≤{v_large}={vl:.4f} (k={k:.3f},r={ratio})")) + + # ── Type 4: Algebraic projection roots ───────────────────────── + for mc in problem.compiled_constraints: + if mc.kind!="equality" or not mc.projections: continue + for v,projs in mc.projections.items(): + lo,hi=problem.bounds.get(v,(-1e9,1e9)) + for proj in projs: + try: + val=float(proj["func"](*[b_mid.get(s,0.0) for s in proj["syms"]])) + if math.isfinite(val) and lo<=val<=hi: + templates.append(HypothesisTemplate( + template_id=f"proj_{v}_{hash(mc.expr_str)%9999}", + pinned_vars={v:val}, + free_vars=[u for u in problem.variables if u!=v], + source="projection", + confidence=0.72, + derivation=f"Root of {mc.expr_str[:30]} → {v}={val:.4f}")) + except: pass + + # ── Type 5: Symmetry orbits (swap equivalent variables) ───────── + bound_groups=defaultdict(list) + for v in problem.variables: bound_groups[problem.bounds[v]].append(v) + for bnd,grp in bound_groups.items(): + if len(grp)<2: continue + # All variables in group have same bounds — they may be interchangeable + # Test averaged assignment + avg=sum(b_mid[v] for v in grp)/len(grp) + lo,hi=bnd + if lo<=avg<=hi: + pinned={v:avg for v in grp} + templates.append(HypothesisTemplate( + template_id=f"sym_avg_{'_'.join(grp[:3])}", + pinned_vars=pinned, + free_vars=[u for u in problem.variables if u not in pinned], + source="symmetry", + confidence=0.55, + derivation=f"Symmetry orbit: {grp} averaged to {avg:.4f}")) + + # De-duplicate by pinned_vars signature and sort by confidence + seen=set(); unique=[] + for t in sorted(templates,key=lambda t:-t.confidence): + key=str(sorted(t.pinned_vars.items())) + if key not in seen: seen.add(key); unique.append(t) + + return unique[:TEMPLATE_BATCH_SIZE] + +def templates_to_hypotheses( + templates:List[HypothesisTemplate], + problem:Problem, + init_binding:Dict[str,float]) -> List['Hypothesis']: + """Convert templates to Hypothesis objects for batched evaluation.""" + hyps=[] + for t in templates: + binding=dict(init_binding) + binding.update(t.pinned_vars) + hyps.append(Hypothesis( + hid=t.template_id, + binding=binding, + h_type=t.source, + claim=t.derivation, + derivation=[t.source], + pinned_vars=t.pinned_vars, + free_vars=t.free_vars, + confidence=t.confidence)) + return hyps + +# Placeholder — will be filled after Axiom class is defined +_ALL_AXIOMS_PLACEHOLDER:List[str]=[] + +# ══════════════════════════════════════════════════════════════════════ +# SECTION 7: BATCHED MASKED DEDUCTION # ══════════════════════════════════════════════════════════���═══════════ @dataclass class L9Certificate: @@ -499,24 +899,21 @@ def _batched_deduce_and_evaluate( if not hyps: return [] B=len(hyps); V=len(problem.variables) - x_data = [] - mask_data = [] - target_data = [] + x_data=[]; mask_data=[]; target_data=[] for hyp in hyps: - xr, mr, tr = [], [], [] + xr,mr,tr=[],[],[] for v in problem.variables: if v in hyp.pinned_vars: - val = hyp.pinned_vars[v] + val=hyp.pinned_vars[v] xr.append(val); mr.append(0.0); tr.append(val) else: - val = hyp.binding.get(v, (problem.bounds[v][0]+problem.bounds[v][1])/2) + val=hyp.binding.get(v,(problem.bounds[v][0]+problem.bounds[v][1])/2) xr.append(val); mr.append(1.0); tr.append(0.0) x_data.append(xr); mask_data.append(mr); target_data.append(tr) - X = torch.tensor(x_data, device=DEVICE, dtype=torch.float32, requires_grad=True) - mask = torch.tensor(mask_data, device=DEVICE, dtype=torch.float32) - target = torch.tensor(target_data, device=DEVICE, dtype=torch.float32) - + X=torch.tensor(x_data,device=DEVICE,dtype=torch.float32,requires_grad=True) + mask=torch.tensor(mask_data,device=DEVICE,dtype=torch.float32) + target=torch.tensor(target_data,device=DEVICE,dtype=torch.float32) optimizer=torch.optim.Adam([X],lr=0.05) for _ in range(DEDUCE_ADAM_STEPS): @@ -525,7 +922,7 @@ def _batched_deduce_and_evaluate( if isinstance(ce,torch.Tensor) and (ce 1e-4] - n_dom = len(dom_vars) - if n_dom<=1: tension_class="isolated" - elif n_dom==2: tension_class="relational" - else: tension_class="systemic" + dom_vars=[problem.variables[idx] for idx in topk_idx_np[i] + if float(grads_np[i,idx])>1e-4] + n_dom=len(dom_vars) + tension_class=("isolated" if n_dom<=1 else "relational" if n_dom==2 else "systemic") results.append((final_b,float(ce_vals[i]),dom_vars,tension_class)) return results @@ -572,7 +967,7 @@ def _mprt_sample(problem,work_box,N): return {v:float(X[best_idx,i].item()) for i,v in enumerate(var_list)},ce_batch[best_idx].item() # ══════════════════════════════════════════════════════════════════════ -# SECTION 7: AXIOMS +# SECTION 8: AXIOMS # ══════════════════════════════════════════════════════════════════════ class Axiom: CONTINUOUS="CONTINUOUS"; DISCRETE="DISCRETE"; QUADRATIC="QUADRATIC" @@ -589,6 +984,9 @@ class Axiom: ALL_AXIOMS=[getattr(Axiom,a) for a in dir(Axiom) if not a.startswith("__")] AXIOM_ABBR={a:a[:3] for a in ALL_AXIOMS}; AXIOM_ABBR[Axiom.MONOTONE_PRODUCT]="MPR" +# Now fill the placeholder used in compute_sketch +_ALL_AXIOMS_PLACEHOLDER.extend(ALL_AXIOMS) + ADJACENT_CONTRADICTIONS:List[Tuple[str,str]]=[ (Axiom.DISCRETE,Axiom.CONTINUOUS),(Axiom.INJECTIVE,Axiom.SURJECTIVE), (Axiom.ORDERED,Axiom.SYMMETRIC),(Axiom.ATOMIC,Axiom.COMPOSITE), @@ -605,9 +1003,9 @@ def sequence_valid(seq:List[str]) -> bool: return True # ══════════════════════════════════════════════════════════════════════ -# SECTION 8: SHARED DATACLASSES +# SECTION 9: SHARED DATACLASSES # ══════════════════════════════════════════════════════════════════════ -RAY_TYPES=["seed","branch","tension","scout","recombine","invert","target"] +RAY_TYPES=["seed","branch","tension","scout","recombine","invert","target","template"] @dataclass class Hypothesis: @@ -658,53 +1056,74 @@ class StructuralModel: resonant_pairs:List[Tuple[str,str]]=field(default_factory=list) # ══════════════════════════════════════════════════════════════════════ -# SECTION 9: HYPOTHESIS CONSTRUCTORS +# SECTION 10: HYPOTHESIS CONSTRUCTORS (dimension-adaptive fixes) # ══════════════════════════════════════════════════════════════════════ 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) def _hyp_continuous(p,bt,a,m): return [_make_hyp("cnt",bt.binding,"continuous","Manifold",[],{},p.variables,0.45)] + def _hyp_discrete(p,bt,a,m): + """ + FIX 24.0: HC4 delta is now 5% of bound range, not fixed ±1. + Fixed ±1 was meaningless for bounds like [-1000, 1000]. + """ b=dict(bt.binding); pinned={} for sn in p.scope_order: svars=p.scope_vars.get(sn,[]); smcs=[p.compiled_constraints[i] for i in p.scope_groups.get(sn,[])] if svars and smcs: - box={v:IV(b.get(v,0)-1,b.get(v,0)+1) for v in svars if v in p.bounds} + # Dimension-adaptive delta: 5% of each variable's range + box={v:IV( + b.get(v,0)-max(0.05*(p.bounds[v][1]-p.bounds[v][0]),1e-4), + b.get(v,0)+max(0.05*(p.bounds[v][1]-p.bounds[v][0]),1e-4)) + for v in svars if v in p.bounds} cont=_hc4(box,smcs) if cont: - for v,iv in cont.items(): b[v]=iv.mid(); (pinned.update({v:b[v]}) if iv.width()<1e-2 else None) + for v,iv in cont.items(): + b[v]=iv.mid() + if iv.width()<1e-2: pinned[v]=b[v] return [_make_hyp("dis",b,"discrete","TopoScope",[],pinned,p.variables,0.80)] + def _hyp_quadratic(p,bt,a,m): hyps=[]; b=dict(bt.binding) if bt.l9 and bt.l9.dominant_vars: - 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)) + 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)) return hyps + def _hyp_bilinear(p,bt,a,m): hyps=[]; b=dict(bt.binding) - for vi, vj in p.bilinear_pairs: + for vi,vj in p.bilinear_pairs: 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)) if product<=0: continue gm=math.sqrt(product) if lo_i<=gm<=hi_i and lo_j<=gm<=hi_j: nb=dict(b); nb[vi]=nb[vj]=gm - 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)) - for ratio in [0.4, 0.7071, 0.9]: + 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)) + for ratio in [0.4,0.7071,0.9]: vs=gm*ratio; vl=product/(vs+1e-9) if lo_i<=vs<=hi_i and lo_j<=vl<=hi_j and vsvs: nb3=dict(b); nb3[vi]=vl; nb3[vj]=vs - hyps.append(_make_hyp(f"bil_desc_{int(ratio*100)}_{vi}_{vj}",nb3,"bilinear",f"BilDesc({vi}={vl:.3f}>{vj}={vs:.3f})",["bilinear"],{vi:vl,vj:vs},[v for v in p.variables if v not in [vi,vj]],0.75)) + hyps.append(_make_hyp(f"bil_desc_{int(ratio*100)}_{vi}_{vj}",nb3,"bilinear", + f"BilDesc({vi}={vl:.3f}>{vj}={vs:.3f})",["bilinear"],{vi:vl,vj:vs}, + [v for v in p.variables if v not in [vi,vj]],0.75)) return hyps + def _hyp_monotone_product(p,bt,a,m): hyps=[]; b=dict(bt.binding) if not p.monotone_targets: return hyps tb=_global_hc4_tighten_bounds(p) - for v_small, v_large, k in p.monotone_targets: - lo_s,hi_s=p.bounds.get(v_small,(-1e18,1e18)); lo_l,hi_l=p.bounds.get(v_large,(-1e18,1e18)) + for v_small,v_large,k in p.monotone_targets: + lo_s,hi_s=p.bounds.get(v_small,(-1e9,1e9)); lo_l,hi_l=p.bounds.get(v_large,(-1e9,1e9)) for ratio in [0.1,0.2,0.3,0.4,0.5,0.6,0.707,0.8,0.9,0.95]: vs_sq=k*ratio if vs_sq<=0: continue @@ -719,15 +1138,80 @@ def _hyp_monotone_product(p,bt,a,m): for u,iv in cont.items(): if u in p.bounds: nb[u]=iv.mid() pinned={u:nb[u] for u in p.variables if cont[u].width()<1e-2} - 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)) + 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)) return hyps -def _hyp_metric(p,bt,a,m): return [_make_hyp("met",bt.binding,"metric","Radial",[],{},p.variables,0.75)] -def _hyp_symmetric(p,bt,a,m): - hyps=[]; b=dict(bt.binding); vl=p.variables - if len(vl)>=2: - mid=(b.get(vl[0],0)+b.get(vl[1],0))/2; nb=dict(b); nb[vl[0]]=nb[vl[1]]=mid - hyps.append(_make_hyp("sym",nb,"symmetric","AveragePin",[],{vl[0]:mid,vl[1]:mid},p.variables,0.60)) + +def _hyp_metric(p,bt,a,m): + """ + FIX 24.0: Robust sum-of-squares detection for arbitrary dimension. + Handles both unit-sphere patterns and general norms. + """ + hyps=[]; b=dict(bt.binding) + for mc in p.compiled_constraints: + if mc.kind!="equality" or not mc.parsed: continue + if not mc.parsed.is_Add: continue + # Find all squared terms and variables involved + sq_terms=[t for t in mc.parsed.args if t.is_Pow and t.args[1]==2] + if len(sq_terms)<1: continue + vars_in=[str(s) for s in mc.parsed.free_symbols if str(s) in p.variables] + if not vars_in: continue + # Find the constant offset (the target norm) + const_terms=[float(t) for t in mc.parsed.args if t.is_Number] + if not const_terms: continue + target=-const_terms[0] # expr = sum(xi^2) + const = 0 → sum(xi^2) = -const + if target<=0: continue + curr_val=sum(b.get(v,0)**2 for v in vars_in) + if curr_val<1e-8: continue + scale=math.sqrt(target/curr_val) + nb=dict(b) + for v in vars_in: + lo,hi=p.bounds.get(v,(-10,10)) + nb[v]=max(lo,min(hi,b.get(v,0)*scale)) + 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)) return hyps + +def _hyp_symmetric(p,bt,a,m): + """ + FIX 24.0: Check all variable pairs within scope groups, not just [0] and [1]. + Previous version missed symmetry in higher-dimensional problems. + """ + hyps=[]; b=dict(bt.binding) + + # Check all pairs within each scope group + groups_to_check=list(p.scope_vars.values()) if p.scope_vars else [p.variables] + if not any(p.scope_vars.values()): groups_to_check=[p.variables] + + seen_pairs=set() + for grp in groups_to_check: + if not grp: continue + vl=grp if grp else p.variables + for i in range(min(len(vl),8)): # cap at 8 to avoid O(n²) explosion + for j in range(i+1,min(len(vl),8)): + vi,vj=vl[i],vl[j] + if (vi,vj) in seen_pairs: continue + 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=b.get(vi,0); bvj=b.get(vj,0) + # Valid swap: each value must fit in the other's bounds + if lo_i<=bvj<=hi_i and lo_j<=bvi<=hi_j: + nb=dict(b); nb[vi],nb[vj]=bvj,bvi + 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)) + # Also test average (sometimes the symmetric solution IS the average) + avg=(bvi+bvj)/2 + if lo_i<=avg<=hi_i and lo_j<=avg<=hi_j: + nb2=dict(b); nb2[vi]=avg; nb2[vj]=avg + 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)) + return hyps[:10] # Cap output + def _hyp_ordered(p,bt,a,m): return [_make_hyp("ord",bt.binding,"ordered","OrderBal",[],{},p.variables,0.67)] def _hyp_monotone(p,bt,a,m): return [_make_hyp("mon",bt.binding,"monotone","MonoPath",[],{},p.variables,0.67)] def _hyp_convex(p,bt,a,m): return [_make_hyp("cvx",bt.binding,"convex","ConvMix",[],{},p.variables,0.63)] @@ -767,7 +1251,7 @@ def _hyp_atomic(p,bt,a,m): for proj in projs: try: val=float(proj["func"](*[b.get(s,0.0) for s in proj["syms"]])) - lo,hi=p.bounds.get(v,(-1e18,1e18)) + lo,hi=p.bounds.get(v,(-1e9,1e9)) if math.isfinite(val) and lo<=val<=hi: nb=dict(b); nb[v]=val hyps.append(_make_hyp(f"ato_{v}",nb,"atomic",f"Solve({v})",[],{v:val},p.variables,0.70)) @@ -811,7 +1295,7 @@ AXIOM_CONSTRUCTORS={ } # ══════════════════════════════════════════════════════════════════════ -# SECTION 10: CREATIVE SEEDER +# SECTION 11: CREATIVE SEEDER (sketch-aware) # ══════════════════════════════════════════════════════════════════════ class CreativeSeeder: def target_seeds(self,anchors:List[AXLInvariant]) -> List[AxiomRay]: @@ -827,34 +1311,59 @@ class CreativeSeeder: seeds.append(AxiomRay([Axiom.CONSERVED],f"TGT_CSV_{a.name}","target")) return seeds - def intelligent_branch(self,ray,out_baton,remaining_axioms,branch_width) -> List[AxiomRay]: + def intelligent_branch(self,ray,out_baton,remaining_axioms,branch_width, + sketch:Optional[StructuralSketch]=None) -> List[AxiomRay]: + """ + 24.0: Multiplies sketch affinities into allosteric scoring. + Two signals combined: gradient topology (local) + structural sketch (global). + """ dom_vars=out_baton.l9.dominant_vars if out_baton.l9 else [] tension_class=out_baton.l9.tension_class if out_baton.l9 else "unknown" n_dom=len(dom_vars) - effective_width = branch_width - if tension_class == "systemic" and out_baton.ce > 0.1: - effective_width = BRANCH_WIDTH_SYSTEMIC - + effective_width=branch_width + if tension_class=="systemic" and out_baton.ce>0.1: + effective_width=BRANCH_WIDTH_SYSTEMIC + isolated ={Axiom.ATOMIC,Axiom.EXTREMAL,Axiom.MUTABLE,Axiom.DUALITY,Axiom.LOCALITY} - relational ={Axiom.SYMMETRIC,Axiom.BILINEAR,Axiom.MONOTONE_PRODUCT, - Axiom.ORDERED,Axiom.METRIC,Axiom.INJECTIVE} - systemic ={Axiom.CONSERVED,Axiom.NETWORK,Axiom.HOLISM,Axiom.COMPOSITE,Axiom.ENTROPY} + relational={Axiom.SYMMETRIC,Axiom.BILINEAR,Axiom.MONOTONE_PRODUCT, + Axiom.ORDERED,Axiom.METRIC,Axiom.INJECTIVE} + systemic ={Axiom.CONSERVED,Axiom.NETWORK,Axiom.HOLISM,Axiom.COMPOSITE,Axiom.ENTROPY} scored=[] for ax in remaining_axioms: - w=1.0 - if n_dom==1 and ax in isolated: w+=5.0 - elif n_dom==2 and ax in relational: w+=5.0 - elif n_dom>=3 and ax in systemic: w+=5.0 - scored.append((w,ax)) - scored.sort(key=lambda x:x[0]*random.random(),reverse=True) + # Allosteric component (gradient topology) + w_allos=1.0 + if n_dom==1 and ax in isolated: w_allos+=5.0 + elif n_dom==2 and ax in relational: w_allos+=5.0 + elif n_dom>=3 and ax in systemic: w_allos+=5.0 + + # Sketch component (structural prior — the world model) + w_sketch=sketch.axiom_affinities.get(ax,1.0) if sketch else 1.0 + # Combined score: both signals multiply (neither overrides) + w_combined=w_allos*w_sketch + scored.append((w_combined,ax)) + + scored.sort(key=lambda x:x[0]*random.random(),reverse=True) children=[] for _,axiom in scored[:effective_width]: child=ray.extend(axiom,"branch",new_prior=out_baton.ce) if child: child.baton=out_baton; children.append(child) return children + def sketch_weighted_seeds(self,sketch:StructuralSketch, + init_ce:float) -> List[AxiomRay]: + """ + Order seed queue by sketch affinities so high-affinity axioms fire first. + This is not bias — it's the problem telling us what it needs. + """ + affinities=sketch.axiom_affinities + seeds_scored=sorted( + [(affinities.get(a,1.0),i,a) for i,a in enumerate(ALL_AXIOMS)], + key=lambda x:-x[0]) + return [AxiomRay([a],f"S{i}","seed",ce_prior=init_ce) + for _,i,a in seeds_scored] + def tension_seeds(self,max_n:int=3000) -> List[AxiomRay]: results=[] for (a,c) in ADJACENT_CONTRADICTIONS: @@ -890,7 +1399,8 @@ class CreativeSeeder: ib_baton=Baton(binding=ib,ce=ib_ce,ray_id="INTERP") cut=min(len(ray_a.sequence),len(ray_b.sequence))//2 if cut>0: - seq=ray_a.sequence[:cut]+[x for x in ray_b.sequence[cut:] if x not in ray_a.sequence[:cut]] + seq=ray_a.sequence[:cut]+[x for x in ray_b.sequence[cut:] + if x not in ray_a.sequence[:cut]] if sequence_valid(seq): results.append(AxiomRay(seq,f"RC_l{int(lam*100)}","recombine", baton=ib_baton,ce_prior=ib_ce)) @@ -916,17 +1426,17 @@ class CreativeSeeder: CREATIVE_SEEDER=CreativeSeeder() # ══════════════════════════════════════════════════════════════════════ -# SECTION 11: VERIFY LAYER +# SECTION 12: VERIFY LAYER # ══════════════════════════════════════════════════════════════════════ -def _verify(binding:Dict[str,float],base_problem:Problem, - anchors:List[AXLInvariant]) -> Tuple[bool,bool,Dict[str,Tuple[float,bool]],float]: +def _verify(binding,base_problem,anchors): g1_ce=base_problem.scalar_energy(binding) g1_pass=g1_ce=-inv.tolerance @@ -938,9 +1448,10 @@ def _verify(binding:Dict[str,float],base_problem:Problem, return g1_pass,g2_pass,g2,round(g1_ce,6) # ══════════════════════════════════════════════════════════════════════ -# SECTION 12: SEQUENCE RAY TRACER +# SECTION 13: SEQUENCE RAY TRACER (sketch-integrated) # ══════════════════════════════════════════════════════════════════════ class SequenceRayTracer: + def trace(self,axl_def:AXLProblemDef,base_problem:Problem): hero_traces:List[HypothesisTrace]=[] baton_registry:Dict[str,Baton]={} @@ -949,27 +1460,86 @@ class SequenceRayTracer: resonant_pairs:List[Tuple[str,str]]=[] for inv in axl_def.anchors: - if not inv.compiled_func: - inv.compile(base_problem.variables) - + if not inv.compiled_func: inv.compile(base_problem.variables) + + # ── Phase 0: Structural Sketch ────────────────────────────── + _update_state(phase="SKETCHING") + _add_log("🗺 Computing structural sketch…") + sketch=compute_sketch(base_problem) + sketch_summary="; ".join(sketch.sketch_notes[:4]) + _update_state(sketch_summary=sketch_summary) + _add_log(f"✓ Sketch: {sketch.dominant_type} system, DOF={sketch.n_free_dof}") + for note in sketch.sketch_notes[:3]: _add_log(f" · {note}") + + # ── Phase 1: Template Generation ──────────────────────────── + _update_state(phase="TEMPLATING") + _add_log("🔬 Generating hypothesis templates…") + templates=generate_templates(base_problem,sketch) + _update_state(template_count=len(templates)) + _add_log(f"✓ {len(templates)} templates from {sum(1 for t in templates if t.source=='sympy_exact')} SymPy + " + f"{sum(1 for t in templates if t.source=='monotone_prod')} MPR + " + f"{sum(1 for t in templates if t.source=='conservation')} conservation + " + f"{sum(1 for t in templates if t.source=='projection')} projections") + + # ── Phase 2: Initial sampling ──────────────────────────────── init_b,init_ce=_mprt_sample(base_problem, {v:IV(*base_problem.bounds[v]) for v in base_problem.variables},N_MPRT_EXPLORE) seed_baton=Baton(binding=init_b,ce=init_ce,ray_id="SEED", l9=L9Certificate(init_ce,base_problem.variables[:3],[],"systemic")) + # ── Phase 3: Evaluate all templates before rays fire ──────── + best_ce=init_ce; best_binding=dict(init_b) + if templates: + _add_log("⚗ Evaluating templates (Phase 0 batch)…") + template_hyps=templates_to_hypotheses(templates,base_problem,init_b) + t_results=_batched_deduce_and_evaluate(base_problem,template_hyps) + for (th,template),(final_b,final_ce,dom_vars,tc) in zip( + zip(template_hyps,templates),t_results): + g1p,g2p,inv_res,g1ce=_verify(final_b,base_problem,axl_def.anchors) + overall=g1p and g2p + if overall or final_ce=2: candidates=[r for r in successful_rays if r.ray_id!=ray.ray_id] if candidates: @@ -1068,10 +1636,8 @@ class SequenceRayTracer: bb=baton_registry.get(partner.ray_id) if bb is not None: new_children.extend(CREATIVE_SEEDER.recombine(ray,partner,ba,bb)[:3]) - new_children.extend( CREATIVE_SEEDER.resonance_extensions(ray,final_ce,resonant_pairs)) - for child in new_children: if child.ray_type in ("seed","branch","target"): queues["core"].append(child) elif child.ray_type in ("scout","tension"): queues["explore"].append(child) @@ -1079,483 +1645,304 @@ class SequenceRayTracer: queues["core"].sort(key=lambda r:r.ce_prior+(r.depth*0.0001)) queues["genetic"].sort(key=lambda r:r.ce_prior+(r.depth*0.0001)) - + with STATE_LOCK: - GLOBAL_SOLVE_STATE["best_ce"] = best_ce - GLOBAL_SOLVE_STATE["total_fired"] = total_fired - GLOBAL_SOLVE_STATE["best_ray"] = model.best_ray - for t in batch_heroes: - GLOBAL_SOLVE_STATE["recent_traces"].append(t) + GLOBAL_SOLVE_STATE["best_ce"]=best_ce + GLOBAL_SOLVE_STATE["total_fired"]=total_fired + GLOBAL_SOLVE_STATE["best_ray"]=model.best_ray + for t in batch_heroes: GLOBAL_SOLVE_STATE["recent_traces"].append(t) if solved: break return best_binding,best_ce,list(GLOBAL_SOLVE_STATE["recent_traces"]),total_fired,allosteric_counts - -# ══════════════════════════════════════════════════════════════════ -# SECTION 13: LLM BRIDGE (GOOGLE GENAI 3.1) -# ══════════════════════════════════════════════════════════════════ - -ENCODER_SYSTEM_PROMPT = """You are the Encoder for the Practicality Wisdom Layer — a neuro-symbolic +# ══════════════════════════════════════════════════════════════════════ +# SECTION 14: LLM BRIDGE +# ══════════════════════════════════════════════════════════════════════ +ENCODER_SYSTEM_PROMPT="""You are the Encoder for the Practicality Wisdom Layer — a neuro-symbolic constraint satisfaction engine. Your job is STRICT SLOT-FILLING, not reasoning. -You read a natural language problem description and produce a structured -JSON object that represents its mathematical constraints. - -You do NOT solve the problem. You do NOT guess the structural topology. You only translate. - -══════════════════════════════════════════════════════════════════ -PART 1: THE AXL STRUCTURE -══════════════════════════════════════════════════════════════════ - -You must output a single JSON object matching this schema exactly: +You read a natural language problem and produce a structured JSON AXL object. +OUTPUT SCHEMA (JSON only, no markdown): { - "name": string, // CamelCase, no spaces - "description": string, // one sentence - "variables": [ - { - "name": string, // short lowercase identifier (x, v1, theta, etc.) - "lo": number, // OPTIONAL: ONLY provide if the problem explicitly limits this (e.g., > 0) - "hi": number // OPTIONAL: ONLY provide if the problem explicitly limits this - } - ], - "constraints": [ - { - "kind": "EQ" | "GEQ" | "LEQ" | "CONSERVE", - "expr": string, // valid Python/sympy expression using variable names - "weight": number // 1.0 default; 5.0 for hard constraints; 10.0 for conservation laws - } - ], - "anchors": [ - { - "name": string, // snake_case identifier for this condition - "expr": string, // sympy expression that equals 0 when satisfied - "tolerance": number, // how close to 0 counts as solved (default 0.001) - "mode": "eq" | "geq" | "leq" - } - ], - "observations": { - "variable_name": number // variables whose values are STRICTLY KNOWN/FIXED in the prompt - } + "name": string, + "description": string, + "variables": [{"name": string, "lo": number (if bounded), "hi": number (if bounded)}], + "constraints": [{"kind": "EQ"|"GEQ"|"LEQ"|"CONSERVE", "expr": string, "weight": number}], + "anchors": [{"name": string, "expr": string, "tolerance": number, "mode": "eq"|"geq"|"leq"}], + "observations": {"variable_name": number} } -CRITICAL: Output ONLY the JSON object. No preamble, no markdown fences. - -══════════════════════════════════════════════════════════════════ -PART 2: ENCODING RULES -══════════════════════════════════════════════════════════════════ - -VARIABLES & BOUNDS: - • Use short names: x, y, v, w1, cb - • DO NOT INVENT BOUNDS. If the text says "probabilities", set lo=0.0, hi=1.0. - If the text says nothing, omit "lo" and "hi" entirely. - • Fixed values go in "observations", not as tight bounds. - • DO include observed variables in the variables list. The engine handles pinning. - -CONSTRAINTS & ANCHORS: - • EQ: expr = 0 (e.g., "x**2 + y**2 - 1.0") - • GEQ: expr ≥ 0 - • LEQ: expr ≤ 0 - • CONSERVE: inviolable laws (weight 10.0 automatically) - • Expressions must be valid Python/sympy: use **, *, +, -, / - • Do NOT use =, >=, <= in expressions — only the expression that evaluates against 0. - • Anchors are the verification conditions. What MUST be true to accept the solution? - -══════════════════════════════════════════════════════════════════ -PART 3: FAILURE HANDLING & ALGEBRAIC REDUCTION -══════════════════════════════════════════════════════════════════ - -If the user message indicates the PREVIOUS ATTEMPT FAILED: -1. If "Gate 2 failed": Adjust constraint weights or fix signs in the expressions. -2. If "GEOMETRIC SOLVER FAILED": The constraint manifold is too complex (e.g. cubic volumes). - You must perform ALGEBRAIC REDUCTION: - - Identify simple equalities (e.g., y = 2*z). - - Substitute them into the harder equations to eliminate variables. - - Remove the substituted variable from the "variables" list entirely. - - Output the new, mathematically equivalent but lower-dimensional AXL json. - -Output ONLY the JSON. No preamble. -""" - -COLLAPSER_SYSTEM_PROMPT = """You are the Collapser for the Practicality Wisdom Layer. -The system has derived a structural isomorphism (an Axiom Sequence) to collapse -the problem constraints you encoded into a verified numerical solution. - -Your job is to explain the solution using this structural thinking. - -You receive a JSON object containing: - • The original natural language problem - • Whether the solver succeeded (solved/partial/unsolved) - • The verified variable binding (the numerical solution) - • The compiled PSL Program Text (The exact mathematical constraints the engine proved) - • The ISOMORPHISM HYPOTHESIS (best_ray_sequence): The geometric theory that unlocked it. - -══════════════════════════════════════════════════════════════════ -TONE AND FORMAT RULES -══════════════════════════════════════════════════════════════════ -• Write for a domain expert, not a general audience. -• Lead with the status: SOLVED / PARTIAL / UNSOLVED -• Provide the final binding values with domain-appropriate context. -• EXPLAIN THE ISOMORPHISM: Explicitly explain *how* the `isomorphism_hypothesis` - (the Axiom sequence like SYMMETRIC→MONOTONE) structurally describes the - `psl_program_text`. Do not just list the axioms; explain why the problem's - topology fits that geometry. -• Keep the entire output under 300 words. -""" - -def encode_problem_to_axl(problem_text: str, api_key: str) -> AXLProblemDef: - if not api_key: - raise ValueError("Gemini API Key is missing.") - - client = genai.Client(api_key=api_key) - config = types.GenerateContentConfig( +RULES: +• DO NOT invent bounds. Only add lo/hi if the problem text explicitly limits them. +• Expressions: valid Python/sympy (**, *, +, -, /). No =, >=, <= in expressions. +• CONSERVE = inviolable sum (weight 10.0). EQ = equals zero. GEQ = ≥ zero. LEQ = ≤ zero. +• Anchors are verification conditions. What MUST be true for the solution to be valid? +• Fixed/observed values go in "observations". + +If message says PREVIOUS ATTEMPT FAILED: + • Gate 2 fail → Fix constraint signs/weights. + • GEOMETRIC SOLVER FAILED → Perform algebraic reduction: eliminate variables via substitution. +Output ONLY the JSON.""" + +COLLAPSER_SYSTEM_PROMPT="""You are the Collapser for the Practicality Wisdom Layer. +The system found a solution using an axiomatic sequence (the isomorphism). + +You receive: original problem, solution binding, PSL program text, isomorphism sequence, +structural sketch notes (what the world model found), invariant verification results. + +Write for a domain expert. Under 300 words. +• Lead with SOLVED / PARTIAL / UNSOLVED. +• Give the binding with domain context. +• Explain the STRUCTURAL SKETCH: what did the pre-analysis reveal about this problem's topology? +• Explain the ISOMORPHISM: why does the axiom sequence structurally match the constraint geometry? +• Be specific — name the axioms and explain what each geometric move did.""" + +def encode_problem_to_axl(problem_text,api_key) -> AXLProblemDef: + if not api_key: raise ValueError("Gemini API Key missing.") + client=genai.Client(api_key=api_key) + config=types.GenerateContentConfig( system_instruction=[types.Part.from_text(text=ENCODER_SYSTEM_PROMPT)], - response_mime_type="application/json", - temperature=0.1, - ) - - response = client.models.generate_content( + response_mime_type="application/json",temperature=0.1) + resp=client.models.generate_content( model=GEMINI_MODEL, - contents=[types.Content(role="user", parts=[types.Part.from_text(text=problem_text)])], - config=config, - ) - return _parse_axl_json(response.text) - -def _parse_axl_json(raw_json: str) -> AXLProblemDef: - text = raw_json.strip() - if text.startswith("```"): - text = text.split("```")[1] - if text.startswith("json"): text = text[4:] - text = text.strip().rstrip("`").strip() - - d = json.loads(text) - anchors = [ - AXLInvariant( - name=a["name"], expr=a["expr"], - tolerance=a.get("tolerance", VERIFY_G2_TOLERANCE), - mode=a.get("mode", "eq") - ) - for a in d.get("anchors", []) - ] - - variables = [] - for v in d["variables"]: - variables.append({ - "name": v["name"], - # Fallback bounds prevent PyTorch volume explosions in non-linear manifolds - "lo": float(v.get("lo", -1000.0)), - "hi": float(v.get("hi", 1000.0)) - }) - - return AXLProblemDef( - name=d["name"], - description=d.get("description", ""), - axioms=set(), # Engine owns Axioms - variables=variables, - constraints=d.get("constraints", []), - scopes=d.get("scopes", []), - anchors=anchors, - observations=d.get("observations", {}), - ) - -def collapse_solution( - problem_text: str, - axl_def: AXLProblemDef, - psl_text: str, - binding: Dict[str, float], - g1_pass: bool, - g2_pass: bool, - invariant_results: Dict[str, Tuple[float, bool]], - best_ray: str, - total_fired: int, - api_key: str -) -> str: - if not api_key: return "ERROR: Gemini API Key required." - - client = genai.Client(api_key=api_key) - - payload = { - "original_problem": problem_text, - "solved": g1_pass and g2_pass, - "binding": {k: round(v, 6) for k, v in binding.items()}, - "psl_program_text": psl_text, - "isomorphism_hypothesis": best_ray, - "invariant_results":invariant_results, - } - - config = types.GenerateContentConfig( + contents=[types.Content(role="user",parts=[types.Part.from_text(text=problem_text)])], + config=config) + return _parse_axl_json(resp.text) + +def _parse_axl_json(raw_json) -> AXLProblemDef: + text=raw_json.strip() + if text.startswith("```"): text=text.split("```")[1]; (text:=text[4:]) if text.startswith("json") else text + text=text.strip().rstrip("`").strip() + d=json.loads(text) + anchors=[AXLInvariant(name=a["name"],expr=a["expr"], + tolerance=a.get("tolerance",VERIFY_G2_TOLERANCE), + mode=a.get("mode","eq")) for a in d.get("anchors",[])] + variables=[{"name":v["name"],"lo":float(v.get("lo",-1000.0)),"hi":float(v.get("hi",1000.0))} + for v in d["variables"]] + return AXLProblemDef(name=d["name"],description=d.get("description",""),axioms=set(), + variables=variables,constraints=d.get("constraints",[]), + scopes=d.get("scopes",[]),anchors=anchors, + observations=d.get("observations",{})) + +def collapse_solution(problem_text,axl_def,psl_text,binding,g1_pass,g2_pass, + inv_results,best_ray,total_fired,sketch_notes,api_key) -> str: + if not api_key: return "ERROR: API Key required." + client=genai.Client(api_key=api_key) + payload={"original_problem":problem_text,"solved":g1_pass and g2_pass, + "binding":{k:round(v,6) for k,v in binding.items()}, + "psl_program_text":psl_text,"isomorphism_hypothesis":best_ray, + "structural_sketch_notes":sketch_notes, + "invariant_results":inv_results} + config=types.GenerateContentConfig( thinking_config=types.ThinkingConfig(thinking_level="HIGH"), system_instruction=[types.Part.from_text(text=COLLAPSER_SYSTEM_PROMPT)], - temperature=0.2, - ) - - response = client.models.generate_content( + temperature=0.2) + resp=client.models.generate_content( model=GEMINI_MODEL, - contents=[types.Content(role="user", parts=[types.Part.from_text(text=json.dumps(payload, indent=2))])], - config=config, - ) - return response.text - -# ══════════════════════════════════════════════════════════════════ -# SECTION 14: GLOBAL SOLVE TASK (Background Thread) -# ══════════════════════════════════════════════════════════════════ - -def global_solve_task(original_problem_text: str, api_key: str): - _update_state( - is_running=True, phase="ENCODING", high_level_logs=[], - answer="", best_ce=float('inf'), total_fired=0, best_ray="—", recent_traces=deque(maxlen=25) - ) + contents=[types.Content(role="user",parts=[types.Part.from_text(text=json.dumps(payload,indent=2))])], + config=config) + return resp.text - MAX_ATTEMPTS = 3 - current_text = original_problem_text - used_key = api_key or DEFAULT_GEMINI_API_KEY - - for attempt in range(1, MAX_ATTEMPTS + 1): - _add_log(f"🔍 Encoding problem (Attempt {attempt}/{MAX_ATTEMPTS})…") - - try: - axl_def = encode_problem_to_axl(current_text, used_key) - except Exception as e: - _add_log(f"✗ Encoding failed: {e}") - _update_state(is_running=False, phase="ERROR") - return - - _add_log( - f"✓ Encoded `{axl_def.name}` | " - f"Vars: `{', '.join(v['name'] for v in axl_def.variables)}`" - ) +# ══════════════════════════════════════════════════════════════════════ +# SECTION 15: GLOBAL SOLVE TASK +# ══════════════════════════════════════════════════════════════════════ +def global_solve_task(original_problem_text,api_key): + _update_state(is_running=True,phase="ENCODING",high_level_logs=[], + answer="",best_ce=float('inf'),total_fired=0,best_ray="—", + recent_traces=deque(maxlen=25),sketch_summary="", + template_count=0,template_best_ce=float('inf')) + + MAX_ATTEMPTS=3; current_text=original_problem_text + used_key=api_key or DEFAULT_GEMINI_API_KEY + sketch_notes=[] + + for attempt in range(1,MAX_ATTEMPTS+1): + _add_log(f"🔍 Encoding (attempt {attempt}/{MAX_ATTEMPTS})…") + try: axl_def=encode_problem_to_axl(current_text,used_key) + except Exception as e: _add_log(f"✗ Encode failed: {e}"); _update_state(is_running=False,phase="ERROR"); return + _add_log(f"✓ `{axl_def.name}` | vars: {', '.join(v['name'] for v in axl_def.variables)}") _update_state(phase="COMPILING") try: - psl_text = AXL_COMPILER.compile(axl_def) - base_prob = build_base_problem(axl_def) - except Exception as e: - _add_log(f"✗ Compilation failed: {e}") - _update_state(is_running=False, phase="ERROR") - return - - _update_state(phase="SEARCHING") + psl_text=AXL_COMPILER.compile(axl_def); base_prob=build_base_problem(axl_def) + except Exception as e: _add_log(f"✗ Compile failed: {e}"); _update_state(is_running=False,phase="ERROR"); return try: - tracer = SequenceRayTracer() - binding, ce, traces, total_fired, allosteric = tracer.trace(axl_def, base_prob) - except Exception as e: - _add_log(f"✗ Solver error: {e}") - _update_state(is_running=False, phase="ERROR") - return + tracer=SequenceRayTracer() + binding,ce,traces,total_fired,allosteric=tracer.trace(axl_def,base_prob) + except Exception as e: _add_log(f"✗ Solver error: {e}"); _update_state(is_running=False,phase="ERROR"); return - if total_fired == 0: - _add_log("✗ Solver returned no result.") - _update_state(is_running=False, phase="ERROR") - return + with STATE_LOCK: sketch_notes=GLOBAL_SOLVE_STATE.get("sketch_summary","").split("; ") - survived = [t for t in traces if t.survived] - best_t = min(survived, key=lambda t: t.ce_after, default=None) + survived=[t for t in traces if t.survived] + best_t=min(survived,key=lambda t:t.ce_after,default=None) for inv in axl_def.anchors: - if not inv.compiled_func: - inv.compile(base_prob.variables) + if not inv.compiled_func: inv.compile(base_prob.variables) - g1_ce = base_prob.scalar_energy(binding) - g1_pass = g1_ce < VERIFY_G1_THRESHOLD - inv_results: Dict[str, Tuple[float, bool]] = {} + g1_ce=base_prob.scalar_energy(binding); g1_pass=g1_ce= -inv.tolerance - else: passed = val <= inv.tolerance - inv_results[inv.name] = (round(val, 6), passed) - except: - inv_results[inv.name] = (999.0, False) - g2_pass = all(v[1] for v in inv_results.values()) - - solved_str = "✓ SOLVED" if (g1_pass and g2_pass) else "~ PARTIAL" if g1_pass else "✗ UNSOLVED" - best_ray = best_t.ray_name if best_t else "—" - - _add_log(f"🏁 {solved_str} (CE: {ce:.5f}) | Iso: {best_ray}") - - # ── ALGEBRAIC REDUCTION LOOP ── - if not g1_pass and attempt < MAX_ATTEMPTS: - current_text = original_problem_text + f"\n\nPREVIOUS ATTEMPT FAILED (Best CE: {ce}):\nGEOMETRIC SOLVER FAILED to converge. The constraint manifold is too highly dimensional. Please apply ALGEBRAIC REDUCTION: substitute simple equalities into the complex constraints to eliminate variables, then output the simplified AXL." - _add_log(f"⚠ Geometric Solve Failed. Triggering Algebraic Reduction...") - continue - - elif not g2_pass and attempt < MAX_ATTEMPTS: - failed_invs = {k: v for k, (v, ok) in inv_results.items() if not ok} - current_text = original_problem_text + f"\n\nPREVIOUS ATTEMPT FAILED:\nGate 2 invariants that did not pass:\n{json.dumps(failed_invs, indent=2)}\n\nPlease revise the constraint encoding to better capture these conditions." - _add_log(f"⚠ Gate 2 Failed. Retrying with structural feedback...") - continue - - _add_log(f"🔤 Collapsing Isomorphism to Domain Language…") + val=float(inv.compiled_func(*[binding.get(v,0.0) for v in inv.syms_used])) + err=abs(val) + passed=(err=-inv.tolerance if inv.mode=="geq" else val<=inv.tolerance) + inv_results[inv.name]=(round(val,6),passed) + except: inv_results[inv.name]=(999.0,False) + g2_pass=all(v[1] for v in inv_results.values()) + + solved_str="✓ SOLVED" if (g1_pass and g2_pass) else "~ PARTIAL" if g1_pass else "✗ UNSOLVED" + best_ray=best_t.ray_name if best_t else "—" + _add_log(f"🏁 {solved_str} (CE: {ce:.5f}) | Ray: {best_ray}") + + if not g1_pass and attempt{l}" - log_html += "" - - ray_trail = "" + phase=GLOBAL_SOLVE_STATE["phase"]; ce=GLOBAL_SOLVE_STATE["best_ce"] + fired=GLOBAL_SOLVE_STATE["total_fired"]; best_ray=GLOBAL_SOLVE_STATE["best_ray"] + traces=list(GLOBAL_SOLVE_STATE["recent_traces"]); logs=GLOBAL_SOLVE_STATE["high_level_logs"] + sketch_summary=GLOBAL_SOLVE_STATE["sketch_summary"] + template_count=GLOBAL_SOLVE_STATE["template_count"] + template_best=GLOBAL_SOLVE_STATE["template_best_ce"] + + ce_color="#4CAF50" if ce{l}" + log_html+="" + + sketch_html="" + if sketch_summary: + sketch_html=(f"
" + f"🗺 Sketch: {sketch_summary[:120]}
") + + template_html="" + if template_count>0: + t_ce=f"{template_best:.5f}" if template_best" + f"🗺 Templates: {template_count} generated | floor CE: {t_ce}") + + ray_trail="" for t in reversed(traces): - icon = RAY_ICONS.get(t.ray_type, "·") - c = "#4CAF50" if t.survived else "#555" - star = " ◀" if t.survived else "" - ray_trail += (f"
" - f"{icon} [{t.ray_name}] CE={t.ce_after:.4f} " - f"({t.tension_class[:3]})" - f"{star}
") + icon=RAY_ICONS.get(t.ray_type,"·") + c="#4CAF50" if t.survived else "#555" + star=" ◀" if t.survived else "" + ray_trail+=(f"
" + f"{icon} [{t.ray_name}] CE={t.ce_after:.4f} " + f"({t.tension_class[:3]})" + f"{star}
") return f""" -
-
● Phase: {phase}
-
- {log_html} -
-
- Best CE: {ce:.6f} - Rays Fired: {fired:,} +
+
● Phase: {phase}
+
{log_html}
+ {sketch_html}{template_html} +
+ Best CE: {ce:.6f} + Rays: {fired:,}
-
Best Isomorphism: {best_ray}
-
- {ray_trail} +
+ Best Iso: {best_ray}
-
- """ - -with gr.Blocks(css=CSS, title="Practicality Unified Server") as demo: +
{ray_trail}
+
""" +with gr.Blocks(css=CSS,title="Practicality 24.0") as demo: gr.Markdown( - "## ⚗ Practicality Unified Server\n" - "`[Gemini 3.1 Encoder] → AXL/PSL → [PyTorch Ray Solver] → [Gemini 3.1 Collapser]`" + "## ⚗ Practicality 24.0 — Structural Sketch & World Model Prior\n" + "`[Gemini Encoder] → [Structural Sketch] → [Template Engine] → [Ray Solver] → [Gemini Collapser]`" ) - with gr.Row(): with gr.Column(scale=2): - api_key_input = gr.Textbox( - label="Gemini API Key", - type="password", - placeholder="AIza...", - value=DEFAULT_GEMINI_API_KEY, - elem_classes=["solver-log"] - ) - problem_input = gr.Textbox( - label="Problem Description", - placeholder=PLACEHOLDER_HINT, - lines=5, - elem_classes=["solver-log"], - ) + api_key_input=gr.Textbox(label="Gemini API Key",type="password", + placeholder="AIza...",value=DEFAULT_GEMINI_API_KEY, + elem_classes=["solver-log"]) + problem_input=gr.Textbox(label="Problem Description", + placeholder=PLACEHOLDER_HINT,lines=5, + elem_classes=["solver-log"]) with gr.Row(): - solve_btn = gr.Button("⚗ Solve", variant="primary") - clear_btn = gr.Button("Clear") - + solve_btn=gr.Button("⚗ Solve",variant="primary"); clear_btn=gr.Button("Clear") with gr.Column(scale=1): - gr.Markdown("**Device & Mode**") gr.Textbox( - value=f"Compute: {DEVICE.type.upper()}\n" - f"Axioms: {len(ALL_AXIOMS)}\n" - f"Max rays per attempt: {MAX_RAYS_PER_ATTEMPT:,}\n" - f"Batch: {RAY_BATCH_SIZE:,}\n" - f"LLM: {GEMINI_MODEL}", - lines=5, interactive=False, - elem_classes=["solver-log"], - ) + value=(f"Compute: {DEVICE.type.upper()}\n" + f"Axioms: {len(ALL_AXIOMS)}\n" + f"New: StructuralSketch + Templates\n" + f"New: SymPy pre-solver (n≤{SYMPY_MAX_VARS})\n" + f"New: Sketch-weighted branching\n" + f"New: Dim-adaptive constructors"), + lines=6,interactive=False,elem_classes=["solver-log"]) with gr.Row(): - live_html = gr.HTML(value=build_live_html_dashboard()) - - answer_box = gr.Textbox( - label="Isomorphic Collapse", - lines=18, - interactive=False, - elem_classes=["answer-box"], - ) - - def fetch_ui_state(): + live_html=gr.HTML(value=build_live_html()) + answer_box=gr.Textbox(label="Isomorphic Collapse",lines=20,interactive=False, + elem_classes=["answer-box"]) + + def fetch_ui(): while True: time.sleep(1.0) - yield build_live_html_dashboard(), GLOBAL_SOLVE_STATE["answer"] + yield build_live_html(),GLOBAL_SOLVE_STATE["answer"] - solve_btn.click( - fn=trigger_solve, - inputs=[problem_input, api_key_input], - outputs=None, - ) + solve_btn.click(fn=trigger_solve,inputs=[problem_input,api_key_input],outputs=None) + clear_btn.click(fn=lambda:("","",""),inputs=[],outputs=[problem_input,live_html,answer_box]) + demo.load(fetch_ui,inputs=None,outputs=[live_html,answer_box]) - clear_btn.click( - fn=lambda: ("", "", ""), - inputs=[], - outputs=[problem_input, live_html, answer_box], - ) - - demo.load(fetch_ui_state, inputs=None, outputs=[live_html, answer_box]) - - gr.Markdown( - "Built with Gradio · Practicality 23.1 · Stable Manifold + Algebraic Reduction", - elem_classes=["status-bar"] - ) + gr.Markdown("Practicality 24.0 · Structural Sketch + World Model Prior", + elem_classes=["status-bar"]) -if __name__ == "__main__": - print(f"[UNIFIED SERVER] Compute: {DEVICE.type.upper()}") - print(f"[UNIFIED SERVER] System 23.1: Manifold Stabilizer + Algebraic Reduction Loop.") - demo.launch(server_name="0.0.0.0", server_port=7860, share=False) \ No newline at end of file +if __name__=="__main__": + print(f"[SYSTEM 24.0] Compute: {DEVICE.type.upper()}") + print(f"[SYSTEM 24.0] New: StructuralSketch · Templates · SymPy pre-solver · Sketch-weighted branching") + demo.launch(server_name="0.0.0.0",server_port=7860,share=False) \ No newline at end of file