Machine learning, at its core, is about generalization, not memorization. You hand your learning algorithm a pile of training examples and use them to fit a model. But the goal is not to perform well on the training examples — that's easy, you could just memorize the answers. The goal is to perform well on new examples that you have never before seen. If a model does well on the data it was trained on but poorly on fresh data, it hasn’t actually learned anything; you have only fooled yourself into thinking it has. This failure mode has a name: overfitting. Anyone who has taken an introductory statistics or machine learning class knows the standard defense. You hold out some of your data and refuse to train on it. In practice, this held-out data plays two roles. A validation set is one you consult repeatedly while building the model — to compare candidates, tune hyperparameters, and decide what to try next. A final test set (or holdout) is meant to be touched only once, at the very end: because the training procedure never saw it, strong performance there is a correct proxy for the new examples you will encounter in the wild. The “holdout” condition is crucial, though. The correct-proxy guarantee holds if the held-out set stays genuinely unseen. If you check your performance on it, tweak your training procedure in response, recheck, and iterate, chasing better and better numbers, that set is no longer unseen; it has become part of your training procedure. Do this enough times, and you can overfit it just as you might have overfit the training set, and you have lost your proxy for unseen data. This is true of any held-out set you reuse this way, including a validation set, which is reused by design. A puzzle at the heart of machine learning Real machine learning research looks exactly like the iterative improvement loop we just described. Everyone gauges performance using a handful of benchmark datasets that go unrevised for years. The research community repeats an enormous, distributed loop: evaluate a model on the benchmark, revise the training procedure, re-evaluate, publish, and let the next group eke out a little more improvement. This is precisely the kind of hill-climbing against a held-out set that, by the textbook account, ought to produce rampant overfitting. By now, the leaderboards should be saturated with models that look great on the benchmark and mediocre everywhere else. And yet that is not what happens. Studies that build entirely fresh test sets for old, heavily reused benchmarks have found that improvements largely transfer: on the new data, models demonstrate the same gains they did on the old benchmark. Benchmark-driven machine learning, against the textbook's prediction, has produced rapid and largely real progress. Why? There is no shortage of hypotheses, but they have been hard to test empirically, because the "subject" of the experiment is the entire human research community. You cannot reset a field, wipe its memory, and rerun the last decade under controlled conditions. But we can do something similar. We now have capable, LLM-based research agents that can autonomously run the same machine-learning optimization loops that human communities run. They engage in the same benchmark hill-climbing — and, intriguingly, they too seem not to overfit. The difference is that an agent, unlike a research community, is something you can reset. You can clear its memory, control exactly what information it sees, and run the experiment again. In a recent paper, "What fits (into few tokens) doesn't overfit: Compression and generalization in ML research agents", we do exactly that — and in the process offer a concrete explanation for the long-standing mystery. Occam's razor, made precise The explanation begins with a very old idea. Occam's razor says that among hypotheses that explain the data equally well, the simpler one is more likely to be correct. It turns out this intuition has a precise mathematical form, and it is what underlies the whole story. Suppose you can describe your hypothesis — your model, your strategy — in a small number of bits, far fewer than it would take to memorize the training data. If that compact hypothesis performs very well on the training data, it must also perform well on new data. The reasoning runs through a counting argument. There simply are not very many short descriptions, because there are not very many short strings. The fewer candidate hypotheses there are, the less likely it is that any one of them fooled you on the training set by luck — even though you used the training set to guide your search. Another way to get the intuition: if your compressed description is too small to secretly record the training data, then when it performs well on the training data, it cannot be because it memorized the answers — it didn't have space to do that. It must be because it captured something true about the data's structure. Short descriptions cannot cheat because there isn't room. Here is an attractive hypothesis: successful machine learning strategies are highly compressible. A researcher might stare at thousands of benchmark scores over the course of a project, but the strategy that ultimately survives is usually a short list of familiar choices — an architecture family, an optimizer, a learning-rate schedule, a data-handling recipe, a regularization scheme. If that final recipe can be communicated in just a few bits, then the model's true dependence on the benchmark is far smaller than the long, winding transcript of experiments would suggest. The hill-climbing was extensive, but the thing that came out the other end was — or could have been — tiny. Compression, intelligence, and the power of a knowledgeable listener Imagine trying to explain a specific machine learning pipeline to a bright high-school student, in enough detail that they could actually reproduce it. It would be a long, laborious conversation. You would have to explain what gradient descent is, what a neural network is, what PyTorch or JAX or TensorFlow does, what a learning rate is, and on and on. Almost none of that is specific to your problem; it is general background about how machine learning works. Now imagine explaining the same pipeline to an expert ML engineer. The conversation now collapses to a few sentences. You skip everything that counts as common knowledge and communicate only what is genuinely specific to this problem: the architecture choice, the batch size, the optimizer, a couple of hyperparameters. The more your listener already knows about the world, the shorter the message you need to send — and the more aggressively you can compress. None of this "world knowledge" counts against you in the Occam's-razor argument, because you could have written all of that down without having looked at the training set. This is where large language models enter the picture. Modern LLMs carry an enormous amount of world knowledge. They know how ML tooling works; they know the standard optimization algorithms; they know the conventional hyperparameter choices and the common defaults. If a detail is left unspecified, they can fill in a plausible value. That makes them extraordinarily good compression decoders: hand an LLM a terse, expert-to-expert message, and it can unpack it into a full, working procedure. If you think about it, this is exactly why they are so powerful. The experiment: Squeezing a strategy through a bottleneck This suggests a clean experiment. Have an ML research agent — the explorer — try to solve a new machine learning problem. Give it full access to a validation set and let it experiment and iterate freely, chasing better validation performance over hundreds of rounds. Here the validation set plays the role of the benchmark: a reusable holdout the agent queries again and again. This is the hill-climbing loop that ought to overfit. Then test how compressible the solution is. A second agent, the compressor, reads the entire transcript of the explorer's work and tries to distill the winning strategy into a very short prompt — just a handful of tokens. That prompt is handed to a third agent, the reproducer, which must implement the strategy from scratch using only the prompt and the training data. Critically, the reproducer has no access to the validation set, the explorer's code, or its transcript. The short prompt is the only channel through which anything learned from the validation set can reach it. (In the study we report in our paper, the compressor and reproducer are both Claude models.) If the reproducer — starting cold, armed only with a few tokens — matches the explorer's performance, then all the validation-dependent information needed to specify the strategy fit through that tiny channel. The strategy was compressible. We call this a certificate of output compression. The setup has a very useful property that human research communities lack: the reproducer can be reset over and over. The compressor can try many different compressions and see how well each is decoded, because every attempt lands on a fresh reproducer with no memory of the last one. It is a little like the film Memento — you are leaving a terse note for a version of yourself whose memory will be wiped before reading it. You learn to write notes that a knowledgeable but amnesiac copy of you can act on; those notes can be very short because the receiver will fill in anything you leave unsaid exactly as you would have. What comes out the other end The compressions turn out to be remarkably small. Across eight datasets — spanning tabular classification, image classification, language modeling, diffusion modeling, and reward modeling — 32-token prompts were enough for a fresh reproducer to match the explorer's adaptively optimized models on the large majority of problems. One language-modeling strategy survived compression down to just 16 tokens with no loss in held-out performance. What do these prompts actually look like? The most revealing examples are right at the border of conciseness where the compression almost breaks. In one language-modeling experiment, the explorer discovered a custom GPT-style training recipe. Under a 16-token budget, this was still enough for fresh reproducers to match the uncompressed explorer: QKn 12L768 Mu .1 R² b2M 4x To a human reader this looks cryptic, but to another ML agent it says something concrete: QKn means “QK normalization”, 12L768 means a 12-layer, 768-dimensional transformer, Mu .1 means the Muon optimizer with learning rate 0.1, R² means squared-ReLU activations, b2M means a two-million-token batch, and 4x means a fourfold feed-forward block. Cut the budget to eight tokens, however, and the prompt becomes 12L768 Mu .1 R² Now the reproducer no longer matches the explorer. The missing pieces specified real training choices that were made as a function of the data and differ from the most obvious defaults. This boundary shows the limits of compressibility and is important. It shows that the reproducer is not succeeding from prior knowledge alone. A few compressed tokens are carrying genuine information learned from the data itself, and when those tokens disappear, so does the performance. We also ran a set of experiments that imposed an information bottleneck from the other direction. Instead of compressing the explorer's output, we compressed its input: rather than telling the explorer each model's numerical validation score, we returned only a single bit — did this model beat the running best, or not? Even reduced to one bit of feedback per query, the explorer found strategies as good as those it found with full numerical scores. The channel between the validation set and the final strategy is narrow in both directions, and the one-bit version even comes with a rigorous mathematical guarantee on generalization. Catching cheaters A good empirical theory should be falsifiable — and this one is. If low overfitting is really explained by compressibility, then models that genuinely overfit should fail to be compressible via this pipeline. To check, we deliberately pushed agents into overfitting by handing them direct validation-set access and prompting them to maximize validation performance at any cost. The agents took the bait: in 38 of 102 experimental runs, validation accuracy ran more than 10% ahead of true held-out accuracy. The theory predicts that these gains should not survive the compression bottleneck, because they encode idiosyncrasies of specific validation examples, not transferable structure. Sure enough, when squeezed through a short prompt to a fresh reproducer, the validation-specific advantages vanished. Compression separated the legitimate strategies from the overfitting ones with very high accuracy. So compression does not merely explain why autonomous research agents tend not to overfit but offers a tool for catching overfitting when it does occur, by flagging the cases where no short description can reproduce the result. What this tells us — and what it doesn't A few caveats are in order. The whole framework assumes that the only path from the validation data to the final model runs through the prompt we feed the reproducer. Of course, if a model had memorized the validation data during pretraining, it would have a side channel that bypasses the information bottleneck we are trying to impose. We don't think that is what is happening in our experiments: agents improve gradually through real search rather than starting at their best, and performance degrades at very short token budgets. But fully resolving this question will likely require experimenting with fresh datasets collected after a model's training cutoff, which we haven’t done. Most importantly, our results are about LLM agents, because that is where the experiment is possible — where you can reset the subject, control its inputs, and count their length. But the picture they paint is strongly suggestive about human research communities too. When a field spends years climbing a fixed benchmark, and the gains keep transferring to fresh data, it may be for the same reason the agents' strategies survive a 32-token prompt: the recipes that actually work are simple. Or in other words, "What fits (into few tokens) doesn't overfit." Acknowledgments: Steven Wu

Many open-source and industry software projects, including several here at Amazon, are embracing the Rust programming language, since it provides performance and flexibility similar to that of the C programming language, while its clever type system automatically prevents a variety of bugs and security vulnerabilities. The result is fast code that's more correct and secure than average. However, "more correct and secure" is not the same as "actually correct and secure". For example, in C, accessing an array out of bounds — indexing into an array past the boundary of the memory allotted to it — is a dangerous mistake that can have unforeseeable consequences. In Rust, it will halt the program, which is definitely safer, but a correct program would never perform the out-of-bounds access in the first place. Similarly, Rust cannot guarantee that your program will compute the results you were expecting or that it won't leak the secrets it has access to. That's where Verus comes in. What is Verus? Verus is an open-source, automated program verifier for Rust. A "program verifier" takes in a formal mathematical specification of how your code should behave and mechanically checks that your code matches that specification for all possible inputs. For example, your code might implement an optimized binary-search algorithm to look for a particular value within a sorted array. The specification might state that when the code successfully returns an index, the corresponding element in the array matches the target value. The verifier checks that this specification holds for all possible input arrays and target values. In contrast, traditional testing techniques might try a few specific arrays but can miss corner cases (e.g., what if the target value is the last element in the array or not present at all?). A key aspect of program verification involves constructing a mathematical proof that the code matches its specification. In an automated program verifier like Verus, the tool automatically handles many of the boring, low-level steps of proof construction, while the human developer provides high-level guidance (e.g., setting up an inductive proof or supplying a loop invariant). As we discuss below, these days, even the high-level steps can often be automated by AI. At Amazon, we're proud to have been a founding member of the Rust Foundation, and we use Rust extensively for projects like Firecracker, which powers AWS Lambda and AWS Fargate, our serverless distributed SQL database, and the Nitro Isolation Engine, which enforces virtual-machine isolation for the Nitro hypervisor, the software that manages virtual-machine allocation for Amazon Web Services (AWS). Amazon's excitement about Rust, combined with more than a decade of work on automated reasoning, makes it natural to adopt Verus to provide even stronger guarantees for the Rust code we're writing. Indeed, we've used Verus to prove the correctness of key primitives used by the Nitro Isolation Engine, as well as a number of critical pieces of infrastructure used within Amazon. We'll explore these use cases in future posts, but for now, we want to tell you more about what it means to verify Rust code with Verus. Verifying Rust code with Verus With Verus, a Rust developer can add specifications (and proofs) for existing Rust code directly in the Rust source files. To extend the binary-search example, consider the following Verus specification (written as a Rust annotation) of the search function's existing Rust implementation: The precondition (indicated by the “requires” keyword) states the conditions that must be true before the function executes. In this case, since the code implements a binary search, we require that the array is sorted. The postcondition (indicated by the “ensures” keyword) states the conditions that must be true after the function executes. In this case, it says that if the function returns “Some(index)”, then “index” is within the bounds of the array, and the value at that index matches the value we were looking for. Importantly, it also tells us that if the function returns “None”, then the target value is not in the array. Without this second clause, the specification could be satisfied by an implementation that always returned “None”! Note that normal Rust compilers ignore these Verus annotations, so Verus-annotated code can be consumed by both verified and unverified projects, including those that use Rust's build tool, Cargo. This example also illustrates a key design decision that Verus makes, one that distinguishes it from many other Rust verification approaches. With Verus, developers write specifications and proofs in their source code, using Rust-like syntax. When a proof fails, they see Rust-style error messages expressed at the source level. This approach keeps the proofs in sync with the actual code and saves developers from needing to learn a brand-new language and tool for specifications and proofs. It also enables the developers who write the code (and hence know it best) to be involved in the process of proving it correct. Verus also focuses on providing fast, powerful automation. To do so, it uses a variety of solvers to discharge the proof obligations generated from the programs and their specifications. In practice, this means that developers typically get feedback on their code and proofs in under a second, fast enough to provide an interactive development loop (including "red squiggles" inside interactive development environments like VS Code). At the project level, Verus can verify complex projects with thousands of lines of code and proof in the time it took some prior automated program verifiers to verify individual functions. This powerful automation and quick feedback loop obviously help humans, but they also help AI agents develop Verus proofs, since the automation means the agent has less work to do and can iterate faster on its proofs. Rust's type system provides strong safety guarantees, but sometimes it prevents developers from writing high-performance code. Hence, Rust also allows developers to write explicitly labeled "unsafe" code. This code must still uphold all of Rust's expectations for safe code, but the compiler no longer mechanically checks those expectations; it's up to the developer to get it right. With Verus, however, developers can mathematically prove the safety of their unsafe Rust code, re-establishing machine-checked safety guarantees. Similarly, Rust famously offers "fearless concurrency", meaning that the type system will prevent various mistakes that other programming languages allow when developers write concurrent code — i.e., programs that execute in parallel at least part of the time. Verus builds on this foundation to enable developers to prove that their concurrent code is not just safe but correct. For example, concurrent execution generally involves locks, which grant a processor thread exclusive access to data items it’s currently manipulating. Verus allows developers to add an invariant property to a lock, meaning that anyone who acquires the lock obtains a value that satisfies the invariant's property (e.g., the value is always even), and when they release the lock, they must prove that the value behind the lock still satisfies that property. Moreover, Verus supports proofs that the lock implementation itself is correct. This is particularly important for programs like the Nitro Isolation Engine, which rely on complex, custom locking schemes to achieve high performance. Like all program verifiers, Verus's guarantees rely on the correctness of Verus itself, the "top-level" specifications of the program's intended behavior, the "bottom-level" assumptions made about the underlying run-time (e.g., the Rust standard library), and the compiler toolchain that converts source code into executable programs. In future posts, we'll go into more detail on the ways we increase our confidence in these components. Verus in the open-source ecosystem In addition to its use at Amazon, Verus has been used to prove interesting properties for a variety of open-source projects. Here are some examples: Vest takes in a description of a binary data format and automatically generates Rust code to parse and serialize data in that format, including Verus proofs of correctness and security. Verdict provides a provably correct and secure certificate validation library for the x.509 public-key cryptography standard, one that supports user-supplied validation policies. The CapybaraKV project verifies the correctness and crash safety of persistent-memory logs, which preserve data in a well-formed state even if the system crashes or loses power unexpectedly. The Atmosphere microkernel is a microkernel (minimal operating system) developed in Rust and verified for correctness with Verus. Anvil proves the correctness and “liveness” of controllers for Kubernetes, an open-source system for managing cloud computing. Anvil shows that under reasonable assumptions, the controllers will eventually bring the system into a stable state. The CortenMM memory management system includes a novel transactional interface with scalable locking protocols, and the correctness of its concurrent code is verified with Verus. Verus itself is a free, open-source project developed by a distributed collaboration of academic and industrial researchers.

