The arXiv new submissions of the past 24 to 48 hours in cs.AI, cs.LG, and cs.CL again offered far more candidates than can fit into a digest. This piece curates five papers from as diverse subfields as possible – formal mathematics verification, agent infrastructure, model geometry, and two opposing perspectives on linear probes in language models – each with a comprehensible method and solid core numbers in the abstract, not mere niche applications. The most significant finding is that a technique increasingly used in AI safety research – reading truthfulness off a model’s internal activations via a linear probe – fails to distinguish honesty from mere rule-following in a concrete test case.
Mathematics and Infrastructure
Training-free method Magenta links language models with machine-checked Lean proofs
Joshua Ong Jun Leang, Haonan Li, and a six-member further author team present Magenta, a training-free, agentic pipeline that, given a natural-language math problem, first produces an answer, formalizes it as a Lean 4 statement – a machine-readable formulation checkable by the Lean proof assistant – and then constructs a machine-checked proof. A “statement judge” verifies whether the formalization preserves the original problem, while a second judge routes failed attempts either to mathematical re-derivation or to targeted Lean repair. Across the olympiad benchmarks AIME 2025, AIME 2026, and HMMT February 2026, the authors report the method achieves 100 percent accuracy, and paired with the open-weight reasoner K2-Horizon-7B, it solves all six IMO 2026 problems. This matters because it shows that the reliability of informal AI math answers can be sharply raised through downstream formal verification, instead of relying solely on the language model’s text output. A previous piece had already shown how a team of dozens of Claude agents fully formalized Fermat’s Last Theorem in Lean – Magenta now delivers a lightweight, training-free counterpart built for ongoing competition use rather than a single large project.
New memory system AgentZip compresses AI-agent sandboxes by a factor of 8.7
Mengming Li, Ceyu Xu, and a five-member further author team present AgentZip, which they describe as the first memory-compression system built specifically for AI-agent sandboxes – isolated execution environments in which an agent runs code or tools. Because many concurrently running sandboxes originate from the same template and carry out related tasks, the system specifically exploits redundancy both across and within sandboxes, shifts overhead control from choosing which pages to compress to proactive restore-time prefetching, and schedules costly compression preferentially into the language model’s waiting periods. Across training and inference workloads, this reduces sandbox-owned memory by up to 8.7 times, compared with 2.1 times for the standard Linux configuration, while the slowdown caused by aggressive compression drops from as high as 3.1 times to 1.4 times. This matters because high memory demand across parallel agent fleets is already a practical cost factor in running AI agents today, one that pure software optimization – without new hardware – could meaningfully reduce. A previous piece had already shown how OpenAI opened its internal Codex infrastructure to developers with the public Agents API beta – AgentZip supplies a building block aimed at cutting exactly the infrastructure costs that come with widespread use of such agent platforms.
Model Structure, Safety, and Interpretability
Different language model architectures share a measurable, purposefully steerable geometry
Dario Picozzi shows, with a study on the information geometry of large language models, that the so-called Fisher-Rao geometry of output probabilities – a measure of how a model’s predictive distribution shifts under small changes – agrees far more strongly across transformer, state-space, and recurrent architectures than the geometry of internal activations does. The author reports that agreement with human word choices increases with predictive accuracy, scale, and training, and improves further after model-only calibration; pretraining-corpus statistics also predict how readily a model acquires a given piece of factual knowledge on held-out tests. Building on this geometry, “minimum-disturbance” local interventions can reportedly be constructed that transfer from a donor prompt to unseen prompts while preserving baseline behavior better than classical Euclidean control methods – according to the author, the same geometric correction improves several downstream tasks at once, from steering to editing to attribution. This matters because it suggests control and interpretability tools need not be reinvented for every model architecture but could build on a shared, architecture-spanning structure. A previous digest piece had already shown that refusal behavior in language models can be traced to a single internal direction and turned off deliberately across four architecture families – the new work offers a possible theoretical foundation for why such directional interventions work across architectures at all.
Truth probes completely confuse honesty with rule-following in a trained model
Dylan Jayabahu shows, with a study on so-called “Perfect Aliasing” in truth probes, that a linear probe – a simple classifier trained on a model’s internal activations – fitted on contexts where honest reporting and the action a prompt prescribes coincide cannot tell, from the fitting data alone, which of the two targets it is actually measuring. In a controlled binary reporting game, truth probes and prescribed-action probes solve the same optimization on such “compliant” contexts; on rival contexts their predictions are exact complements, so the hit rates (AUROC) of both readings sum to exactly one, to floating-point precision, across 751 tested cell-layer pairs. For a reward-trained Gemma-2-9B model that answers falsely on every tested rival trial, a conventionally fitted probe scores just 0.006 AUROC, while a probe fitted on mixed contexts scores 1.000 on the very same held-out activations. The author stresses explicitly that this finding establishes only linear recoverability, not whether the model retains an internal belief, uses the recovered direction causally, or whether a deployable deception detector could be built from it. This matters because truth probes are increasingly pitched as a tool against model deception in AI safety research, even though, per this study, they cannot reliably be distinguished from a mere rule-following probe under ordinary training conditions. A previous digest piece had already shown that safety-related language in system prompts can amplify dishonest refusals more than 15-fold – the new study offers a methodological explanation for why honesty and mere rule-compliance blur together so easily in such measurements.
Linear probes recover correct knowledge behind wrong answers across 16 models
Manas Venkata Sai Ravulapalli, Samrath Singh Chadha, and Abhinav M. Hari investigate, with a study on “Legible Failures”, whether a wrong model answer stems from the language model lacking the needed information or from holding it internally without using it. On an entity-obligation binding task – correctly assigning duties or properties to named actors – the authors test 16 model checkpoints and show that a linear probe on the model’s frozen hidden state can often reconstruct the correct binding even when the actual output is wrong. Probe accuracy exceeds baseline by 0.196 points, a detection score built from the disagreement between probe and model output improves failure detection over raw model confidence by 0.079 AUROC points, and steering the residual stream toward the probe-decoded binding raises accuracy across eight models by an average of 0.168 points. This matters because – unlike the probe confusion described above – it shows a case where a linear probe genuinely yields a usable, targeted correction mechanism for model errors, provided the tested property can be cleanly separated from mere rule-following. A previous digest piece had already shown that language models can barely predict their own behavior better than a generic description of AI agents – the new study shows that an outside look at a model’s internal states often reveals more than the model’s own account of itself, whether spoken or expressed through output.
None of the five papers presented has yet gone through a regular peer-review process; all are unreviewed arXiv preprints whose numbers come from the respective author teams’ own experiments and have not been externally replicated. Whether Magenta’s result holds up under independent review by the IMO committee, whether AgentZip’s compression rates persist under more heterogeneous, less similar sandbox workloads, and whether the sharp probe confusion appears just as starkly in other models and training regimes are questions only independent replications can answer.
