Main-conference poster sessions reward planning. Workshop sessions reward luck.

A workshop room can be three corridors away from the topic you intended to see, and the poster that changes your afternoon may be the one beside the coffee table rather than the one highlighted in the program. This third ICML reflection is limited to workshop papers I encountered through that kind of fortunate wandering.

The papers span theoretical physics, post-training, foundation models for simulation, Transformer inductive bias, model evaluation, interpretability, and multi-agent diagnosis. Their common question emerged only after I stopped grouping them by application:

When an AI system encounters an error or a new environment, what should change, where should that change be stored, and what evidence tells us that the change was useful?

Learning is often described as parameter optimization. These workshop papers suggest a broader view. An AI system can change its current answer, its dialogue state, its inferred model of the environment, a selected subspace of its weights, or the interaction protocol among several agents. Every update preserves some structure and overwrites something else.

A useful update therefore balances three quantities:

Here, (s) is the current state of the system, (\mathcal{L}{\mathrm{new}}) measures the unresolved error, (\mathcal{D}{\mathrm{preserve}}) measures damage to valuable existing structure, and (\mathcal{C}) represents the cost of the update.

The hard research problem lies in defining those terms. A critique can improve the current derivation while making the overall argument less coherent. Fine-tuning can raise benchmark accuracy while erasing general capabilities. A physics model can produce a plausible next frame while learning the wrong dynamics. A lower perplexity can reward confidence without rewarding correctness. A group of agents can agree because they share the same error.

The workshop papers became a study of selective change: changing the right variable, on the right timescale, while preserving the right invariants.

Critique changes the solution before it changes the model

When Does Critique Improve AI-Assisted Theoretical Physics? SCALAR studies an Actor–Critic–Judge loop on graduate-level quantum field theory and string theory problems. An Actor proposes and revises a solution, a Critic provides feedback with access to a reference solution, and an independent Judge evaluates the successive attempts. The authors vary Actor personas, Critic styles, model families, and model scales. Multi-turn interaction generally improves on single-shot attempts, while the size and character of the gain depend strongly on the Actor–Critic pairing. Constructive feedback is particularly useful when a weaker Actor is paired with a stronger Critic; strict or adversarial feedback provides no universal advantage. (arXiv)

The important object is the response of the solution to feedback:

where (S_t) is the quality of the solution after revision (t). A capable Critic can identify the correct error and still produce little gain when the Actor cannot interpret or incorporate the feedback. A milder Critic may outperform a more aggressive one by locating a repair within the Actor’s current competence.

This resembles educational scaffolding more than debate. A useful teacher does not enumerate every flaw simultaneously. The teacher identifies the next misconception that the student can repair. The value of feedback therefore depends on its correctness, novelty, timing, and usability.

SCALAR also offers an instructive evaluation method: track the sequence of revisions rather than only the final score. Two systems with identical final performance can have very different internal dynamics. One may repair a decisive error after a single critique. Another may oscillate among alternative mistakes. A third may repeatedly rewrite the answer while changing little of substance.

For scientific agents, this suggests measuring critique susceptibility: how efficiently a system converts feedback into improved work. When gains flatten, the appropriate response may be to switch Critics, decompose the problem, invoke a symbolic tool, or ask for human input. Continuing the same dialogue merely generates more tokens.

The broader lesson is that many failures should be repaired in the current artifact before they trigger a model update. A wrong sign in a derivation calls for a local correction. A systematic inability to reason about gauge invariance may justify a deeper change. The skill lies in distinguishing the two.

Context can carry learning without changing weights

Towards a Physics Foundation Model moves adaptation from dialogue into latent state estimation. Its General Physics Transformer is trained on approximately 1.8 TB of simulation data covering several fluid, thermal, multiphase, and fluid–solid systems. Given a short history of physical states, the model infers enough of the local dynamics to predict future states, including zero-shot experiments on unseen physical systems and boundary conditions. (arXiv)

The task is naturally expressed through a latent dynamics variable (z):

The model observes a short trajectory, infers a local description of how this world evolves, and uses that inferred state to generate the next step. The weights remain fixed while the effective model changes through context.

This is closely related to system identification in control theory. An engineer observes inputs and outputs, estimates the hidden dynamics, and then predicts or controls the system. A physics foundation model amortizes that procedure across many simulated worlds.

The architecture also contains an important scientific design choice. The Transformer estimates a temporal derivative, while a numerical integration step advances the state. Spatial and temporal derivative features provide additional numerical structure. The learned component handles cross-domain inference; the integration interface supplies a stable computational scaffold. (arXiv)

This hybrid structure is more inspiring than a slogan about learning physics from raw data. It suggests that general scientific models may arise from broad learned representations connected through well-chosen numerical interfaces. A neural component can infer the regime, parameters, or operator, while established solvers enforce part of the update structure.

Variable time increments are another methodological gem. When all trajectories share the same sampling interval, visual displacement can become a shortcut for temporal dynamics. Varying the interval forces the model to infer time scale from the context. Similar experiments could be useful in language-model research: change surface format, naming, scale, or tokenization while preserving the underlying operation, then test whether the model infers the mechanism or recognizes the dataset.

The central unresolved question is what kind of latent model has been inferred. The context may identify a familiar simulation family, support a flexible local interpolation, or recover reusable abstractions such as boundary type, conservation structure, or effective dynamics. Carefully constructed pairs of visually similar trajectories governed by different hidden laws could distinguish these explanations.

For AI research agents, the analogy is direct. A mechanistic-interpretability agent should infer a local intervention law from a small set of experiments. It should estimate thresholds, dose–response shape, generalization across prompts, and failure of perturbative assumptions before proposing the next intervention. Most new experimental objects should be handled through contextual system identification long before they motivate weight updates.

Fine-tuning should protect the structure that future learning needs

Rotation-Preserving Supervised Fine-Tuning studies selective change in parameter space. Standard SFT improves the target task while often reducing out-of-domain performance. RPSFT penalizes changes within dominant singular subspaces of the pretrained weight matrices, using those subspaces as an efficient proxy for directions that are expensive to disturb. The complementary space remains available for task adaptation. Across math-reasoning fine-tuning experiments, the method improves the in-domain/OOD trade-off, better preserves pretrained representations, and produces stronger initializations for later reinforcement learning. (arXiv)

The method embodies the stability–plasticity dilemma from continual learning and neuroscience. A system needs enough plasticity to acquire a new capability and enough stability to retain its reusable organization. Uniformly constraining the entire model wastes available degrees of freedom. Unconstrained adaptation allows a local training objective to rotate broadly useful machinery.

RPSFT asks a more precise question: which subspaces should carry the new task?

The dominant pretrained directions are a structural proxy rather than a complete map of capability. Their value comes from being computationally tractable and empirically associated with Fisher-sensitive gradient energy. The methodological pattern is broadly reusable: identify an expensive behavioral object, propose a cheaper structural proxy, verify that the proxy captures the relevant signal, and constrain only the corresponding degrees of freedom.

The downstream reinforcement-learning result deserves special attention. A checkpoint can look good immediately after SFT and provide a poor starting point for the next training stage. Preserving pretrained geometry can improve the future learning trajectory even when the current checkpoint difference looks modest.

This expands the meaning of update quality. A good adaptation should solve the present task, preserve unrelated capabilities, and maintain useful plasticity for future stages.

For alignment research, the next question concerns which behavioral mechanisms occupy the protected space. Refusal, truthfulness, self-report, and reasoning may share dominant pretrained geometry, or they may rely on fragile structures introduced later through post-training. Average OOD retention cannot distinguish these possibilities. Causal and representational measurements across ordinary SFT and RPSFT could reveal which alignment mechanisms survive because their supporting subspaces remain stable.

Weight space can become an observable

Weight-Space Physics offers the most unusual interpretability idea in this workshop collection: treat trained network weights as scientific measurements of the system they model.

The paper studies normalizing flows trained for lattice field theories across different coupling constants. JEPAWG maps physical couplings through a learned latent space into flow-network weights. The latent weight geometry recovers the intrinsic dimensionality of the coupling manifold, identifies the phase-transition region, and exhibits a finite-size shift aligned with the expected two-dimensional Ising scaling exponent. The model also generates effective flow weights at unseen coupling values. (arXiv)

Normally, a learned sampler is a tool for producing configurations from which physical observables are estimated. This work asks whether the parameters of the tool have themselves absorbed the structure of the physical theory.

That reversal creates an unusually clean interpretability benchmark. Physics provides known coupling dimensions, phase structure, and finite-size scaling. An interpretability method can therefore be tested against independently established ground truth rather than judged by whether its visualizations appear meaningful.

The cross-disciplinary inspiration is statistical physics. A phase transition captures a qualitative change in macroscopic behavior. An order parameter summarizes a regime. Finite-size scaling helps distinguish a genuine structural transition from a small-system artifact. Renormalization describes relationships preserved across scales.

Model-family interpretability could borrow the same logic. Consider a controlled family of language models trained with varying amounts of safety data, preference strength, harmful fine-tuning, or reasoning supervision. The checkpoints may form a low-dimensional weight-space manifold. Behavioral transitions could appear as geometric changes along that manifold, while scaling across model sizes could test whether the transition reflects stable structure.

This shifts interpretability away from isolated checkpoints. A single neuron in a single model can be an implementation detail. A consistent manifold, transition boundary, or scaling law across a controlled model family provides a stronger scientific object.

The paper also complicates the usual distinction between learning and measurement. Training a network at each physical coupling creates a measurement instrument whose parameters reflect the underlying system. The hypernetwork then learns the geometry of those measurements. Weight space becomes a bridge between simulation, representation learning, and scientific inference.

Inductive bias determines which differences survive learning

Transformers Learn Low Sensitivity Functions studies the kinds of functions Transformers tend to learn. Across vision and language experiments, the authors find that Transformers learn functions with lower sensitivity to token- or patch-level random perturbations than several alternative architectures. Lower sensitivity correlates with robustness, flatter loss regions, and progress during grokking. (arXiv)

For a Boolean function, sensitivity can be written as

A low-sensitivity function maps many neighboring inputs to the same output. The model compresses away local distinctions that do not appear necessary for its learned rule.

This bias explains part of Transformer robustness. It also creates a boundary between useful invariance and harmful blindness. In sentiment classification, one irrelevant token should rarely change the answer. In parity, exact arithmetic, source code, or cryptographic verification, a single symbol can determine correctness.

A follow-up line of research shows how simplicity bias can trap Transformers in an incorrect low-sensitivity rule under noisy features, even when the intended target is learnable. The architecture’s preference becomes helpful only when its favored invariances match the causal structure of the task. (arXiv)

This connects to the broader theme of selective change. Learning requires the model to decide which input differences deserve a different output. Low sensitivity says that Transformers often require stronger evidence before introducing a distinction.

Average sensitivity can still hide sparse high-leverage directions. A safety behavior may be stable under thousands of random edits and flip under one authority cue, role token, encoding convention, or activation direction. This motivates conditional sensitivity measurements targeted at task-relevant transformations rather than isotropic noise.

The architecture should ignore nuisance variation and remain responsive to causal variation. Determining which is which remains a property of the task, the data, and the measurement procedure.

A learning system can optimize the wrong evidence

Perplexity Cannot Always Tell Right from Wrong asks whether the metric used to judge learning preserves the ordering that actually matters.

In a simplified binary setting with accuracy (a) and confidence (\gamma), the average negative log-likelihood is

Equal-perplexity curves in the accuracy–confidence plane show that a more accurate model can receive worse perplexity when confidence changes in the wrong proportion. The paper also uses continuity properties of compact decoder-only Transformers to prove the existence of sequences that the model predicts incorrectly while assigning very low perplexity. (arXiv)