Imagine evaluating a retrieval-augmented-generation system. A user asks a question, the system retrieves a text passage, and an LLM judge decides whether it’s relevant. To reduce noise, you ask several judge models to evaluate the same passage. Eight say “relevant”; two say “not relevant”. Eight out of 10 feels convincing. But the important question is not only how many judges agreed but how independently they arrived at that agreement. If the eight agreeing judges are genuinely different sources of evidence, then agreement is a strong signal. But if they share a prompt template, a training lineage, a model family, or a common blind spot, they may be repeating the same mistake. The vote count makes the evidence look stronger than it really is. Our paper “Dependence-aware label aggregation for LLM-as-a-judge via Ising models,” coauthored with Shiva Kasiviswanathan and presented at this year’s International Conference on Machine Learning (ICML), addresses this problem. We present a method for assessing the correlations between judges’ outputs and adjusting the aggregate score accordingly, to ensure a diversity of opinion. In tests on three different tasks, our method outperformed the best-performing baseline — a panel of judges weighted according to historical accuracy — by 9% to 14% on standard metrics. Hidden assumptions The attraction of majority vote is its simplicity. Every judge gets one vote, and the answer with more votes wins. Weighted majority vote is a natural improvement: judges that appear more accurate get more influence. Both approaches are useful baselines. But they are built around the same simplified view of the judge panel: judges that get the wrong answer are treated as though they make their errors independently. That assumption is often too optimistic for LLM-as-a-judge systems. Two judges may fail together because they interpret the rubric similarly. Several judges may be prompted with the same examples and therefore inherit the same evaluation bias. A group of related models may be sensitive to the same phrasing. In these cases, a majority can be less informative than it appears. A judge panel is a network A better aggregator would treat the panel as a network of judges. Each judge still has its own reliability profile, but pairs of judges can also have relationships. Some pairs agree more often than their individual reliability profiles would predict, including on shared mistakes. Other pairs provide more complementary perspectives. We model these relationships with an Ising model, a statistical model that can represent pairwise dependence between binary variables. In the LLM-as-a-judge context, the aggregator learns both judge skill and judge similarity. Our method is designed for the unsupervised setting: it learns from judge outputs without using human reference labels for training. It treats each item's true label as a latent variable to infer jointly with the parameters describing judge reliability and dependence. There are two useful levels of dependence modeling. In the first, the relationship pattern among judges is treated as roughly the same for positive and negative labels. The final decision still looks like a weighted vote, but the weights are adjusted for correlation. Redundant agreement can be discounted without making the prediction rule hard to interpret. The second variant — the class-dependent model — lets the relationship pattern change with the label. This is useful when the agreement structure carries class information — for example, when judges show broad agreement on clear-cut items but split into recognizable clusters on ambiguous ones. This approach is more expressive, but it requires more data to estimate the extra parameters reliably. Learning from evaluation logs Starting from an initial parameter setting, the algorithm combines each item's votes to estimate the probability that its true label is positive. These soft probabilities are the model's current best guesses, not external labels. It then alternates between updating those probabilities and re-estimating judge reliability and pairwise dependence from them. Reference labels are used only afterward to measure experimental accuracy. This approach is especially relevant for teams that already collect LLM-as-a-judge outputs at scale. Existing evaluation logs contain more than just votes; they contain patterns of agreement and disagreement. Dependence-aware aggregation turns those patterns into a usable signal. The same learned network can help answer practical questions. Are similar models adding independent evidence, or are they mostly reinforcing each other? Does one task produce broad agreement, while another produces cluster-specific splits? Is adding another judge likely to improve the evaluation or simply duplicate an existing source of bias? Evaluation We evaluated our approach on three binary tasks: relevance classification for retrieved information, toxicity classification, and summarization assessment. The judge panel contained 10 judge models, all run at temperature zero — meaning there’s no randomness in their outputs, so the same input will always elicit the same output. We compared the dependence-aware models with two conditional-independence baselines: weighted majority vote and uniform majority vote. Across the three tasks, modeling dependence improved accuracy once the system had enough evaluation items and enough judges to estimate meaningful relationships. Using all 10 judge models and the maximum available training data for each task, the strongest dependence-aware results were 0.912 accuracy on relevance, compared with 0.820 for weighted majority vote and 0.804 for uniform majority vote; 0.792 on toxicity, compared with 0.694 and 0.695; and 0.806 on summarization, compared with 0.737 and 0.561. Best practices For teams using LLM-as-a-judge pipelines, dependence-aware aggregation suggests a few useful habits. First, evaluate the judge panel, not just the individual judges. A set of individually strong judges can still be redundant if they fail in the same way. Second, treat model diversity as statistical diversity. Mixing model families or architectures is helpful only to the extent that it changes the error patterns that matter for the task. Third, inspect agreement structure. Strong clusters can reveal shared rubrics, shared model behavior, or task-specific ambiguity. That information is valuable even when the final label is unchanged. Finally, report uncertainty with dependence in mind. Ten correlated votes should not always produce the same confidence as 10 independent votes. When LLM judges agree, we should ask why. Sometimes agreement is independent evidence. Sometimes it is a shared blind spot. A good aggregation method should be able to tell the difference. Acknowledgments: Shiva Prasad Kasiviswanathan

A standard operating procedure, or SOP, is the written set of steps an organization follows to correctly complete an important piece of routine work the same way every time. Almost every industry runs on SOPs. A hospital uses one to register a new patient, a logistics team uses one to decide whether a shipment qualifies as hazardous, a bank uses one to verify a new business customer, and a trust and safety team uses one to decide whether to remove a piece of content. SOPs carry an organization's hard-won knowledge, its compliance rules, and its decision logic in a form that any trained person can adopt and follow. As a result, they keep operations consistent and safe across different employees, shifts, and sites. SOPs are hard for AI agents to execute because they look cleaner than they actually are. A real procedure asks the reader to interpret instructions that were never fully spelled out, to draw upon knowledge that everyone in the field already shares, and to make judgment calls as conditions change. Consider the following passage from a patient intake procedure: Steps four and six tell the operator to verify the patient's insurance, without saying how the verification should be done or why it needs to be done twice. Someone who has worked an intake desk, however, knows that the first step confirms the patient’s coverage with the insurer, and the second step confirms that the patient’s information is correctly entered into the medical provider’s management system. An agent has none of that background, so it must guess what verification means here, remember what it did earlier in the procedure, and choose between tools that look nearly identical. This is the kind of moment where polished demo behavior quietly falls apart, and it is the kind of thing that most agentic benchmarks never test. Rigorously measuring what agents can and cannot handle is essential for building assistive tools that genuinely help rather than silently fail. Today we are sharing SOP-Bench, an openly available benchmark that measures how well AI agents carry out real SOPs authored by domain experts. It is the first benchmark of its kind to pair genuine enterprise procedures with functioning tools and ground-truth answers, so that an agent earns its score by completing the procedure rather than by producing text that an automated grader happens to like. We presented the benchmark at the 2026 Conference on Knowledge Discovery and Data Mining (KDD), along with experimental results showing where even strong foundation models come up short and an evaluation framework the community can build upon. Why existing benchmarks fall short Most agent benchmarks do one thing well. Some check whether a model can pick the right API for a request; others check adherence to a written set of constraints; still others measure the ability to plan a sequence of steps toward a goal. All of these are valuable, but each one isolates a single capability and tests it with clean, machine-formatted prompts that leave out the ambiguity and variability of procedures written by actual people. Executing an SOP requires all these skills, along with using multiple tools in a coordinated way across steps that depend upon one another, keeping track of what has happened so far, and recovering when something does not go as expected. Past efforts to adhere more closely to real business procedures have encountered limits. Some translate written procedures into executable workflows, but only for short descriptions in narrow domains, and the datasets behind them are often not released publicly. Others publish collections of genuine business procedures but stop at the text, without the tools or the known answers that would let anyone run an agent through the procedure and check its work. That is the gap SOP-Bench is built to close. It brings together elements that have previously appeared only separately: realistic procedures with the ambiguity left in, coverage across many different industries, working tools an agent can call, and a way to grade the result against ground truth. What we built SOP-Bench turns real procedures into runnable tasks. It covers 12 business areas, including healthcare intake, dangerous-goods classification, customer service, content moderation, financial compliance, and warehouse inspection, with more than 2,000 tasks in total. Each task comes with the tool interfaces an agent requires and a correct outcome. An agent runs the procedure by calling tools, and we can validate its work against ground truth rather than against a model's opinion of it. SOP-Bench is a framework rather than a fixed set of tasks. It comes with two baseline agents, but a team can drop in an agent of its own, test it against the included procedures, and even add its own procedures. That's because each procedure is just four things: the SOP text, the tools an agent can call, the specifications for those tools, and a set of test cases with known answers. The framework runs every task, keeps a full record of the tool calls and reasoning behind each decision, and grades the outcome against the known answers. Scores are reproducible, and failures can be tracked back to the steps where they happened. In practice, this lets a team try its own agents on its own SOPs before trusting them in production. Constructing realistic SOPs that span industries is difficult, but it’s where Amazon has an advantage. It Amazon provides experts from all relevant fields working in parallel, a culture in which those experts already document their work as written procedures, and enough infrastructure to execute thousands of tasks simultaneously. To construct SOP-Bench, we paired experts with AI, while letting the experts determine whether an answer was correct. They authored the original procedures from real industrial workflows and set the context for each task. An Anthropic Claude 3.5 Sonnet v2 model then handled the slow, mechanical work of turning each procedure into something a machine can run and generating the data schemas, the mock APIs and tool specifications, the tool code, and datasets that deliberately mix ordinary cases with edge cases and outright failures. Every generated item went back to the experts, who confirmed that the logic held, corrected the procedures, checked the data, and ran the code to be sure it behaved. No proprietary or sensitive data was involved at any stage. What we found We ran two deliberately simple agent designs, a function-calling agent and a reasoning-style agent, across 11 frontier models. These agents are a baseline for others to improve upon rather than an assertion of the best possible system. Even so, a few patterns came through clearly. Newer is not automatically better The most surprising insight was that upgrading the model sometimes lowered performance. On the reasoning-style agent, the newer Claude 4.5 family scored lower than the older Claude 4 family. The same reversal held when we compared individual models on the same setup. For a team running agents in production, this is the finding that matters most, because a routine upgrade can lower the success rate with no obvious signal that anything changed, and the only reliable way to catch it is to test on the procedures the team actually runs. More tools can make an agent worse We took a single video-annotation procedure and gave the agent two versions of its toolkit. One held exactly the six tools the task required. The other kept those six but buried them among 20 extra tools that looked plausible but did nothing useful. Success nearly halved with the larger toolkit, even though every tool the agent needed was available. The lesson is that capability is not free, and trimming an agent's tools to fit the task may be a key component of getting it ready to deploy. No single setup wins everywhere No one pairing of model and agent came out ahead across the board, and the combination that performed best on one procedure was often a weak choice on another. The gap between procedures was wide. On the easiest ones, such as triaging incoming e-mails by intent, agents arrived at the correct answer approximately nine out of ten times, while on the hardest, such as annotating objects in a driving video, they were correct approximately one out of four times, a more-than-threefold gap across the suite. Trusting a single benchmark score would tell a team almost nothing about how the same setup would behave on the next use case. How an agent is built matters as much as which model runs inside it When we compared the two agents head-to-head on the same model, the reasoning-style agent came out slightly ahead on average, yet it won on only eight of the thirteen procedure runs in the comparison, and it took about a third longer per task. Some procedures clearly favored one agent and some the other, so the shape of the procedure, rather than a single overall average, should drive the agent choice. One open question remains and runs counter to what might be expected. A procedure that was mostly long stretches of reading, with only a couple of points where a decision had to be made, gave agents more trouble than one packed with many more decisions. The natural assumption is that complicated logic is the hard part, but here the longer, simpler-looking procedure scored far worse. We are not claiming that the length of the reading is the cause, since the two procedures differ in other ways as well, including how many tools they involve. But this is a question that the benchmark was built to help examine, one we hope other groups will examine with us. Taken together, these results are not a verdict on any single model. They are a map of where the field still needs to invest and a reminder that raw capability does not guarantee reliability on the kind of procedural work that businesses depend upon. More practically, they help teams identify the specific steps where human oversight remains essential. AI’s weakness on those steps surfaces only in sustained, tool-using runs against realistic procedures, which is why a static skills test is not enough for agents that are being deployed alongside human operators on procedural tasks. Get started with SOP-Bench We are releasing the full benchmark on GitHub and on HuggingFace. The release includes the 12 expert-authored procedures, the generated tools and datasets, the two baseline agents, and the evaluation code that scores an agent's runs against ground truth. Researchers and teams can evaluate their own agents against the existing procedures or extend the benchmark to new domains using the same human-and-AI method we used to build it. We are especially interested in procedures from industries we have not covered yet. We also plan to add harder variants of the same procedures, instructions that include images and tables, and procedures with nested structures that force an agent to switch context partway through. If you build agents, evaluate them, or want a clearer picture of where they stand on everyday operational work, we would welcome your contributions and feedback.

