Explore completed research outputs

Continual learning methods frequently reduce forgetting by adding replay, regularization, or routing constraints, yet activation functions are usually treated as fixed nonlinearities rather than adaptive components of the retention mechanism. We study a task-agnostic setting where task identities are unavailable and dynamic activation updates must operate under matched replay and optimization budgets. In this setting, we define an interference-gated projected activation update, formalize a one-step forgetting-proxy comparison against static-gate baselines, and introduce a fairness-normalized attribution predicate that blocks invalid comparisons when memory or optimization controls differ. The empirical study executes seed-aggregated runs on reduced Split CIFAR-100, reduced Split TinyImageNet, and a third real fallback online digits stream, with static GELU, ReLU, Mish, A-GEM, EWC, and ablated dynamic variants as comparators. Results show that the full dynamic gate is indistinguishable from static GELU in the executed matrix, while replay-family changes can worsen forgetting and destabilize backward transfer, yielding mixed support for retention-improvement claims. Symbolic checks confirm local first-order identities and fairness-accounting completeness but expose a failed simplification in one projection-bound audit, limiting formal conclusions to local validity windows. These findings sharpen the boundary between plausible mechanism intuition and supported claim scope: activation-state adaptation can be audited rigorously, but global forgetting guarantees remain unresolved without stronger alignment conditions and broader benchmark execution.

Long-horizon research automation needs stronger semantics than prompt chaining or schema-only artifact passing. We study a restricted contract-governed formulation of Quarks in which a finite active workflow branch is modeled as a typed directed acyclic graph, each node carries explicit assumptions and guarantees over artifact spaces, cross-node transport is mediated by sound adapters and admissible aggregators, and execution state is split into a global append-only provenance ledger and branch-local working memory. Within that regime we prove three results. First, typed local admissibility composes over the branch when the contract premises hold. Second, branch isolation and provenance monotonicity follow from the append-only, non-merge memory discipline. Third, local validator passes do not imply unrestricted graph-level correctness: we construct a two-node counterexample and then prove a narrow positive corollary for a manuscript-defined typed property class under explicit coverage, adapter, and memory assumptions. The proof package is complemented by seeded finite theorem audits and implementation-alignment checks against the Quarks architecture context. The positive audit families close completely in the declared regime, with 40/40 contract-composition cases, 45/45 memory cases, and 15/15 restricted-assurance cases passing; each theorem also retains a nontrivial archive of negative witnesses outside the proved setting. The result is a bounded but useful semantics for research orchestration: it supports typed admissibility, provenance discipline, and limited assurance claims without upgrading branch merges, semantic quality, or unrestricted agent competence into theorem-level guarantees.

Long-horizon autonomous research systems now execute multi-stage workflows with planner, tool, and reviewer modules, yet most guarantees remain local or empirical. We formalize a contract-governed orchestration model in which execution is a finite directed acyclic phase graph with typed interfaces, adapter maps, decidable transition guards, and validator-mediated control. Within this setting, we define a safety objective that minimizes contract violations and a recoverability objective that minimizes halting time under bounded control. We prove a graph-level safety theorem by composing edge admissibility and invariant propagation, and we prove a bounded recoverability theorem with an explicit finite halt envelope; we also prove an impossibility boundary when boundedness or monotone escalation is removed. The formal statements are paired with theorem-audit evidence from symbolic checks and seeded trace sweeps: fail-closed bounded runs satisfy the proven envelope, while fail-open or non-monotone regimes produce counterexamples exactly where the theory predicts failure. The resulting manuscript gives a theorem-first blueprint for contract-compositional orchestration that separates theorem-supported claims from diagnostic, out-of-regime observations.

Long-horizon autonomous research pipelines require stronger guarantees than prompt-level coordination alone. We study a contract-governed orchestration framework in which research execution is modeled as a typed directed acyclic graph with validator-gated transitions, bounded corrective policies, and append-only provenance traces. We adopt validator-gated workflow patterns and protocol threat assumptions from prior orchestration and security work, and we define three optimization objectives for committed-prefix safety, bounded recovery, and security--provenance tradeoffs. Theoretical analysis establishes three results under explicit assumptions: committed-prefix soundness under compositional semantic and type guards, non-oscillation under finite corrective depth and strict potential descent, and false-acceptance contraction for covered attack classes under composite guards together with provenance invariance under hash-linked append-only traces. We connect these statements to audit experiments on a real orchestration substrate with symbolic checks and adversarial boundary tests. Evidence shows zero unsafe commits only in the intended compositional regime, recovery remains bounded only under finite-depth and descent conditions, and security gains hold for covered attack classes with uncovered-class failures reported as caveats. The result is a formal and empirical blueprint for auditable, extensible, and scientifically interpretable multi-agent research orchestration.

