CORTEXA
← Browse
arxivcs.AIcs.LGcs.PL2026-07-18

Exact Network Surgery: Functional Invariance and Gradient Plasticity in Reactive Computational Graphs

Abdallah Khemais

Function-preserving network growth techniques such as Net2Net and progressive stacking expand a model's capacity without destroying its learned function, but existing formulations either tolerate numerical perturbations or require a full rebuild of the training program. We formalize Exact Network Surgery: the in-place insertion of a residual block into a live computational graph such that (i) the network function is preserved -- bit-exactly under explicit floating-point hypotheses -- and (ii) inserted parameters remain trainable immediately after insertion. We prove an identity-morphism theorem for gated residual blocks, a structural-locality theorem showing that a reactive invalidation engine recomputes exactly the downstream cone of the insertion point, leaving every other node's value and optimizer state untouched, and an escape-from-initialization proposition showing that the Gradient Shadowing gate alpha, initialized at zero over a randomly initialized branch, receives a generically non-zero gradient at insertion time. We identify a degenerate configuration -- zero-initialized output projections combined with a zero gate -- that is an exact saddle point gradient descent cannot escape. Every claim is validated on the reference implementation in NeuroDSL, a reactive graph engine in Julia: grafting is bit-exact on every logit tested (0 mismatches out of 1600); the gate escapes zero at the first optimizer step and unlocks branch gradients at the second, exactly as predicted; the degenerate configuration exhibits gradients identically zero for the entire 600-step run; surgery cost tracks downstream cone size with r = 0.9992 while graft-plus-invalidation bookkeeping is constant (about 0.75 ms) across insertion depths; and training resumes bit-identically across a real process restart. A flagged preliminary appendix reports first single-seed observations on post-insertion gate dynamics.

View free PDFSource page

Related papers

arxivcs.LGcs.AIcs.PL2026-07-03

Differentiate the Evaluator, Not the Program: An Efficient Runtime Representation for Neuro-Symbolic Learning

Lucas Sheneman

AI systems increasingly propose executable scientific models whose value depends on both their symbolic structure and their fitted continuous parameters. This makes parameter calibration the bottleneck of program-and-parameter co-search: an outer loop can generate thousands of ca…

View free PDFSource page
arxivcs.PLcs.AIcs.LGcs.MA2026-07-20

ETAS: An Effect-Typed Language for Agent Systems

Huiri Tan, Yikun Wang, Puyang Zhang, Shangyu Li, Jiasi Shen

ETAS is a programming language for agent systems that treats model-backed agents, tool calls, prompts, typed memory, human approvals, policies, and execution traces as semantic program elements rather than library conventions. It separates deterministic computation from agentic n…

View free PDFSource page
arxivcs.PLcs.AIcs.LG2026-07-20

Decode-Time Grammars: Constrained LLM Generation over a Refinement Order of Grammar Fragments

Shuoming Zhang, Ruiyuan Xu, Haofeng Li, Qiuchu Yu, Yangyu Zhang, Chunwei Xia, et al.

Large language models now write a growing share of the world's code, increasingly inside agents and serving systems that compile, execute, or dispatch generated code without line-by-line review. This works well for mainstream languages but remains brittle for low-resource program…

View free PDFSource page
arxivcs.SEcs.AIcs.LGcs.PL2026-07-17

AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang, Wenda Li, Haonan Li, Luke Ong, et al.

Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this effort, but their heavy token consumption and API cost remain a major obstacle. We trace this cost to…

View free PDFSource page
arxivcs.PLcs.AIcs.LG2026-07-15

Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code

Niels Mündler-Sasahara, Hristo Venev, Dawn Song, Martin Vechev, Jingxuan He

Languages with rich static semantics, such as Rust, provide stronger guarantees for AI-generated code, but their strictness makes generation more difficult. Off-the-shelf compilers can provide useful feedback post-generation, but does not guide intermediate generation steps, such…

View free PDFSource page
arxivcs.AIcs.CLcs.LGcs.PL2026-07-14

Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

Marcus J. Min, Mike He, Zhaoyu Li, Zixuan Yi, Sharad Malik, Aarti Gupta, et al.

Autoformalization translates informal natural language into formal, machine-verifiable languages. While most work focuses on individual statements, real formalization efforts are inherently theory-level: they require an entire web of axioms, definitions, and lemmas before target…

View free PDFSource page