Agent harness reliability, recoverable self-evolution, and formal limits on language and structure

Hanzhang Jia, Liheng Zeng, Hao Cheng, Yi Gao, Bo Ma

The paper shows that the spatiotemporal-composability calculus for agents does not require a single shared process. It constructs Logos as a ROS-like harness in which each plugin is an independent process whose only shared state is an append-only transcript. Experiments demonstrate that eighty sessions resume without repeated side effects after kills at every boundary of the tool-call cycle, while a single-process baseline loses every co-resident session to one fault.

Tanmay Sah, Dolly Sah, Harshul Jain, Tanya Sah

EvoUndo formalizes self-modification of prompts, tools and harnesses so that every capability-improving mutation can be verified for recoverability across counterfactual states. Of 197 natural capability-gaining mutations that fail recoverability, conventional repair recovers none, while an extended recovery calculus plus exact state-address grounding recovers the large majority under oracle analysis. The results show that reliable self-evolution requires joint design of verification, grounding, witness semantics and recovery-language expressivity rather than iterative prompting alone.

Zhuoshi Pan, Qizhi Pei, Junru Lu, Honglin Lin, H. Vicky Zhao, Di Yin, Xing Sun

ContextPilot augments the agent toolset with planning, long-term memory and soft offloading primitives, then trains context-editing policy with an RL method that identifies critical edits via context and entropy variation and estimates action-level advantages from branched trajectories. On long-context QA and deep-search tasks the method yields higher accuracy with substantially more compact working contexts than prior proactive-management baselines across multiple base models.

Xiaoqing Wang, Keman Huang, Bin Liang, Hongyu Li, Xiaoyong Du, Wuqiong Pan

DoCtOR first attributes the decisive error step and agent via automated failure analysis, generates a counterfactual correction, and then elicits targeted reflection only from the responsible agent. The diagnose-then-correct loop improves success rates by 22-27 percent over strong reflection baselines on HotPotQA, ChartQAPro and Mind2Web while avoiding contamination of non-culpable agents' memories.

Minghui Xu, Zi Wang

After diagnosing that calculation errors dominate Countdown failures, the authors create tool-formatted SFT data and then apply on-policy RL (RLOO, GRPO, DAPO) with verifiable final-answer rewards. Tool-DAPO raises pass@1 from 35.8 percent (tool-SFT) to 66.0 percent on a fresh 1024-problem held-out set, showing that RL further improves tool-calling even under sparse outcome rewards.

Vishvesh Bhat

PLVR learns explicit programs composed of deterministic and neural primitives by symbolic backpropagation: typed ontologies propagate required input contracts backward via type inference, yielding dense per-step verifiable rewards. On LiveCodeBench and Tau2Bench, 30B models equipped with the learned programs outperform matched-budget RL and much larger frontier models; ablating the backward pass collapses program quality, identifying credit assignment rather than the type system as the source of gain.

Emily Cheng, Ryan Cotterell

Modeling language as a joint distribution over meanings, contexts and utterances, the authors derive information-theoretic upper bounds on the probability that any featurizer (including LLM hidden states) recovers intended meaning from the utterance representation alone. The bounds separate irreducible uncertainty from uncertainty resolvable only by extralinguistic context and hold for both discrete and continuous meaning spaces; experiments on artificial languages, Mandarin zero pronouns and color reference corroborate the theory.

Vincenzo Collura, Karim Tit, Eleonora Giunchiglia, Mike Papadakis, Maxime Cordy

The decoder precomputes bounded pushdown summaries that label reachability and upper-bound distance to acceptance, then uses them online for horizon-aware pruning and beam search. Every generated string is guaranteed to be accepted by the target CFG; on JSON, SQL and LTL the method simultaneously enforces syntactic validity and improves completion quality relative to existing constrained decoders.

Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, Tianyi Peng

Prove2Me lets users launch formalization missions that AI agents complete in Lean 4, with specialized harnesses and reuse mechanisms so agents can build on one another's partial proofs. The platform turns large-scale verified mathematics into a crowd-sourced human-AI collaboration whose correctness is machine-checked rather than peer-reviewed.

Mahdi Babaei, Xueshen Li, Yutao Kuang, Jolene P. Reid, Yu Gan

MAIL treats hypothesis generation as a temporally grounded process that maintains an evolving conceptual memory path continuously reinterpreting the chemical literature. On TOMATO-Chem and a new high-novelty Nature/Science challenge set it recovers central ideas and methods of historical targets more effectively than baselines and receives the highest expert scores for scientific quality and mechanistic plausibility.