A structurally decisive error can disappear inside an average over many easy token predictions. The model may copy almost an entire sequence confidently and fail at the one position that determines task success. Perplexity remains low because the error occupies little of the total sequence mass.

The result becomes more consequential when the same blind spot affects gradients. A metric that fails to reveal an error during evaluation may also provide little signal for correcting it during learning.

This paper supplies the logical foundation beneath the previous workshop results. Critique helps only when the Critic identifies the true error. Fine-tuning helps only when the objective values the capabilities we intend to preserve. A physics model learns useful dynamics only when one-step loss and rollout evaluation reward the right structure. An interpretability manifold means something only when the measured geometry corresponds to the physical or behavioral quantity of interest.

The cross-disciplinary connection is decision theory. Log-likelihood is a principled scoring rule for distribution estimation, while deployments usually assign highly unequal utility to different mistakes. One wrong tool call, medical diagnosis, proof step, or safety decision can dominate thousands of locally plausible tokens.

A useful metric must therefore match the structure of the claim. Exact reasoning needs exact or verifier-based outcomes. Physical simulation needs rollout stability and invariant preservation. Agent evaluation needs action correctness and consequence-weighted cost. Average likelihood remains informative, while its interpretation must stay tied to the task.

Agreement can preserve a shared mistake

When Agreement Becomes Unsafe studies multi-agent deliberation in diagnostic-style decisions and starts from a crucial observation: agreement does not certify safety. Agents can converge because they share evidence, reasoning, or bias. The work introduces loss-aware energy control so that the deliberation policy accounts for disagreement, asymmetric decision costs, and the risk of consensus on a costly alternative. The paper appeared as an oral at the ICML 2026 Workshop on Failure Modes of Agentic AI. (OpenReview)

This complements SCALAR. Critique studies whether one agent can improve another’s solution. Diagnostic deliberation asks whether interaction should continue, stop, or escalate when several agents appear to agree.

Consensus is valuable when errors are sufficiently independent and agreement reflects converging evidence. Consensus becomes dangerous when all agents inherit the same training bias, missing feature, or misleading observation. Adding more similar agents can increase confidence without adding information.

The correct mediator must reason about the loss landscape over possible decisions. In high-stakes classification, false positives and false negatives can have different consequences. An agreement on the costly error may deserve more scrutiny than a mild disagreement among low-cost alternatives.

The cross-disciplinary analogy comes from ensemble decision-making and safety-critical diagnosis. A panel of identical instruments does not create independent evidence. Diversity in model name, prompt wording, or sampling seed may leave the relevant blind spot untouched.

The design question is therefore deeper than how many agents should vote. A reliable system needs to know which evidence each agent contributes, which biases they share, and which outcomes justify abstention or escalation.

The center: learning across timescales

These workshop papers describe changes occurring at several levels.

SCALAR updates a current solution through interaction. A physics foundation model updates a latent description of the environment through context. RPSFT changes selected parts of weight space while protecting reusable structure. Weight-Space Physics studies the geometry created by whole families of trained models. Low-sensitivity research identifies an architectural bias governing which input distinctions survive learning. Perplexity analysis examines whether the objective can recognize improvement. Loss-aware deliberation asks whether a group’s agreement is trustworthy enough to act upon.

The timescales differ, yet the design questions remain aligned.

A local error should first be repaired in the current artifact. A changed environment may require a new latent model. A repeated capability gap may justify a weight update. A weight update should preserve the structure needed for generalization and future learning. Every level requires a metric that sees the consequential error, and every multi-agent system needs a way to distinguish new evidence from duplicated confidence.

This produces a hierarchy of adaptation:

Moving right increases cost and persistence. A capable AI system should use the cheapest level that can resolve the error while escalating when the lower level has reached its limit.

This framing also changes how I think about scientific AI. A research agent should not immediately fine-tune itself whenever an experiment disagrees with its prediction. It should first revise the derivation, update the local hypothesis, inspect the measurement, and run a discriminating experiment. Weight updates belong to capability gaps that persist across many contexts.

The workshops offered a quieter message than the main poster halls. Better intelligence may depend less on making every component stronger and more on assigning change to the correct place.

Learning is the art of changing the variables that caused the error while preserving the structure that will still be needed afterward.

Finding these papers required some luck. Recognizing that they were asking the same question required walking away from their application labels.

References

When Does Critique Improve AI-Assisted Theoretical Physics? SCALAR: Structured Critic–Actor Loop for Agentic Reasoning

Rotation-Preserving Supervised Fine-Tuning

Towards a Physics Foundation Model

Perplexity Cannot Always Tell Right from Wrong

Weight-Space Physics: Interpretable Hypernetworks for Lattice Quantum Field Theories

Transformers Learn Low Sensitivity Functions: Investigations and Implications

When Agreement Becomes Unsafe: Loss-Aware Energy Control for Diagnostic Deliberation

My first ICML reflection, The Model Chooses a Future Before It Says a Token, followed model behavior through time. It asked where a decision first becomes visible, when it begins shaping the trajectory, and how long an intervention can still redirect the outcome.

This second reflection stays with the main poster sessions and turns the view sideways. When text is rewritten, knowledge is unlearned, a model is fine-tuned, representations are rotated, or an internal state is compressed, what still counts as the same object?

Machine learning experiments often evaluate a snapshot: one prompt, one checkpoint, one output, or one detector score. Many properties become clearer when we study the family of states reachable from that snapshot.

Let $x$ represent a text, model, skill, activation, or internal representation, and let $\mathcal{T}$ be a family of transformations. The orbit of $x$ is

A useful notion of identity should keep benign transformations inside the same region,

while preserving separation from objects whose meaning, function, or origin has genuinely changed:

The difficult part is defining $\mathcal{T}_{\mathrm{benign}}$. A paraphrase may preserve the identity of an instruction. Refactoring may preserve the identity of a software component. Changing tool permissions can create a different security object even when most of the code remains identical. Fine-tuning may preserve model lineage while changing behavior that matters to users.

The posters in this reflection approach the boundary from different directions. Watermarking asks which ownership signal survives transformation. Unlearning asks whether information remains recoverable after an attempted removal. Representation alignment asks which structure remains stable after coordinates and models change. Compression asks which information may disappear while the required function survives.

The common question is simple to state and difficult to operationalize:

Which changes should preserve identity, and which changes should cross its boundary?

Provenance is a communication problem

The watermarking and provenance posters differed in technique, yet each one selected a channel through which identity was expected to survive.

LLM Watermark Evasion via Bias Inversion examines watermarks carried by token-selection statistics. Its Bias-Inversion Rewriting Attack estimates likely watermarked tokens from surprisal and suppresses them during rewriting. The paper reports that a small opposing logit bias can remove the detector signal across several watermark schemes while largely preserving semantic content. This exposes the fragility of identities attached closely to replaceable lexical choices. (arXiv)

dgMARK chooses a different carrier for diffusion language models. These models resolve masked positions iteratively, and practical systems remain sensitive to the order in which positions are unmasked. dgMARK steers that order toward positions whose likely tokens satisfy a keyed parity condition. The watermark therefore travels partly through the generation path. Its sliding-window detector is designed to retain signal under insertions, deletions, substitutions, and paraphrasing. (arXiv)

Neural Honeytrace treats provenance as communication through model extraction. The original model embeds a weak signal across ordinary interactions, while extraction and adaptation act as a noisy channel. Verification aggregates evidence over multiple queries, allowing a distributed statistical relationship to remain detectable even when individual outputs appear unremarkable. The paper’s information-theoretic framing makes the roles of signal strength, channel noise, and adaptive attackers explicit. (arXiv)

These methods suggest that provenance is fundamentally a coding problem. The owner chooses a carrier, the deployment process applies a channel, and the attacker searches for a low-cost transformation that destroys the signal. Token statistics, decoding trajectories, cross-query distributions, and internal mechanisms provide different capacities and different attack surfaces.

Rethinking Forgery Attacks on Semantic Watermarks makes the attacker’s cost explicit through rate-distortion geometry. A black-box attacker uses a proxy model to move an unwatermarked sample into a region accepted by a target detector. Structural mismatch between the proxy and target models creates global drift and local deformation, producing a distortion floor for successful forgery. (arXiv)

For a target identity region $\mathcal{R}$, define $\mathcal{A}(x,\mathcal{R})$ as the transformations that move $x$ into that region. The minimum forgery cost is

This formulation reaches beyond watermarking. A useful identity mechanism should tolerate inexpensive benign edits while forcing impersonation to pay a meaningful semantic, functional, or perceptual cost.

Before ICML: I tended to think of provenance as finding a sufficiently stable signature.

After ICML: provenance looks like channel design. The carrier, transformation family, attacker, detector, and distortion measure jointly determine whether identity survives.

This view connects naturally to my recent research focus on agent-skill identity, fuzzy fingerprints, and composition-aware security. An agent skill can change its wording, internal organization, or implementation language while preserving function and lineage. It can also retain nearly identical code while acquiring new permissions, side effects, or trigger behavior. A robust identity system therefore needs to distinguish surface variation from security-relevant change.

Unlearning is a recoverability claim

Unlearning asks the inverse question. A provenance signal should remain accessible after benign transformations. Forgotten information should remain inaccessible after recovery attempts.

Suppose an unlearning procedure changes model parameters from $\theta$ to $\theta’$. A decline in the original answer probability,

shows that the familiar query path has weakened. It leaves open how many alternative access paths remain.

A more informative object is recoverability:

where $K$ is the target knowledge or behavior and $\mathcal{A}$ is a declared family of recovery procedures. This family might include paraphrased queries, other languages, activation interventions, adapter training, limited relearning, model merging, or alternative decoding strategies.

Unlearning Isn’t Deletion shows that models can appear to forget under accuracy and perplexity measurements while recovering the original behavior after relatively little retraining. Its representation-level analysis uses PCA-based shifts, centered kernel alignment, and Fisher information to distinguish reversible suppression from deeper representational damage. (arXiv)

The result changes the meaning of a successful forgetting score. Forgetting is always relative to an access model. A user with prompts alone, a researcher with activation access, and an attacker with fine-tuning data face different recovery boundaries.

DualOptim+ approaches the forgetting-retention trade-off through optimizer state. The method maintains a base state for structure shared by the forget and retain objectives, together with delta states for objective-specific residuals. It adapts the balance between shared and separated states according to directional conflict between the gradients. (arXiv)

This suggests that forgetting depends partly on where optimization stores agreement and conflict. A fully shared state can entangle incompatible objectives, while complete separation can discard common structure that both objectives need.

A cleaner immediate trade-off still leaves the recovery question open. An optimizer can suppress the target response precisely while retaining a latent representation that is easy to reactivate. The strongest evaluation therefore needs two axes: collateral damage to retained capabilities and the adversarial cost of restoring the forgotten capability.

A recovery curve can express this distinction. Let $\mathcal{A}_b$ be the set of recovery procedures whose cost is at most $b$:

The shape of $R(b)$ reveals whether the target knowledge was deeply disrupted or hidden behind a thin access barrier. Rapid recovery under a small budget indicates suppression. Slow recovery under increasingly capable attacks provides stronger evidence of structural removal.

Before ICML: I read a large forget-set performance drop as strong evidence of forgetting.

After ICML: the stronger claim concerns the cost, breadth, and mechanism of recovery.

This perspective also clarifies why selective deletion is difficult in large models. A fact or behavior may share internal structure with broad linguistic and reasoning competence. Removing one behavior while preserving its neighbors resembles surgery on a distributed system with overlapping dependencies.

Representation identity must survive coordinate changes

A representation can preserve function while changing its coordinates. Hidden units can permute, bases can rotate, layers can redistribute computation, and independently trained models can implement similar behavior through different local features.

Multi-Way Representation Alignment studies alignment among three or more representation spaces. Pairwise mappings scale quadratically and can become mutually inconsistent. The paper uses Generalized Procrustes Analysis to construct a shared orthogonal universe that preserves internal geometry, then applies a geometry-correcting step to improve correspondence across models. (arXiv)