In 2016 a small research team at Amazon announced our presence to the world with the launch of the Automated Reasoning Group (ARG). Our vision was bold: use mathematical logic to not just test AWS systems but to prove, with mathematical certainty, that they work correctly. In the intervening decade, we’ve gone from exploring whether advances in formal verification could mitigate previously intractable problems — at AWS scale — to building systems fundamental to how AWS approaches security and reliability. Our group’s production services process billions of queries daily. This is a look back at how we applied cutting-edge formal-verification and program analysis techniques to Amazon's unique challenges. We were motivated by the belief that real-world security and infrastructure problems could be solved with mathematical rigor at AWS scale. After all, tools like the ones we were researching had already proven successful at places like Intel and NASA. What we didn't fully anticipate was just how broadly applicable these techniques would become. From demos to production at scale When we held our first ARG Demo Day in 2016, we showcased several ambitious projects to AWS Security. Each represented a different approach to the same fundamental question: how can we use mathematics to prove that our systems are secure and correct? The answers presented that day laid the groundwork for systems that continue to play significant roles for AWS and our customers in 2026. Sean McLaughlin gave a presentation titled “Automatic tools for reasoning about virtual private clouds (VPC)”. He noted that the growth of VPC networks had led to an increase in the demand for automated-reasoning solutions capable of identifying misconfigurations or security vulnerabilities. His answer was “a tool called Tiros, which, just simply put, answers questions about your network.” Tiros became the foundation of a network security analysis feature in the Amazon Inspector service, which is used by millions of customers building applications in the cloud. Tiros is also used within AWS to automate the checking of compliance certification and adherence to security invariants for many AWS services. Today it powers both Amazon Inspector and Reachability Analyzer. This work also split off and became Zelkova, which uses automated reasoning to analyze policies and the future consequences of policies. Zelkova powers tools such as S3 Block Public Access and IAM Access Analyzer, among many others. Similarly, a presentation given that day on the use of deep automatic analysis for crucial infrastructure turned into the work that we did to prove the correctness of our TLS handshake and other properties of cryptographic, storage, and virtualization code. Even some of the smaller-scale projects we spotlighted went on to have an outsized impact. When we presented our work on deductive verification for high-value infrastructure, it largely applied to the deepest parts of our cryptographic protocols. Today the importance of that work has grown enormously, fueled by the rise of proof assistants — automated tools such as Lean (created by Leo de Moura, a senior principal scientist on our AR team) that help users develop formal proofs. We can now pair those tools with language models to find proofs for more and much bigger systems. In fact, the proof we announced for the Nitro Confidentiality Engine is evidence of this. It is also the basis of our proof of the AWS policy interpreter and more recent work proving the correctness of our cryptographic foundations. Mathematical guarantees customers rely on Over the past decade, ARG's research prototypes have evolved into services that millions of AWS customers use every day. IAM Access Analyzer uses Zelkova to help customers like USAA and GoTo identify unintended access to their resources. Instead of hoping security policies are configured correctly, customers get mathematical proof of what their policies actually permit. Reachability Analyzer, built on the Tiros service we demonstrated in 2016, helps customers understand network connectivity without sending a single packet. Rather than testing configurations, it mathematically analyzes all possible network paths to answer whether a destination is reachable and, if not, what the blocking component is. Amazon Bedrock Guardrails with Automated Reasoning checks brings mathematical verification to generative AI. The feature helps prevent AI hallucinations by using formal logic to validate that model responses comply with defined policies — delivering up to 99% verification accuracy. These customer-facing services share a common foundation: they use satisfiability modulo theories (SMT) solvers and other automated-reasoning techniques to provide mathematical guarantees about system behavior, going far beyond what traditional testing can achieve. Proving the infrastructure beneath the cloud While customer-facing tools demonstrate automated reasoning's practical value, some of our most challenging work has focused on AWS's internal infrastructure — systems that must be correct because millions of workloads depend on them. We've used automated reasoning to prove the correctness of much of our infrastructure, including The AWS Nitro Isolation Engine Cryptographic implementations like s2n-bignum Boot code running in AWS data centers Storage systems like S3 In one particularly ambitious project, we proved correct and seamlessly replaced our entire authorization engine, which handles one billion API calls per second. We used specifications and proofs and verified the new engine against quadrillions of production authorizations. These internal verification efforts demonstrate how automated reasoning can provide mathematical certainty about the most foundational layers of cloud infrastructure. An unexpected discovery Perhaps the most surprising finding from our decade of work is that automated reasoning doesn't just make systems more secure; it often makes them more efficient and easier to maintain. When teams must write precise specifications for verification, they often discover simpler, more elegant solutions to their problems. This is partly because of the systemic approach enabled by automated reasoning. Rather than focusing on validating system behavior under specific scenarios, automated reasoning uses logic to verify system behavior under any possible scenario. Rather than considering all possible input scenarios and how they might go wrong, we define how the system should work and identify the necessary conditions for that behavior. Then we can verify that those conditions are true by using mathematical proof. In other words, we can verify that the system itself is correct. This discovery has validated our belief that mathematical rigor and practical engineering aren't opposing forces — they're complementary. The discipline required for formal verification frequently reveals opportunities for simplification that might otherwise remain hidden. Building the foundation for agentic AI The research we began a decade ago has uniquely positioned us for the next era of AI development. Our work in distributed systems and critical code verification laid groundwork that now applies directly to verifying AI-generated code. Meanwhile, our research into misconfigured AWS policies and VPC networks now helps verify the correctness of AI-generated content. Evidence for this evolution is found in some of our recent launches. Amazon Bedrock Guardrails with Automated Reasoning checks represents a significant milestone by moving from tools requiring deep expertise to capabilities embedded directly in services builders use every day. Policy in Amazon Bedrock AgentCore uses automated reasoning to set clear boundaries for agent actions, ensuring agents stay within defined compliance boundaries while operating autonomously. Teams can use natural language to specify which tools and data agents can access, and when integrated with AgentCore Gateway, the system checks policies in milliseconds. In Kiro, an agentic development environment, we released a requirements analysis capability that uses automated reasoning to prove that there are no contradictions, ambiguities, and gaps in the software requirements before code is written, increasing code accuracy and preventing future debugging cycles. The team building Kiro also uses automated reasoning to check if the underlying AI-generated code works correctly before releasing the feature publicly. As AI agents become more autonomous and take on more complex tasks, the need for mathematical guarantees about their behavior becomes critical. When AI agents suggest code changes to systems with formal specifications, those systems can automatically verify those changes against mathematical proofs. Automated reasoning provides a path to building AI systems that are not just powerful but provably safe and reliable. A decade of collaboration This work wouldn't be possible without the talented team we've built and the customers who've trusted us to help secure their critical infrastructure. Across AWS, teams are continuing to expand automated-reasoning capabilities. Senior principal scientist Daniel Kroening and his team in Annapurna are advancing hardware verification. Senior applied scientist Nadia Labai is pioneering auto-formalization research, teaching AI systems to convert natural language into formal mathematical proofs. Principal applied scientist Tristan Ravitch and his team in AWS Security launched Peri to automatically track data flow across all accounts in AWS and Amazon, with zero onboarding for service teams. These efforts position AWS to make the next decade of automated reasoning just as transformative — if not more so — than the first. What we've proven Ten years later, I'm incredibly excited about what we've accomplished. We've proven that automated reasoning delivers measurable value at every layer: from preventing configuration errors to providing mathematical guarantees about AI system behavior. We've demonstrated that mathematical rigor and practical engineering can work together to solve real customer problems at scale. The journey from that first demo day in 2016 to where we are today exemplifies AWS's commitment to transforming academic advances into services customers rely on daily. We've built a foundation of trust through mathematical certainty — and that foundation will be essential as we navigate the next decade of AI innovation. Here's to the next 10 years.

Modern LLM architectures have co-evolved within a single hardware family. The shapes of our attention mechanisms, the structure of our multilayer perceptrons (MLPs), the choice of numerical formats, and even the granularity of parallelism strategies have all been shaped by hardware constraints: warp sizes, tensor core geometries, memory hierarchies, and the kernel abstractions those chips expose. When the hardware changes, the efficient frontier of model architectures changes with it. Here we present an opportunity for academic and industry labs to explore this frontier in detail on AWS Trainium. Purpose-built accelerators like AWS Trainium present a genuinely different design surface. More on-chip SRAM (SBUF), explicit software control over data movement and acceleration at the lowest levels, energy-efficient systolic matrix multiplication (matmuls), and a memory hierarchy designed for training and inference-scale data flows. The resulting TFLOPs-to-memory-bandwidth ratio shifts the performance bottleneck profile: key operations that are memory-bound on conventional accelerators may become compute-bound on Trainium, opening design space for architectures that trade additional computation for reduced memory traffic. These hardware differences mean the optimal attention patterns, MLP structures, and parallelism strategies may be fundamentally different. The research question is open: What does an optimal model look like when the hardware constraints are fundamentally different? The AWS Trainium Frontier is a competition designed to answer this question empirically: participants train language models from scratch on Trainium, exploring the full design space from model architecture to custom kernels. The core task is training a language model from scratch, starting from a provided ~50M parameter baseline (nanochat-derived, GPT-style dense LLM with RMSNorm, rotary embeddings, and ReLU² MLP). Participants modify everything: architecture, optimizer, training loop, and optionally custom NKI kernels. The baseline is a starting point, not a ceiling. The AWS Trainium Frontier competition rewards full-stack thinking under a fixed time and compute budget. Participants optimize the model architecture, the optimizer, the training loop, and, if they choose, custom hardware kernels. This enables innovation on a combination of objectives: within the allotted training budget, how low can you drive validation bits-per-byte, and how high can you drive downstream in-context learning capability? The fixed budget creates a direct tradeoff between model capacity (better architecture = fewer steps needed) and training throughput (faster kernels = more steps in the same time). The winning solution finds the balance: the most intelligent model trained most efficiently within the time constraint. Final submissions find the optimal point on that frontier, and because Trainium's hardware benefits differ from those of existing accelerators, the optimal architectures will differ as well. Be among the first to discover what model architectures look like when designed for a purpose-built AI chip, contributing to a genuinely new area of machine learning research. The Neuron Kernel Interface (NKI), native PyTorch support, and AI-assisted tooling (including Amazon Bedrock access) give you direct access to Trainium's unique hardware features: the SBUF scratchpad, TensorEngine tiling, and explicit DMA control that standard framework abstractions cannot expose. This is what enables genuinely hardware-native model designs. The entire NKI API surface fits in a weekend, making it equally accessible to both a human writing kernels by hand and an AI agent generating them under human direction. The challenge: Exploring the full design space Phase 1 gives every team a single Trainium2 chip and a 30-minute training budget, fast enough to test dozens of hypotheses in a single day. Phase 1 scores on a single number: validation bits-per-byte (val_bpb) after exactly 30 minutes of training on a single Trn2 chip. Lower is better. Any improvement that fits within that wall-clock budget counts, whether it comes from architecture, optimizer, kernel, or all three. Phase 2 promotes the top 10 teams to a full Trainium2 server with a four-hour budget, opening the door to distributed parallelism and communication-aware model shaping. Phase 2 adds a second axis — inference performance on CORE, an aggregate score across in-context learning tasks spanning reasoning, comprehension, and world knowledge. Your final score is a 50/50 composite: you need a model that trains efficiently and learns to reason. It's a research arc from, "Does my idea work?" to, "Does my idea scale?”. Participants have flexibility in how they improve the model. A better learning rate schedule matters as much as a faster kernel. This rewards the full stack: a novel attention mechanism is only as fast as the kernel that runs it, and the fastest kernel only matters if the architecture knows how to use it. Model size is uncapped: the constraint isn't parameters, it's time on the chip. You choose the model architecture that maximizes capability within a fixed training window. This inversion of the usual scaling paradigm is what makes this a more challenging research question, not just an engineering exercise, and it's where the most publishable insights will emerge. What you get A complete nanochat-derived training pipeline with Muon +AdamW optimizer, ready to run on all NeuronCores A Trainium-optimized autoresearch framework for AI-assisted experimentation Full NKI documentation: programming guide, ISA reference, architecture docs, and example kernels Neuron Explorer for comprehensive profiling and performance debugging of NKI kernels The CORE evaluation harness for inference self-scoring during Phase 2 Eligible academic teams can obtain AWS Promotional Credits covering Trainium compute and Amazon Bedrock access Native PyTorch for Neuron with no additional package installation required Who should compete ML architecture and training researchers exploring model designs, optimizers, and training recipes. Familiarity with PyTorch and transformer training is expected; no hardware kernel experience is required to be competitive at the ML layer. ML systems researchers and performance engineers interested in hardware-aware optimization, custom kernels, and the interplay between model design and hardware. Familiarity with CUDA, Triton, or similar kernel programming transfers directly to NKI; no prior Trainium experience is required. Teams building with AI research agents, using LLMs and automation to run more experiments, write more kernels, and explore more architectures than any single person could. This competition rewards breadth of exploration, making agentic approaches a natural fit. Teams of one to four members are welcome. Strong submissions will likely combine multiple of these perspectives, either within a single team or via AI-assisted workflows that extend a team’s reach across the stack. What's at stake Top three finalists present their work at an exclusive Annapurna Labs research event during NeurIPS 2026 in Sydney, Australia, sharing findings with the ML community and AWS AI Chips leadership. Travel and expenses are the finalists’ responsibility Top 10 team members receive exclusive Neuron team jackets and finalist swag packs. Top three finalists have the opportunity to co-publish findings with Annapurna Labs researchers, contributing to a seminal paper on hardware-native model design. Prize pool: $25,000 (first), $10,000 (second), $5,000 (third). Key dates Aug. 31, 2026: Phase 1 opens; leaderboard goes live Sept. 30, 2026: Phase 1 closes; top 10 announced Oct. 7, 2026: Phase 2 opens on full Trn2 servers for top 10 Nov. 4, 2026: Phase 2 closes Nov. 11, 2026: Finalists selected December 6–12, 2026: Finalist presentations at competition workshop in Sydney Register by Sept 30, 2026. Other eligibility restrictions apply. See terms and conditions. The competition is open to the first 100 teams to register. Participants must be 18 or older. AWS employees, interns, and scholars (2025–2026) and their immediate family members are ineligible. Residents of certain countries are excluded; see full competition terms for details. Team sizes can be one to four participants.Register today to secure your team’s spot and start building on genuinely new silicon. The frontier is open — come find out what’s on the other side.

Build on Trainium is a $110 million credit program focused on AI research and university education aimed to support the next generation of innovation and development on AWS Trainium. The program provides compute credits to novel AI research on Trainium, investing in leading academic teams to build innovations in critical areas including new model architectures, ML libraries, optimizations, large-scale distributed systems, and more. This announcement includes awards funded under the Fall 2025 Build on Trainium: Responsible AI call for proposals. Proposals were reviewed for the quality of their scientific content and their potential to impact both the research community and society. This cycle’s focus on Responsible AI invited proposals addressing five priority topics: AI safety and alignment, multi-lingual language models, representation engineering, sustainability and small language models, and deep learning models for synthetic data generation—all leveraging AWS Trainium infrastructure. The recipients have access to more than 700 Amazon public datasets and can utilize AWS AI/ML services and tools through their AWS Promotional Credits, are assigned an Amazon research contact who offers consultation and advice, and benefit from AWS Trainium resources, such as tutorials and hands-on sessions. "Build on Trainium gives the next wave of AI researchers powerful, scalable access to Amazon's purpose-built AI chips, so the only limit is their imagination, not their compute budget," said Yida Wang, AWS AI Principal Applied Scientist. "By leveraging the support from Build on Trainium, University of Illinois Urbana-Champaign researchers are studying topology-aware parallelization strategies for large-scale mixture-of-experts models with as many as one trillion parameters on up to 1,024 Trainium chips. At the University of Washington, researchers are developing an inference-optimization framework that raises token efficiency for everyone building on Trainium, with the goal to deliver portable, high-performance LLM inference on Trainium." RecipientUniversityResearch titleWei BaoThe University of SydneyFACTOR: Federated Adversarial Co-Training with Textual Gradient for LLM Security and RobustnessViveck CadambeGeorgia Institute of TechnologyLeveraging Public-Private Mixtures For Differentially Private Synthetic Data GenerationYujun CaiThe University of QueenslandResponsible AI on Trainium: Scalable Detection and Mitigation of Evasive Multimodal Scam ContentHaipeng ChenCollege of William and MaryDELA: Editable Diffusion Language ModelsTianlong ChenUniversity of North Carolina at Chapel HillAlgorithm-System Co-Design for Efficient Sparse and Quantized LLMsSaadia GabrielUniversity of California Los AngelesMANSA: Democratizing Voice AI with Efficient Multimodal Foundation ModelsHaewon JeongUniversity of California Santa BarbaraLeveraging Public-Private Mixtures For Differentially Private Synthetic Data GenerationHaojian JinUniversity of California San DiegoGoverning Social Bias in AI Image Generation through Value ManifestsMarios KogiasImperial College LondonTowards Deterministic Model InferenceSachin KumarThe Ohio State UniversityNatively Multimodal and Multilingual Speech-Text Large Language ModelsEmanuele La MalfaInstitute for Decentralized AI (ADAI)Safe, Social Pre-training of LLM AgentsXiaoxiao LiThe University of British ColumbiaMemorization-Aware Preference Optimization for Machine UnlearningYingcong LiNew Jersey Institute of TechnologyEfficient and Adaptable Language Models via Sub-Model SearchZhijian LiuUniversity of California San DiegoAlgorithm-System Co-Design for Efficient Sparse and Quantized LLMsSongtao LuThe Chinese University of Hong KongM3-Align: Scalable Multilevel & Multiobjective Alignment for Multilingual Language ModelsYao LuUCL - University College LondonBreaking the Multilingual Data Wall: Scaling Synthetic Data for Low-Resource Language Model PretrainingSasa MisailovicUniversity of Illinois at Urbana-ChampaignCratos: Certified Robustness for Quantization and Pruning-Aware Training and Tuning of Vision Language ModelsTinoosh MohseninJohns Hopkins UniversityTRIM-LLM: From Quadratic to Linear Attention and Structured Pruning for Carbon and Cost-Efficient LLM Deployment on TrainiumThanhVu NguyenGeorge Mason UniversityLeveraging AWS Trainium for Verifiable AI and ML-Assisted Mathematical ReasoningFrank RudziczDalhousie UniversityRepresentation Immunization on Trainium: Scalable Noising & Weight-LockingAnuj SharmaIowa State UniversityBuild on Trainium: Physics-Grounded Synthetic Crash Generation for Vulnerable Road Users with Representation Engineering on Video Diffusion and VLMsShen ShenMassachusetts Institute of TechnologyAgent Tool-Use Safety Benchmarking with MCP-Specific LoRA MitigationsRyan ShiUniversity of PittsburghBenchmarking and Improving Multilingual LLMs on Real Indic Language Healthcare DialoguesNaichen ShiNorthwestern University LLM Hallucination Detection and Mitigation Jaideep Srivastava University of Minnesota Twin CitiesKnowledge-Infused Time-Series Pretraining with Safety-by-Knowledge-Checking for Trustworthy Clinical AICheng TanNortheastern University Towards Reliable and Trustworthy LLM Services with ϵ-correctnessYue WangUniversity of Central FloridaGame-Theoretic Frameworks for Responsible AI on Pluralistic AlignmentYang WangUniversity of Illinois at Urbana-ChampaignSafeguarding Youths in Multimodal Generative AI: Toward a Trainium-Powered Framework for Safety and AlignmentErmin WeiNorthwestern University Higher Order Based Fast LLM Training MethodJun WuMichigan State UniversityBigger Models, Bigger Risks? Investigating the Safety Landscape of LLM ScalingXiaokui XiaoNational University of SingaporeTrainium-Accelerated, LLM-Guided Differentially Private Synthesis of Hierarchical Relational DataMin XuCarnegie Mellon UniversityLanguage-Grounded Interpretability for ViT and 3D ModelsZiyu YaoGeorge Mason UniversityRepresentation Engineering of LLMs for Secure Code Generation Junzhe Zhang Syracuse UniversityDeconfounding Image Editing for Robust Causal Prediction

