❌

Normal view

Gradient-based Planning for World Models at Longer Horizons

BallNav demo Push-T demo

GRASP is a new gradient-based planner for learned dynamics (a “world model”) that makes long-horizon planning practical by (1) lifting the trajectory into virtual states so optimization is parallel across time, (2) adding stochasticity directly to the state iterates for exploration, and (3) reshaping gradients so actions get clean signals while we avoid brittle “state-input” gradients through high-dimensional vision models.

Large, learned world models are becoming increasingly capable. They can predict long sequences of future observations in high-dimensional visual spaces and generalize across tasks in ways that were difficult to imagine a few years ago. As these models scale, they start to look less like task-specific predictors and more like general-purpose simulators.

But having a powerful predictive model is not the same as being able to use it effectively for control/learning/planning. In practice, long-horizon planning with modern world models remains fragile: optimization becomes ill-conditioned, non-greedy structure creates bad local minima, and high-dimensional latent spaces introduce subtle failure modes.

In this blog post, I describe the problems that motivated this project and our approach to address them: why planning with modern world models can be surprisingly fragile, why long horizons are the real stress test, and what we changed to make gradient-based planning much more robust.


This blog post discusses work done with Mike Rabbat, Aditi Krishnapriyan, Yann LeCun, and Amir Bar (* denotes equal advisorship), where we propose GRASP.


What is a world model?

These days, the term “world model” is quite overloaded, and depending on the context can either mean an explicit dynamics model or some implicit, reliable internal state that a generative model relies on (e.g. when an LLM generates chess moves, whether there is some internal representation of the board). We give our loose working definition below.

Suppose you take actions $a_t \in \mathcal{A}$ and observe states $s_t \in \mathcal{S}$ (images, latent vectors, proprioception). A world model is a learned model that, given the current state and a sequence of future actions, predicts what will happen next. Formally, it defines a predictive distribution on a sequence of observed states $s_{t-h:t}$ and current action $a_t$:

\[P_\theta(s_{t+1} \mid s_{t-h:t},\; a_t)\]

that approximates the environment’s true conditional $P(s_{t+1} \mid s_{t-h:t},\; a_t)$. For this blog post, we’ll assume a Markovian model $P(s_{t+1} \mid s_{t-h:t},\; a_t)$ for simplicity (all results here can be extended to the more general case), and when the model is deterministic it reduces to a map over states:

\[s_{t+1} = F_\theta(s_t, a_t).\]

In practice the state $s_t$ is often a learned latent representation (e.g., encoded from pixels), so the model operates in a (theoretically) compact, differentiable space. The key point is that a world model gives you a differentiable simulator; you can roll it forward under hypothetical action sequences and backpropagate through the predictions.


Planning: choosing actions by optimizing through the model

Given a start $s_0$ and a goal $g$, the simplest planner chooses an action sequence $\mathbf{a}=(a_0,\dots,a_{T-1})$ by rolling out the model and minimizing terminal error:

\[\min_{\mathbf{a}} \; \| s_T(\mathbf{a}) - g \|_2^2, \quad \text{where } s_T(\mathbf{a}) = \mathcal{F}_{\theta}^{T}(s_0,\mathbf{a}).\]

Here we use $\mathcal{F}^T$ as shorthand for the full rollout through the world model (dependence on model parameters $\theta$ is implicit):

\[\mathcal{F}_{\theta}^{T}(s_0, \mathbf{a}) = F_\theta(F_\theta(\cdots F_\theta(s_0, a_0), \cdots, a_{T-2}), a_{T-1}).\]

In short horizons and low-dimensional systems, this can work reasonably well. But as horizons grow and models become larger and more expressive, its weaknesses become amplified.

So why doesn’t this just work at scale?


Why long-horizon planning is hard (even when everything is differentiable)

There are two separate pain points for the more general world model, plus a third that is specific to learned, deep learning-based models.

1) Long-horizon rollouts create deep, ill-conditioned computation graphs

Those familiar with backprop through time (BPTT) may notice that we’re differentiating through a model applied to itself repeatedly, which will lead to the exploding/vanishing gradients problem. Namely, if we take derivatives (note we’re differentiating vector-valued functions, resulting in Jacobians that we denote with $D_x (\cdots)$) with respect to earlier actions (e.g. $a_0$):

\[D_{a_0} \mathcal{F}_{\theta}^{T}(s_0, \mathbf{a}) = \Bigl(\prod_{t=1}^T D_s F_\theta(s_t, a_t)\Bigr) D_{a_0}F_\theta(s_0, a_0).\]

We see that the Jacobian’s conditioning scales exponentially with time $T$:

\[\sigma_{\text{max/min}}(D_{a_0}\mathcal{F}_{\theta}^{T}) \sim \sigma_{\text{max/min}}(D_s F_\theta)^{T-1},\]

leading to exploding or vanishing gradients.

2) The landscape is non-greedy and full of traps

At short horizons, the greedy solution, where we move straight toward the goal at every step, is often good enough. If you only need to plan a few steps ahead, the optimal trajectory usually doesn’t deviate much from “head toward $g$” at each step.

As horizons grow, two things happen. First, longer tasks are more likely to require non-greedy behavior: going around a wall, repositioning before pushing, backing up to take a better path. And as horizons grow, more of these non-greedy steps are typically needed. Second, the optimization space itself scales with horizon: $\mathrm{dim}(\mathcal{A} \times \cdots \times \mathcal{A}) = T\mathrm{dim}(\mathcal{A})$, further expanding the space of local minima for the optimization problem.

Loss landscape
Distance to goal along the optimal path is non-monotonic, and the resulting loss landscape can be rough.

A long-horizon fix: lifting the dynamics constraint

Suppose we treat the dynamics constraint $s_{t+1} = F_{\theta}(s_t, a_t)$ as a soft constraint, and we instead optimize the following penalty function over both actions $(a_0,\ldots,a_{T-1})$ and states $(s_0,\ldots,s_T)$:

\[\min_{\mathbf{s},\mathbf{a}} \mathcal{L}(\mathbf{s}, \mathbf{a}) = \sum_{t=0}^{T-1} \big\|F_\theta(s_t,a_t) - s_{t+1}\big\|_2^2, \quad \text{with } s_0 \text{ fixed and } s_T=g.\]

This is also sometimes called collocation in planning/robotics literature. Note the lifted formulation shares the same global minimizers as the original rollout objective (both are zero exactly when the trajectory is dynamically feasible). But the optimization landscapes are very different, and we get two immediate benefits:

  • Each world model evaluation $F_{\theta}(s_t,a_t)$ depends only on local variables, so all $T$ terms can be computed in parallel across time, resulting in a huge speed-up for longer horizons, and
  • You no longer backpropagate through a single deep $T$-step composition to get a learning signal, since the previous product of Jacobians now splits into a sum, e.g.:
\[D_{a_0} \mathcal{L} = 2(F_\theta(s_0, a_0) - s_1).\]

Being able to optimize states directly also helps with exploration, as we can temporarily navigate through unphysical domains to find the optimal plan:

Collocation planning in BallNav
Collocation-based planning allows us to directly perturb states and explore midpoints more effectively.

However, lunch is never free. And indeed, especially for deep learning-based world models, there is a critical issue that makes the above optimization quite difficult in practice.

An issue for deep learning-based world models: sensitivity of state-input gradients

The tl;dr of this section is: directly optimizing states through a deep learning-based $F_{\theta}$ is incredibly brittle, à la adversarial robustness. Even if you train your world model in a lower-dimensional state space, the training process for the world model makes unseen state landscapes very sharp, whether it be an unseen state itself or simply a normal/orthogonal direction to the data manifold.

Adversarial robustness and the “dimpled manifold” model

Adversarial robustness originally looked at classification models $f_\theta : \mathbb{R}^{w\times h \times c} \to \mathbb{R}^K$, and showed that by following the gradient of a particular logit $\nabla f_\theta^k$ from a base image $x$ (not of class $k$), you did not have to move far along $x’ = x + \epsilon\nabla f_\theta^k$ to make $f_\theta$ classify $x’$ as $k$ (Szegedy et al., 2014; Goodfellow et al., 2015):

Adversarial example
Depiction of the classic example from (Goodfellow et al., 2015).

Later work has painted a geometric picture for what’s going on: for data near a low-dimensional manifold $\mathcal{M}$, the training process controls behavior in tangential directions, but does not regularize behavior in orthogonal directions, thus leading to sensitive behavior (Stutz et al., 2019). Another way stated: $f_\theta$ has a reasonable Lipschitz constant when considering only tangential directions to the data manifold $\mathcal{M}$, but can have very high Lipschitz constants in normal directions. In fact, it often benefits the model to be sharper in these normal directions, so it can fit more complicated functions more precisely.

Adversarial perturbations leave the data manifold

As a result, such adversarial examples are incredibly common even for a single given model. Further, this is not just a computer vision phenomenon; adversarial examples also appear in LLMs (Wallace et al., 2019) and in RL (Gleave et al., 2019).

While there are methods to train for more adversarially robust models, there is a known trade-off between model performance and adversarial robustness (Tsipras et al., 2019): especially in the presence of many weakly-correlated variables, the model must be sharper to achieve higher performance. Indeed, most modern training algorithms, whether in computer vision or LLMs, do not train adversarial robustness out. Thus, at least until deep learning sees a major regime change, this is a problem we’re stuck with.

Why is adversarial robustness an issue for world model planning?

Consider a single component of the dynamics loss we’re optimizing in the lifted state approach:

\[\min_{s_t, a_t, s_{t+1}} \|F_\theta(s_t, a_t) - s_{t+1}\|_2^2\]

Let’s further focus on just the base state:

\[\min_{s_t} \|F_\theta(s_t, a_t) - s_{t+1}\|_2^2.\]

Since world models are typically trained on state/action trajectories $(s_1, a_1, s_2, a_2, \ldots)$, the state-data manifold for $F_{\theta}$ has dimensionality bounded by the action space:

\[\mathrm{dim}(\mathcal{M}_s) \le \mathrm{dim}(\mathcal{A}) + 1 + \mathrm{dim}(\mathcal{R}),\]

where $\mathcal{R}$ is some optional space of augmentations (e.g. translations/rotations). Thus, we can typically expect $\mathrm{dim}(\mathcal{M}_s)$ to be much lower than $\mathrm{dim}(\mathcal{S})$, and thus: it is very easy to find adversarial examples that hack any state to any other desired state.

As a result, the dynamics optimization

\[\sum_{t=0}^{T-1} \big\|F_\theta(s_t,a_t) - s_{t+1}\big\|_2^2\]

feels incredibly “sticky,” as the base points $s_t$ can easily trick $F_{\theta}$ into thinking it’s already made its local goal.1

Adversarial world model example

1. This adversarial robustness issue, while particularly bad for lifted-state approaches, is not unique to them. Even for serial optimization methods that optimize through the full rollout map $\mathcal{F}^T$, it is possible to get into unseen states, where it is very easy to have a normal component fed into the sensitive normal components of $D_s F_{\theta}$. The action Jacobian’s chain rule expansion is

\[\Bigl(\prod_{t=1}^T D_s F_\theta(s_t, a_t)\Bigr) D_{a_0}F_\theta(s_0, a_0).\]

See what happens if any stage of the product has any component normal to the data manifold. ↩


Our fix

This is where our new planner GRASP comes in. The main observation: while $D_s F_{\theta}$ is untrustworthy and adversarial, the action space is usually low-dimensional and exhaustively trained, so $D_a F_{\theta}$ is actually reasonable to optimize through and doesn’t suffer from the adversarial robustness issue!