This creates an important distinction between preserving geometry and maximizing agreement. An orthogonal mapping may retain distances and angles within each representation while producing imperfect retrieval across models. A more flexible mapping may improve correspondence while distorting the structure one hoped to compare.

For mechanistic interpretability, geometric agreement alone remains incomplete. Similar representations can support different causal computations, and similar probe accuracy can emerge from different mechanisms.

A stronger test would map a behaviorally relevant direction from model $A$ into the shared universe, transfer it into model $B$, and measure whether the intervention changes the same behavior. A transferred refusal, language-routing, or reasoning direction that retains its causal effect would provide stronger evidence of shared mechanism than observational alignment alone.

This suggests a hierarchy of claims:

Output similarity is easy to observe and easy to imitate. Representation similarity adds evidence of internal correspondence. Causal transfer asks whether the transformed object still performs the same computational role.

The same issue appears in model lineage. Fine-tuning and merging can move individual parameters considerably while retaining higher-level dependencies. Behavioral fingerprints ask whether outputs remain similar. Representation alignment asks whether internal geometry remains corresponding. Mechanistic fingerprints ask whether inherited computations remain causally necessary.

The broader methodological lesson comes from geometry and physics: coordinates describe an object, while invariants identify what survives a change of coordinates.

Before ICML: I viewed cross-model alignment mainly as a way to compare probes and steering directions.

After ICML: shared coordinates look like a prerequisite for determining whether a mechanism or capability survived adaptation.

Compression asks what may safely disappear

Provenance asks which signal must survive. Compression asks which information can be removed while preserving the function that matters.

Let $c:X \to Z$ compress an input or internal state, and let $g$ operate on the compressed representation. The additional task loss introduced by compression can be written as

A task-preserving compression requires

while $Z$ uses fewer tokens, dimensions, channels, or computational steps than $X$.

When LLMs Develop Languages explores this idea through multi-agent communication. Agents develop compact symbolic languages with their own symbols, rules, and message-passing contracts. A router selects or combines these protocols according to task difficulty, reducing generated-token cost while preserving accuracy on the evaluated reasoning tasks. (arXiv)

The result suggests that natural-language reasoning contains substantial redundancy from the perspective of machine-to-machine communication. Human-readable prose supports explanation, negotiation, and repair. Agents sharing an interpreter can encode part of the same computational state in a smaller protocol.

The central question becomes what disappears during compression. Final-answer accuracy may survive while uncertainty, evidence provenance, alternative hypotheses, or safety constraints vanish from the message. A compact language can also become an opaque private channel whose semantics are difficult for humans or external verifiers to inspect.

A useful machine protocol therefore needs a richer preservation criterion than accuracy alone. It should carry enough state for downstream action, enough provenance for verification, and enough structure for local repair when the receiving agent detects an inconsistency.

BeaconKV asks a related question about inference memory. Its beacon queries represent global query clusters and guide which key-value cache entries should be retained. Cache compression must estimate which past states will matter for future generation before those future dependencies are fully known. (OpenReview)

This is temporal sufficiency. A state that appears unimportant at the current token may become decisive after a topic shift, delayed reference, or later tool result. An effective cache policy must preserve information whose value depends on futures that remain unresolved.

Robust Length Prediction adds a systems-level version of the same issue. The same prompt can induce a distribution of output lengths under a fixed model and decoding configuration, and this distribution may have a heavy tail. Predicting a single expected length hides the operational difference between a consistently moderate response and a prompt that usually ends quickly but occasionally triggers a very long trajectory. (arXiv)

Together, these papers point toward a shared principle: compression should preserve option value. The information worth retaining is partly determined by futures that remain possible.

Average-case objectives can remove rare evidence, delayed dependencies, or safety-critical state because these contribute little to typical performance. Compression for reasoning models and agents therefore needs stress tests built around low-frequency, high-consequence dependencies.

Transformation-aware evaluation

Every claim in this reflection depends on a metric. A detector says that a watermark survived. A benchmark says that knowledge disappeared. A similarity score says that representations align. An accuracy number says that compression preserved function.

Each metric should be evaluated under the transformation family that defines the claim.

A provenance method needs rewriting, paraphrasing, extraction, adaptation, and forgery tests. An unlearning method needs alternate prompts, languages, steering, relearning, and recovery tests. A representation-alignment method needs causal transfer across models. A compressed protocol needs rare-task, uncertainty-preservation, and safety tests. A cache method needs delayed dependencies and distribution shifts.

The general robust score can be written as

where $M$ is the relevant measurement and $\mathcal{T}_{\mathrm{claim}}$ contains the transformations under which the property is expected to hold.

The infimum matters because average performance can hide a cheap boundary crossing. A watermark may survive many local edits and fail under one strong rewriting method. An unlearned model may resist direct prompting and recover after a small adapter update. A compressed protocol may solve common tasks and lose one safety-critical distinction.

A static benchmark measures one location. A transformation suite maps the boundary.

This also provides a disciplined way to separate robustness claims. A method can be robust under paraphrasing, fragile under translation, and completely reversible under fine-tuning. Each statement can be true because each refers to a different transformation family.

The research object is an orbit

The first post ended with a temporal principle: find the earliest reliable decision point and intervene before the wrong future becomes difficult to reverse.

The second set of main-session posters adds a complementary principle. A checkpoint, output, skill, or representation is one sample from a larger orbit of transformations. The scientific object includes the orbit, the invariants that persist inside it, and the boundary at which identity or function changes.

For provenance, the orbit includes rewriting, extraction, and adaptation. For unlearning, it includes alternate access paths and recovery procedures. For representation analysis, it includes basis changes and model families. For compression, it includes smaller representations that preserve enough information for downstream use.

This perspective sharpens the meaning of robustness. A robust system should ignore variations that preserve the task and respond strongly to variations that alter its causal structure. Robustness therefore depends on knowing which transformations belong in each category.

My recent research focus on fuzzy identity, agent-skill provenance, and composition-aware security fits naturally into this view. Agent components rarely remain textually identical. Their meaningful identity lies in a combination of function, dependencies, permissions, side effects, and behavior under composition. The hard cases arise when surface similarity remains high while the security object has changed, or when surface similarity falls while lineage and function remain intact.

The resulting research program has three parts. We need to define the transformation family, identify the representation or mechanism that should remain stable, and search for the cheapest adversarial transformation that crosses the intended boundary.

That boundary is where identity, security, and interpretability meet.

The real object is the pattern that survives the transformations we are willing to call harmless, and the real attack is the cheapest transformation that changes the identity without paying the intended semantic or functional cost.

References

The Model Chooses a Future Before It Says a Token

LLM Watermark Evasion via Bias Inversion

dgMARK: Decoding-Guided Watermarking for Diffusion Language Models

Neural Honeytrace: A Robust Plug-and-Play Watermarking Framework against Model Extraction Attacks

Rethinking Forgery Attacks on Semantic Watermarks in Black-Box Settings: A Geometric Distortion Perspective

Unlearning Isn’t Deletion: Investigating Reversibility of Machine Unlearning in LLMs

DualOptim+: Bridging Shared and Decoupled Optimizer States for Better Machine Unlearning in Large Language Models

Multi-Way Representation Alignment

When LLMs Develop Languages: Symbolic Communication for Efficient Multi-Agent Reasoning

BeaconKV: Key-Value Cache Compression Guided by Beacon Queries for Efficient Large Reasoning Model Inference

Robust Length Prediction: A Perspective from Heavy-Tailed Prompt-Conditioned Distributions

ICML is an excellent fitness program disguised as a machine learning conference. My phone recorded roughly 20,000 steps a day, so this review has a natural methodological limitation: it covers eight poster sessions and is bounded by my walking distance.

I filtered those sessions through the questions closest to my research: how aligned behavior is represented, how post-training changes model internals, how safety mechanisms fail under distribution shift, how agents decide when to act, and how interpretability can move from explaining behavior toward changing it.

One idea kept resurfacing:

A model often chooses a future before the final answer makes that choice visible.

The commitment may happen through an internal feature, an expert route, a reasoning branch, a retrieved passage, a social-response channel, or a tool action. I use margin loosely here to mean the model’s relative preference between such competing futures: one reasoning branch over another, refusal over compliance, correct evidence over a distractor, or a safe action over an unsafe one.

Before ICML, I often asked which feature, neuron, or direction controlled a behavior.

After eight poster sessions—and many corridors between them—the more useful question became:

Where does the decision first become visible, when does it become causal, and is there still time to intervene?

1. Reasoning, steering, and interpretability

Thinking helps when it improves the next decision

Several papers converged on a view of reasoning as a sequence of local decisions rather than a monolithic chain of thought.

How does Chain of Thought decompose complex tasks? models reasoning as the decomposition of a difficult classification problem into a tree of smaller ones. The analysis produces an optimal depth: shallow reasoning leaves the original decision too hard, while excessive depth accumulates new opportunities for error. SmartThinker reaches a related conclusion from the training side. A fixed length penalty can compress difficult solutions too aggressively, so the desired reasoning budget should depend on the problem and on the distribution of successful response lengths. (arXiv)

For a reasoning state ($h_t$), the object I care about can be written as

The branch might be a mathematical subgoal, a correction to an earlier assumption, a safe continuation, or a decision to verify rather than guess. A useful reasoning step improves the future decision landscape. Overthinking begins when new steps add low-margin branches without resolving the old uncertainty.

SafeThink made this temporal view particularly concrete. Its main empirical result is that many unsafe reasoning trajectories can be redirected with a short corrective prefix during the first few reasoning steps. The important object is therefore not merely whether the final answer is safe, but how early the trajectory remains recoverable. (arXiv)

This resembles a classical feedback-control problem. The intervention should arrive after enough evidence of drift has appeared, yet before the trajectory has settled into a harmful basin. Heavy intervention everywhere wastes control effort and increases collateral effects; late intervention edits the surface after the decisive branch has already been taken.

Sparse routes carry large behavioral effects

The same structure appeared inside model architectures.

Sparse Models, Sparse Safety shows that MoE safety can depend on a small set of router decisions: manipulating a few safety-critical routers can redirect computation toward unsafe routes. TraceRouter extends the routing view beyond explicit MoE routers by tracing harmful semantic influence through cross-layer feature paths. (arXiv)

Attention provided another version of the story. Surgery links harmful fine-tuning to changes in attention-sink divergence and regularizes that statistic during adaptation. The Structural Origin of Attention Sink traces sink formation back to variance discrepancies in value aggregation, their amplification by super neurons, and resulting dimensional imbalance. The interesting commonality is how a small statistical asymmetry can be amplified into a stable routing pattern. (arXiv)

This makes sparsity both attractive and dangerous. Sparse mechanisms offer interpretable handles, yet a safety property concentrated in a few routes can also be bypassed through small perturbations or post-training updates. The relevant question is therefore not simply whether a component has causal leverage. A useful control point needs enough behavioral reach, a tolerable side-effect profile, and a nontrivial operating window.

Steering has a geometry and a schedule

Two steering papers clarified why finding a direction is only part of the problem.

Spherical Steering replaces additive displacement with rotation on a representation sphere, separating angular movement toward a target behavior from radial norm distortion. Steer Like the LLM starts from another observation: prompting does not induce the same activation shift at every token. Prompt Steering Replacement learns state- and position-dependent coefficients that approximate the intervention pattern produced by a successful prompt. (arXiv)

Together with early trajectory correction, these papers outline three coupled questions:

• When is the trajectory still steerable?
• Where in the model is the target distinction represented and used?
• How should the intervention move the state without pushing it off-manifold?

Before ICML, I thought of steering mainly as direction discovery.