Neurosymbolic answer set programming (ASP) systems often achieve exact semantics only after manual encoding redesign, which makes runtime gains difficult to scale beyond expert-curated benchmarks. We present AutoTW-ASP, a hybrid exact-inference method that automates two coupled decisions: (i) whether a candidate rewrite of a grounded ASP program should be accepted under explicit semantic guards, and (ii) whether each instance should be executed with stable-model enumeration or compilation-based counting. The method combines structure-aware proxies, a guarded rewrite objective, and uncertainty-gated routing. On six benchmark families and nineteen seeds, AutoTW-ASP preserves semantic equivalence for guarded rewrites and reduces median runtime relative to fixed exact baselines, while exposing where calibration and counterexample detection remain brittle. The strongest empirical signal is exactness preservation with runtime improvement against naive exact baselines; the weakest signal is universal closure of strict threshold targets for router-envelope violations and cache counterexample recall. These bounded findings support the central claim that exact neurosymbolic optimization can be automated without relaxing stable-model correctness, while making clear which components still limit generalization.

Recent neurosymbolic Answer Set Programming (ASP) pipelines frequently rely on manual encoding redesign to exploit treewidth-sensitive exact inference backends, creating a reproducibility and scalability bottleneck. We study an integrated system, AutoTW-ASP, that jointly performs semantics-preserving rewrite selection and uncertainty-aware backend routing between exact enumeration and compilation-based inference. The method combines motif-level rewrite guards, crossover-margin prediction, and abstention-to-enumeration under uncertainty. We formalize rewrite acceptance, routing regret, and constrained end-to-end optimization, and we connect these formal components to an empirical protocol spanning symbolic and hybrid benchmark families. Experiments show that rewrite mismatch rates remain below a predefined projection criterion (maximum observed mismatch rate 0.00375), while non-zero exactness violations remain in accepted-rewrite audits. Routing maintains strong severe-shift coverage (0.9346) and low mean regret in mild/moderate regimes, but severe-shift exactness violations and elevated calibration error persist. Integrated training achieves median 1.140\(\times\) speedup, which is below a 1.20\(\times\) acceptance target, and therefore does not fully support the strongest end-to-end claim under strict exactness constraints. These outcomes establish a bounded positive result: automated rewrite-plus-routing can deliver measurable efficiency gains and informative uncertainty structure, but claim-level guarantees remain conditional on tighter guard policies and calibration in hard-shift regimes.

Multi-objective decision support now spans classical scalarization, Pareto-evolutionary search, outranking-based multicriteria ranking, and uncertainty-aware formulations, but practical method selection remains unstable because evidence is fragmented across incompatible metrics, reporting protocols, and software defaults. This manuscript presents a contradiction-aware survey framework that unifies these families through a shared mathematical problem setting, explicit assumption gates, and a dual-layer recommendation rule separating candidate-set quality from stakeholder-facing utility. We formalize three linked contributions: an affine-normalization invariance and stability-guard criterion for recommendation robustness, a scalarization theorem gate that combines convex-regime completeness with a constructive non-convex counterexample boundary, and a descriptor-aware decision rule that integrates uncertainty and provenance penalties into utility judgments. We then assemble and analyze a synthesis validation package that reports calibrated instability thresholds, theorem-gate outcomes, transportability behavior under descriptor perturbations, and cross-framework lineage sensitivity. The resulting evidence supports bounded recommendations rather than universal rankings: two claims are strongly supported, while transportability claims remain conditional under implementation drift. The manuscript closes with a reproducibility and limitations synthesis that converts negative evidence into actionable follow-up protocols for future survey and benchmarking work.

Multi-objective decision support is fragmented by a representation mismatch: Pareto-set methods, outranking relations, and scalarization-based methods emit different mathematical objects, yet review articles often compare them as if they were directly commensurable. We present a representation-conditioned synthesis framework that formalizes within-family comparability, separates cross-family evidence grading from raw metric aggregation, and makes theorem-level assumptions explicit. The manuscript contributes two proved formal results and one boundary analysis linked to executed validation artifacts: (i) an impossibility result showing that no family-blind scalar embedding can preserve bidirectional order fidelity when Pareto incomparability is present, (ii) a constructive existence result showing that typed contradiction-loss minimization attains zero loss under finite-acyclic and separability assumptions, and (iii) a local bridge-stability characterization for preference perturbations that is valid only inside a margin-Lipschitz regime. Executed evidence supports these claims with typed violation mean 0.0083 versus family-blind violation mean 0.2863, typed zero-loss feasibility in 405/540 runs under satisfied assumptions, and a sign-flip increase from 0.0723 inside the stability regime to 0.2108 outside it. The resulting survey protocol yields defensible method-selection guidance without asserting unsupported universal rankings across non-equivalent method families.