Network diagram showing high-dim state vs low-dim action
The action input is usually lower-dimensional and densely trained (the model has seen every action direction), so action gradients are much better behaved.

At its core, GRASP builds a first-order lifted state / collocation-based planner that is only dependent on action Jacobians through the world model. We thus exploit the differentiability of learned world models $F_{\theta}$, while not falling victim to the inherent sensitivity of the state Jacobians $D_s F_{\theta}$.

GRASP: Gradient RelAxed Stochastic Planner

As noted before, we start with the collocation planning objective, where we lift the states and relax dynamics into a penalty:

\[\min_{\mathbf{s},\mathbf{a}} \mathcal{L}(\mathbf{s}, \mathbf{a}) = \sum_{t=0}^{T-1} \big\|F_\theta(s_t,a_t) - s_{t+1}\big\|_2^2, \quad \text{with } s_0 \text{ fixed and } s_T=g.\]

We then make two key additions.

Ingredient 1: Exploration by noising the state iterates

Even with a smoother objective, planning is nonconvex. We introduce exploration by injecting Gaussian noise into the virtual state updates during optimization.

A simple version:

\[s_t \leftarrow s_t - \eta_s \nabla_{s_t}\mathcal{L} + \sigma_{\text{state}} \xi, \qquad \xi\sim\mathcal{N}(0,I).\]

Actions are still updated by non-stochastic descent:

\[a_t \leftarrow a_t - \eta_a \nabla_{a_t}\mathcal{L}.\]

The state noise helps you “hop” between basins in the lifted space, while the actions remain guided by gradients. We found that specifically noising states here (as opposed to actions) finds a good balance of exploration and the ability to find sharper minima.2


2. Because we only noise the states (and not the actions), the corresponding dynamics are not truly Langevin dynamics. ↩


Ingredient 2: Reshape gradients: stop brittle state-input gradients, keep action gradients

As discussed, the fragile pathway is the gradient that flows into the state input of the world model, \(D_s F_{\theta}\). The most straightforward way to do this initially is to just stop state gradients into \(F_{\theta}\) directly:

  • Let $\bar{s}_t$ be the same value as $s_t$, but with gradients stopped.

Define the stop-gradient dynamics loss:

\[\mathcal{L}_{\text{dyn}}^{\text{sg}}(\mathbf{s},\mathbf{a}) = \sum_{t=0}^{T-1} \big\|F_\theta(\bar{s}_t, a_t) - s_{t+1}\big\|_2^2.\]

This alone does not work. Notice now states only follow the previous state’s step, without anything forcing the base states to chase the next ones. As a result, there are trivial minima for just stopping at the origin, then only for the final action trying to get to the goal in one step.

Dense goal shaping

We can view the above issue as the goal’s signal being cut off entirely from previous states. One way to fix this is to simply add a dense goal term throughout prediction:

\[\mathcal{L}_{\text{goal}}^{\text{sg}}(\mathbf{s},\mathbf{a}) = \sum_{t=0}^{T-1} \big\|F_\theta(\bar{s}_t, a_t) - g\big\|_2^2.\]

In normal settings this would over-bias towards the greedy solution of straight chasing the goal, but this is balanced in our setting by the stop-gradient dynamics loss’s bias towards feasible dynamics. The final objective is then as follows:

\[\mathcal{L}(\mathbf{s},\mathbf{a}) = \mathcal{L}_{\text{dyn}}^{\text{sg}}(\mathbf{s},\mathbf{a}) + \gamma \, \mathcal{L}_{\text{goal}}^{\text{sg}}(\mathbf{s},\mathbf{a}).\]

The result is a planning optimization objective that does not have dependence on state gradients.


Periodic “sync”: briefly return to true rollout gradients

The lifted stop-gradient objective is great for fast, guided exploration, but it’s still an approximation of the original serial rollout objective.

So every $K_{\text{sync}}$ iterations, GRASP does a short refinement phase:

  1. Roll out from $s_0$ using current actions $\mathbf{a}$, and take a few small gradient steps on the original serial loss:
\[\mathbf{a} \leftarrow \mathbf{a} - \eta_{\text{sync}}\,\nabla_{\mathbf{a}}\,\|s_T(\mathbf{a})-g\|_2^2.\]

The lifted-state optimization still provides the core of the optimization, while this refinement step adds some assistance to keep states and actions grounded towards real trajectories. This refinement step can of course be replaced with a serial planner of your choice (e.g. CEM); the core idea is to still get some of the benefit of the full-path synchronization of serial planners, while still mostly using the benefits of the lifted-state planning.


How GRASP addresses long-range planning

Collocation-based planners offer a natural fix for long-horizon planning, but this optimization is quite difficult through modern world models due to adversarial robustness issues. GRASP proposes a simple solution for a smoother collocation-based planner, alongside stable stochasticity for exploration. As a result, longer-horizon planning ends up not only succeeding more, but also finding such successes faster:

Push-T planning demo
Push-T demo: longer-horizon planning with GRASP.
Horizon CEM GD LatCo GRASP
H=40 61.4% / 35.3s 51.0% / 18.0s 15.0% / 598.0s 59.0% / 8.5s
H=50 30.2% / 96.2s 37.6% / 76.3s 4.2% / 1114.7s 43.4% / 15.2s
H=60 7.2% / 83.1s 16.4% / 146.5s 2.0% / 231.5s 26.2% / 49.1s
H=70 7.8% / 156.1s 12.0% / 103.1s 0.0% / — 16.0% / 79.9s
H=80 2.8% / 132.2s 6.4% / 161.3s 0.0% / — 10.4% / 58.9s

Push-T results. Success rate (%) / median time to success. Bold = best in row. Note the median success time will bias higher with higher success rate; GRASP manages to be faster despite higher success rate.


What’s next?