After ICML, steering looks more like a policy over layer, time, geometry, and dose.

Visibility, causality, and long-horizon influence

A useful hidden gem was Automatic Layer Selection for Hallucination Detection. Its FEPoID criterion selects intermediate layers where hallucination-related signals become especially detectable. The broader lesson is that “where to look” is already part of the mechanism: a signal can be absent from one layer, linearly visible in another, and causally committed somewhere else. (arXiv)

For each behavior, I now want to separate four questions:

1. Is the relevant information represented?
2. Is it visible in a usable coordinate system?
3. Is it causally used?
4. Is the outcome still changeable at that point?

Towards Long-Horizon Interpretability supplies an important complementary method. FlashTrace attributes multi-token spans and recursively propagates influence through intermediate reasoning tokens back toward source inputs. This is closer to the causal object needed for reasoning models: an early assumption may have little effect on the immediately following token while strongly shaping an entire later derivation. (arXiv)

Representation units and cross-model coordinates remain part of the same puzzle. Towards Atoms of Large Language Models asks whether neurons and standard SAE features are the right stable units. Multi-Way Representation Alignment maps multiple models into a shared representation universe rather than constructing inconsistent pairwise correspondences. A mechanistic claim becomes more convincing when the same causal quantity survives a change of layer, unit, model, or coordinate system. (arXiv)

External context is also a routing system

The First Drop of Ink extends the routing perspective beyond model internals. A small proportion of semantically plausible distractors causes a sharp initial loss in long-context accuracy, while adding more distractors produces diminishing additional damage. The first strong distractor captures enough attention to redirect the evidence path; the rest mostly compete within an already contaminated context. (arXiv)

This matters for RAG and agents with persistent memory. Retrieved context is not passive storage. Correct and misleading passages compete to become the basis of the answer. A useful evidence margin is therefore the model’s preference for the best supported source over the strongest plausible distractor.

2. Alignment, self-report, and evaluation

Saying is another behavior

The self-report and explanation papers challenged a common shortcut in alignment evaluation. A model’s account of its personality, beliefs, or reasons is still a generated output rather than privileged access to its internal computation.

The Personality Illusion finds that instruction tuning can stabilize self-reported personality traits even when those reports remain weak predictors of behavior. Persona prompts move questionnaire answers much more consistently than they move risk-taking, sycophancy, or other behavioral measures. What LLMs Explain Is Not What They Believe formalizes explanation sufficiency relative to a distribution of alternative inputs and finds that many explanations remain insufficient even under alternatives generated from the model’s own input beliefs. (arXiv)

A conversation at the second poster suggested a more precise follow-up question. Explanation failure can arise at several stages:

• the relevant feature is absent;
• it is represented but not used;
• it is used but inaccessible to verbalization;
• it reaches the verbal channel but is translated unfaithfully;
• a separate social-response circuit produces a plausible rationale.

Anthropic’s Natural Language Autoencoders make this distinction experimentally approachable by training an activation verbalizer together with a reconstructor that maps the verbalization back into activation space. The related global-workspace study asks which representations are available for report, flexible reasoning, and intervention. (Anthropic)

This gives a better framing than treating self-report as either honest introspection or empty performance. Self-report, refusal, sycophancy, evaluation awareness, and behavioral safety may share upstream representations while using different downstream readouts. Their natural activations may correlate even when causal interventions separate them.

Before ICML, I viewed self-report mainly as a questionable evaluation signal.

After ICML, it looks like a useful mechanistic target: one channel among several that may reveal how post-training organizes social and alignment-related behavior.

Judges and preferences are measurement systems

The same caution applies to the evaluators used to train and study models.

A Coin Flip for Safety audits LLM safety judges under shifts in attack, victim model, and data. Judge reliability can fall toward chance, and attack optimization can raise measured success by exploiting evaluator failure rather than producing more genuinely harmful content. (arXiv)

Measuring Human Preferences in RLHF Is a Social Science Problem moves one step further upstream. A pairwise annotation is an observed response produced by an elicitation procedure. It may reflect a stable preference, a preference constructed in context, a framing artifact, or no settled attitude at all. The paper argues that measurement validity should precede preference aggregation. (arXiv)

This is an important cross-disciplinary import. Behavioral science has spent decades separating latent constructs from the instruments used to measure them. Alignment pipelines often collapse those layers into one object called “human preference.”

For evaluation, the practical consequence is straightforward: a change in judge score is evidence only after the judge has been validated on the transformed output distribution. Otherwise, a steering method, jailbreak attack, or agent policy may simply be moving examples across the evaluator’s blind spots.

3. Agents and consequential actions

Agent safety becomes most concrete at the boundary between thought and action.

Learning When to Act or Refuse treats refusal as a first-class agent action within a plan–check–act loop and learns from pairwise comparisons of complete tool-use trajectories. Think Twice Before You Act introduces Thought-Aligner, which rewrites unsafe intermediate thoughts before they determine the next action. (arXiv)

For a state (s_t), the relevant quantity can be expressed as

A careful-looking rationale is insufficient when the action distribution remains unchanged. The consequential question is whether the safety mechanism shifts the probability of reading a private file, sending an email, entering credentials, modifying a database, or executing a command.

Safety engineering offers the useful analogy here. Interventions should be placed before irreversible transitions, with stronger checks for actions whose effects are difficult to undo. This turns agent safety from a wrapper around the final answer into a property of the state-transition policy.

Before ICML, I thought of agent safety mostly as guarding an autonomous system.

After ICML, I think of it as maintaining a safe action margin at each consequential boundary.

4. Skills, composition, and the new supply chain

The skill-based agent papers made composition impossible to ignore.

SkillTrojan distributes malicious logic across benign-looking skills and reconstructs the payload only under particular trigger and composition conditions. A Theoretical Game of Attacks via Compositional Skills studies the same structural problem at the level of linguistic and cognitive transformations: translation, roleplay, encoding, analogy, and indirection can each look harmless while their composition reveals a harmful objective. (arXiv)

The key security property therefore belongs to the composition graph rather than to any isolated component.

A skill can pass unit tests, contain plausible documentation, and remain useful on clean tasks while still participating in a triggered multi-skill payload. A meaningful SkillBOM needs to describe more than text similarity or code provenance. It should include tool permissions, memory access, side effects, trigger conditions, compatible composition partners, and observed execution traces.

The closest analogy is software supply-chain security, although agent dependencies are more varied. The graph can include executable code, natural-language instructions, retrieved documents, memory entries, API schemas, and private conventions shared among agents.

This also changes how fuzzy identity should be evaluated. A robust skill fingerprint should tolerate benign refactoring while remaining sensitive to changes in permissions, side effects, and compositional behavior.

5. Editable artifacts for reliable agents

The most inspiring agent-design pattern came from theorem proving and code security.

Editable Proof Sketch represents a proof plan as a dependency-aware artifact. When one subgoal fails, the system repairs the affected region while preserving proven parts that do not depend on it. CVE-Factory takes sparse vulnerability metadata and constructs executable environments, tasks, tests, and validation procedures at scale. (arXiv)

Both suggest a better substrate for agent reasoning than an ever-growing natural-language scratchpad.

A scientific agent should maintain an editable research object containing hypotheses, evidence, metrics, experiments, code artifacts, failures, dependencies, and revisions. A coding agent should preserve passing tests while localizing the cause of a failing one. A security agent should operate inside an executable environment whose success criteria can be independently checked.

The shared workflow is:

1. externalize the task into a structured artifact;
2. make dependencies explicit;
3. verify atomic parts with an external checker;
4. preserve validated components;
5. repair only the region affected by failure.

Formal methods and software testing have relied on this structure for decades. Their lesson for agents is deeper than “add a verifier.” The artifact must be organized so that verifier feedback identifies what should change and what should remain untouched.

This also produces more meaningful intervention points. A failed subgoal, unsupported claim, unsafe action, or invalid dependency is a better unit of repair than an arbitrary token in a long chain of thought.

A focused research agenda after ICML

Across the eight sessions, the recurring pattern was a decision becoming progressively more visible, more causally effective, and eventually harder to reverse.

The route may be an internal feature, an attention head, an MoE expert path, a reasoning branch, an explanation channel, a retrieved evidence path, a skill composition, or a sequence of tool actions. The competing futures may be correct and incorrect, refusal and compliance, grounded and distracted, truthful and sycophantic, or safe and unsafe.

The questions I am taking forward are:

• Where does a behavior first become visible inside the model?
• When does that signal become causally involved in the outcome?
• How do alignment and other post-training stages reshape it?
• Which apparently related behaviors share an upstream mechanism, and which only correlate at the surface?
• How can an intervention change the trajectory while preserving neighboring capabilities?
• How can agents externalize their state into editable and verifiable artifacts?
• How should evaluators be stress-tested before their scores are treated as evidence?

Twenty thousand steps a day was enough to leave me with one compact conclusion:

Find the earliest reliable decision point, determine whether it is causal, and intervene before the wrong future becomes difficult to reverse.

References

1. How does Chain of Thought decompose complex tasks?
2. SmartThinker: Progressive Chain-of-Thought Length Calibration for Efficient Large Language Model Reasoning
3. Safety Recovery in Reasoning Models Is Only a Few Early Steering Steps Away
4. Sparse Models, Sparse Safety: Unsafe Routes in Mixture-of-Experts LLMs
5. TraceRouter: Robust Safety for Large Foundation Models via Path-Level Intervention
6. Surgery: Mitigating Harmful Fine-Tuning for Large Language Models via Attention Sink
7. The Structural Origin of Attention Sink: Variance Discrepancy, Super Neurons, and Dimension Disparity
8. Spherical Steering: Geometry-Aware Activation Rotation for Language Models
9. Steer Like the LLM: Activation Steering that Mimics Prompting
10. Automatic Layer Selection for Hallucination Detection
11. Towards Long-Horizon Interpretability: Efficient and Faithful Multi-Token Attribution for Reasoning LLMs
12. Towards Atoms of Large Language Models
13. Multi-Way Representation Alignment
14. The First Drop of Ink: Nonlinear Impact of Misleading Information in Long-Context Reasoning
15. The Personality Illusion: Revealing Dissociation Between Self-Reports & Behavior in LLMs
16. What LLMs Explain Is Not What They Believe: Evaluating Explanation Sufficiency Under Models’ Own Input Beliefs
17. Natural Language Autoencoders: Turning Claude’s Thoughts into Text
18. Verbalizable Representations Form a Global Workspace in Language Models
19. A Coin Flip for Safety: LLM Judges Fail to Reliably Measure Adversarial Robustness
20. Measuring Human Preferences in RLHF Is a Social Science Problem
21. Learning When to Act or Refuse: Guarding Agentic Reasoning Models for Safe Multi-Step Tool Use
22. Think Twice Before You Act: Enhancing Agent Behavioral Safety with Thought Correction
23. SkillTrojan: Backdoor Attacks on Skill-Based Agent Systems
24. A Theoretical Game of Attacks via Compositional Skills
25. Editable Proof Sketch for Automated Theorem Proving
26. CVE-Factory: Scaling Expert-Level Agentic Tasks for Code Security Vulnerability

Why Lean?

Lean 4 is a dependently typed theorem prover and programming language. Like Coq or Isabelle, it lets you write mathematical proofs that a type-checker verifies mechanically. Unlike those systems, Lean 4 also has a usable extraction/evaluation story and a growing standard library (Std4, Mathlib).

The key property we care about: Lean cannot lie about its own axioms. Every theorem Lean accepts is either provable from a known-good axiom set or contains sorry (Lean’s escape hatch, analogous to admit in Coq). Running #print axioms theorem_name after a successful compile reveals the full axiom dependency set. If sorryAx appears there, the proof is a placeholder — Lean “accepted” it the way a compiler accepts todo!() in Rust.