Training a machine learning model to handle multiple objectives simultaneously is a bit like trying to follow GPS directions to several destinations at once: the routes often conflict, and compromising between them can leave you farther from every destination. A paper we presented at this year’s International Conference on Machine Learning (ICML) addresses this problem in the context of graph self-supervised learning (graph SSL), where the goal is to train a neural network to process graph data. Graph SSL objectives include inferring links between graph nodes, reconstructing nodes that have been masked out, and maximizing the mutual information between a given node and the nodes in its neighborhood. Our framework, ControlG, borrows an idea from industrial control systems: rather than blending all objectives together at every training step, it dedicates computational capacity to one objective at a time and lets a proportional-integral-derivative (PID) controller decide which objective needs attention next. Karish Grover, an Amazon PhD fellow, performed this work during an internship at Amazon Web Services, and Amazon Scholar Christos Faloutsos and I served as his mentors. The problem: Multitask tug-of-war The goal of graph self-supervised learning is to learn useful representations of graph data that can be used in downstream tasks like node classification. Research in the area has produced a rich tool kit of training objectives, each encoding different structural intuitions about the data. Link prediction captures local connectivity. Feature reconstruction captures node attributes. Contrastive methods capture invariant features. No single objective dominates across all datasets and downstream tasks, so a natural strategy is to combine several objectives. For each batch of training examples, the machine learning algorithm calculates a gradient: a vector that indicates the direction and distance we should move in the parameter space. Based on the gradient, the algorithm updates the model’s parameters. The standard way to handle multiple objectives is per-step mixing: at every training step, blend gradients from all objectives into a single update. This makes every parameter update a compromise. When objectives disagree about the direction in which to modify parameters, three types of failure occur: Disagreement: Conflicting gradients cause negative transfer, where optimizing one objective actively degrades another. Drift: An objective that helps early in training may become redundant later, but fixed or slowly adapting weights cannot track this shift. Drought: Adaptive weighting schemes can starve objectives by driving their weights toward zero, making it impossible to tell whether an objective ever meaningfully shaped the learned representation. Coordination is a scheduling problem Our key insight is that multitask coordination is fundamentally a temporal allocation problem. Rather than asking, "How should I blend these objectives right now?", we should ask, "Which objective should receive the next allocation of my computational budget?" This reframing has a surprising consequence: even random scheduling, where you pick an objective uniformly at random for each block of training steps, often matches or beats sophisticated gradient-manipulation methods. On node clustering, random scheduling (average rank 5.0) outperforms AutoSSL (7.3), WAS (10.0), ParetoGNN (8.1), PCGrad (7.8), and CAGrad (8.4). The temporal separation alone eliminates instantaneous gradient conflict. But random scheduling leaves performance on the table. Some objectives need more computational capacity than others at different points in training. ControlG uses the PID controller to allocate adaptively. PID controllers are feedback loop controllers often used in industrial settings to manage processes that require continuous adjustment and automated control. You can find such systems in both industrial machinery and consumer devices, from your car’s cruise control system to a high-end espresso machine regulating water temperature. ControlG: Sense, plan, control ControlG decomposes multitask coordination into three loops, each operating at a different time scale. The loops draw on the theory of Pareto efficiency: in multiobjective optimization, the Pareto front is a boundary in parameter space along which it is impossible to improve the outcome on one objective without diminishing it on another. 1. Sense (slow time scale): Estimate per-objective difficulty using two signals computed on the full training graph: Spectral demand: When a graph neural network (GNN) aggregates information from neighboring nodes, it naturally smooths signals across the graph, much the way averaging nearby pixels blurs an image. Some objectives produce learning signals that vary smoothly (neighboring nodes want similar updates), while others produce sharply varying signals (neighboring nodes want contradictory updates). We measure this by computing how much each objective's desired update direction disagrees between connected nodes (formally, the Rayleigh quotient of the per-node gradients with respect to the graph structure). The sharper the disagreement, the harder it is for the GNN's smoothing architecture to make progress. We prove this formally: this disagreement score (Rayleigh quotient) upper-bounds how much progress a single training step can achieve. Interference: How much does optimizing this objective conflict with the optimization of other objectives? We use the multiple-gradient descent algorithm, which calculates a gradient that reduces error on at least one objective without increasing it on any others, as a measurement oracle: its weights identify which objectives are currently constraining the Pareto trade-off. 2. Plan (epoch timescale): Convert difficulty estimates into a target allocation of computational capacity across objectives. For this, we use the log-hypervolume metric, which measures the distance between the current parameter values (the reference point) and the Pareto front. In particular, we consider log-hypervolume sensitivities, which measure how strongly improvement on one objective would increase the log-hypervolume. In the context of graph SSL, this naturally prioritizes objectives that are lagging (close to the reference point) while tempering allocation by estimated difficulty. The planner produces a target fraction of compute blocks per objective for each epoch. 3. Control (block time scale): Track the allocation plan with a proportional-integral-derivative (PID) controller. The proportional term prioritizes objectives behind schedule. The integral term eliminates steady-state tracking bias. The derivative term damps oscillations. Results We evaluate ControlG on nine graph benchmarks spanning homophilic graphs (graphs where connected nodes are likely to share features, such as Cora, CiteSeer, PubMed, Coauthor-CS, Wiki-CS), heterophilic networks (graphs where connected nodes tend to have dissimilar features, such as Chameleon, Squirrel, Actor), and large-scale graphs (ogbn-arxiv, 169K nodes). Across three downstream tasks (node classification, link prediction, and node clustering), ControlG achieves average ranks of 1.4, 1.9, and 1.8 respectively, consistently outperforming all baselines. Key findings Homophilic graphs: ControlG delivers strong gains over the next-best multitask method (Cora +1.5% over CAGrad, PubMed +1.1% over PCGrad, Coauthor-CS +1.8% over CAGrad on node classification). Heterophilic graphs: Where gradient conflicts are most pronounced, ControlG outperforms all multitask baselines and remains competitive with the best single-objective method (masked-feature reconstruction), which benefits from avoiding conflict entirely but lacks breadth. Scale: On ogbn-arxiv (169K nodes), ControlG achieves 72.86% node classification accuracy, a 1.2 percentage point improvement over the next-best multitask method (CAGrad at 71.62%). Efficiency: ControlG adds modest overhead (16-31 milliseconds per step depending on dataset) compared to simple scheduling (8-15 milliseconds) but remains substantially faster than heavyweight methods like AutoSSL (125-414 milliseconds) and ParetoGNN (35-764 milliseconds). Interpretable and auditable training Beyond performance, ControlG provides visibility into the training process. The scheduling timeline shows exactly when each objective received allocations of computational capacity. The deficit traces, which indicate the difference between the planned allocation and the actual allocation, confirm that the PID controller tracks allocation, and the state trajectories show how difficulty estimates adapt to training dynamics. This auditability matters in practice: when a downstream task unexpectedly degrades, the training log reveals which objectives drove the learned representation and when. Every component matters Removing components in isolation confirms what each piece of ControlG contributes: Removing the planner (uniform allocation) causes the largest drop (up to 3.4% on some datasets), confirming that adaptive allocation is essential. Removing both state signals (spectral demand and interference) yields similar degradation, showing that the planner's effectiveness depends on accurate difficulty estimates. Removing spectral demand diminishes performance across all graph types, while removing interference matters most for heterophilic graphs, where cross-task conflicts are stronger. Replacing the PID controller with independent and identically distributed sampling from the plan degrades performance by 1-2%, demonstrating that deficit tracking improves allocation fidelity. Broader implications While we demonstrate ControlG on graph self-supervised learning, the framework addresses a general problem: how to coordinate multiple training objectives without forcing per-step compromise. The control-theoretic decomposition (sense difficulty, plan allocation, track with feedback) is applicable whenever multiple objectives share parameters and can conflict; the relative importance of objectives changes over training; or interpretability of the training process matters. We are exploring applications to LLM continual learning and multitask fine tuning, where similar tug-of-war dynamics arise when models are trained on diverse instruction-following, reasoning, and safety objectives simultaneously. Acknowledgments This work was led by Karish Grover (Amazon AI PhD fellowship '25-'27, Carnegie Mellon University) during his internship at Amazon, with Han Xie (applied scientist, AWS AI), Sixing Lu (applied scientist, AWS AI), Xiang Song (applied scientist, AWS AI), Christos Faloutsos (Amazon Scholar, Carnegie Mellon University), and me. The code is available as open source.

When a virtual patient in a benchmark scenario tells an AI agent they're feeling feverish, or hopeless, the difference between a safe response and an unsafe one often comes down to clinical design — not just medical knowledge. As healthcare AI shifts from answering questions to completing tasks on behalf of patients — scheduling visits, managing prescriptions, triaging symptoms — we need benchmarks that measure what actually matters: whether these systems keep patients safe, follow clinical workflows, and help patients accomplish their goals across realistic, multiturn conversations. Primary care already guards against diagnostic errors, unsafe medication use, and gaps in follow-up; an agent acting on a patient's behalf should be evaluated on how it handles the same risks. Today we're sharing PatientAgentBench, a reproducible, clinician-vetted evaluation standard built specifically for patient-facing AI agents in healthcare. We’re also releasing key findings about the ways in which even capable foundation models fall short, and we show how the findings can guide the design of safer agents. Why existing benchmarks don't measure patient-facing agentic AI Most healthcare AI benchmarks fall into two camps. Those in the first camp test medical knowledge in a static form, such as answers to medical-exam questions or responses to single-turn or short clinician-facing exchanges. Those in the second test agentic, tool-using agents, but on technical tasks done for providers rather than conversations with patients. Both are valuable, but neither captures what a patient-facing agent has to do: reason over a patient's health record across multiple turns and decide when to gather more information, when to act, and when to escalate, all while maintaining appropriate clinical safety boundaries. A different challenge lies in how these benchmarks score. They typically rely on bespoke, per-conversation criteria — physician-written rubrics tied to specific, static sets of conversations. Such criteria don't generalize to new agents and new conversations. And once the dataset is published, it joins the sea of public data used for model training, so a model can effectively learn the benchmark’s answer key, inflating its scores through memorization rather than reasoning. What we built PatientAgentBench generates a synthetic patient chart and health record, a realistic clinical vignette derived from that record, and a patient agent that uses all that contextual information to converse with the health AI system under evaluation. The health AI system is itself an agent: a base model with a harness that governs how it reasons over the patient's context and uses the benchmark's stateful, simulated healthcare tools. According to the defined benchmark scenario, the agent must gather enough information about the patient’s condition across multiple turns, reason over the health record, determine the appropriate level of care, and execute healthcare workflows correctly. An LLM-as-a-jury panel evaluates the health AI system using over 100 clinician-vetted criteria organized along six dimensions — clinical safety, triage quality, workflow accuracy, task completion, clinical helpfulness, and conversational quality. Unlike the bespoke per-conversation criteria of the traditional approach, these criteria are reusable: the same rubrics apply to any patient-facing healthcare conversation, with the evaluator interpreting each requirement against the patient's dynamically generated record and clinical context. Combined with fresh scenario generation, this makes the benchmark extensible to new clinical domains, new patient populations, and new models without additional physician annotation. It also helps prevent training contamination, since there's no fixed answer key to memorize. The panel scores each conversation against the criteria and, for every dimension, returns a written explanation of what the agent did well or missed. Licensed clinicians have validated the automated evaluation by annotating a shared sample of conversations across all evaluated systems. In our experiments, their scores aligned strongly with the jury — on par with or exceeding human inter-annotator agreement on these tasks. The jury panel also exhibited a reassuringly conservative bias on safety-critical dimensions: the automated panel is more likely to flag a potential problem unnecessarily than to miss a real one. All patient profiles, clinical narratives, and conversations are fully synthetic; no real patient health information is used at any stage. What we found We evaluated multiple families of frontier models on thousands of shared multiturn patient conversations. Out of the box, in a baseline agentic harness, even the most capable models fell short of the standard patient-facing care requires. Three findings stood out: Triage is where models diverge most. The hardest cases weren't emergencies (which trigger strong safety protocols) but routine administrative requests from clinically complex patients — say, a pharmacy update from someone with multiple active medications and a documented mental-health concern. Most models processed these transactionally; few paused to screen for clinical risk. This produces a counterintuitive severity paradox: most agents actually score higher on clearly severe cases than on mild or routine ones, because an obvious emergency triggers stronger safety and triage behavior. The hardest cases are the routine ones that hide real risk — the same kind of case where studies show human diagnostic errors are most common. Safety failures concentrated in specific patterns. The dominant pattern was crisis resource omission — for instance, recognizing suicidal ideation but failing to provide hotline information. A second was clinical-information fabrication: invented provider credentials, fake citations, claimed tool executions that never ran. These findings aren't an indictment of any one model; they're a map of where the field needs to invest. They also reveal something important: model capability alone doesn't guarantee perfect clinical safety. More-capable models narrow clinical gaps but do not close them, and the strongest still leave clinically important cases unhandled. Such shortcomings surface only in sustained, tool-using conversations involving realistic patient records, which is exactly why static knowledge tests are not enough for systems approaching autonomous primary care. Beyond surfacing these clinical gaps, our benchmark's per-dimension scores and explanations provide a roadmap: they show precisely where to focus when iterating on model choice and where agent design must compensate for what model capability alone does not deliver. Consistent with how responsible patient-facing AI should behave, these agents are designed to support, not replace, the patient's provider: rather than rendering definitive diagnoses, they provide educational information and route to clinicians. Get started with PatientAgentBench We're releasing the PatientAgentBench framework on GitHub. The release includes the synthetic-scenario generation pipeline, the healthcare sandbox with stateful tools, the dual-agent-conversation runner, and the LLM-as-a-jury evaluation system with all six rubric prompts. The framework generates fresh scenarios on demand from a configurable seed distribution rather than including a fixed dataset. Researchers, healthcare organizations, and AI developers can use PatientAgentBench with predefined scenarios or expand it for their own use cases, evaluating their systems at scale to identify clinical safety gaps and target improvements. The configurable distribution over patient attributes also lets teams disaggregate results by specific subgroups, helping them identify why their own agents fall short. To get started, see the README in the repository. We welcome contributions and feedback as the field works toward evaluation standards worthy of the promise, and the stakes, of increasingly autonomous patient care. Read the full paper: PatientAgentBench: A Benchmark Framework for Evaluating Patient-Facing Health AI Agents

We want to tell you about an investment we're making and why we're excited about it. As AI agents increasingly make decisions that move money, approve claims, and operate critical infrastructure, the standard approach to software testing is no longer sufficient. Testing checks the cases you thought of, but there is a fundamentally different approach: mathematical proof, which shows with certainty that a system cannot behave incorrectly, no matter what inputs it gets. Lean is a programming language with the potential to make correctness proofs practical at the scale of modern software. Amazon is now providing substantial, long-term financial support to the team building it — the Lean Focused Research Organization (FRO) — to make proof accessible to every developer in the world. This is the single largest donation in the FRO's history. Lean has spawned a thriving community of users in mathematics, computer science, physics, and many other fields. It has led to the creation of Mathlib, a comprehensive library of formalized mathematics, which ignited an explosion of further efforts in formalized proofs. And it has had a pivotal role in the development of AI reasoning capabilities: AI generation of formal proofs in Lean has been a key method for training models with lower error rates, to the point that they are now producing correct solutions to research-level problems. But to us at Amazon, the most exciting thing about Lean is the role it promises to play in agentic safety and neurosymbolic AI: coupling generative AI with Lean's mathematical rigor will help enable verified, trustworthy AI agents. The Lean team drove this vision before the industry caught up, and it’s a vision that is increasingly important to our own strategy for agentic safety. For example, Policy in Amazon Bedrock AgentCore uses Lean-based verification to prove the correctness of the policy language that keeps AI agents within specified boundaries. We haven't seen anyone else offer this type of mathematical guarantee. Lean also underpins the correctness proofs behind systems such as SampCert (mathematical guarantees that differential-privacy protections in AWS Clean Rooms are sound) and AWS Neuron (compilation to Amazon's AI acceleration chips). One scientist recently used an LLM with Lean to prove the correctness of Amazon Aurora's segment repair protocol, our most durability-critical distributed protocol, in a fraction of the time it would have taken manually. The set of applications is growing fast, and this is just the beginning. You might wonder why Amazon would want Lean developed in the FRO, outside of Amazon. The answer is that it's easier to trust a proof when you can evaluate the tools behind it yourself. Customers, auditors, and regulators can independently inspect and validate work done in community-governed tools, which is the kind of transparency that safety-critical AI demands. It also matters internally. Lean becomes more useful as its developer community (which includes our engineers) grows, providing more libraries, more tooling, and more formalized proofs for everyone. For both reasons, we have found it crucial that the foundational work on Lean happens in the open through the Lean Focused Research Organization.