There is still plenty of work to be done for modern world model planners. We want to exploit the gradient structure of learned world models, and collocation (lifted-state optimization) is a natural approach for long-horizon planning, but it’s crucial to understand typical gradient structure here: smooth and informative action gradients and brittle state gradients. We view GRASP as an initial iteration for such planners.

Extension to diffusion-based world models (deeper latent timesteps can be viewed as smoothed versions of the world model itself), more sophisticated optimizers and noising strategies, and integrating GRASP into either a closed-loop system or RL policy learning for adaptive long-horizon planning are all natural and interesting next steps.

I do genuinely think it’s an exciting time to be working on world model planners. It’s a funny sweet spot where the background literature (planning and control overall) is incredibly mature and well-developed, but the current setting (pure planning optimization over modern, large-scale world models) is still heavily underexplored. But, once we figure out all the right ideas, world model planners will likely become as commonplace as RL.


For more details, read the full paper or visit the project website.


Citation

@article{psenka2026grasp,
  title={Parallel Stochastic Gradient-Based Planning for World Models},
  author={Michael Psenka and Michael Rabbat and Aditi Krishnapriyan and Yann LeCun and Amir Bar},
  year={2026},
  eprint={2602.00475},
  archivePrefix={arXiv},
  primaryClass={cs.LG},
  url={https://arxiv.org/abs/2602.00475}
}

Reading today's open-closed performance gap

20 April 2026 at 18:25

It’s a clear, current equilibrium that open models will be in perpetual catch-up of closed models, but this gap being viewed as a single number, a “distance”, covers up a nuanced and crucial dynamic at what capabilities the models are covering. The most popular benchmark to comment on this gap is the Artificial Analysis Intelligence Index — a composite benchmark of ~10 sub-evals that they maintain over time to capture the “frontier” of current language model capabilities.

Particularly, I spend a lot of time understanding how dynamics that feed into that index are misunderstood by the natural tendency to reduce performance and trends to one number. Examples include:

  • How benchmarks evolve over time, becoming more or less correlated with how people actually use models,

  • How different models’ real-world performance relates to their benchmark rankings, and

  • How training regimes evolve over time to move said benchmarks.

Agentic benchmarks are in a decent place, but benchmarks are no longer as trusted as a correlate to real-world performance. A key example to this gray area is Gemini 3’s incredible benchmarks and remarkable irrelevance in where AI tools currently are being tested and deployed (agents). These trends point to obvious and lasting flaws in our measurements.

Share

At the root of this dynamic — the dance of correlating model real-world performance and benchmark scores — is the constant shift of the industry. As all the models, i.e. both open and closed, evolve over time, the topics of focus for benchmarking shifts about every 12 to 18 months. All of the domains of interest have very different training domains associated with them, especially in post-training. The longer a single paradigm goes on, the better the industry gets at measuring performance. In a new era of rapid post-training improvements, I’m at a relative minimum in my personal confidence in benchmarks.

Task evolution and LLM paradigms

Right after ChatGPT the focus was a mix of chat, math, and simple code. Instruction tuning and RLHF dominated. Chat capabilities saturated and faded quickly, then mathematics became less focal. Through 2025 and to today, especially once reasoning models became the default, the focus shifted to more complex coding and other simpler agentic tasks. We’re at the tail end of this first era. Recent training recipes are all dominated by reinforcement learning with verifiable rewards (RLVR), but the domains it is applied in have shifted dramatically from basic question-answer checking to complex environments.

What we’re seeing is that the closed, frontier labs are investing astounding sums of money in mastering these current foci — i.e. code, terminal tasks, etc. — while starting to push into more diverse knowledge work tasks. These newer tasks encompass specialized domains, such as accounting, law, healthcare, etc. They are still agentic, but require more expertise and often integrations with existing software or domain-specific tools.

We have very limited evidence on the true balance of capabilities of these newer domains, but these are the areas I’m focusing on when I say open models will struggle to keep up. The problem is that evaluating complex language model workflows is also a challenging research problem in itself.

The tasks are getting harder and the data needed to hillclimb on them is getting more private (relative to code, which has swaths of code on GitHub). Leading open model labs are helped by dynamics happening in the data industry that are economically similar to building chip fabs. The few, leading labs in the U.S. pay astronomical sums to buy new environments and datasets, then the fast-following labs (often in China), buy these later at a steep discount.

This is a key missed point — that the levers non-frontier labs pull to keep up constantly shift over time. A focus on distillation as the key lever to Chinese models’ progress reflects a blind-spot to the importance of RL environments to current training regimes. If an environment can be built either as a single evaluation in the Artificial Analysis Index, or to mirror it, currently the Chinese labs will be able to keep up.

Interconnects AI is a reader-supported publication. Consider becoming a subscriber.

Economic pressure to reinvent “the frontier”

The question worth dwelling on is: How crucial is the current set of tasks (again, coding and terminal tasks), where the likes of OpenAI and Anthropic have a massive business-adoption advantage over leading open weight models (and even Google alike), is crucial to maintaining revenue numbers? In order to maintain these record growth numbers and trajectories, there needs to keep being a meaningful edge in performance. Many companies would love to reduce their token expenditure cost if they can swap in a far cheaper, open model equivalent.

If agentic coding abilities saturate and the “frontier” of AI performance moves elsewhere, a large amount of the enterprise revenue could be reliant on well-formed customer relationships, inertia, and better product development, rather than the models being leaps and bounds better.

This precarious position is what I describe as the frontier labs needing to constantly reinvent themselves, and the field’s prospects, for monetizing the vast buildout of AI infrastructure. I still tend to fall on the side that the buildout will be worth it, and Anthropic and OpenAI will be astronomically profitable businesses, so I take this as a faith of a mix of them continuing to unlock compelling, new, valuable use-cases for the models, and that the benchmarks the open models are closing in on as not being a complete signal.

I operate with a sort of presumption where the leading open models from China are focused slightly more on benchmarks than the leading closed labs in the U.S. They’re incentivized to do so — they want to present the image as constantly being on the heels of the best closed models. Saying the Chinese labs are only in this narrative because they’re overfitting to benchmarks would be incredibly naive and incorrect. They’re genuinely strong models, and these dynamics of overselling and real innovation are a fine balance.

There are a few out-of-distribution benchmarks where open-weight models are very far behind, such as WeirdML or ARC AGI 2, but there are countless random benchmarks that show these open models as being unexpectedly strong. When you use the models, you can pick up on this lack of robustness (e.g. in long-context capabilities, and needing to reset your agent context more often than Claude/Codex), but they’re not a category error in the sense that they’re fundamentally different classes of models. They’re far closer than many would’ve expected.

How long can open models keep up?

Read more

My Workflow for Understanding LLM Architectures

18 April 2026 at 11:24

Many people asked me over the past months to share my workflow for how I come up with the LLM architecture sketches and drawings in my articles, talks, and the LLM-Gallery. So I thought it would be useful to document the process I usually follow.

The short version is that I usually start with the official technical reports, but these days, papers are often less detailed than they used to be, especially for most open-weight models from industry labs.

The good part is that if the weights are shared on the Hugging Face Model Hub and the model is supported in the Python transformers library, we can usually inspect the config file and the reference implementation directly to get more information about the architecture details. And “working” code doesn’t lie.

Figure 1: The basic motivation for this workflow is that papers are often less detailed these days, but a working reference implementation gives us something concrete to inspect.

I should also say that this is mainly a workflow for open-weight models. It doesn’t really apply to models like ChatGPT, Claude, or Gemini, where the weights and details are proprietary.

Also, this is intentionally a fairly manual process. You could automate parts of it. But if the goal is to learn how these architectures work, then doing a few of these by hand is, in my opinion, still one of the best exercises.

Figure 2: At a high level, the workflow goes from config files and code to architecture insights.

Read more

Isabelle/HOL: The proof assistant behind the Nitro Isolation Engine

17 April 2026 at 13:00
At Amazon’s 2025 re:Invent conference, Amazon Web Services (AWS) announced the Nitro Isolation Engine (NIE), a software module tasked with providing resources to AWS clients while ensuring the security of customer data. AWS also announced the formal verification of the isolation engine’s correctness and security guarantees, using a proof assistant called Isabelle/HOL. As the first formally verified cloud hypervisor, NIE sets a new standard for cloud security. A proof assistant is an automated tool that can help human users develop formal proofs — of mathematical theorems, the validity of hardware or software systems, or anything in-between. Several proof assistants are in common use, and we chose Isabelle/HOL because it struck the right balance among expressiveness, automation, proof readability, and scalability. So what do I mean by that? Logical reasoning by computer There is no fixed language of mathematics, but we can create languages for expressing mathematical reasoning, just as programming languages express computational tasks. And just as programming languages involve trade-offs between expressiveness and performance, mathematical languages involve trade-offs between expressiveness and ease of automation. Automation is vital because the construction of a formal proof is both time consuming and extremely tedious, analogous to constructing a ship in a bottle. The most elementary mathematical language is Boolean logic, the world of the binary operators AND, OR, and NOT. Because this language is so simple, powerful automatic solvers exist for it. In 2016, Carnegie Mellon professor Marijn Heule — now an Amazon Scholar — and his colleagues encoded into Boolean logic an unsolved mathematical question, the Boolean Pythagorean Triples Problem, and used automatic solvers to help create the largest proof ever, 200 terabytes long. A richer mathematical language called first-order logic allows us to talk about some domain of interest — the integers, say — and to define functions over that domain. And we can go beyond Boolean logic by including the quantifiers "for all" and "there exists" in assertions. In this sort of language, we can express statements such as "every prime number greater than two is odd". We can also prove the following theorem, due to Lewis Carroll: No ducks waltz; no officers ever decline to waltz; all my poultry are ducks. Hence, none of my poultry are officers. However, most people prefer a still stronger mathematical language, where they can define types, as they do in programming. In higher-order logic, there are even function types, as found in functional programming languages such as Haskell. Higher-order logic is much richer than first-order logic, able to express statements such as Every set containing the number 1 and closed under addition contains all the positive integers. It appears to be rich enough to express most of mathematics. The richest mathematical languages — called dependent-type theories — even allow types to take arbitrary values as parameters, e.g., T(i), where i is an integer. The best-known such languages are Lean and Rocq. Powerful automatic theorem provers exist for first-order logic, but for higher-order logic and beyond, full automation is not available. This is the price of expressiveness. A proof assistant allows users to build proofs interactively, supported by partial automation and the possibility of coding their own proof searches. A proof assistant enforces strict compliance with the laws of logic, typically through a kernel architecture that gives only a limited portion of the code the right to create a theorem. A proof assistant also supports the interactive development of a possibly huge formal-specification hierarchy. For example, verification of the Nitro Isolation Engine (NIE) rests on specifications of the architecture of the Graviton-5 processor, the Rust code of the hypercalls and their functional correctness, and the security properties that are to be proved. These take up much of the quarter of a million lines constituting the formal proof. Higher-order logic is supported by HOL and HOL Light, two closely related proof assistants, and has been used to verify hardware designs, floating-point algorithms, and pure mathematics since the 1990s. AWS senior principal applied scientist John Harrison developed HOL Light, and he has used it to improve the performance of digital signatures on Amazon’s Graviton2 chip by up to 94%, by verifying an optimized version of the cryptographic algorithms. The code was delicate, and exhaustive testing is not feasible; only a formal verification of full functional correctness would do before the deployment of such critical software. But today we are interested in Isabelle/HOL. Overview of Isabelle/HOL The most visible difference between Isabelle/HOL and the other HOL systems — which are all based on higher-order logic — is its specification and proof language. With most proof assistants, users state what they want to prove, followed by lists of commands that replace the original goals with series of subgoals in a kind of whack-a-mole game. In Isabelle and to some extent Lean, the proof language allows desired intermediate goals to be written out explicitly, allowing a better controlled proof process and a more legible proof document. There are plenty of examples online. Other notable features are as follows: a user-configurable parser, which allowed us to embed a significant fragment of the Rust language into our specifications; type classes for principled overloading, so that say + can be given its natural meaning, not just for a variety of numeric types but for machine words and in other appropriate contexts; locales, a lightweight module system allowing a hierarchy of specifications to be defined and interpreted in various ways, even within a proof; powerful built-in automation through simplification and backchaining proof search; sledgehammer: one-click access to even more powerful external automation; counterexample-finding tools, for identifying claims that are actually false; code generation from executable higher-order specifications, which we used to test conformance. For the verification of NIE, we began by implementing a specialized language called separation logic on top of Isabelle/HOL. Separation logic is designed for verifying program code operating on shared resources. We coded our own proof automation and also used what was built in. We therefore could use separation logic but also plain higher-order logic when we wanted to. Isabelle turned out to be resilient enough and efficient enough to cope with the truly gigantic subgoals. It could run that quarter-million-line proof in half an hour using an off-the-shelf laptop. Some applications of Isabelle/HOL The single most impressive application of Isabelle prior to NIE is probably the verification of seL4, a widely used microkernel. This proof was also about a quarter of a million lines when first announced, although it is now much longer. The seL4 developers proved that the microkernel’s C implementation refined the abstract specification, yielding full functional correctness of the core operations. And they have observed no bugs in the verified parts of the code, although testing still plays a role in covering unverified parts and certain assumptions that cannot be formalized. Isabelle was also used in the following projects: to formalize the semantics of the WebAssembly language, to identify errors and, in particular, to prove the soundness of its type system; to create a verification framework for the Cogent programming language; to prove the correctness of algorithms for conflict-free replicated data types, which are used for distributed editing; to formalize numerous results in pure mathematics; to verify cryptographic protocols at an abstract level. Isabelle is free, open source, and available to download. It runs on all the main operating systems on any machine that has enough memory.

My bets on open models, mid-2026

15 April 2026 at 18:20

We’re living through the period of time when we’ll learn if open models can keep up with closed labs. The obvious answer is that no, they won’t. This answer is a form of saying they won’t keep up in every area. This framing closes off a popular prediction where the open models completely catch up, as in all models saturate and open and closed models only become increasingly similar. In living through this, it’s evidently very unclear when the longer-term stable balance of capabilities will solidify.

This is a very complex dynamic, where the core point we monitor is a capability gap between models. At the same time, this gap is intertwined with evolving dynamics in the funding of open models, who builds open models, how techniques like distillation that enable fast-following translate through new application domains, potential regulation hampering the open-source AI ecosystem, and of course who actually uses open models.

The capabilities gap is one signal in a complex sea of forces, pushing supply and demand into different shapes. In many cases the demand — where obviously tons of individuals, organizations, and sovereigns want, or need, open models — is largely separated from supply. Supply is fully dictated by economics. The question of “which business strategies support releasing open models” is still at stake.

Interconnects AI is a reader-supported publication. To receive new posts and support my work, consider becoming a subscriber.

With this complexity, I wanted to distill my key beliefs down into a clear list. These are downstream of 10+ pieces I’ve written or recorded on open models this spring (which are linked throughout).

  1. It’s surprising that the top closed models did not show a growing capability margin over open models, based on compute differences for training and research, especially in the second half of 2025 and through today.

  2. Open model labs are technically very strong at keeping pace on well-established benchmarks. This will continue and reflects a balance of abundant talent and sufficient computing power.

  3. Chinese open-weight labs focus slightly more on benchmark scores than comparable closed labs in the U.S. Distillation helps the Chinese LLM companies do so, but it’s not a panacea. Changes in the distillation dynamic (e.g. regulation) will not be a determining factor on the balance of capabilities. This increase in focus is a natural evolution of their incentives in keeping the narrative on keeping up with the frontier alive, which is crucial to fundraising and adoption.

  4. To date, closed models tend to be more robust and generally useful than similarly scoring open models. Closed models have certain hard-to-measure qualities that are not well captured in current or past benchmarks. This will be key to enabling closed models to dominate in markets where an individual user constantly presents new challenges, i.e. supporting knowledge workers as a direct assistant.

  5. The open vs. closed model race, as monitored through benchmarks, will largely be a game of economic staying power and fast-following, until the market structure constricts. I expect Chinese open-weight labs to face funding difficulties first, as soon as later this year. Funding difficulties will be seen in different capability trajectories 3-9 months later.

  6. The RL dominated training era has increased the relevance of distribution to real-world use-cases as a key factor in continued capabilities improvements. These are tasks where users directly use tools like Claude Code or Codex to solve problems in their job with agents. This is the first clear technical area that closed labs can dominate open-weight models on capabilities, potentially leveraging online RL directly based on user feedback.

  7. Open models will be increasingly adopted in repetitive automation tasks, as measured in the relative share of the API market, for repetitive tasks across the ecosystem. This takes the form of many new AI-native applications, business backend automation, etc. The success of this will drive more investment in domain-specific, efficient open models.

This is a complex picture, where the long-term trajectory is more of an economics question rather than an ability one. Many other outlets can paint a far more simplistic narrative that “China will assuredly catch us in AI” and get more distribution because it is a simple story. The reality is complex. Only real AI revenue begets more investment, eventually that’ll be linked to the ability to keep improving models at a rapid rate. Economic realities have not yet impacted scaling open models, as a general category.

Share

This economic-focused angle relates to my positions on the open model ecosystem more broadly.

  1. Recurring calls to ban certain types of open models will continue to come but are in practice impossible to implement. Training strong AI models (i.e. near but not at the frontier) is a relatively small cost compared to large-scale deployments. E.g. if the U.S. bans open models over a certain compute threshold, another sovereign entity will eventually train them and release them publicly, with the models entering the U.S. market with less oversight.

  2. The second derivative of influence on open models has shifted, and the U.S. will slowly regain ground in adoption metrics of open models starting in early 2027 (it takes a long time for China’s velocity to slow, then flip). Examples include Google’s Gemma 4 (a wild success), Nvidia’s Nemotron, and Arcee AI.

  3. As ever-stronger closed models are built, previewed, and released, there will be more safety-shocks saying that open-weight versions of the strongest AI models never can be allowed to exist, similar to reactions to Claude Mythos. These can spur burdensome regulation on open models.

  4. With the above, there will also be increased long-term interest in open models, as sovereign entities and existing power structures realize the coming, super powerful AI tools cannot land in the hands of only one or a few companies. These entities will see open models as a different governance paradigm.

  5. New funding structures for open models will emerge, as many stakeholders realize dependencies on single, for-profit companies for access to intelligence are unreliable.

  6. Local agents, OpenClaw, and other personal agents represent a large, to date, mostly ignored market for open model usage. It is a sort of dark matter, with pervasive, massive potential for influence on the balance of open-to-closed models.

A single word governs this post and is intentionally repeated — complex.

This complex reality has been driving me to think more deeply about how to clearly describe the open model gap, and why I can hold it in my head that I expect American closed labs to clearly draw ahead, despite the fairly unequivocal evidence in support of the capabilities of recent open-weight models. More on the nuance in the open-closed gap in another piece coming soon, so please subscribe!

Let me know any positions that I missed.

Customized Amazon Nova models improve molecular-property prediction in drug discovery

15 April 2026 at 16:10
In recent years, large language models (LLMs) have become indispensable assistants for software engineers and knowledge workers. Nimbus Therapeutics enlisted us at Amazon’s Generative AI Innovation Center and Artificial General Intelligence (AGI) organization to investigate whether it’s possible to make equally capable assistants for medicinal chemists discovering new drugs. Such an agent could significantly speed up drug discovery, potentially saving lives. AI in drug discovery has traditionally involved models called graph neural networks, or GNNs. GNNs are the workhorses of molecular-property prediction across pharmaceutical R&D, and for good reason: they deliver strong accuracy on well-defined tasks. Typically, multiple GNNs, specialized for different molecular properties, have to be built and maintained in-house — an expensive, operationally complex process. In recent years, the success of LLMs in a variety of research domains has caught the eye of biotech firms, but for drug discovery, general, off-the-shelf LLMs have proven to be less accurate than GNNs or other computational methods. We have adopted a new approach that combines the accuracy of GNNs with the generalizability and reasoning ability of LLMs. Using supervised fine tuning (SFT) and reinforcement fine tuning (RFT) to customize a general-purpose LLM, we were able to achieve results comparable to those of using multiple GNNs, at a fraction of the time and labor. Fine-tuned LLMs offer a significantly simplified workflow. In the traditional setting, each GNN has a separate interface, with its own quirks, data formats, and failure modes. Results come back as disconnected numbers that the chemist must manually integrate. When a new property needs to be predicted, someone must construct a multitask dataset and train and validate an entirely new model, a process that can take weeks. In contrast, a single, fine-tuned LLM allows a chemist to submit one query and receive predictions on all molecular properties of interest. Adding a new property requires incremental fine tuning rather than building a new model from scratch. Moreover, a language model opens the door to a qualitatively different capability: conversation. With a fine-tuned LLM, it’s now possible to ask for the reasoning behind the model outputs or to suggest molecular modifications that might yield the desired properties. This points toward an assistant that unifies molecular-property prediction and generation in one interactive experience, which we see as the ideal next step for AI-assisted drug design. Customized LLMs unlock domain-specific scientific assistants, giving lean biotech teams a practical way to collaborate with AI systems that speak their scientific language. Today, bringing a single drug to market takes 10 to 15 years and costs on average over $2 billion, with only about 8 percent of drug candidates that enter clinical trials receiving FDA approval. We believe that AI assistants could particularly improve productivity in the early stages of this pipeline, where chemists design molecules with druglike properties. Increasing the speed of development and the number of viable candidates would maximize the chances of delivering a safe and efficacious drug to the clinic. What we looked at Our work with Nimbus Therapeutics focused on properties spanning three categories critical to drug development: Lipophilicity (which has one associated property) determines whether a molecule can cross biological membranes. It is fundamental to drug absorption and distribution and affects all other characteristics of a drug. Permeability (four associated properties) measures how easily a drug enters the body via the bloodstream. Clearance (six properties) determines how quickly the body eliminates a drug. A drug that takes too long to be cleared could become toxic; one that is cleared too quickly won’t be effective. These properties span different value ranges and exhibit complex interdependencies — in practice requiring separate multitask GNN models . We tested the general-purpose LLMs Claude Sonnet 4 and Nova 2 Lite on the task of predicting all three sets of properties for particular molecules. Despite their impressive capabilities elsewhere, the models significantly underperformed specialized GNNs, with an accuracy gap that ranged from 40% to over 200% error, as measured by the root mean squared error (RMSE), depending on the property. However, we discovered that Nova 2 Lite with supervised fine tuning (SFT), followed by reinforcement fine tuning (RFT), could close that gap. Our single, fine-tuned LLM predicted 11 different molecular properties with accuracy similar to that of multiple separately trained multitask GNN models. How we did it Our approach to fine-tuning the LLM follows a principle common to both human-expertise development and machine learning: foundational knowledge must precede performance optimization. During SFT, the model learned core concepts such as molecular structure and property relationships. Then, during RFT, training shifted to the development of predictive judgment through practice and feedback. During SFT, we exposed Nova 2 Lite to more than 55,000 molecules labeled with experimental measurements across 11 properties. SFT was essential because the domain-specific tasks we asked the model to perform fall far outside Nova 2 Lite’s generalized pretraining data. For example, we use a notation called SMILES (simplified molecular-input line entry system) to represent chemical structures. Without SFT, the LLM wouldn’t have been able to perform a task like “predict chemical property from SMILES strings in structured JSON format”. The second training stage, reinforcement fine tuning (RFT), is especially critical for properties with limited experimental data, where SFT alone struggles to generalize. RFT also enables the intramodel transfer of learning across properties. For instance, lipophilicity affects permeability, and both can inform metabolism predictions. Further, RFT shifts the learning objective from pattern matching ("given molecule X, output value Y based on similar examples") to quality optimization ("minimize prediction error across all properties"). We tested the SFT and RFT models on 15,000 molecules unseen during training. We also built a system prompt that encompassed a knowledge of both core chemistry and our 11 chemical properties of interest, including their definitions and expected value ranges. During the RFT stage, we experimented with three strategies for generated rewards, which guided the learning process. Molecular-property prediction is particularly amenable to reward engineering for RFT since the output is a single number, which allows us to measure exactly how far off each prediction is. Our first strategy was to use an exponential decay function, so predictions closer to the true value received exponentially higher rewards. But at high error, improving from “terrible” to merely “bad” yielded almost no reward difference, keeping the model from learning from its worst predictions, while at low error, small changes resulted in large reward differences, which made the reward signal noisy and ultimately unhelpful. Our second strategy, binary pass/fail rewards, created the opposite problem. The model received zero reinforcement for gradual improvement: it either crossed an arbitrary threshold (in our case, correct within 10 percent) or learned nothing. Rewards based on the Huber loss — a metric proposed in 1964 by the Swiss statistician Peter Huber, which limits the influence of outliers — solved both issues. Unlike exponential decay, Huber rewards don't become negligible on large errors — the model always receives a meaningful signal to improve — yet they remain stable near the correct answer, refining predictions without overreacting to small fluctuations. This yielded our best result, a 4.9% R² improvement over baseline, and we used the Huber reward as the default for training the model on multiple molecular properties simultaneously. Carrying this forward into multiproperty training, we fine-tuned a single model to predict all 11 properties simultaneously. Our best-performing model was Nova 2 Lite with RFT on top of full-rank SFT, meaning that all the model parameters were updated. It outperforms Claude Sonnet 4 by 39% and base Nova 2 Lite by 37% on average RMSE. While averaging 5% behind the baseline GNN, it matches or outperforms the GNN on 7 of 11 properties — a striking result given that a single LLM is going toe-to-toe with multiple independently trained multitask GNN models, reducing not just model count but the entire infrastructure footprint around training, deployment, and maintenance. It’s important to note that Nova Forge — a service that allows Amazon Web Services customers to use proprietary data during both pretraining and SFT — supports both SFT and RFT on SageMaker, enabling extensive model customization. Since SageMaker handles the training framework and infrastructure maintenance internally, organizations avoid the cost of building and maintaining custom training pipelines from scratch. What’s next? Based on these initial experiments and results, Nimbus Therapeutics recently deployed its Novus model on Amazon Bedrock. Novus is the company’s custom-built LLM, created through Nova Forge. In its current form, Novus handles molecular-property prediction with an accuracy that is competitive with purpose-built GNNs. The next milestone is extending those capabilities toward molecular design, enabling the model to propose structural modifications, predict their downstream properties, and explain its reasoning, all in a single conversation. Acknowledgements Leela Dodda (Nimbus), Aarush Garg (Nimbus), Matthew Medina (Nimbus), Md Tamzeed Islam , Elyse Zhang, Clement Perrot, Rohit Thekkanal, Shiv Vitaladevuni

Partnering with Auctor

By: sbarry
15 April 2026 at 16:00

Partnering with Auctor: AI Autopilot for Software Implementation

Matt, Will and Sky.

For every dollar spent on software, six are spent on services. Why? Because buying enterprise software is easy. Implementing it is hard, and still leans heavily on labour. Across the top 10 software ecosystems (ServiceNow, Salesforce, SAP, AWS, and others), 9 million implementation consultants represent more than $500 billion in annual labour spend, still growing 10%+ a year. It’s one of the largest markets in technology, and one of the least disrupted.

Enterprise platforms have thousands of components that change daily. A single deployment can span hundreds of requirements, dozens of stakeholders, and months of back-and-forth between what a business needs and what the system can actually do. Today, consultants hold all of this together through experience and pattern recognition. But they forget context between meetings. They miss dependencies across systems. They can’t track thousands of platform updates simultaneously. Unlike LLMs, their context windows are limited by biology. 

Auctor is the autopilot for software implementation, from the moment a customer requirement is captured all the way through to delivery. It brings together the requirements, decisions, and context that typically live across meetings, documents, and dozens of disconnected systems, and translates them directly into the outputs needed to move a project forward. What used to take teams weeks of scoping now gets done in a single sitting.

We first partnered with Auctor at the Seed, shortly after the team graduated from YC. At Sequoia, each year we select a handful of portfolio companies and take their founders to meet executives at some of the most important technology companies in Silicon Valley. For an hour, these leaders effectively join the team, helping us and the founders think through strategy, positioning, and go-to-market. In our very first meeting with the C-suite of a major enterprise platform, the executives asked for a pilot halfway through the conversation, before we’d even demoed the product. 

What gave us conviction beyond the market was the team. This is a category where speed of execution determines the winner given the first mover advantage. Will, Sky, and Matt are the hardest-charging, fastest-moving team we’ve met in this space. They shipped their platform and landed their first major enterprise contract within months of graduating YC. They’ve set up shop in New York and are pulling in talent the way only a team with this much momentum can.

We’re leading Auctor’s Series A and couldn’t be more excited to partner with Will and the team to bring software implementation into the age of AI.

Share

Share this via email
JOIN OUR MAILING LIST

Get the best stories from the Sequoia community.

The post Partnering with Auctor appeared first on Sequoia Capital.

❌