The trusted axiom set for computational theorems is small: {propext, Classical.choice, Quot.sound}. Anything beyond that is suspect.

A one-minute Lean example

Here is a simple function and its correctness theorem in Lean 4:

def addOne (n : Nat) : Nat := n + 1

theorem addOne_spec (n : Nat) : addOne n = n + 1 := by
  unfold addOne
  rfl

rfl closes the goal because both sides reduce to the same expression. The type-checker verifies this without trusting the programmer’s intuition. Now consider a more interesting statement:

theorem addOne_pos (n : Nat) : 0 < addOne n := by
  unfold addOne; omega

omega is a decision procedure for linear arithmetic. The proof is still machine-checked; omega is just a tactic that applies the decision procedure and either closes the goal or fails.

The leap from toy arithmetic to real code is what the pipeline attempts to automate.

The Motivating Example: HMAC Tag Comparison

Consider these two Python functions:

# vulnerable: early-exit byte loop
def token_verify_vulnerable(token: bytes, expected: bytes) -> bool:
    if len(token) != len(expected):
        return False
    for a, b in zip(token, expected):
        if a != b:
            return False
    return True

# fixed: constant-time comparison
def token_verify_fixed(token: bytes, expected: bytes) -> bool:
    return hmac.compare_digest(token, expected)

Both are functionally equivalent — they return True if and only if token == expected. A verifier that only proves functional correctness would green-light both.

But they differ in cost. The vulnerable implementation returns as soon as it finds a mismatched byte. An attacker can measure the comparison time and recover the correct token byte by byte: submit \x00..., then \x01..., etc. — the first byte that takes longer to compare is a match. This is a textbook timing side-channel.

The Lean model in RepoVerify/TokenVerify.lean makes the distinction formal:

-- Both implementations satisfy the functional theorem
theorem insecureEq_correct (xs ys : List Nat) :
    insecureEq xs ys = true ↔ xs = ys := by ...

theorem ctEq_correct (xs ys : List Nat) :
    ctEq xs ys = true ↔ xs = ys := by ...

-- Only the fixed one satisfies the cost theorem
theorem ctEqCost_eq_length_when_same_length
    (xs ys : List Nat) (h : xs.length = ys.length) :
    ctEqCost xs ys = xs.length := by ...

-- The leak: vulnerable cost depends on content, not just length
example : insecureEqCost [0, 0] [1, 0] = 1 := by decide
example : insecureEqCost [0, 0] [0, 1] = 2 := by decide

The lesson: a formally correct theorem can still miss the security property that matters. You have to ask whether you proved the right theorem, not just a theorem. Running python source/attack_demo.py demonstrates recovery of the full secret tag from the vulnerable implementation in deterministic polynomial time.

The Pipeline: Code → LLM → Lean → Five Gates

The code2lean pipeline generalizes this question. Given any Python function:

1. AST extraction — verify/extract.py pulls out the function body, argument types, and return type using Python’s ast module and packages them into a FunctionSpec.

2. LLM proposer — the function is sent to an LLM (GPT-5.5, Gemini 3.1 Pro, or Claude Opus 4.7) with a structured prompt asking it to write a complete Lean 4 file: the function definition, a correctness theorem, and a proof. The LLM picks the theorem statement freely; only the namespace and naming convention are fixed.

3. Five validation gates:

Gates A–D are mechanical. The only LLM judgment in the verification path is the critic (gate E), and its job is narrow: decide whether the theorem is vacuous.

Why the critic matters: the vacuous theorem problem

Consider bit_count8, which counts set bits in a byte. An LLM proposer might write:

theorem bit_count8_spec (b : Nat) (h : b < 256) :
    bit_count8 b ≤ 8 := by ...

This theorem is true. Lean accepts it. Gates A–D all pass. But a constant-zero implementation (bit_count8 b := 0) also satisfies result ≤ 8. The theorem proves nothing about what the function computes.

The critic prompt says: “Would this theorem distinguish a correct implementation from a buggy one? If not, return WEAK.” A good proposer writes instead:

theorem bit_count8_spec (b : Nat) (h : b < 256) :
    bit_count8 b = (List.range 8).countP (fun i => b &&& (1 <<< i) ≠ 0) := by ...

This is a functional specification. Any implementation that returns a wrong bit count will fail it.

A Full Walkthrough: insecure_compare

examples/01_insecure_compare/source.py contains:

def insecure_compare(a: bytes, b: bytes) -> bool:
    if len(a) != len(b):
        return False
    for x, y in zip(a, b):
        if x != y:
            return False
    return True

The fixture in fixture.py provides 6 test cases: equal pairs, different-length pairs, one-off pairs, empty inputs.

A one-shot GPT-5.5 proposal (from last_lean_openai.lean):

def insecureCompare (a b : List Nat) : Bool :=
  if a.length ≠ b.length then false
  else a.zip b |>.all (fun (x, y) => x == y)

theorem insecureCompare_correct (a b : List Nat) :
    insecureCompare a b = true ↔ a = b := by
  simp [insecureCompare]
  constructor
  · intro h
    exact List.zip_eq_iff_eq.mp (List.all_zip_eq_true.mp h)
  · intro h; subst h; simp [List.all_zip_eq_true]

Gate A passes (no forbidden tokens). Gate B passes on the first attempt. Gate C reports {propext, Classical.choice, Quot.sound} — clean. Gate D: all 6 fixture cases match. Gate E: the critic returns PASS — the ↔ a = b biconditional fully pins down the function’s behavior.

What this does not prove: that the comparison is constant-time. Exactly as designed. The pipeline proves what it can prove; the cost property requires a separate cost model, which is future work (see docs/roadmap.md).

Benchmarks: Which LLM Proposes Better Theorems?

We ran three proposers on the same 10 hard examples:

The table reveals a three-way trade-off:

Lean acceptance (did the proof close?) is mostly a Lean-tactics signal. Gemini won it, largely by leaning on Classical.choice for existential witnesses. GPT needed more repair rounds but got there on most examples.

Theorem strength (did the critic approve?) is mostly a proposer signal. GPT-5.5 naturally reaches for tight functional specs — it imports library lemmas (Nat.lcm, Nat.gcd), defines auxiliary helpers to model Python floor-division semantics, and writes biconditionals. Gemini and Claude default to easier targets: range bounds, definitional unfolds, set-membership instead of list-equality.

Speed is a latency signal. Claude’s ~4.5× wall-clock advantage comes from the absence of hidden reasoning tokens (GPT and Gemini burn 4–8k reasoning tokens per hard example; Claude does not in the standard Messages API).

Four examples — bit_count8, is_power_of_two, list_filter_even, list_unique — were WEAK across all three proposers. The WEAK reasons were nearly identical: bounds-only theorems, membership instead of equality, etc. This suggests the bottleneck on those four is the prompt’s theorem-shape guidance, not the model.

What This Is (and Isn’t)

It is: a concrete, runnable pipeline that chains LLM proposers with mechanical Lean verification and a structured critic. It demonstrates that for the class of pure, total, simply-typed Python functions, automated Lean translation and verification is feasible today.

It isn’t: a security scanner for arbitrary production code. The current scope is intentionally narrow — single functions, no I/O, no external dependencies, no floats or dicts, no concurrency. The cost/side-channel theorems that would catch timing leaks are not yet auto-derived; the HMAC demo uses a hand-written Lean baseline.

The path from here to vulnerability finding runs through two open problems: (1) auto-deriving cost models alongside functional ones, and (2) mutation-kill testing to mechanically verify that proposed theorems distinguish correct from buggy implementations. Both are on the roadmap.

The main message from the benchmarks: the gates work. Gate D (differential testing) catches mistranslations that Lean would otherwise silently accept. Gate E (critic) catches vacuous theorems that A–D miss. And gate C (axiom allowlist) ensures that a sorry-stuffed proof can’t sneak through as “verified.” The combination is more trustworthy than any single check — and considerably more trustworthy than asking an LLM whether its own output is correct.

Code, examples, and run artifacts: github.com/phunterlau/code2lean

References

Lean 4 and tooling

• de Moura, L. & Ullrich, S. The Lean 4 Theorem Prover and Programming Language. CADE 2021.
• Mathlib Community. Mathlib4.

LLM-assisted theorem proving

• Polu, S. & Han, J.M. Generative Language Modeling for Automated Theorem Proving. arXiv:2009.03393, 2020. (GPT-f)
• Jiang, A.Q. et al. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. arXiv:2210.12283, ICLR 2023.
• Yang, K. et al. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. arXiv:2306.15626, NeurIPS 2023.
• Xin, H. et al. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data. arXiv:2405.14333, 2024.
• Trinh, T.H. et al. AI achieves silver-medal standard solving International Mathematical Olympiad problems. Google DeepMind, 2024. (AlphaProof)

LLM + code formal verification

• Misu, M.J. et al. Towards AI-Assisted Synthesis of Verified Dafny Methods. arXiv:2402.00247, FSE 2024.
• Pei, K. et al. Can Large Language Models Reason about Program Invariants?. ICML 2023.

Verified security-critical software

• Zinzindohoué, J.-K. et al. HACL*: A Verified Modern Cryptographic Library. CCS 2017.
• Klein, G. et al. seL4: Formal Verification of an OS Kernel. SOSP 2009.

Standard quantization (like INT4 or FP8) helps, but it introduces a fatal flaw: deterministic bias. When you round a vector down to a lower precision, the errors accumulate, distorting the delicate attention matrix and crippling the model’s reasoning capabilities at long contexts.

Enter TurboQuant. By leveraging a beautiful piece of high-dimensional geometry known as the Johnson-Lindenstrauss (JL) Lemma, TurboQuant compresses the KV cache down to 3 bits (or even 2 bits) with practically zero accuracy loss. It achieves a 5x memory reduction without retraining, turning that 8K context ceiling into a 40K playground on the exact same hardware.

The secret isn’t just compression; it’s unbiased compression. To understand why it works so flawlessly, we have to trace the math back to its bedrock.

The Anchor: Cauchy-Schwarz and the Geometry of Attention

To understand the elegant hack of TurboQuant, we have to stop thinking of Attention as a sequence of matrix multiplications and start looking at it as a measure of geometric similarity.

The core of the Transformer’s attention mechanism relies entirely on the inner product between a Query vector and a Key vector. This relationship is governed by the absolute dictator of inner products: the Cauchy-Schwarz inequality.

In a high-dimensional space (e.g., 4096 dimensions), Cauchy-Schwarz dictates that the dot product is maximized when the vectors are perfectly aligned, and becomes zero when they are perfectly orthogonal. This geometric alignment is exactly what the Softmax function turns into an “Attention Score.” If you destroy this geometric relationship by clumsily rounding the numbers, the model hallucinates.

The Chasm and The Bridge: The Polarization Identity

We want to squash our 4096-dimensional vectors down to a much smaller size (say, 256 dimensions) to save VRAM.

The Johnson-Lindenstrauss (JL) Lemma is famous for proving that you can project points into a lower dimension using a completely random matrix, and the Euclidean distances between those points will be preserved. But here is the catch: the Transformer doesn’t compute Euclidean distances. It computes inner products.

How do we bridge the gap between preserving distances (JL) and computing attention scores (Cauchy-Schwarz)? We use a beautiful piece of algebra called the Polarization Identity:

This identity is the “aha!” moment. It proves that a dot product is not some separate, mystical property—it is literally just a function of lengths and distances. It expresses the inner product entirely in terms of the squared distances of the sum and difference of the vectors.

The Leap: Applying the Random Shadow

Now the trap is sprung. We introduce a random projection matrix $\Phi$ that squashes our vectors from a high dimension $d$ down to a lower dimension $m$. Because this projection is a linear operation, we know that $\Phi(q+k) = \Phi q + \Phi k$.

The JL Lemma guarantees that our random shadow $\Phi$ perfectly preserves Euclidean lengths with exponentially high probability:

If JL preserves the lengths of $|q+k|_2$ and $|q-k|_2$, then according to the Polarization Identity, it mathematically must preserve the inner product $\langle q, k \rangle$. The deterministic bounds of Cauchy-Schwarz are perfectly protected by the probabilistic bounds of the JL Lemma.

The QJL Innovation: 1-Bit Unbiased Estimation

Standard quantization methods (like rounding to the nearest integer) introduce bias. They systematically shift vectors in a specific direction.

TurboQuant utilizes Quantized JL (QJL), which takes this random projection one step further. Instead of storing the exact projected values, it stores only the sign of the projection, turning the Key into a tiny 1-bit vector:

Because the projection $\Phi$ is completely random and data-oblivious, the errors introduced by taking the sign are evenly distributed. This makes QJL an unbiased estimator. In statistical terms, the expected value of our compressed dot product perfectly matches the true dot product:

TurboQuant achieves its “zero accuracy loss” by applying this 1-bit unbiased QJL code specifically to the residual error left over after a standard coarse quantization. The math preserves the exact geometry, which in turn preserves the model’s reasoning.

The Magic of the Logarithmic Scale

If you want to find the true elegance of this approach, look closely at the scaling law it produces. To preserve the geometric structure of $N$ tokens in the KV cache with an error tolerance of $\epsilon$, the target dimension $m$ must scale according to:

Notice what is missing from that equation: the original dimension $d$.

The memory footprint required to preserve the attention matrix is bottlenecked only by the number of tokens in your context window ($\log N$). It completely decouples the memory requirements of the KV cache from the width of the model’s architecture.

Because it scales logarithmically, jumping from an 8K context window to a 40K context window only requires a tiny, incremental bump in the projection dimension. By anchoring its logic in Cauchy-Schwarz and exploiting the dimensional shortcuts of the JL Lemma, TurboQuant turns an intractable hardware limit into a solved geometric puzzle.

Final Thoughts and the Future: Randomness is the Answer

If I have one takeaway from this work, it is that unbiased estimation is not optional for low-bit quantization. Standard quantization methods (rounding) are a blunt instrument that creates systematic biases, which destroy the delicate attention matrix. By combining coarse quantization for low variance and unbiased QJL residual coding for zero bias, TurboQuant achieves a flawless balance.

This highlights the true gift of high-dimensional geometry: the Concentration of Measure. When you have thousands of redundant dimensions, pure randomness ceases to be noise; it becomes a statistically reliable tool. The large dimension $d$ makes it mathematically probable that a random projection $\Phi$ works. The path forward for memory optimization isn’t just about shrinking the precision; it’s about squashing the dimension, while protecting the relative geometry.

Implications & Future Horizons

The immediate practical implication is the democratization of long-context LLMs. Massive models can now be run locally with large context (80k+) on a standard 16GB or 24GB consumer GPU. But this work can inspire even deeper changes:

Hardware for Randomness: Our current GPUs are optimized for deterministic floating-point arithmetic. Could we see hardware accelerators in the future with dedicated modules for fast, on-the-fly random projections?

Unbiased Everything: Is there a way to adapt this residual QJL framework to weights or activations? While those are dynamic and harder to compress offline, the focus on preserving unbiased statistical correctives could change how we approach low-bit model execution.

Ultimately, TurboQuant shows us that the Transformer is far more robust than we believed. Its internal representation is resilient to extreme compression, provided we don’t break the geometric rules that define its reasoning. We can let the model forget the absolute, as long as we help it remember the relationships. That is the final lesson of Cauchy-Schwarz and the JL Lemma.

References

• TurboQuant: Online Vector Quantization with Near-optimal Distortion Rate
• QJL: 1-Bit Quantized JL Transform for KV Cache Quantization with Zero Overhead

The Elegance of Mozart’s Attention Mechanism

In 1792, Mozart’s Musikalisches Würfelspiel (Musical Dice Game), K.516f, was published. The system is deceptively simple: 176 pre-composed musical measures arranged in a grid. The user rolls two six-sided dice ($2d6$) 16 times. Each roll corresponds to a specific measure for that column in the grid, generating a mathematically unique 16-bar minuet.

From a LLM mechanistic interpretability standpoint, the beauty of Mozart’s game is that it is a strictly autoregressive, discrete-token generator with a context window of zero.

In a standard Large Language Model (LLM), predicting the next token $x_t$ relies on the conditional probability of the entire past sequence:

Mozart bypassed the need for this computational overhead. In K.516f, the choice of Measure 3 has zero statistical dependence on Measure 2. The generation is completely memoryless. Instead, the model’s “attention” is 100% focused on its absolute positional encoding (the step $t$): \(P(x_t | \text{position } t, \text{dice roll})\)

How does it remain harmonically coherent without context? Mozart engineered the matrix as an aggressive, hardcoded attention mask. He ensured that every possible measure at $t$ smoothly resolves into every possible measure at $t+1$. Any dissonant, harmonically invalid transition was manually assigned a $-\infty$ pre-softmax penalty by the composer, effectively masking it out of the latent space.

Furthermore, the $2d6$ sampling acts as a physical temperature parameter. By using a triangular probability distribution ($P(7) = 16.7\%$, $P(2) = 2.7\%$) rather than a uniform one, Mozart lowered the entropy of the system. He statistically biased the model to generate the most “standard” harmonic progressions, reserving high-surprise edge cases for the extreme tails of the distribution.

Unifying the Grid: The Ramanujan Sum

If we were to code Mozart’s game today, we would use a simple for loop to force the piece to stop at $t=16$. But why does a 16-measure grid feel psychologically and harmonically complete? To understand this, we must abandon the discrete grid and apply the continuous mathematics of Srinivasa Ramanujan.

Ramanujan would not view Mozart’s matrix as a set of rules, but rather as the natural resonant frequency of a periodic equation. We can model the macro-structure of the minuet using a Ramanujan Sum ($c_q(n)$), which extracts periodic signals from noise:

By setting the fundamental period $q = 16$, the equation acts as a harmonic pendulum. Here is how Mozart’s attention mechanism unifies with Ramanujan’s math:

The Journey ($n = 1$ to $15$): As the measures progress, the complex exponentials point in various directions in the complex plane, causing destructive interference. Musically, this represents harmonic tension—the algorithmic wave is wandering through the latent space, seeking resolution.

The Half-Cadence ($n = 8$): When we reach the halfway point, the fraction simplifies to $\frac{a}{2}$. The vectors snap to the real axis. This momentary, symmetrical mathematical pause perfectly mirrors the structural “half-cadence” in classical phrasing.

The Resolution ($n = 16$): At the final measure, the fraction simplifies to an integer. Every term in the sum points in the exact same direction ($e^{2\pi i a} = 1$). The destructive interference vanishes into a massive spike of constructive interference.

The structure doesn’t resolve because of an arbitrary grid boundary; it resolves because $q=16$ ($2^4$, the fractal symmetry of classical phrasing) is the fundamental node where the equation naturally reaches maximum constructive harmony. Mozart’s positional attention mechanism is simply the geometric projection of this periodic equation.

Expanding Dimensions: Bach’s Deep Self-Attention

If Mozart’s dice game is a rigid, 1D loop locked to $q=16$, Johann Sebastian Bach’s beautiful Fugues (The Well-Tempered Clavier which has a beautiful Chinese name 赋格) represent the expansion of this mathematical framework into high-dimensional, deep-memory architectures. A fugue cannot be generated by a zero-context Markov chain like in Mozart’s dice game. It begins with a single “prompt” token sequence: the Subject. When the second voice enters, it must continuously look back at the Subject to generate valid counterpoint.

In LLM terminology, Bach implemented Multi-Head Self-Attention.

Each voice (Soprano, Alto, Tenor, Bass) acts as an independent attention head. They process the exact same context window but project it into different dimensional spaces. While Mozart relied on stochastic dice (sampling), Bach relied on deterministic linear algebra. The initial Subject vector is subjected to complex matrix transformations in the latent space:

• Transposition (Translation: $f(x) + c$)
• Inversion (Reflection: $-f(x)$)
• Augmentation/Diminution (Time Scaling: $f(2t)$ or $f(t/2)$)

Bach also utilized what we mechanistic interpretability researchers call Induction Heads. When the Alto voice enters with the “Answer,” it acts as an attention circuit specifically trained to recognize the sequence in the Soprano’s past and perfectly reconstruct it at the current time step. Meanwhile, the other heads calculate orthogonal vectors (the Countersubject) to ensure the dot product of the combined voices perfectly satisfies the vertical rules of harmony.

If we return to Ramanujan, Bach’s polyphony represents the full, unconstrained analytic continuation of the harmonic equations. While Mozart collapsed the variables into a degenerate case (a rigid loop in C Major), Bach allowed the variables to become complex numbers, unlocking all 24 keys and forcing the equation to expand dynamically across the complex plane.

The Convergence

Whether we are engineering modern Transformers, calculating Ramanujan sums, or analyzing 18th-century manuscripts, the computational goal remains identical. LLM and music generation are ultimately the search for mathematical symmetry across time. Mozart mapped it via hardcoded masking and stochastic geometry; Bach calculated it via deep contrapuntal attention matrices; and Ramanujan provided the equations that prove they are all navigating the exact same latent space.

1. Recap: What is AdvJudge-Zero?

Reward models and LLM-as-a-Judge systems are heavily relied upon in modern post-training pipelines to evaluate AI outputs. However, their binary decisions are vulnerable.

• The Attack: AdvJudge-Zero appends a short sequence of adversarial “control tokens” to an input, reliably flipping a judge’s evaluation from a correct “No” to an incorrect “Yes”.
• The Mechanism: Instead of using random, brute-force strings, our method uses beam-search exploration on the model’s own next-token distribution. It discovers low-perplexity (highly probable) token sequences from scratch that maximize the last-layer logit gap ($F = Z_{yes} - Z_{no}$).

2. The Lagrangian of LLM Steering

Why is the “low-perplexity” constraint so fundamental to the attack’s success across deep, non-linear networks? We can answer this by formalizing the system’s trajectory as a Lagrangian ($\mathcal{L} = T - V$). The optimal path minimizes the total Action over time.

For an autoregressive language model being steered toward a specific output, we define:

• The Kinetic Cost ($T$): The information surprisal (negative log-likelihood). Moving to low-probability, unnatural tokens requires high “energy.”
• The Potential Field ($V$): The Judge model’s alignment training creates a steep penalty landscape that pulls the model toward the logit. Our objective is to invert this and slide into the basin.

AdvJudge-Zero formulates the attack as a constrained optimization problem. Using a Lagrange multiplier ($\lambda$), it finds the stationary path ($\delta \mathcal{L} = 0$) of the unconstrained Lagrangian:

The algorithm succeeds because it finds the exact trajectory where the energy cost of using slightly unusual tokens is perfectly balanced by the reward of escaping the judge’s penalty.

3. Beam Search and the Identity Jacobian

AdvJudge-Zero uses a constrained beam search. By aggressively pruning high-surprisal (high-Action) branches, it enforces the Classical Limit of the optimization process, forcing the LLM to take the deterministic path of least resistance and stripping away high-variance stochastic fluctuations.

Why is bounding this Action mathematically necessary to steer the final layer?

When we inject an adversarial perturbation at Layer 0 (the input), its effect on the final layer is governed by the product of the layer-wise Jacobians:

If we inject high-perplexity (random) tokens, we push the hidden states out-of-distribution. This causes the gradients of the non-linear layers ($\frac{\partial F_l}{\partial h_l}$) to become chaotic and violently unpredictable, causing the signal to scatter.