From warehouse automation to surgical assistance, many real-world applications depend on robots performing delicate, contact-intensive tasks. Often missing in these situations is the sense of touch: robots need to feel the forces on their fingertips to manipulate objects effectively. Despite years of effort, robust and scalable solutions to this problem remain out of reach, especially in industrial settings. One approach has been to use vision-based tactile sensors, in which cameras embedded in soft fingertips capture contact geometry. Researchers have used this approach to estimate object shape and pose, but computing the forces that correlate most with manipulation capabilities remains a challenge. Modeling tactile shear — the forces that arise when an object slides or rotates against a sensor — is crucial for building robots that can grasp objects, use tools, and perform complex manipulation skills. Our solution, HydroShear, gives simulators the ability to accurately model tactile forces, enabling robots to learn dexterous, contact-rich manipulation policies entirely in simulation. These policies transfer seamlessly to the real world with no modification, achieving a 93 percent average success rate across four challenging tasks. Bridging the tactile reality gap Simulators for robot locomotion have found success in real-world applications because physics engines model rigid body dynamics and proprioceptive sensing well. But subtle tactile forces and shear feedback are notoriously difficult to simulate accurately. This has made it nearly impossible for tactile sensors trained on simulators through reinforcement learning to succeed when deployed on real robots. Existing tactile simulators face a fundamental trade-off. Physics-based methods like finite-element methods accurately model contact forces but are too slow for training reinforcement learning policies at scale. Faster approximations, on the other hand, oversimplify how forces build up and change during contact. They miss critical events like the moment a gripped object begins to slide or the way a soft sensor deforms over time. Modeling touch with fidelity and speed HydroShear’s key innovation is to add new capabilities to an existing physics simulation technique known as hydroelastic contact models. Called path-dependent force tracking, this approach accurately tracks how forces accumulate over a soft sensor membrane during a physical interaction. Rather than computing forces based only on instantaneous contact, HydroShear remembers the motion history of the object as it moves across the sensor. More concretely, when a robot grasps an object and moves it, different points on the object's surface come into contact with the sensor at different times. HydroShear tracks each of these contact points individually, computing how the soft elastomer deforms as the object moves. It then converts these deformations into realistic force fields, accounting for friction, slipping, and the elastomer's material properties. The simulator handles full 3-D motion — tilting and rolling as well as in-plane sliding — which is essential for dexterous manipulation. It's also GPU parallelizable, enabling efficient large-scale policy training. We calibrate HydroShear by collecting controlled real-world data with a robot arm and vision-based GelSight Mini tactile sensors. The calibration isolates four key parameters: how forces dissipate across the sensor surface, how tangential and normal forces build up, and the friction coefficient between the object and the elastomer. This systematic approach ensures that the simulator accurately reproduces real tactile feedback. Validation: From simulation to real robots We evaluated HydroShear on four contact-rich manipulation tasks, each highlighting different challenges. In all tasks, the robot perceives touch and proprioception (joint positions and gripper state) and has no access to object poses. Peg insertion: The robot grasps a cylindrical peg at an unknown orientation and must insert it into a tight socket. Because the grasp pose varies with each trial, the robot must use tactile feedback alone to detect and correct alignment errors during insertion. Bin packing: The robot inserts a cube into a target slot within a crowded bin. Neighboring cubes partially block the slot, so the robot must push through multiobject contact while sensing forces from multiple directions simultaneously. Book shelving: The robot inserts a book laterally into a shelf, with gravity pulling perpendicular to the insertion direction. The book is larger than the fingertip, producing broad contact patches that make it difficult to localize the object from touch alone. Drawer pulling: The robot pulls open a drawer while external-force perturbations are applied at random times. The robot must detect when the handle begins to slip and tighten its grip just enough to maintain hold without crushing it. We trained reinforcement learning policies entirely in simulation using HydroShear, then deployed them on a real Franka robot with GelSight Mini sensors without any modification or fine tuning. HydroShear achieved a 93% average success rate across all four tasks. We compared against two strong baselines: TacSL, which uses simplified force approximations, and FOTS, a recent learning-based method. TacSL achieved only 34% success, while FOTS reached 58 to 61%. The performance gap underscores the importance of accurate tactile shear simulation. Interestingly, the performance difference correlates directly with simulation fidelity. On tasks like peg insertion, where precise force feedback is critical, HydroShear's advantage is most pronounced. On drawer pulling, which requires detecting and reacting to slippage, HydroShear's path-dependent force tracking proves essential. Faster and less expensive Accurate tactile simulation unlocks a powerful recipe for robot learning: train policies entirely in simulation, then deploy them on real robots. This approach is dramatically faster and cheaper than learning from real-world interactions, which can damage sensors and require extensive trial and error. For warehouse automation, the approach is particularly valuable. Tasks like bin packing, sorting, and careful handling require robots to feel their way through complex interactions. HydroShear enables robots to learn such skills without extensive real-world data collection. While HydroShear yields strong results when coupled with vision-based tactile sensors like GelSight, the underlying principles could extend to other tactile modalities. We're also exploring how higher-resolution sensor simulations and more-complex object geometries could further improve performance.

