CORTEXA
← Browse
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 candidate programs, but each needs an inner gradient-based optimization before it can be assessed. Staging each candidate into its own differentiable graph makes individual models fast but sacrifices the program-as-data property that keeps search fluid; interpreter-based approaches preserve programs as runtime data but pay interpreter overhead that dominates the numerical work. We present the Native Differentiable Virtual Machine (NDVM), a runtime representation that differentiates executable programs without compiling each candidate into a separate graph. NDVM separates symbolic structure from differentiable numeric state: tags, symbols, environments, and control remain native runtime data, while numeric payloads live in dense batched buffers with exact reverse-mode gradients recorded along the realized execution trace, so one evaluator walk is amortized across large populations of parameter vectors. A locked cost model of a real differentiable self-hosted Scheme interpreter motivates the design. We realize NDVM as a native runtime with forward and gradient equivalence to the reference backend, about 60x per-lane batch amortization, near-linear multicore scaling, and two independent front ends. In fixed-budget co-search over LLM-proposed programs, NDVM reaches high-quality solutions about 24x sooner in wall-clock time, suggesting runtime differentiation as a practical systems foundation for scientific discovery workflows.

View free PDFSource page

Related papers

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.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 formal…

View free PDFSource page
arxivcs.LGcs.AIcs.LOcs.MAcs.PL2026-07-06

PatchOptic for Shared-State LLM Workflows with Projected Views and Verified Structured Updates

Zhaoyu Bai, Jiaqi Cai

Agentic workflows often operate over shared, structured state. Because LLM context windows are limited, each model invocation is typically shown only the state fragment needed for the current workflow step, a pattern commonly known as progressive disclosure. Modern systems constr…

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