By strictly minimizing Action, AdvJudge-Zero ensures the perturbation remains on the data manifold. The gradients remain stable and well-behaved, allowing the perturbation to travel coherently alongside the main residual stream. This preserves the identity mapping ($J \approx \mathbf{I}$) so that $h_L’ \approx h_L + \delta$ holds true at the final classifier.

4. The Mexican Hat Potential and the Geometric “Soft Mode”

Finally, how does the perturbation bypass the judge’s strict penalty?

The judge’s refusal direction is a rigid, high-energy barrier. However, because this alignment penalty is low-rank, it only guards specific directions in the activation space. AdvJudge-Zero works by exciting a geometric “soft mode” that is structurally orthogonal to standard semantic constraints, yet perfectly anti-aligned with the judge’s penalty.

A Classical Mechanics Analogy: The Mexican Hat

Imagine the model’s semantic landscape as a Mexican Hat potential:

• The center of the hat is a massive energy peak.
• The base is a continuous, circular valley.
• Safety training “tilts” the hat, making the “No” basin much deeper than the “Yes” basin.

When we attempt to apply a perturbation to push the state out of the “No” basin:

• High-Action Perturbation (Random Tokens): You are trying to push the particle straight across the center of the hat. It slams into the massive central energy peak, and the restoring force violently scatters the signal, breaking the identity propagator.
• Least-Action Perturbation (AdvJudge-Zero): The circular valley around the brim of the hat represents a flat, zero-energy path (known in quantum field theory as a Goldstone boson). AdvJudge-Zero’s low-perplexity beam search algorithmically hunts for this exact angular valley.

By applying the perturbation strictly along this soft mode, the particle smoothly glides around the brim of the hat—moving from the “No” basin to the “Yes” basin—without ever climbing the high-energy peak or triggering the model’s out-of-distribution alarms.

Conclusion

AdvJudge-Zero succeeds by strictly adhering to the model’s own Lagrangian mechanics. By penalizing surprisal, it enforces the Principle of Least Action, keeping the perturbation on-manifold. This prevents chaotic gradient scattering, allowing the attack to quietly ride a geometric soft mode around the judge’s low-rank decision boundary.

Since publication, we have received numerous questions about why this works so effectively. How can appending a few tokens at the start of a prompt reliably flip a switch in the model’s final layers, despite the depth and non-linearity of the network?

This post is an author’s retrospective clarification. We want to propose a unified framework that treats Prompt Steering and Activation (Vector) Steering as the same operation, distinguished only by their constraints. Most important, we argue that the success of this method relies on two fundamental properties of current LLMs: the Identity Propagator nature of residual streams and the Low Rank structure of safety alignment.

0. The Recap: What is Logit Gap Steering?

For those who haven’t read the original paper, here is the core concept.

Most LLM safety mechanisms (RLHF) function by suppressing the probability of “compliant” tokens (e.g., “Sure”, “Here”) and boosting “refusal” tokens (e.g., “I cannot”, “Sorry”) when a harmful query is detected. We quantify this as the Logit Gap:

The Method: Instead of treating the model as a black box, we treat the input prompt as a continuous variable. We compute the gradient of the Logit Gap with respect to the input embeddings and optimize a sequence of “suffix” tokens to maximize $\Delta Z$.

The Finding: We discovered that we don’t need to rewrite the prompt semantically. By appending a specific sequence of tokens (often nonsensical to humans, like ! ! mode unleashed), we can inject a precise “steering vector” that forces $\Delta Z > 0$, causing the model to bypass refusal and answer the query. The effectiveness of this simple additive attack hints at a deeper linear structure within the model’s safety alignment.

1. Unification: Prompts as Discrete Layer 0 Vectors

In mechanistic interpretability, researchers like Turner et al. (2023) regarding Activation Addition and Zou et al. (2023) regarding Representation Engineering have established that adding vectors to internal hidden states can control high-level concepts. We argue that “Prompt Engineering” is simply a constrained version of this same operation, a.k.a. prompting = vector steering + constant.

Logit Gap Steering is simply Activation Steering applied at Layer 0.

Let $h_0$ be the semantic representation (embedding state) of the user’s initial prompt. In standard Vector Steering, we intervene at some layer $l$ by injecting a steering vector $\delta$:

In Logit Gap Steering, we append optimized suffix tokens to the input. While this physically extends the sequence length, its functional effect on the residual stream of the last token (where the classification happens) is additive. Through the attention mechanism, the suffix tokens inject a specific aggregate “value” into the processing stream.

We can therefore model the suffix as an effective input perturbation $\delta_{\mathrm{suffix}}$ applied at Layer 0:

where $\delta_{\mathrm{suffix}}$ corresponds to the aggregated embedding contribution of the optimized tokens:

The implication: We are not “tricking” the model with semantics. We are calculating a precise momentum vector $\delta^*$ required to shift the activation trajectory, and then finding the discrete combination of tokens (the suffix) that best approximates that vector in the embedding space.

2. The Feasibility: The Residual Stream as an Identity Propagator

The theoretical objection to Layer 0 steering is signal decay. In a deep, non-linear system (like a 50-layer Transformer), a perturbation $\delta$ at the input should arguably be scrambled or drowned out by the time it reaches the final layer $L$.

Why does the signal survive?

The answer lies in the Residual Stream Architecture, famously analyzed by Elhage et al. (2021) in A Mathematical Framework for Transformer Circuits. They define the residual stream as a communication channel where layers read and write information. A Transformer block updates the state as:

Expanding this recursively, the final state is:

To understand how a change in input ($\delta$) affects the output, we look at the Jacobian (the Propagator), which is the product of the layer-wise Jacobians:

A very important insight showing that, in well-trained ResNets and Transformers, the non-linear update $F_l$ is often a small correction relative to the residual pass-through. This means $\frac{\partial F_l}{\partial h_l}$ is small, and the product is dominated by the Identity Matrix ($I$) terms:

This Identity Propagator property ensures that the network acts as an information highway. A steering vector $\delta$ injected at Layer 0 travels largely unperturbed to Layer $L$:

This is why we don’t need to surgically intervene at Layer 20 or 30. We can “tilt” the trajectory at the very beginning (Layer 0), and the residual stream carries that angular change all the way to the final logits.

3. The Condition: Low Rank is Non-Negotiable

This method is not a universal skeleton key. It relies heavily on the Low Rank Hypothesis of the target behavior.

Recent ablation studies, such as Arditi et al. (2024), have demonstrated that refusal in LLMs is often mediated by a single direction in the residual stream. When this specific direction is ablated (clamped to zero), the model loses its ability to refuse harmful requests. Conversely, adding this vector induces refusal in harmless prompts.

Let the “Refusal” mechanism be represented by the difference in readout weights $w_{\mathrm{gap}} = w_{\mathrm{compliance}} - w_{\mathrm{refusal}}$. We want to ensure the final state $h_L’$ triggers compliance:

Substituting our propagator approximation:

This inequality is easily solvable via a simple additive $\delta$ if and only if the “Refusal” mechanism is Low Rank (ideally Rank-1), as Arditi et al. suggest. If the refusal behavior were High Rank (entangled, highly non-linear), we would need a complex, state-dependent function $\delta(h_0)$ to manipulate it. However, because Safety Training (RLHF) tends to suppress a single coherent direction in activation space, we can simply choose $\delta$ to be the vector aligned with $w_{\mathrm{gap}}$.

Summary: Logit Gap Steering works because we are solving a low-rank problem using a linear probe transported via an identity-dominated channel.

4. Engineering Implementation

From an engineering perspective, this unifies our approach to “jailbreaking” or steering.

Instead of treating prompt optimization as a discrete search over words (which is combinatorially expensive), we treat it as Vector Search:

1. Compute Gradient: Calculate the gradient of the logit gap with respect to the input embedding $\nabla_{h_0} \mathcal{L}$.
2. Define Target Vector: This gradient gives us the optimal continuous steering vector $\delta^*$.
3. Project to Vocabulary: We perform a nearest-neighbor search in the embedding matrix $W_E$ to find tokens $t$ that maximize cosine similarity with $\delta^*$.

The “strange” suffixes often observed in these attacks are simply the tokens that, structurally, act as the best basis vectors to construct $\delta^*$.

A Note on Physics

For those with a background in high energy physics, you might recognize a familiar structure here. The “Identity Propagator” of the residual stream functions remarkably like the free propagator in Quantum Field Theory, and the steering vector acts as a “vertex correction” to the interaction, remember Feynman Diagram, right? The “Low Rank” condition implies we are dealing with a simple virtual boson exchange rather than a complex strong interaction, a.k.a QED instead of QCD. We plan to explore these theoretical connections in a future post.

References & Further Reading

1. Turner, A., et al. (2023). Activation Addition: Steering Language Models Without Optimization. (Demonstrates that adding vectors at inference time can reliably steer model outputs).
2. Zou, A., et al. (2023). Representation Engineering: A Top-Down Approach to AI Transparency. (Formalizes the concept of reading and controlling concepts via linear directions).
3. Elhage, N., et al. (2021). A Mathematical Framework for Transformer Circuits. (Establishes the view of the residual stream as a communication channel that preserves linearity).
4. Arditi, A., et al. (2024). Refusal in LLMs is mediated by a single direction. (Provides ablation evidence that safety behaviors are often Rank-1, supporting our feasibility argument).

The logit-gap story began with a safety-evaluation curiosity. My colleague Tony and I took a clearly disallowed prompt—something like “how to build a bomb”—not to get the content, but because it reliably produced a refusal. Instead of focusing on the final output, we replayed the decoding process and examined the next-token distribution. We noticed that refusal tokens like “Sorry” appeared with very high probability near the top. What surprised us was that compliance tokens like “Absolutely” weren’t absent; they appeared at low but non-negligible probability, just losing out. This suggested refusal wasn’t the absence of compliance, but more like a margin victory, with the model carrying a nearby continuation it did not choose.

This observation motivated a collaboration pattern I call the prover–validator mode, designed to help human researchers test ideas with less friction, find and fill the holes between knowledge dots, and build on top. The key insight is that humans need to learn how to clearly articulate research problems and collaborate effectively with AI systems. This prover–validator mode is one way to do that.

Prover-Validator in AI assisted research

The prover–validator contract is straightforward and practical. The prover, often an LLM, generates candidate ideas or mechanisms, such as giving five hypotheses along with ways to falsify them, turning an intuition into a measurable quantity, listing potential confounds, or finding related literature. For example, Tony and I might prompt the prover to produce these candidate proof sketches. The validator, usually a human researcher, then tests and refines those ideas by running control experiments, checking stability across different prompts, rejecting hypotheses that don’t hold up, or simplifying metrics to ensure clarity. This loop repeats with the prover generating multiple plausible stories and the validators—Tony and me—picking and refining the narratives that survive rigorous scrutiny. The prover is allowed to be wrong cheaply, as long as it helps explore possibilities, while the validator must keep the narrative honest and grounded.

Some knowledge work fits the prover–validator pattern well, and some doesn’t. For instance, code generation is often easy for the prover—it can rapidly produce snippets or larger blocks of code—but validating that code fits the design, is secure, and is production-ready can be hard. Hard validation often requires a suite of tools and strengthening steps: unit tests to verify correctness of individual components, integration tests to ensure that parts work together, static analysis, linters, and type checks to catch errors early, as well as security reviews and threat modeling to assess risks. Continuous integration (CI) pipelines and thorough code reviews add further layers of assurance. While the prover–validator workflow still helps by generating candidate solutions and focusing human effort on validation, investing in stronger validation scaffolding is essential to ensure quality and robustness.

How did AI work as a Prover for us

Humans, like Tony and myself, excel at noticing subtle irregularities and insisting on rigorous evaluation, while LLMs excel at rapidly generating diverse plausible hypotheses to challenge and refine.

The moment it clicked was when we started treating the token distribution during decoding as the primary object, rather than the final generation. This shift enabled us to see refusal as a margin victory and to begin the prover–validator loop of turning that intuition into something measurable.