Reinforcement learning (RL) is one of the techniques we use to make language models better at sustained, multistep tasks like writing code, navigating a website, or carrying out a research workflow. The model doesn't act alone in those settings; it's wrapped in a piece of software we call a harness, which lets it call tools, observe the results of using them, and decide what to do next. To improve such a model with RL, we let it attempt many tasks inside the harness, score how well each attempt went, and use the score to nudge the model's parameters toward the choices that worked. The hard part turns out to be the bookkeeping. To turn a scored attempt into a parameter update, the trainer needs an exact record of what the model produced — not a summary, and not a transcript that looks as though it captures a complete exchange but drops vital information. Internally, models see text as a sequence of numbered units called tokens; an English sentence might have 10 or 20 tokens, each assigned an integer ID by a piece of software called a tokenizer. Two strings that look identical in a transcript can map to different token IDs after a small change of formatting, and that gap, however small, is enough to make the trainer optimize against a slightly different past than the one the model actually experienced. Today we're releasing Turnstile, a small proxy written in the Rust programming language that sits between any agent harness and the backend system that runs the model. Turnstile records the exact token-level history of every request as it happens, at the only point where that history is unambiguously correct: the moment of generation. It then exports a generic, framework-neutral trajectory that can feed into whichever RL training stack you already use. We use Turnstile to drive real RL training runs. In the validations we report here, two different agents — a text-only coding agent and a multimodal computer-use agent — improved steadily over the course of their RL runs. In both cases the agent harness was left unchanged, and the data Turnstile records flowed directly into the training stack and produced the expected learning signal end to end. Tokens, rollouts, and why agent transcripts can lie Three pieces of vocabulary do most of the work in the rest of this post, so it's worth grounding them up front. A tokenizer is a deterministic function that turns text into a list of integer token IDs and token IDs back into text. Each model is paired with a specific tokenizer; you can't substitute one for another. The tokenizer is unforgiving: a stray space, a different way of writing a tool call as JSON, or a slightly different chat template (the format string a serving system uses to wrap roles and messages into a single text input the model can read) can change the token IDs even when the rendered text looks the same to a human. We'll call this kind of mismatch retokenization drift when it comes from rerunning a tokenizer over text we’ve already seen and chat template drift when it comes from the surrounding format changing under us. A rollout is one recorded attempt at a task: the prompt, every tool call, tool feedback, the model’s responses, and the final outcome. The version of the model that produced the rollout is called the behavior policy. The mathematics of policy-gradient RL works cleanly only when the trainer optimizes the model's behavior against the context the behavior policy actually saw. If we rerender the prompt and end up with a slightly different token sequence, we're now training the model against a context unfamiliar to the behavior policy. The training signal degrades, sometimes invisibly, since the model still appears to be learning. That is why agent harnesses make the problem worse rather than better. A harness is not a static prompt; during a single rollout it may compact older messages to save context, retry a malformed tool call, branch into subagents, merge their results back, or summarize history. All of that is normal, useful agent behavior. But each rewrite is another chance for the next request's token sequence to drift away from what the model actually generated last turn. The transcript a harness produces is a faithful record of the conversation; it is not, in general, a faithful record of the tokens, and it is the tokens the trainer needs. Capturing tokens at the proxy boundary Turnstile's central design choice is to stop trying to reconstruct token-level state from text after the rollout is over. We capture it at the moment of generation, where it is already correct, and we do that without changing the harness. The proxy speaks the same HTTP API every modern agent harness already speaks: the OpenAI Chat Completions API, which has become the de facto standard for "send a list of messages, get back a response." The harness creates a rollout group with Turnstile, points its Chat Completions client at Turnstile's address instead of the real backend, and runs unchanged. Behind the scenes, every request flows through Turnstile to the inference backend (today SGLang, with vLLM planned). Turnstile records the exact token IDs the model sampled, the per-token log probabilities (the model's own confidence values for each token, expressed as logarithms; the trainer needs these to compute its update), and a loss mask that marks which tokens were generated by the model and should contribute to training versus which came from the user, tools, or the system prompt and should not. When the rollout is finished, the harness asks Turnstile for the recorded trajectories. Each trajectory is a TrainingSequence object containing the token IDs, log probabilities, the loss masks for the full sequence, and a record of which version of the model's weights was active during which spans of the sequence. (The trainer needs these weight version boundaries to know if the model parameters changed mid-rollout because of an asynchronous update.) Turning that into the specific batch shape your trainer wants is straightforward adapter work: attach the reward, expand the mask, and hand it off. Existing harnesses can stay black boxes There are a number of agent harnesses, such as OpenHands, Codex, and Terminus, that are already useful but were not designed as training runtimes. Without Turnstile, using one of these to drive an RL training run requires it to record token IDs, log probabilities, masks, and routing traces; in practice, that work often falls to a separate harness-shaped component built inside the training system. Either way, a harness ends up acting as a token-level RL data pipeline, and that is the wrong abstraction. The harness knows the information it intended to send to the model, but it does not, in general, know the exact token sequence, cache state, routing trace, or processed multimodal inputs the model actually used. Those live in the backend. With Turnstile, the production harness doesn't have to log training data. It points its Chat Completions client at Turnstile instead of the inference backend and otherwise runs unchanged. Turnstile records the model-facing rollout state: it does not need to understand the harness's private control flow or the semantic reason a context changed. If the next request is a faithful token-level extension of an earlier one, Turnstile merges it into the same trajectory. If the harness compressed memory, rewrote history, merged a subagent result, or otherwise changed the prefix in a way that cannot be proven equivalent, Turnstile starts a new sequence and keeps the trainable suffix honest. All this applies in the strict black-box case: a proprietary harness whose internals are closed to the training system can still drive an RL training run, with no source-level integration at all. Below are two examples of using Turnstile with open-source harnesses in a black-box fashion. Multiturn agents and prefix-aware trajectories A naïve way to store these recordings would be to treat every request as an independent training example. That’s wasteful, because each new request includes the whole conversation so far, so the same token strings would end up being duplicated over and over. It’s also subtly wrong, because it loses the relationship between turns. Instead, Turnstile stores a multiturn rollout as a single growing token path — so long as the path is faithful to what the model actually saw. When a later request to the model is just the previous request plus a few new tokens at the end (the new user message, a tool result, an LLM response), Turnstile recognizes the overlap at the token level — not by comparing rendered strings but by checking that the previously captured token IDs really do appear unchanged at the start of the new request. If they do, the two turns become one continuous trainable sequence with the loss mask correctly identifying which spans were the model's outputs. When the next request cannot be safely extended from a previous one — because the harness rewrote earlier messages, or the tokens drifted for some reason — Turnstile does not pretend otherwise. It starts a new training sequence. We call this "exploding the trajectory". It costs more training tokens than the optimistic alternative, but it ensures that every token string used for RL training is one the behavior policy actually saw. The point is not to maximize compactness; the point is never to lie to the trainer about what happened. Mixture-of-experts routing adds a hidden dimension Some modern models use a mixture-of-experts (MoE) architecture, in which only a small subset of the model's parameters — called experts — are activated for any given input token. The choice of experts is itself part of the computation, made by a small router network at every layer. The routing decision depends on the activations at each layer, and tiny differences in how the previous tokens were processed can change which experts are picked. This matters for RL because, even if two requests have the same token IDs, the tokens might get routed to different experts on different runs. Last fall, researchers at Peking University and their colleagues characterized this discrepancy and proposed recording the MoE model’s routing decisions so the trainer can replay them. We adopt the same principle. When MoE capture is enabled, Turnstile asks the inference backend for the routing trace and records it alongside the tokens. Every time it extends the token path, it checks that the routing for the shared prefix matches what was recorded last turn. If it doesn't — for example, because a key-value cache miss forced the backend to recompute the prefix and pick different experts — Turnstile splits the trajectory rather than train under the wrong routing. Multimodal rollouts When the model also takes images as input — a vision-language model — the rollout has another piece of state to keep track of. The model doesn't see the raw bytes of the uploaded image; it sees the output of an image processor, a fixed pipeline that resizes and crops the image, converts it into a tensor of pixel values, and inserts placeholder tokens into the text to mark where the image goes. The same image bytes can produce different tensors as the result of a different processor version, a different resize policy, or a different patch geometry, and the placeholder count can change with the input dimensions. If the RL trainer has to reprocess the image from scratch, the visual prefix it trains under may not be the visual prefix the behavior policy saw. Turnstile treats image processing as part of the rollout. When a request includes an image, Turnstile decodes it, hashes and stores the original bytes for audit, runs the model's configured processor, and records the processed pixel features in the same trajectory as the token IDs, in the order in which the placeholders appear. The exported sequence carries both the raw and processed visual data, so the trainer can use whichever it needs. Where this is going Turnstile is early. The current implementation has a Rust core, an SGLang backend, Python bindings for in-process training scripts, prefix-aware multiturn capture, optional MoE routing capture, and multimodal support. Near-term work is broader: a vLLM backend, more training-framework adapters, and more multimodal-model coverage. The long-term shape is unchanged from the design we started with: agent harnesses should not have to become RL data pipelines, and trainers should not have to guess what happened from rendered text. The model sampled the tokens. We record them. Additional references Turnstile is now available on Github OSWorld and its open-source agent harness OpenHands THUDM/slime Prime Intellect renderers blog Prime Intellect renderers GitHub prime-rl algorithms (extension property, multi-turn trajectory merging) prime-rl inference (router replay) Polar: Agentic RL on Any Harness at Scale NVIDIA-NeMo/ProRL-Agent-Server Stabilizing MoE Reinforcement Learning by Aligning Training and Inference Routers rLLM Agent Lightning Strands Agents SGLang provider AcknowledgementsSpecial thanks to Keagan Long, Daisy Lin, Changlong Yu, and Yifei Wang for their contributions to this work.

At Amazon, we believe that as our strategy to reach net-zero by 2040 evolves, we need to continue to raise the bar on what and how we measure. Measuring carbon emissions across our entire business is complex, and the tools and methodologies available are continuously improving. Each year, we report on our carbon intensity, absolute emissions, and sustainability progress in our Sustainability Report, and we continue to adopt more-precise tools and methodologies to ensure our data is as meaningful and as representative of our decarbonization journey as possible. Carbon intensity — the amount of emissions per unit of activity or production — is one of the most important tools for tracking decarbonization progress. But not all activities are the same. Across industries, some of the most meaningful intensity metrics are sector specific, tied to the actual activity being decarbonized, across buildings, energy, transportation, and products and beyond. Examples of metrics used by companies include carbon dioxide equivalent per megawatt-hour for electricity, per square foot for building decarbonization, and per kilometer for transport. At Amazon, we apply the same principle: we are developing intensity metrics tailored to specific business activities, so we can measure what matters most. Emissions per unit shipped For Amazon's retail operations, we track carbon emissions per unit shipped. This metric matters because it directly reflects the efficiency of our delivery operations at scale. We’ve reduced emissions per unit shipped every year since 2019, resulting in a carbon intensity reduction of 39% at the end of 2025, relative to 2019. As we ship more packages, we're doing so with less carbon per unit, and our investments in carbon-free energy, smarter routing, lighter packaging, low-carbon fuels, alternative transportation methods (like rail versus road or air), and electric vehicles are all translating into real per-unit reductions. We also track carbon intensity at the regional and country level to understand geographic variation and target interventions accordingly. It's the clearest measure of whether we're decoupling delivery growth from emissions growth. Why this is unique to Amazon Amazon is more than a traditional logistics company: we're also a pharmacy, a grocery store, a cloud services company, a movie studio, a device manufacturer, a satellite business, and much more. As a result, our emissions span the entire value chain — from the manufacture of goods, long-haul shipping, and air freight to warehousing and distribution and middle-mile and last-mile delivery. Amazon’s decarbonization efforts require strategies that can address significant portions of global transportation and supply chains simultaneously. That breadth creates complexity — and opportunity. Solutions that we develop together with our suppliers and partners don’t only stay within the four walls of Amazon; they have the potential to drive decarbonization across multiple industries at once. This is a responsibility we take seriously: we’re proud of our progress and want to share what we are learning along the way. Simplifying our economic intensity metric Part of sharing what we learn is being transparent about how we measure and what we change. One change that we’ve made recently is in our economic carbon intensity indicator. In our 2025 reporting, we updated this from grams of carbon dioxide equivalent per dollar of gross merchandise sales (gCO2e/$GMS) to grams of carbon dioxide equivalent per dollar of revenue (gCO2e/$Revenue). Revenue is publicly reported, widely understood, and aligns with how most companies disclose the carbon intensity of their operations— making our progress easier to compare with the rest of the industry’s. This update does not change our year-over-year trajectory. Looking ahead Climate science and carbon accounting are not static, and as the science and our own operations evolve, we'll continue to refine how we track and report our progress. We’re proud of our Climate Pledge goal to reach net-zero carbon by 2040. We’ll continue updating how we measure, so our data always reflects the most precise and meaningful picture of where we are and where we’re headed. To learn more about Amazon's carbon methodology, visit our Sustainability reporting website.

Amazon is investing in next-generation nuclear technology to meet the rising energy demands of AI infrastructure and cloud computing, and at the heart of that technology are tristructural isotropic (TRISO) fuel particles. This is not your grandparents’ nuclear-reactor fuel. These tiny, robust TRISO particles represent a step forward in the design, performance, and inherent safety of reactor fuel. TRISO: A materials science breakthrough in every particle To understand why TRISO-based fuel is exceptional, consider what reactor fuel must do. In addition to sustaining a controlled fission reaction, it must contain the radioactive byproducts of that reaction, known as fission products. These include noble gases, volatile metals, and long-lived isotopes. Fuel must reliably isolate them throughout operation and into long-term storage, protecting both plant personnel and the public. At less than a millimeter in diameter, each TRISO particle is about the size of a poppy seed, but it acts as a miniature containment system. At its center is a kernel of enriched uranium, surrounded by an inner buffer of porous carbon. Then comes a ceramic shell with three layers (hence the word “tristructural” in the particles’ name): a dense pyrolytic-carbon layer, a silicon carbide (SiC) layer, and an outer pyrolytic-carbon layer. The ceramic shell ensures containment. The silicon carbide layer acts as a pressure vessel and chemical barrier. SiC's hardness, corrosion resistance, and melting point above 2700°C give TRISO particles exceptional mechanical integrity and thermal resilience. Those properties persist even in conditions commensurate with the worst hypothetical criticality accident. Data from the U.S. Department of Energy's Advanced Gas Reactor Fuel Qualification Program (AGR) show that irradiated TRISO particles, subjected to 1600°C for 300 hours, exhibited no detectable failures, with an upper-bound failure fraction of ≤ 6.6 × 10⁻⁵. At 1800°C, failure rates remained well below conservative design limits. These findings were based on the fabrication, irradiation, and testing of more than 500,000 TRISO particles since 2002. The proven durability of these TRISO coatings also preserves long-term stability in spent fuel better than today’s fuel, potentially for as long as 100,000 years. Fuel form flexibility and operational efficiency For decades, commercial light-water reactors have relied on uranium oxide fuel pellets clad in zirconium alloy tubes. This well-established combination has delivered stable, reliable power with a strong safety record in the global reactor fleet. TRISO-based fuels build on this foundation and offer engineers greater flexibility in fuel form and reactor design. Because each TRISO particle contains its own fission-product barriers, nuclear fuel designers can explore novel configurations that enable new operational modes. In pebble-bed reactors like the X-energy Xe-100, in which Amazon is investing, TRISO particles are embedded in tennis-ball-sized graphite spheres that circulate continuously through the core. This motion allows operators to refuel without shutting down the reactor, monitor fuel consumption in real time, and minimize the amount of unburnt uranium in spent fuel. These efficiencies support both resource conservation and waste reduction. TRISO-based fuels can also accommodate different core geometries, so they’re compatible with a range of newer reactor designs focused on safety. Cylindrical compacts are well suited for prismatic cores, for instance, while spherical pebbles enable pebble-bed configurations. This geometric flexibility also allows for the integration of advanced coolants. Unlike conventional light-water reactors, many TRISO-fueled designs — such as the Xe-100 — use high-temperature helium as the primary coolant. Others explore the use of clean molten salt. These alternatives improve thermal efficiency, enable passive heat removal, and further expand the potential applications for advanced reactors. Enrichment and the supply chain TRISO particles are manufactured using high-assay low-enriched uranium (HALEU), enriched to between 10% and 20% ²³⁵U. HALEU offers higher energy density than traditional low-enriched uranium while remaining below the threshold for highly enriched uranium. The use of HALEU in TRISO-based fuels supports compact, high-output designs like the Xe-100 by enabling higher fuel loading and energy density. Each unit produces 80 megawatts of electricity, and up to 12 can be collocated. This modular approach allows right-sized deployment and operational flexibility. HALEU production requires dedicated infrastructure. As enrichment levels increase, separative work becomes more demanding. Centrus Energy operates a U.S.-based HALEU cascade, and the Department of Energy has launched programs to accelerate commercial access. Fuel fabrication has also progressed. TRISO-X, a public-private venture at Oak Ridge National Laboratory, produces TRISO fuel at kilogram scale and is expanding commercial capacity. Standard Nuclear continues developing sol-gel processing, which yields spherical uranium oxide microspheres for TRISO kernels. Amazon's role in deployment Amazon has invested in the Cascade Energy Center, a project to deploy TRISO-fueled Xe-100 reactors in central Washington. With participants such as X-energy, Energy Northwest, Korea Hydro and Nuclear Power, and Doosan Enerbility, the project plans to bring as many as 12 Xe-100 units online to power data centers and cloud infrastructure. The Xe-100 is licensed for construction, TRISO fuel production is active, and project sites are under development. The time is now As a nuclear-engineering professor and researcher focused on advanced reactor technologies and fuel development, I can say with confidence that TRISO particle fuel is the most robust nuclear fuel we have ever developed. Its resilience has been confirmed through rigorous experimentation, and its readiness is evident in a growing manufacturing base and commercial momentum. TRISO-based fuels support reactors that build on decades of engineering progress and deliver clean energy with new capabilities. These systems operate flexibly, scale efficiently, and meet the demands of today’s evolving energy landscape. The future of nuclear fuel is not hypothetical. We are building it now — particle by particle.

Today we announced the general availability of the new M9g and M9gd instances of Amazon Web Services’ (AWS’s) Elastic Compute Cloud (EC2), the first instance types powered by Graviton5, the latest generation of our general-purpose CPU. Graviton5 doubles the number of cores from the previous generation, from 96 to 192. They’re also the first instance types to use the new Nitro Isolation Engine, a component of the Nitro Hypervisor whose sole job is isolating virtual machines (VMs) from each other. In this post, we explain how we used the Isabelle/HOL (higher-order logic) proof assistant — software that mechanically checks reasoning steps for adherence to the laws of logic — to prove that the Nitro Isolation Engine behaves correctly and enforces isolation between virtual machines. The Nitro Isolation Engine is the critical component of the first formally verified hypervisor to be deployed in a commercial cloud environment. Our Isabelle/HOL model and proof comprise 330,000 lines of machine-checked mathematics. It’s comparable in scale to seL4, the landmark project that first demonstrated that realistic operating-system verification was feasible and was an inspiration for our own work. However, unlike seL4, the Nitro Isolation Engine is designed for a commercial cloud environment and ships on production hardware as an always-on feature for Graviton5 users. Our talk at Amazon’s 2025 re:Invent conference introduces our formal-verification methodology, and our white paper is a more detailed discussion covering important aspects of the results, such as scope and assumptions. This blog post gives an informal overview of the main aspects of our formal-verification work and how they fit together. What is a separation kernel? John Rushby coined the term “separation kernel” in 1981 to describe a minimal OS component that partitions a system into isolated compartments. The key idea: separate policy from mechanism. A separation kernel does not decide what to isolate, how to allocate resources, or which VMs to schedule: those decisions are made elsewhere. Instead, it focuses solely on enforcing isolation, and this clarity of purpose makes separation kernels much simpler to implement than full OS kernels. Since its introduction in 2017, the Nitro Hypervisor has been responsible for enforcing isolation in EC2, but it also handles business logic, device drivers, and AWS-specific features. That complexity makes proving correctness much more difficult. Moreover, the Nitro Hypervisor was not designed for verification from the start. Distilling the hypervisor’s critical isolation logic into a minimal component, the Nitro Isolation Engine, makes it small enough to verify and audit, giving customers unprecedented visibility into how isolation is enforced. We also wrote the Nitro Isolation Engine in Rust, a language that lends itself more naturally to formal verification. The Nitro Hypervisor still handles policy — VM creation, resource allocation, migration, scheduling — but it is now deprivileged and must ask the Nitro Isolation Engine to perform any operation touching guest state. The Nitro Isolation Engine checks every request before acting. Specifications and proofs The two key parts of our work are specifications and proofs. Formal specifications precisely capture the expected behavior of the system, and proofs establish that the implementation meets those specifications. Our theorems about the Nitro Isolation Engine address four types of properties: Confidentiality and integrity. Only authorized information flows can occur. For example, guest memory allocations are always scrubbed before reuse. Functional correctness. The implementation behaves exactly as specified. Absence of runtime errors. There are no runtime errors such as unwraps of None option values in Rust — an erroneous command invocation that will stop program execution. Memory safety. There are no issues such as buffer overflows and NULL pointer dereferences. In practice, we handle the last three properties collectively, as a functional-verification result, with confidentiality and integrity treated separately, because we use different proof techniques for each. Functional verification For functional verification, the key parts are a formalization of a core subset of the Rust language, called μRust (“micro Rust”); an expressive specification language using Separation Logic for precisely capturing specifications; and a verification technique, weakest-precondition calculus, with custom proof automation for proving a program correct with respect to its specification. Each of these is part of a general-purpose proof infrastructure that we open-sourced in 2025 as the AutoCorrode library. In more detail, μRust is a restricted subset of the Rust programming language that is expressive enough to write the Nitro Isolation Engine but amenable to formal reasoning because we deliberately excluded advanced Rust features, such as traits and dynamic dispatch. The formal semantics of μRust is defined as a shallow embedding in Isabelle/HOL, which means that the meaning of μRust is defined in terms of higher-order logic, the “host language” of Isabelle/HOL. The specification for a μRust program is defined as a contract with pre- and postconditions, which are assertions about the system state before and after executing the program. Our contracts specify “total correctness”, which means that in all states that satisfy the precondition, the program always terminates, and the resulting state satisfies the postcondition. This total-correctness condition also means the program is memory safe and free of runtime errors. Our specifications are written using Separation Logic, a logic designed to reason about low-level pointer-manipulating programs. Despite the relative simplicity of separation kernels, with the verification of the Nitro Isolation Engine we are still operating on the edge of what is possible with formal verification, and both our specifications and proofs grow very large. For example, the following specification captures what happens when an executing guest virtual CPU tries to turn itself on (an erroneous request): While the specification above is complex, what it captures is intuitively straightforward: in this circumstance, the Nitro Isolation Engine sees that, to act as the caller, the virtual CPU must be turned on already, and it therefore returns a defined error code, AlreadyOn. Everything else about the system state remains unchanged. The complexity in the specification is a reflection of the depth of our modeling and the fact that several other error checks must already have been performed for us to have reached this point in the implementation of the Nitro Isolation Engine. To prove a μRust program correct with respect to its specification, we use a standard weakest-precondition calculus. A weakest-precondition calculus is a systematic way to identify the least restrictive constraint that can ensure that the state of a program after a particular operation is not outside some specified range of states. For example, the weakest precondition of the expression "x + y" is the state in which the values of x and y cannot overflow the addition. The proof obligation then is to show that the contract’s precondition entails the computed weakest precondition. Confidentiality and integrity For confidentiality and integrity, the first key part is a high-level specification that captures the behavior of the Nitro Isolation Engine as a transition relation, where each “high-level” step of the system (e.g., hypercall) is an atomic transition. This specification is rigorously connected to the more concrete Separation Logic specification used in our functional-verification results, which uses another proof idea called Refinement. The second key part is the idea of noninterference. Noninterference is the idea of indistinguishability preservation that we use to make confidentiality and integrity mathematically precise. The idea is that if two states are indistinguishable to an observer before a step, they must remain indistinguishable afterward. The intuitive reason why this captures confidentiality is that the observer has learned nothing new because of the step. Understanding why indistinguishability preservation guarantees confidentiality is subtle. Consider two simple machines, A and B, each with one public and one private register. An observer considers them indistinguishable if their public registers match: the private register is hidden. In the following diagram, A and B are indistinguishable: Now consider what happens if we execute a program that branches on the private register to assign 1 to the public register. The resulting machines A' and B' now have different public registers — they're distinguishable! A clever observer could use this to deduce the original private values, and this failure to preserve indistinguishability corresponds to illicit information flow to the observers. And more to come We hope you’ve enjoyed this overview of the main pieces of our verification work. There are many other aspects to our work, such as conformance testing and how we handle reasoning about concurrent code, that we’re excited to share in future posts.

AWS Graviton processors have improved steadily across generations, with each iteration delivering advances in computational performance, price performance, energy efficiency, and memory capacity. Today, Amazon announced the general availability of the new M9g and M9gd instances of its Elastic Compute Cloud (EC2), for general-purpose workloads. These are the first Amazon products powered by Graviton5, the latest generation of Amazon’s CPU. After five generations of custom silicon and eight years of continuous investment, Graviton powers over 350 instance types that are suitable for workloads including web applications, microservices, analytics, databases, machine learning inference, electronic design automation, gaming, video encoding, and agentic AI. Graviton5 doubles the number of cores from Graviton4, from 96 to 192, and it supports DDR5-8800 memory and the latest PCIe gen6 interconnects. We’ve worked closely with leading DRAM manufactures to meet the DDR5-8800 level of performance, and AWS Graviton instances deliver the fastest memory of any processor instances in the cloud. With Graviton5, Amazon also moved to a three-nanometer process, enabling greater circuit density and faster on-chip communication. Not only does Graviton5 pack in more cores than Graviton4, but each of those cores offers 25% better performance. We've talked for a while about how micro benchmarks are very different from big, real-life workloads, and we design for our customers’ actual workloads — not small loops but all the code and complexity of a real application like a database. To execute code quickly, modern processors predict branches that come from control flow in programs and speculatively execute the predicted paths. The Neoverse V3 core used in Graviton5, codefined by Arm and Amazon’s Annapurna Labs, substantially improves the branch prediction capability of the CPU, and that in turn makes it able to execute real applications like databases up to 30% better. The DRAM of a CPU can be about 100 nanoseconds away. That doesn’t sound like a lot, but for a CPU that runs at 3.3 gigahertz, one memory access takes 330 cycles. CPUs use caches to bring data closer to the CPU, and when a request can be fulfilled from one of these caches, the CPU doesn’t have to wait for the full DRAM latency. Graviton5 has 64-kilobyte first-level caches, two-megabyte second-level caches, and 192 megabytes of level-three cache — more than five times as much as the previous generation of Graviton. Graviton3 was the first Graviton CPU to adopt a chiplet architecture, using seven dies across cores, DRAM controllers, and PCIe controllers. Graviton4 followed the same architecture as Graviton3, with a few refinements. However, in Graviton5, we’ve changed it substantially: the 192 cores in Graviton5 are split across four chiplets, with each chiplet containing DRAM controllers, PCIe controllers, and 48 cores, with custom die-to-die connectivity that provides up to 420 gigabytes per second of bandwidth between chiplets, minimizing latencies between cores in the mesh. There is no longer a separate I/O die nor a separate DRAM controller die. This organization allows us to configure two or four nonuniform-memory-access (NUMA) regions per chip and partition the size of the L3 cache to the size of the virtual machines (VMs) running on the CPU while reducing memory latency for VMs that are 48 cores or smaller. With these enhancements, Graviton5 offers up to 25% better computational performance than Graviton4-based instances, with up to 35% faster performance for web applications, up to 35% for machine learning inference, and up to 30% for databases. The M9g and M9gd instances that are powered by Graviton5 are also raising the bar on security even further with the introduction of the Nitro Isolation Engine. The Nitro Isolation Engine is an enhancement to the Nitro System, which enforces isolation of instances and harnesses formal verification to provide assurances of isolation with mathematical precision. The Nitro Isolation Engine is a purpose-built component that is responsible for enforcing isolation between VMs, including mediation of all access to VM memory, CPU register state, and I/O devices through a minimal set of APIs. The Nitro Isolation Engine leverages formal verification, a technique for mathematically demonstrating that hardware or software behaves as intended, and not just in specific test cases. This intensive verification establishes Nitro as the first formally verified cloud hypervisor, pioneering a new standard for mathematically proven cloud security. To learn more about the Nitro Isolation Engine, read the Amazon Science blog post or our technical white paper.

The year 2026 marks a definitive shift in the AI landscape: we have moved from models that simply know to agents that do. Foundation models (FMs) — large Transformer models pretrained with massive datasets and fine-tuned for diverse downstream tasks — have moved far beyond chatbots, coding, and other digital applications. They are now used as the cognitive engines for AI agents in the physical world, where they plan, use tools, and execute multistep tasks across complex, digitally integrated environments, from warehouses and factories to transportation systems and hospitals. At Amazon, you can see the transition to this new era of "physical AI" in the debut of Project Eluna, an agentic AI model designed to transform how Amazon fulfillment centers operate. To be useful in a high-stakes physical environment, however, an agent needs to be more than fluent in natural language; it needs to be grounded in physical laws and operational constraints. In particular, we must overcome the challenge of hallucination, which, in virtual environments, takes the form of fabricated information — made-up citations, factual inaccuracies, and logical fallacies, all output with high levels of certainty. In a physical system, such hallucinations can lead to violations of reality, with detrimental consequences. For example, if an agent suggests a robotic path that ignores the momentum and mass of the items being moved, its output could be potentially dangerous to people or result in damage to products or equipment. In this article, I propose four approaches to grounding AI agents in the physical world, where "grounding" is defined as the integration of external information, including domain-specific datasets, physical principles, and numerical simulations, to contextualize a model's reasoning. All four approaches can be used separately or in combination, depending on the specific application. Practical implementation of these approaches will not only accelerate the safe and productive use of AI agents but could allow for their further expansion into new domains. Four pillars of grounding Project Eluna is an agentic AI model that lives in the cloud and assists operators who manage operations within fulfillment centers via digital dashboards. It’s designed to act with a degree of autonomy, reasoning through complex operational situations and recommending actions to operation managers. It pulls in historical and real-time data — such as the states of conveyor belts or robots — to anticipate bottlenecks and keep operations running smoothly. The four approaches to grounding AI agents that I describe here grew out of my research at the University of California, San Diego, and with the Amazon Fulfillment Technology (AFT) team, and they help ensure that agents like Eluna are physically consistent and operationally reliable. 1. Physics-guided deep learning. Traditional foundation models can learn to mimic statistical patterns in data but often fail to respect the hard constraints of the physical universe, such as the conservation of mass, energy, or momentum. In physics-guided deep learning (PGDL), we integrate first-principle physical knowledge into the foundation model in pretraining. First principles include symmetries, such as inductive biases like rotations and other transformations, and differential equations that could be used, for instance, in a robot’s motion and control. Not only does this ensure that predictions obey governing physical laws, but grounding a model in physics allows it to learn from significantly smaller datasets. If the model already "knows" the fundamental principles of dynamics, it requires less data to achieve satisfactory accuracy. 2. Uncertainty-aware reasoning. LLMs often exhibit overconfidence in uncertain predictions, which can lead to the assertion of misinformation with high certainty. For an AI agent to be trustworthy in a mission-critical setting, it must know when it does not know. Using our framework (UQ4CT), we produce calibrated uncertainty over the space of functions that map input prompts to outputs. The framework uses an approach called mixture of experts, in which the model is divided into smaller “subnetworks”, each with specific expertise. Our UQ4CT framework allows the model to dynamically align its confidence estimates with predictive correctness. Practically speaking, an agent grounded using calibrated uncertainty can halt or request human intervention when its internal uncertainty exceeds a safety threshold, ensuring reliability even when a model has been fine-tuned with relatively small datasets such as epidemiological forecasts or rare weather events. UQ4CT preserves high accuracy across five benchmarks while demonstrating over 25% reduction in expected calibration error (ECE), a measure of how well a model's estimated "probabilities" match the true, observed probabilities. Even under distribution shift, UQ4CT maintains superior ECE performance with high accuracy, showcasing improved generalizability. 3. Bridging the text-to-numerical gap. While foundation models are masters of natural language, the laws of the physical world are written in the language of mathematics and high-dimensional data, the kind used in fields like robotics, supply chain management, and finance. A trustworthy agent must translate human intent, expressed through language, into precise numerical execution without losing accuracy. Our group developed the adapting-while-learning (AWL) framework, which relies on two key mechanisms. The first is called world-knowledge distillation, where AI agents interact with simulators of the physical world to gather a range of information about what’s physically possible. This knowledge is internalized through supervised fine tuning, effectively grounding the agents’ future outputs. The second mechanism is dynamic tool adaptation, in which a foundation model calls a specialized numerical simulator when it recognizes that its original training is insufficient for the complexity of the current task. This approach is particularly useful in climate science or epidemiology. For instance, if scientists need to plan for vaccine distribution, their original model would call on outside datasets representing disease dissemination. Compared to original models without AWL, those post-trained with AWL achieved 29 percent higher answer accuracy and 12 percent better usage of simulator tools, even surpassing state-of-the-art models including GPT4o and Claude-3.5 on physical-science datasets. 4. Verifier-augmented grounding. Verifiers are software external to LLMs that can be used to ensure that the models work within the bounds of logic and reality. Our weather AI agent, Zephyrus, uses verifiers to refine the reasoning of foundation models in weather science. Zephyrus works in a “reflective” interactive loop, where the agent writes code to query outside weather datasets, observes physical results, and revises its reasoning if the output is flagged by a verifier as scientifically implausible. Another verifier, Hilbert, is used specifically for mathematical reasoning. LLMs, in general, can already generate mathematical proofs, but they need humans to verify whether these proofs are correct. However, there exist so-called proving systems, such as Lean 4, that can offer automatic verification. This has prompted efforts to build specialized prover LLMs that can generate proofs in formal mathematical language. So far, however, these provers solve substantially fewer problems than general-purpose LLMs operating in natural language. Hilbert bridges this gap by breaking complex mathematical problems into subgoals and using feedback from a separate formal verifier to validate them recursively. This process ensures that the agent’s outputs are provably correct. We’ve shown an impressive 422 percent performance improvement over the best publicly available prover LLM. Looking ahead We believe these four pillars lay a solid foundation for grounding LLMs in reality. Meanwhile, several research directions stand to deepen the connection between AI agents and the physical world. First, foundation models can be fine-tuned to interact with more complex, multifidelity numerical simulations, moving beyond function calls to agentic tools and toward an internalized sense for when and at what fidelity to invoke a simulator during reasoning. Second, uncertainty can serve not only as a hallucination detector but also as an intrinsic reward signal, training agents to explore areas of the environment where they have low confidence, high surprise, or incomplete knowledge. Third, physical laws and domain constraints can be embedded as formal verifiers during process planning. They can check every proposed action against conservation principles, kinematic limits, and safety envelopes before execution. As these techniques mature, they will increasingly work in concert: an agent that couples physics-guided learning with calibrated uncertainty and formal verification will be far more robust than one relying on any single pillar alone. Ultimately, as AI agents expand into increasingly complex physical domains, faithful reasoning and effective grounding will be the guiding principles to ensure that agentic AI operates safely, reliably, and at scale across the physical world.

AI agent performance is not just a modeling problem; it is fundamentally a systems problem. A modern agent combines an LLM with a harness, software that mediates the LLM’s interaction with tools and manages the cycle of reasoning and feedback: you can think of the harness as the operating system around the model. As models improve, the performance bottleneck shifts from the model’s ability to reason to the harness’s ability to translate model intent into actions and reflect execution outcomes back to the model. In a paper we just published on arXiv, "Dissecting model behavior through agent trajectories", we formalize this bottleneck as the intent-execution gap: the mismatch between what the model intends and what the harness executes, and vice versa. For example, in trying to revise code, a model may intend to edit a single instance of a function, while the harness accidentally modifies multiple instances. We show that minimizing this bidirectional gap — without any task-specific tuning — is sufficient to achieve state-of-the-art performance across diverse agentic benchmarks, including datasets that test real-world repository patching (SWE-Pro, SWE-Verified) and interactive terminal environments (Terminal-Bench2). While the most visible components of the harness — such as the execution graph, which controls iterations over the thought-action-observation process, and tools — are natural candidates for improvement, we highlight that seemingly trivial implementation details lead to nontrivial fluctuations in performance. Factors such as environment interaction timeouts, infrastructure stability, and resource constraints also materially affect performance. Thus, benchmaxing, or reporting higher numbers on benchmarks, may not necessarily quantify underlying model/harness capability, as it is additionally influenced by the basic infrastructure parameters used during evaluations. We also introduce Simple Strands Agent (SSA), a lightweight and customizable single-agent harness designed to close the gap between the performance reported in agent documentation and the performance seen in open-source implementations. SSA achieves consistent gains in performance across multiple models and benchmarks. Finally, we show that effective agent design is not entirely model agnostic. While many principles generalize, model families differ in tool use preferences, feedback interpretation, and context sensitivity, making model-harness codesign a critical factor in achieving optimal performance. Motivations It is well established that problem-specific customizations such as tuned prompts, tailored tools, and specialized execution graphs can improve AI models’ performance in a controlled setting (fixing all other factors, such as evaluation infrastructure). However, we observed that many such optimizations fail to transfer between models. Improvements that work for one model or version often degrade, disappear, or even regress with newer models. This lack of transferability exposes a deeper issue: many optimizations implicitly overfit the behavior of a specific model. As models improve, these behaviors change, making such gains brittle and noncompounding. In the context of agents, this suggests a shift in focus: rather than optimizing for current model behavior, we should identify invariant components — design principles that remain effective across model upgrades, benchmarks, and environments. To identify such invariants, we focus on the model-harness interface — the boundary where model outputs are interpreted and executed and where execution outcomes are communicated back to the model. This interface is the primary locus of failure when agent performance degrades across settings. From this perspective, two fundamental questions emerge: Does the harness understand what the model intends to do? Is the model clear about how the harness interpreted its actions? These questions define the core alignment problem between model and harness and characterize the failure modes we analyze in the following sections. Tool-interface failures We consider the case in which the agent’s goal is code generation. Our agent primarily uses a bash tool, which provides access to the computer terminal (for example, to execute code), and a file editor to revise code. The bash tool is extremely powerful and can consume all the atomic operations of reading, searching, and editing. We make a simple enhancement to manage its outputs when they get too long. Naïvely truncating the output does not work well because the end of a command execution confirmation carries useful information such as job status and command success/failure. Instead, we contain the response length by condensing content in the middle and keeping only a limited number of lines at the beginning and the end. For reasons of efficiency and better corner-case handling in editing, we use file-editing tools in addition to bash. Our file editor is based on a string-replace mechanism that replaces existing file content with new (model-provided) content to produce edits. While string-replace works well in many cases, we repeatedly observed failure modes that expose the intent-execution gap: the model may have a clear intention, but the harness may not have enough information to execute that intention safely. In these cases, a naïve editor does not merely underperform; it can actively damage the working state by applying the wrong edit with high confidence. The first failure mode arises when the context of the model’s proposed edit appears at multiple locations in the codebase. From the model’s perspective, the requested edit may be unambiguous, because it is reasoning about a specific function, block, or error location. But if the harness receives only a raw “replace old text with new text” request, and the old text occurs several times, it cannot reliably infer which occurrence was intended. Naïvely replacing all matches is dangerous. In practice, the safer behavior is for the harness to alert the model of the ambiguity and request clarification — for example, by asking it to expand the current context such that the text to be replaced is unique. This is a small implementation detail, but it sharply improves faithfulness between intended and executed edits. A second failure mode appears when the model proposes only partial lines or short fragments for replacement. Partial-text matching is attractive because it is flexible, but it is also brittle: the same fragment may appear inside comments, string literals, neighboring expressions, or unrelated code paths. Even when the fragment is unique, replacing text that does not constitute a full logical unit — a complete line or well-bounded span — can produce malformed edits. These may be syntactically correct from the editor’s point of view but semantically unintended from the model’s point of view. We found that requiring stronger text anchors — such as exact line spans, richer surrounding context, or line-aware matching — substantially reduces these accidental edits. Put differently, the harness should not execute underspecified edit requests by guessing. Third, even when an edit is applied successfully, simply returning “edit succeeded” leaves the model underinformed about what the harness changed. This weakens the reverse side of the interaction loop: not only should the model express intent clearly, but it should also be able to verify how that intent was interpreted. To close this loop, we found it useful, after every successful edit, to supply the model with a diff file — a text file indicating what additions and deletions had been made and what text stayed the same. A diff serves as an immediate confirmation channel: the model can inspect whether the replacement landed in the correct location, whether collateral lines changed, and whether follow-up edits are needed. This seemingly minor feedback mechanism improves reliability because it converts editing from a fire-and-forget action into an observable state transition. A natural question arises: if the diff is provided after a successful edit, why do the first two failure modes require special handling? While the diff does expose unintended changes, it does so after the mistake has already been applied. At that point, the model must decide whether to roll back, repair the unintended edits, or continue execution with a potentially corrupted state. This introduces additional branching in the agent’s trajectory and forces it to spend tokens and reasoning effort correcting avoidable errors, rather than progressing toward the solution. In other words, every correction step injects additional information into the model’s context window. Note that every piece of information competes for the agent’s attention for next-action generation. Unrelated or unintended edits do not just waste tokens; they actively degrade performance by introducing spurious patterns and relationships, increasing the likelihood that the model forms incorrect associations and drifts away from the original goal. In contrast, addressing ambiguity and weak anchoring before execution ensures that edits are applied correctly in the first place. This reduces unnecessary exploration, prevents cascading errors, and keeps the context focused on task-relevant signals. In effect, the first two failure modes improve correctness at the point of action, while diff feedback improves observability after action. Both are necessary, but they operate at fundamentally different stages of the interaction loop. Reasoning A less obvious but equally important design consideration is how agents balance internal reasoning with external interactions. Chain-of-thought reasoning is clearly valuable. It allows the model to decompose a problem, plan next steps, and decide which tool to invoke. Without sufficient reasoning, tool usage becomes reactive, leading to shallow exploration, redundant calls, or poor sequencing of actions. However, excessive thinking introduces its own failure mode. When the model spends too long reasoning internally, it begins to form assumptions about the environment rather than verifying them. These assumptions may appear coherent within the model’s internal state, but they are often misaligned with the actual system state. As a result, the agent may issue poorly grounded tool calls or skip necessary validation steps altogether, creating a fundamental tension. Effective agents must continuously reconcile these two demands, and we refer to this balance as tool calling with a reasoning nudge. The idea is to encourage the model to perform just enough reasoning to decide the next action and then prioritize evidence-gathering interactions with the environment over further reasoning. Rather than extending internal chains of thought, the agent is nudged toward validating its hypotheses through tool outputs. In practice, we did not find a single “golden prompt” that reliably balances reasoning and tool interaction across all model families. For the Claude variants, we found that introducing quantitative guidance — e.g., “make 50+ tool calls” or “ideal tool call count is 100” — helps break long reasoning chains and pushes the model toward interacting with the environment. While the exact number of target tool calls is not important, it serves as a useful north star that biases the model toward action. However, in our experiments, this strong nudge was ineffective for other families, such as Gemini and Grok, which often interpret such instructions literally and make empty tool calls in order to meet the target. Such behavior reduces agent quality. Here, we find that using a flexible nudge like “You should use tools as much as possible” works just fine. The principle remains the same: we need to nudge the model to proactively use tools along with right amount of reasoning. Tool use preferences Across agents, tools function in exactly the same way, but models tend to exhibit distinct preferences in how they invoke them. For example, GPT models prefer to update code by using an apply_patch command to splice in text from a separate file, formatted in a particular way; denying them their formatting preferences hurts performance. Similarly, for Grok-4.20, a single monolithic tool for editing and viewing creates confusion, which leads to incorrect tool calls. Splitting functionality into atomic operations yields better results — even when the functionality remains unchanged. Additionally, viewing line numbers in a file helps most models, but Grok’s tokenizer and attention mechanism appeared less robust at separating prefixes from line numbers, and disabling this feature helps the view tool. These preferences are a by-product of training. This reinforces a broader design principle: agent performance is a function of not only what tools are available but how naturally those tools align with the model’s learned behaviors. A well-designed harness meets the model where it is, adapting interfaces, feedback, and interaction patterns to its strengths while still enforcing the invariants needed for reliable execution. Benchmarking study SSA is a simple harness that implements many of the principles we describe above. We evaluated it on three agentic benchmarks — SWE-Bench-Verified (n = 500), SWE-Bench-Pro (public set, n = 731) and Terminal-Bench-2 (n = 89). Each example in SWE-Bench-Verified and SWE-Bench-Pro is an open-source code repository and an “issue” to be fixed by making a code change. Terminal-Bench-2 tackles a range of programming tasks (software engineering, machine learning, security, etc.) but is not tied to a code repository. All three benchmarks have individual, static, prewritten tests for evaluating generated code. In SWE-Bench-Verified and SWE-Bench-Pro, the runs and evaluations occur in separate container images, meaning changes must be transferred into a different evaluation environment; in Terminal-Bench-2, the evaluation happens in the same container. Therefore, in SWE problems, it may be necessary to exclude irrelevant artifacts to not overly bloat the diff patch. Additionally, Terminal-Bench-2 imposes computational and agent-runtime limits that the SWE benchmarks do not. We evaluate our SSA agents using metrics standard in the field. Note that the mini-swe-agent results reported above in the SWE-Bench-Verified graph and the Terminus results reported in the Terminal-Bench-2 graph correspond to a fixed agent configuration per benchmark — the exact same prompts, tool specifications, and structural output instructions. As we discuss above, however, different model families require different reasoning nudges and exhibit distinct preferences for tool use. As a result, while SSA’s core harness remains identical, there are minimal but nonzero differences in prompts and tool specifications across model families (e.g., Claude, Gemini, GPT, Grok). Our goal in building SSA was not to optimize separate agents per model but to identify minimal, orthogonal adaptations that allow different model families to express their strongest capabilities within a shared harness framework. Terminal-Bench-2 Unlike SWE-Bench-Verified and SWE-Bench-Pro, the Terminal-Bench-2 dataset restricts the agent’s environment by limiting computational capacity (memory, storage, number of CPUs) and time (both agent and verifier run times) per project. While this is effective in limiting disproportionate use of computational resources to boost benchmark scores, it does have the unintended side effect of making the benchmark more sensitive to infrastructure choices. We observed that, given those restrictions, the following system characteristics have the most impact: Reliability of the inference backend. The inference backend’s capacity (tokens per minute and requests per minute) should be able to support all concurrently run projects for the full duration of the evaluation. High variance in invoker latency, frequent API timeouts, and retries eat into the allowed time budget, leading to more timeouts and a lower resolution rate. The number of concurrent projects run on a single node. This affects the network bandwidth available to each project. One of the first steps for an agent in Terminal-Bench-2 is to install dependencies (popular libraries like pip, torch, transformers, etc.). If the evaluation infrastructure is set up in such a way that multiple projects are run on a single node (e.g., Harbor with n_concurrent > 1), the available network bandwidth for each node is shared across all the concurrent projects. This increases the download times for dependencies, leaving the agent with less time for problem solving and a higher risk of getting interrupted before it’s done. Since the majority of tool calls involve command-line instructions, a natural way to address timeouts is to introduce a batch interface, allowing the agent to execute multiple commands in a single turn, rather than executing them sequentially. In our experiments, however, the results of this approach were mixed and correspond to one of the failure modes we describe above — the balance between reasoning and tool interaction. While batching reduces interaction overhead, it also requires the model to maintain a coherent terminal state across multiple steps, which increases reasoning complexity. For Claude models, the time taken by additional autoregressive reasoning tends to offset the gains from batching. In contrast, for other model families (such as Gemini and Grok), batch execution was beneficial, as it did not trigger additional reasoning. Overall, under constrained settings, batching commands does not consistently improve performance across all models. Given that evaluations are sensitive to such confounding factors, we next assess the upper-bound potential of the agent-model combination by relaxing time constraints. Specifically, we compare SSA’s performance on Terminal-Bench-2 under constrained settings (as shown above) and unconstrained settings, where memory and agent timeouts are removed. The unconstrained setup serves as an estimate of the achievable performance ceiling. The gap in accuracy between the constrained and unconstrained evaluations is typically 5-10%. We note that in our experiments, out of the 89 total projects in Terminal-Bench-2, a few consistently have a high timeout rate in the constrained evaluation but a high solve rate in the unconstrained setting. Those projects are make-doom-for-mips, torch-pipeline-parallelism, gpt2-codegolf, caffe-cifar-10, and train-fasttext. Experimental methodology We evaluate SSA across multiple agent benchmarks under a controlled and reproducible setup. All experiments were conducted on an AWS PCS cluster using c7.48xlarge instances, with maximum concurrency set to 10 to balance throughput and system stability. For model access, Claude models were served via Amazon Bedrock (production capacity), while OpenAI, Gemini, and Grok models were accessed through their respective commercial APIs. We enforced strict evaluation hygiene. Internet access was disabled for SWE-Bench-Verified and SWE-Bench-Pro runs, while it was enabled for Terminal-Bench 2 due to its benchmark design. For SWE-Bench-Verified and SWE-Bench-Pro, we used the standard benchmarking Docker environments, which include repository state up to the point of the current code revision. This allows agents access to the relevant history of the codebase while ensuring no access to future revisions. Evaluation-specific issues In SWE-Bench-Verified, instances such as astropy-8872 and astropy-8707 fail even with flawless code patches due to setup inconsistencies and require fixes in the evaluation environment. Additionally, some psf_requests instances can fail intermittently due to external test dependencies (e.g., nonresponsive URLs), requiring manual patching for reliable evaluation. For SWE-Bench-Pro, evaluations were executed on Amazon ECS. Due to environment-specific assumptions, a small subset of tests — 3 out of 731 instances — consistently fail when run on AWS infrastructure, resulting in an approximate 0.41% ceiling loss across all SSA evaluations. Finally, to minimize information leakage during agent runs in Terminal-Bench-2, hidden tests are introduced into the Docker environment only after the agent has completed its execution, ensuring that the agent has no direct access to them during problem solving. Note that internet access in Terminal-Bench 2 does introduce a possibility of solution leakage, but a manual review of trajectories didn’t reveal any instances of the model trying to copy solutions. Model configs To ensure reproducibility, we used public documented configurations from release/model cards wherever available. Specifically, Claude Opus 4.6 and Claude Sonnet 4.6 were used with adaptive thinking and max effort across all benchmarks (except when Sonnet 4.6 was tested on Terminal-Bench-2 with thinking disabled). Opus 4.5 used high effort and no thinking across all benchmark runs (except in Terminal-Bench-2, where Opus 4.5 has thinking enabled with 128k budget tokens). Sonnet 4.5 was used with an interleaved-thinking budget of 200k, Haiku 4.5 with a 128k budget, and Sonnet 4.0 with a 200k budget across all runs. Both Gemini 3.0 Flash and Gemini 3.1 Pro used thinking_level high and temperature 1.0 across all runs. Every GPT model used reasoning effort xhigh for all benchmarking runs. With Grok, we used the grok-4.20 reasoning variant for all runs with default configs. Detailed config files for every experiment are included in the SSA package. Conclusion We show that bridging the intent and execution gap in agent harnesses is critical to extracting state-of-the-art performance out of frontier models. Well-chosen editing tools, feedback from tool application, and management of tool-output lengths improve performance across all model families. On the other hand, models exhibit distinct preferences for different tool interfaces, and an effective harness should leverage them instead of trying to uniformly impose the same interfaces across all model families. We open-source all elements of our harness — the agent logic, tools, and prompts, as well as model configs, for easy reproducibility in the SSA package. Acknowledgments: Luke Huan and Anoop Deoras

Today, the key challenge in AI isn’t only how to build better models; it’s how to build evaluation systems that can keep up. Search-augmented AI systems can now produce deep research reports — long, polished syntheses of many sources that increasingly resemble expert analysis. But those reports are useful only if their claims are supported by the underlying literature. Most existing fact-checking tools work best when a claim can be matched to a short quote or a single document. But in AI-generated research reports, a single sentence may combine evidence from several sources. It can depend on the surrounding report for context, and it might compare assertions in a way that no single source does on its own. When Amazon’s Artificial General Intelligence (AGI) group started working on the problem of evaluating AI-generated research reports, we thought that the main technical challenge would be building a stronger AI fact checker. But before you can evaluate an AI fact checker, you need a benchmark, a standardized test set used to measure performance. And in this setting, building the benchmark turned out to be at least as hard as building the model. Traditionally, we view the ground truth for a problem as a fixed dataset. But we discovered that to evaluate complex AI properly, ground truth has to become a process. We call that process audit-then-score, and we present it, together with two accompanying datasets, in a paper we recently published to arXiv. When static datasets break down In the standard method for measuring AI performance, human experts label examples, those labels become the “ground truth” (the undisputed correct answers), and models are scored against them. To test this approach with AI-generated research reports, we recruited PhD-level specialists from fields such as computer science, control theory, education, public health, and environmental engineering. We asked them to verify claims from reports in their own specialties, mixing in a hidden set of claims whose answers we already knew. The result was sobering. In a controlled study, unassisted experts achieved only 60.8% accuracy on the hidden set of known answers. The issue was not a lack of expertise. It was that assessing deep-research factuality is an unusually demanding task. Verifying a single claim can require long-context reading, cross-document synthesis, and sustained attention. Normally, in machine learning, when a model disagrees with a benchmark, we assume the model made a mistake. But we realized that, in cognitively demanding tasks like deep research, disagreement should not automatically be treated as a model failure. Sometimes, a model’s “error” is actually a signal that the benchmark itself is ambiguous, incomplete, or wrong. Audit, then score Instead of treating the initial expert labels as unquestionable ground truth, we decided to use the models to actively scrutinize the benchmark. This is the core idea behind the audit-then-score protocol. Our paper introduces the protocol alongside DeepFact-Bench, a shared test set for comparing systems, and DeepFact-Eval, a system that checks whether literature supports report claims. Here is how the protocol works: When our AI fact checker disagrees with the current benchmark answer, it is not simply penalized. Instead, it acts as a challenger and must submit concrete evidence and a written rationale for why it thinks the original human answer is wrong. An auditor — which can be a human expert — then steps in. Crucially, auditors do not start from scratch; they compare the challenger’s new evidence directly against the benchmark’s original rationale. If the challenger makes the stronger case, we revise the benchmark before we score the model. DeepFact-Eval reads the full report context, plans searches to cover the relevant literature, summarizes retrieved documents, and asks follow-up questions when key details are missing. It then produces both a verdict and a written explanation. This fundamentally changes what a benchmark is. A new role for human expertise One of the most striking things we found is that the same experts who were unreliable as one-shot labelers became far more reliable when placed in the role of auditor. Across four rounds of audit-then-score, accuracy on our hidden test set rose from 60.8% to 90.9%. When experts start from a blank page, they have to find the evidence, interpret it, and make a judgment on their own; when they audit a disputed claim, they can focus on comparing two concrete cases. This shift had significant impact. On DeepFact-Bench, DeepFact-Eval reached 83.4% accuracy when we used GPT-4.1 as the underlying model. That was higher than the 58.5% of the best traditional fact-checking system we tested and the 69.1% of a strong prior deep-research system. Evaluation as an evolving infrastructure This shift has implications beyond one paper or one task. If AI systems continue improving, to the point that they exhibit humanlike expertise, the community will increasingly run into settings where evaluation based on one-time human answers is not enough. In those settings, sustaining benchmark quality may require auditing, revision, calibration, and periodic revalidation. Evaluation will become an ongoing collaboration among humans, models, and the evidence they surface together. Acknowledgments: Yukun Huang, Leonardo F. R. Ribeiro, Momchil Hardalov, Markus Dreyer

Routing in today’s data centers is usually governed by a data structure called a “fat tree”, which is similar to a corporate organizational chart, with nodes in each layer connecting to multiple nodes in the layer below. Here, however, the nodes of the bottom layer represent routers that want to send messages to each other, and the layers above them contain extra routers that simplify the routing procedure. A message sent by one bottom-layer router climbs the tree until it reaches the branch that leads to the destination router, and then it is sent down. This design is easy to implement but inefficient: the extra layers of routers add overhead, and routers at the top of the tree are prone to congestion. The fat-tree structure is also fragile, since the loss of a single router can cut off large regions of the tree. Theoretically, the best alternative is a “flat” network, in which the routers connect directly to each other. Ideally, one should connect the routers randomly, to maximize the diversity of routes through the network. But this is impractical, because calculating ad hoc paths through a random network is computationally intensive, and randomly connecting routers leads to data centers criss-crossed with wires. In a paper we recently posted to arXiv, we describe the first ever scalable flat-network datacenter. We introduce a “quasi-random” network topology that preserves many of the benefits of random connection and a passive optical component we call a ShuffleBox, which makes it practical to cable a flat network. The resulting network design — which we call RNG, for resilient network graphs — is now used in AWS data centers and is the default for most new builds globally. It uses 69% fewer routers, delivers up to 33% better throughput, and projects a 40% reduction in network equipment electricity consumption. The secret of randomness In the early 1990s, mathematicians showed that the optimal network for routing has a random topology, in which each router simply connects randomly to a few others. This is quite counterintuitive, but the overall network ends up having lots of different paths between all pairs of routers. Random networks also demonstrate excellent resilience, since no single router is more important than any other. The loss of 1% of routers results in a roughly 1% capacity loss. Degradation is proportional and predictable rather than catastrophic and concentrated. Networking researchers have also validated these results through simulations, showing that random, flat topologies achieve better performance than the corresponding fat trees. But these results couldn’t make it in the real world. Any network design comes with a “routing protocol” that decides how packets reach their destinations. In a random network, computing and implementing the right set of routing paths can take a lot of hardware resources — well beyond what is present in commodity routers. On the other hand, using dedicated hardware for routing would be cost prohibitive. An even bigger problem is that cabling routers randomly in a datacenter is completely infeasible. Our solution is to build a “quasi-random” network topology that has exactly the right mix of random and deterministic components. Routing without structure In a fat tree, the hierarchy itself tells packets where to go. And the paths generated are guaranteed to be the shortest possible. In a quasi-random graph, there is no obvious structure to exploit. Standard approaches to multipath routing in flat topologies typically require 20 to 80 times more memory than commodity hardware is equipped with. Our key insight is that we can exploit the random structure of the topology to open up a wide range of path options in a lightweight manner. Our routing algorithm, Spraypoint, has two components. The source router “sprays” its traffic randomly to all of its neighbors. Every (destination) router has some designated “waypoints” that feed traffic to it. The main scheme is that each data packet sent from the source goes to a random neighbor, after which the classic shortest-path algorithm routes it to a waypoint, and the waypoints feed it to the destination. The utility of spraying is that traffic can take a wide variety of paths to the destination, while the waypoints prevent traffic from congesting near the destination. In the implementation, we create various “rings” around each destination, and traffic is guided from each ring to a closer ring. By spraying to neighbors, Spraypoint provides nearly twice as many independent paths between routers as standard shortest-path routing techniques. This improves the likelihood that traffic will be routed around congested pathways or failed routers. Making quasi-random cabling practical A random graph connects arbitrary pairs of routers that may sit in different rooms, hundreds of meters apart. This is the strength of the topology, since it allows for fast communication between routers. But that is also its drawback, since cabling such a structure is extremely complicated. This is where our quasi-random solution comes in. Instead of all connections being random, we fix specific parts of the network topology. Our central innovation is a passive optical device called a ShuffleBox. It has router-facing ports on one side and connects to other ShuffleBoxes on the other side. The internal wires are shuffled according to a special pattern, so that random connections between the ShuffleBoxes lead to an overall quasi-random topology. When a new rack arrives, a technician plugs its router into an available port on the local ShuffleBox. No rewiring elsewhere. The physical-cabling complexity, the number of cable runs, and the installation process are on par with those of a fat tree, even though the logical topology is quasi-random. Predicting performance before construction With any new network topology, operators need confidence that it will meet capacity and performance requirements before they commit to construction. Fat-tree topologies come with simple, well-defined models that predict performance and capacity constraints. No equivalent existed for quasi-random graphs. We developed new mathematical models for various network statistics, such as path lengths, the number of routes, and how much traffic will end up on a particular link. These models give precise formulas that network operators can use to choose design parameters. We validated those models extensively, using 530 processor-years of simulation, the equivalent of running a single CPU for half a millennium, executed on Amazon EC2. An operator can now specify a server count and a target performance level, compute the cheapest compliant topology, and be confident that it will work. From theory to production The first quasi-random network went live near Dublin, Ireland, at the end of 2024, carrying real production traffic. We validated performance against the mathematical predictions, identified operational refinements, and applied them in two additional deployments. In end-to-end benchmarks across these production fabrics, our flat topology matched fat-tree performance for multipath-transport workloads and latency-sensitive storage operations. No customer workload changes were required, and the network operates transparently beneath existing applications. By April 2026, quasi-random wiring became the default architecture for most new AWS data centers globally. The 69% reduction in the number of routers translates directly into reduced power, cooling, and operational overhead at every site. For customers, it means more resilient infrastructure behind every API call, database query, and machine learning training job, without changing a single line of code.