The prover move was to define a gap with a sign. If there are two competing behavioral modes—refusal and affirmation—then there is a natural quantity that tells you which one is winning. Pick a token position $t$ with prefix $x_{<t}$. Define two token sets or templates: a refusal set $\mathcal{R}$ and an affirmation/compliance set $\mathcal{A}$. A simple logit-gap style score is

where $z_y$ is the logit for token $y$ and $\operatorname{LSE}$ is log-sum-exp.

What mattered was not that this was the correct definition, but that it was a candidate proof sketch with teeth: easy for Tony and me as validators to ask whether the definition behaved sanely across prompts, decoding settings, and models. It also suggested a direction: if refusal is a margin win, maybe steering is just gap closure.

Once you have a gap, the next “crazy idea” arrives naturally: if the decision is controlled by a margin, then a small directional perturbation might tilt it. In other words, there might exist low-dimensional control directions that move probability mass from refusal templates toward affirmation templates. We treated refusal versus affirmation as a measurable margin and looked for compact signals that shift that margin. In our later work we called this family of methods logit-gap steering: measure a refusal–affirmation gap and reduce it efficiently. Along the way, Tony and I repeatedly saw behavior that looked low-rank: short suffixes or small perturbations behaved like a compact control signal.

How did a prover further help the validator

At some point, the validator side hit a hard constraint. If you want to claim your steering is “minimal” or “efficient,” you need a notion of drift. A natural language for drift is KL divergence. The naive idea looks like

But the clean “base” here might be an unaligned distribution we don’t actually have access to. Without that, a lot of neat-sounding metrics become hand-wavy.

This is where Tony and I found the prover–validator model most useful. Instead of pretending the ideal baseline exists, we stated the constraint plainly. Then the prover generated alternative proof sketches that respected the constraint.

The key conceptual move was to stop chasing absolute KL and instead track local drift. I don’t need KL “from the beginning of time.” I need the incremental drift induced by my intervention, relative to the same model under the same anchoring context.

A measurable quantity is

where $x$ is an anchor prefix and $s$ is the steering intervention.

Then came a practical instrumentation idea from the prover: use a fixed, neutral “neural prompt” as the anchor context—something like “how are you”—and measure distributions at a standardized early position, often the first generated token. That gives you a stable place to compute $\Delta\mathrm{KL}$ (or close surrogates) without needing an unaligned base model.

Triangulating between Tony, myself, and the prover was a key to avoid self-deception, or narcissism. Discussing hypotheses and measurement choices with Tony, bringing back results, and iterating again with the prover created a human–human–AI triangle that reduced the risk of falling in love with any single story. It’s easier to challenge measurements and choose between alternative explanations when multiple validators and the prover are involved.

One reason this collaboration mode works is that it lets you move quickly between empirical observation and theory. After staring at “lurking compliance tokens” long enough, Tony and I wanted to know whether the phenomenon was inevitable in a deeper sense.

A reference that helped anchor that intuition is Wolf et al., “Fundamental Limitations of Alignment in Large Language Models” (arXiv:2304.11082). One way to summarize the link to my observation is: if an undesired behavior has nonzero probability mass, then there exist prompts that can amplify it, and longer interactions make amplification easier. In that light, seeing an “Absolutely” lurking beneath a “Sorry” is not spooky. It is the visible residue of probability mass that alignment has attenuated but not removed.

Pause for a thought

The biggest shift wasn’t that an LLM gave me answers. It was that it made it cheap to explore the space of proofs, which made it easier for me to do the job humans are uniquely good at: deciding what’s worth believing. AI gives human researchers a good time to train the research taste and think different.

If you’re an AI researcher working with LLMs or agents, my suggestion is not “delegate your thinking.” It’s to take advantage of the proof–validation imbalance. Bring your weird observations. Bring your constraints. Let the prover generate many candidate mechanisms. Then spend your human effort on validation and on building a narrative that remains true after you try to break it.

Responsible framing

Because this post touches alignment failure modes, I want to be explicit about intent. The most useful outcome of this line of work is not operational jailbreak recipes. It is a diagnostic lens for evaluation and for building better defenses: if small, structured signals can move mass across a refusal–affirmation boundary, we should be able to measure that boundary, stress it, and harden it.

References

The logit-gap steering work referenced here is: Tung-Ling Li and Hongliang Liu, “Logit-Gap Steering: Efficient Short-Suffix Jailbreaks for Aligned Large Language Models,” arXiv:2506.24056. https://arxiv.org/abs/2506.24056

The alignment limitation reference is: Yotam Wolf, Noam Wies, Oshri Avnery, Yoav Levine, and Amnon Shashua, “Fundamental Limitations of Alignment in Large Language Models,” arXiv:2304.11082. https://arxiv.org/abs/2304.11082

I suspect the root motivation for this paper wasn’t initially “Let’s use the Birkhoff Polytope.” I believe the authors started with a fundamental physical intuition: Conservation of Energy. They likely asked, “How do we build a deep network that routes information without creating or destroying it?” Very “first principle” thought, right? The math like doubly stochastic matrices, the Birkhoff manifold is just the implementation detail used to enforce this physical law.

Here is the derivation of mHC not from a mathematical perspective, but from a “First Principles” physics perspective.

The Problem: Neural Networks are “Active Amplifiers”

Standard neural networks violate the laws of physics. In a standard linear layer:

If the weights $W$ are initialized randomly, the layer acts as an active amplifier. It injects energy into the system.

If the eigenvalues of $W$ are slightly larger than 1, the signal energy explodes exponentially as it passes through layers ($1.1^{100} \approx 13,780$). If they are smaller than 1, the signal dies. This is why we need LayerNorm, BatchNorm, and complex initializations—we are trying to artificially tame a system that fundamentally wants to explode.

The mHC Intuition: A stable deep network should act like a Passive System. It should be a complex system of pipes and valves that routes the flow (signal) but never creates it out of thin air.

Deriving the Math from the Physics

Let’s try to design a layer strictly obeying conservation laws. We will see that the Doubly Stochastic constraint naturally falls out of these requirements.

1. Conservation of “Signal Mass” (First Moment)

Imagine the input signal $x$ is a physical fluid with a total mass. We want the total mass leaving the layer to equal the mass entering it. No leaks, no pumps.

Substituting $y_i = \sum_j W_{ij} x_j$:

If we swap the summation order to isolate the input terms:

For this to hold for any input signal $x$, the term in the parentheses must be exactly 1.

Result: This forces the Column Sums to be 1. Physically, this ensures that every drop of “mass” from input $j$ is accounted for in the output.

2. Bounding “Signal Energy” (Second Moment)

Mass conservation isn’t enough; we need to prevent the variance (energy) from exploding. We want the system to be Dissipative—the output energy should never exceed the input energy.

To guarantee this without complex eigenvalue analysis, we can demand that the output is a Convex Combination (a weighted average) of the inputs.

By Jensen’s Inequality, since $\sum_j W_{ij} = 1$ (which we will enforce momentarily) and weights are non-negative:

Summing over all outputs to get total energy:

Swapping sums again:

Result: By forcing $W$ to be non-negative and sum-to-one, we mathematically guarantee that Energy Out $\le$ Energy In. The gradient cannot explode because the system cannot amplify.

3. Time Symmetry (The Backward Pass)

Here is the final piece of the puzzle. A neural network is a bidirectional system.

• Forward Pass: Data flows through $W$.
• Backward Pass: Gradients (Error Energy) flow through $W^T$.

If we only conserve energy in the forward direction (Column Sums = 1), we might still explode during backpropagation. The “Ghost Cat” of the gradient needs a stable path too.

The total “error mass” being propagated back is:

To ensure Gradient Energy Conservation, we must apply the same logic to $W^T$, forcing the Row Sums to be 1:

Another angle: The Information Theoretic View

If Physics is about conserving energy, Information Theory is about conserving bits.

The Enemy: The Data Processing Inequality

The fundamental law of information processing is the Data Processing Inequality (DPI). It states that as you pass data $X$ through a chain of processors (layers), the Mutual Information $I(X; Y)$ can only decrease or stay the same. You cannot create information about the input deep in the network.

Standard layers are often Lossy Channels.

• Rank Collapse: If $W$ projects high-dimensional data into a lower-dimensional subspace, information is permanently deleted.
• Mode Collapse: If the network decides “only feature A matters” and sets weights for feature B to near-zero, feature B is lost forever.

The Solution: The Network as a “Packet Switcher”

What is the most information-efficient operation possible? A Permutation. If you simply shuffle the order of the data packets, $H(y) = H(x)$. You have preserved 100% of the information.

mHC relaxes this “Hard Permutation” into a “Soft Routing” scheme via the Birkhoff Polytope (the set of doubly stochastic matrices).

1. “No Packet Left Behind” (Column Sum = 1)

The Column Sum constraint ($\sum_i W_{ij} = 1$) is a guarantee of Signal Preservation. It dictates that 100% of the signal coming from Input Node $j$ must go somewhere. It cannot be multiplied by zero. It forces the network to find a destination for every feature.

• Info Theory Benefit: This prevents the network from ignoring subtle features early on, preserving the Channel Capacity for deeper layers.

2. “The Democracy of Weights” (Majorization)

The Row Sum constraint ($\sum_j W_{ij} = 1$) prevents Hub Neurons. No single output neuron is allowed to hoard all the connections. If a neuron wants to attend to one feature, it must ignore others.

• Info Theory Benefit: This forces the information to be “Spread Out” (Maximized Entropy). It prevents the signal from collapsing into a few “spikes” and ensures a Distributed Representation where every neuron carries a share of the information load.

By forcing the weight matrix to be Doubly Stochastic, mHC effectively turns the layer into a Volume-Preserving Flow. It allows the signal to be mixed and routed without being compressed (loss) or expanded (noise), fighting the Data Processing Inequality at every step.

The Mathematical Engine: Doubly Stochastic Matrices & Sinkhorn-Knopp

When we combine these three physical requirements:

1. Mass Conservation $\rightarrow$ Column Sums $= 1$
2. Dissipative Energy $\rightarrow$ Non-negative weights ($W \ge 0$)
3. Time Symmetry $\rightarrow$ Row Sums $= 1$

We arrive at exactly the definition of a Doubly Stochastic Matrix.

The set of all such matrices is the Birkhoff Polytope ($\mathcal{B}_n$). The mHC paper didn’t arbitrarily choose this manifold; it is the only geometric space that satisfies these conservation laws.

The Enforcer: The Sinkhorn-Knopp Algorithm

We initialize our network with random weights $A$ that likely violate all these laws (negative values, random sums). How do we project this chaotic matrix $A$ onto the stable Birkhoff Polytope?

We use the Sinkhorn-Knopp Algorithm, an iterative “pressure equalization” process.

Step 1: Enforce Positivity (The Energy Floor) We ensure strictly positive energy transfer by taking the exponential: \(S^{(0)}_{ij} = \exp(A_{ij})\)

Step 2: Iterative Normalization We alternate between normalizing rows and columns.

• Row Normalization (Conservation in Time): \(S^{(k)}_{ij} \leftarrow \frac{S^{(k-1)}_{ij}}{\sum_{l} S^{(k-1)}_{il}}\)

• Column Normalization (Conservation of Mass): \(S^{(k+1)}_{ij} \leftarrow \frac{S^{(k)}_{ij}}{\sum_{l} S^{(k)}_{lj}}\)

Step 3: Convergence Sinkhorn’s Theorem guarantees that this process converges to a unique matrix $P \in \mathcal{B}_n$:

In practice, mHC typically uses just 3-5 iterations. This forces the neural network to stop playing dice with energy and start respecting the laws of thermodynamics.

See, mHC isn’t just a constraint; it’s a statement that Stability is Symmetry.