Text-to-speech models based on large language models (LLMs) have gotten very good at producing natural-sounding speech, even in voices cloned from short audio files. But some problems with these models still persist. One is accent leakage in polyglot text to speech. It should be possible to transfer a voice recorded in English to French, German, or Spanish with the correct accent and without loss of voice identity. But with most systems, the reference speaker's native accent leaks into the target language, or the target language's accent overwrites characteristics of the speaker’s voice. Expressiveness is another challenge, including the laughs, sighs, hesitations, and other indications of emotion that make speech engaging. And then there’s reliability. Unlike traditional text-to-speech (TTS) systems, LLM-based systems are autoregressive, meaning they generate speech tokens one at a time, without explicitly modeling duration. This can cause hallucinated repetitions, unexpected cutoffs, and inconsistent pronunciation. At Amazon, we're working to address all these issues. Mitigating accent leakage in polyglot TTS We use a locale-specific data augmentation approach to address the problem of accent leakage. Specifically, we use low-rank adaptation (LoRA) to fine-tune our polyglot models on data that is heavily weighted toward target locales. This also allows us to do accent-free polyglot voice cloning: the cloned voice speaks the target language with native-like pronunciation but without loss of speaker identity. Improving expressiveness We use classifier-free guidance (CFG) to generate synthetic reference audio samples with enhanced expressiveness. Using these as conditioning during inference pushes the model toward more expressive prosodic styles. Originally developed for diffusion modeling, CFG controls how strongly generation follows conditioning. CFG-based reference samples decouple speaker identity from accent, teaching the model to preserve voice characteristics while adopting native pronunciation in the target language. This allows us to scale a small number of recorded voices to many new locales and languages, while increasing expressiveness. Scored according to MUSHRA (multiple stimuli with hidden reference and anchor) listening tests, the quality of our models’ polyglot outputs across nine locales spanning English, French, Italian, German, and Spanish improved 5% to 20% over those of our previous model family. LocaleImprovement over baselineUS-English+12.43%Southern US-English+20.05%Great Britain-English+5.97%Australia-English+5.50%US-Spanish+11.78%Spain-Spanish+13.23%France-French+8.44%Germany-German+14.12%Italy-Italian+9.80%Robustness Traditional TTS had failure modes, but hallucination and random truncation weren't chief among them. LLM-based TTS can generate confident-sounding speech that doesn't match the input, and it will sometimes stop mid-sentence. Chain-of-thought for autoregressive TTS Traditional TTS pipelines have explicit stages: grapheme-to-phoneme conversion, duration prediction, and acoustic generation. More recent, non-autoregressive end-to-end models like FastSpeech predict durations explicitly before speech generation. LLM-based TTS takes an alternate approach. Duration emerges implicitly from autoregressive generation. There's no explicit plan for how long the utterance should be or how long each phoneme should take. This is why these models hallucinate (keep generating past the intended content) or truncate (stop too early). To address this problem, we add chain-of-thought reasoning to the model: before generating speech tokens, the model predicts phoneme sequences and estimates duration (total length and per-phoneme timing). This isn't the same as traditional TTS pipelines. Bolting duration prediction onto an autoregressive architecture is a different problem than building it into a non-autoregressive one, and it has its own challenges. Phoneme prediction enables the model to handle heteronyms ("read," "lead") and unusual names more reliably. Duration prediction gives the model a timing plan, which reduces both hallucination and truncation. These predictions are also useful for debugging, as you can see what the model "thought" it was going to generate before it started generating. Guardrails Our guardrails use the chain-of-thought predictions as checkpoints. We know the expected phoneme count and approximate speech duration before generation starts. After generation, we do a pair of checks: does the output duration match the prediction, and is the output length reasonable given the phoneme count? Large deviations flag likely hallucinations or truncations. When an agent detects problems, it can prompt the TTS system to regenerate with different sampling parameters or fall back to alternative approaches. Data filtering To filter the text data passing to the TTS model, we combine speech-recognition-based metrics with metrics based on the LLM’s attention mechanism. Automatic speech recognition (ASR) catches actual transcription errors. Taken together, the metrics keep data that's genuinely well aligned while preserving expressiveness that ASR-only filtering would discard. On generic long-form text, our full array of techniques reduces critical errors to an average of less than one second per hour, where “critical errors” include hallucinations, cutoffs beyond one word, and mismatches between input text and output speech. Conclusion LLM-based TTS models sound noticeably more natural than traditional systems. However, in our experience, they introduce new failure modes that need to be addressed before they can be deployed reliably in production. We have found that LoRA-based fine tuning addresses the heavy accent leakage observed in polyglot TTS, while classifier-free guidance is a useful tool for improving expressiveness. As for reliability, we find that smart data filtering and chain-of-thought reasoning coupled with guardrails and agentic regeneration can significantly reduce hallucination.

Cryptographic encryption algorithms are mathematical procedures that transform readable data into ciphertext that looks like a stream of random bits. The ciphertext can be decrypted only with the corresponding decryption algorithm and the correct key. For data at rest — information stored on disks or in databases — algorithms like AES-XTS encrypt each block before it’s written to storage, protecting against physical theft or unauthorized access to storage systems. For data in transit — information traveling across networks — protocols like TLS combine multiple algorithms: asymmetric encryption algorithms (RSA or elliptic curves) establish secure connections, while fast symmetric encryption algorithms (like AES-GCM) protect the actual data stream and verify that it hasn't been tampered with. At Amazon Web Services (AWS), we use AES-XTS to protect customer data in services like EBS, Nitro cards, and DynamoDB, while TLS with AES-GCM secures all network communication between services and to customers. We took on the challenge of formally verifying an optimized Arm64 assembly implementation of AES-XTS decryption, where “formal verification” is the process of proving mathematically that an engineered system meets a particular specification. Our work follows the IEEE Standard 1619 for cryptographic protection of block-oriented storage devices and focuses on the AES-256-XTS variant of AES-XTS. The “256” specifies the size of the encryption key. Unlike algorithms that process fixed-size blocks, AES-XTS handles variable-length data from 16 bytes up to 16 megabytes, with special logic for incomplete blocks. The assembly code verified was a 5x-unrolled version, meaning that its loops were executed in parallel across five registers (each containing an input block), and it had been optimized for modern CPU pipelines. It was complex enough that manual review couldn't guarantee correctness yet critical enough that errors could compromise customer data security. As part of Amazon Web Services’ s2n-bignum library of formally verified big-number operations, we contributed an improved Arm64 assembly implementation of AES-XTS encryption and decryption, as well as specification and formal verification using the HOL Light interactive theorem prover, which was developed by a member of our team (John Harrison). This was an experiment in the proof-driven development of a large function with multiple paths based on the input length. It resulted in the largest proof so far in the s2n-bignum library. For the typical input size of 512 bytes, the performance of the algorithm either stayed close to that of original code or improved slightly on highly optimized Arm cores. By adding this algorithm and its proof to the s2n-bignum library, we pave the way for more AES-based algorithms to be added. Description of the algorithm AES is a block cipher that implements a keyed permutation. This means that it processes the plaintext files in blocks (in this case, blocks of 128 bits), and for any given key, it defines a bijective (one-to-one and invertible) function mapping each plaintext block to a unique ciphertext block. This mathematical property ensures that decryption can uniquely recover the original plaintext. AES-XTS is the mode specifically designed for storage encryption. It uses AES as its underlying building block but adds position-dependent tweaks and ciphertext stealing — a method for handling partial blocks — to address the unique requirements of disk encryption, where you need random access to any sector and must preserve the exact data size. AES-XTS encrypts storage data using a two-key approach where each 128-bit block and its position-dependent tweak are subjected to an exclusive-OR operation (XOR), a binary operation that outputs a one only if the input values differ. The result of the operation is encrypted with AES, then XORed with the tweak again, ensuring that identical data at different disk locations produces different ciphertext. The tweak is generated by encrypting the sector number with a second key, then multiplying by powers of α in a Galois field, creating unique values for each block position. When the final block isn't a full 128 bits, ciphertext stealing kicks in. Ciphertext stealing borrows bytes from the previous block, allowing encryption of data of any length without padding or wasted space. This lets you read or write any sector independently — critical for disk encryption — while basing each block's encryption on its position. That is a desired feature since the security model of disk encryption allows the adversary to access sectors other than those in question, modify them, and request their decryption. It also ensures that the size of the ciphertext is exactly the same as that of the plaintext, so it fits in its place. Control flow of the assembly implementation We started from an existing implementation of AES-XTS in Amazon’s AWS-LC cryptographic library. AES-XTS loops through the plaintext in 128-bit blocks, and encryption of each block requires 15 steps, each with its own “round key” derived from the encryption key. The existing implementation is 5x unrolled, meaning it processes blocks in parallel, five at a time. If the final block is less than 128 bits in length, there’s a risk of “buffer overread”, or reading beyond the limits of the input buffer. To avoid overread, the existing implementation does complex manipulation over the pointer to the current location in the input buffer. This requires a sophisticated control flow that can be hard to follow: the loop counter is incremented and decremented multiple times before and during the loop, and the loop has two additional exit points other than the final loop-back branch. One exit point is for the case when four blocks remain during the final iteration of the loop; the other exit point is for the case of one to three blocks remaining. The flow of the loop interleaves the load/store instructions with the AES and XOR instructions in an effort to maximize pipeline usage. After the loop exit, the processing of the remaining blocks is intertwined for the lengths of four down to one; if there’s a partial block at the end, the algorithm performs the ciphertext-stealing procedure. Additionally, only seven of the 15 rounds’ keys were kept in registers; the other eight were repeatedly loaded from memory in the loop and outside it. We first investigated whether we could improve the performance of the main loop by letting SLOTHY, a superoptimizer for Arm code, rearrange the instructions to maximize pipeline usage. SLOTHY contains simplified models of various Arm microarchitectures. It uses a constraint solver to provide optimal instruction schedule, register renaming, and periodic loop interleaving. However, for SLOTHY to identify and optimize a loop, the loop has to exhibit typical loop behavior, decreasing the counter at the end of each iteration and then jumping back to the beginning. SLOTHY also cannot handle the nested loop created by loading the eight-round keys. This gave us a reason to start “cleaning up” the loop. First, we freed up registers to permanently hold all round keys; this was possible as the optimized order of instructions required fewer temporary registers than the original code. Second, we removed the multiple exit points and the manipulation of the loop counter to handle the remaining blocks. The value of the counter always indicates the number of five-block chunks remaining in the buffer, conforming to SLOTHY’s requirement; the loop ends before the handling of the remaining blocks. Once the loop ends, we have a separate processing branch to handle each possible number of remaining blocks, from one to four; all four branches end in ciphertext stealing. This can be seen in the control flow graphs of the encrypt and decrypt algorithms (see below). Throughout the code, we maintained the constant-time design mindset; that is, branching and special processing are based not on secret data but only on public values, the input byte lengths. Performance With our modifications to the code, we were able to use SLOTHY to optimize the encrypt algorithm. This resulted in slight performance gains on the AWS Graviton family of Arm processors, although the gains were smaller on the more advanced chips, which have an optimized out-of-order pipeline. Compared to the original implementation, keeping round keys in registers throughout the algorithm’s execution, to save on loading them from memory, allowed us to offset the effects of not interleaving the AES instructions with other ones. Having a cleaner flow of instructions in the loop and modular exit processing allowed us to experiment with various unrolling factors for the loop iterations. We experimented with 3x, 4x, and 6x factors and concluded that 5x is still the best choice across various microarchitectures. Ensuring correctness through formal verification To deploy optimized cryptographic code in production, we need mathematical certainty that it works correctly. While random testing quickly checks simple cases, we rely on formal verification to deliver the highest level of assurance for our AES-XTS implementation. Why HOL Light for AES-XTS? To prove that our implementation matches the IEEE 1619 specification, we use HOL Light, an interactive theorem prover developed by our colleague John Harrison. HOL Light is a particularly simple implementation of the "correct by construction" approach to software development, in which code is verified as it’s written. HOL Light’s trusted kernel is just a few hundred lines of code, which implements basic logical inference rules. This means that even if there's a bug in our proof tactics or automation, it cannot cause HOL Light to accept an incorrect proof. At worst, a bug prevents us from completing a proof, but it cannot make a false statement provable. We chose HOL Light for several reasons specific to AES-XTS verification: Assembly-level verification: We write our implementations directly in assembly rather than relying on compiled code. While more challenging, this makes our proofs independent of any compiler. HOL Light reasons directly about machine code bytes using CPU instruction specifications, providing assurance at the lowest level of the software stack. Existing cryptographic infrastructure: S2n-bignum already provides extensive support for cryptographic verification, including symbolic simulation that strips away execution artifacts and leaves purely mathematical problems, specialized tactics for word operations, and byte list handling. We add proven lemmas about AES operations that we can reuse for the proofs of other AES modes. Complex control flow handling: Unlike fully automated provers that might fail on complex proofs without enough explanation, HOL Light's interactive approach lets us guide proofs through the intricate invariants required for our 5x-unrolled loops, processing arbitrarily long blocks of data and performing the complex memory reasoning required by variable-length inputs and partial blocks. The s2n-bignum framework Using s2n-bignum to implement AES-XTS serves two purposes: it's both a framework for formally verifying assembly code in x86-64 and Arm architectures and a collection of fast, verified assembly functions for cryptography. The library already contains verified implementations of numerous cryptographic algorithms, especially those pertaining to big-number mathematical operations (hence the name), which are the foundation of public-key cryptographic primitives. For details on how HOL Light was used to prove public-key algorithms as part of s2n-bignum, please refer to the previous Amazon Science blog posts “ Formal verification makes RSA faster — and faster to deploy” and “Better-performing ‘25519’ elliptic-curve cryptography”. As we mentioned, AES-XTS is one of the modes of the AES block cipher. AES is based on a substitution-permutation network (SPN) structure, which combines substitution operations (SubBytes using the S-box), permutation operations (ShiftRows, MixColumns), and key mixing. By expanding s2n-bignum to include the AES instruction set architecture (ISA) found in Arm64 and x86_64 processors, specifications for the AES block cipher, and additional specifications for AES-XTS, we're paving the way for the same rigorous verification of more AES-based algorithms. Developing and testing the specification The SPN nature of AES and the modes that are based on it cannot be expressed using simple mathematical formulae — such as modular multiplication, which is fundamental to public-key cryptography — that can be innately understood by a theorem prover. They require writing descriptions of the steps for processing the data. This is why, before verifying the assembly, we needed confidence that our HOL Light specification accurately captured the IEEE standard. We wrote the specification to mirror the standard's structure, using byte lists for input/output and 128-bit words for internal block operations. Then we developed conversions, HOL Light functions that we used to evaluate specifications with concrete inputs while generating proofs that the evaluations are mathematically correct. We validated our specification by conducting unit tests that cover different AES-XTS encryption/decryption scenarios, exercising the processing of all blocks (using recursion) and ciphertext stealing. These tests confirmed that our specification matched the IEEE standard before we tackled the more complex assembly verification. This two-phase approach — first ensuring that the specification is correct through testing, then formally verifying that the implementation matches the specification — gave us confidence we were proving the right thing. The proof strategy Our proofs are compositional, meaning they break the overall problem into subproblems that can be proved separately. Depending on the subproblem, the subproofs can be bounded — true only for a range of inputs — or unbounded. For inputs with fewer than five (or six, in the case of decrypt) blocks, we wrote bounded proofs that exhaustively verify each case. For inputs with five (six, in the case of decrypt) or more blocks, we developed loop invariants — mathematical statements that remain true throughout loop execution — to prove correctness for arbitrarily long inputs. The loop invariants track three critical factors until the loop exit condition is met: register states at each iteration, the evolution of "tweaks" (which make each block's encryption unique), and memory contents as blocks are processed. For partial-block (tail) handling, we proved a separate theorem for ciphertext stealing that could be reused across all cases. The top-level correctness theorem composes all proofs together, asserting the following statement: Memory safety and constant-time proofs Most recently, s2n-bignum was equipped with new functions and tactics for formally defining the constant-time and memory safety properties of assembly functions. With these resources, many assembly subroutines in s2n-bignum were verified to be constant time and memory safe, including top-level scalar-multiplication functions in elliptic curves, big-integer arithmetic for RSA, and the Arm implementation of the ML-KEM cryptography standard (the subject of a forthcoming blog post on Amazon Science). All assembly subroutines identified for use in AWS-LC as of October 2025 were formally verified to be constant time and memory safe. We are exploring whether the new tactics can easily be used to verify assembly subroutines that have subsequently been added, such as AES-XTS. As we mentioned, AES-XTS has a remarkably complex control flow, which resulted in a long and involved functional-correctness proof. That complexity is also a challenge for safety proofs. The process is ongoing, but we have already proved safety properties for the ciphertext-stealing subroutines of the decryption and encryption algorithms. These first proofs focused on crucial memory access procedures that are prone to buffer overread. Proofs for the remaining parts of the decryption and encryption algorithms can use the same methodology, where the constant-time and memory-safety proofs follow the same structure as the functional-correctness proofs but are simpler, since their proof goal is more focused. Continuous assurance of correctness We've integrated formal verification into s2n-bignum's continuous-integration (CI) workflow. This provides assurance that no changes to our AES-XTS implementation can be committed without successfully passing a formal proof of correctness. As part of CI, the CPU instruction modeling is validated through randomized testing against real hardware, "fuzzing out" inaccuracies to ensure our specifications are correct and the proofs hold in practice. Furthermore, the proof guarantees correctness for all possible inputs, since they’re represented in the proof as symbols. This overcomes the typical shortcoming of coverage testing, which may cover all paths of the code but may not be able to cover all input values. For example, a constant-time code, like the one used here, is written without branching on secret values. Typically, then, secret values are incorporated into the operation through the use of masks derived from them. The same instructions are executed irrespective of the secret value. Hence, achieving line coverage is usually within the reach of a developer, but achieving value coverage is left to the formal verification of correctness. This same methodology has enabled AWS to deploy optimized cryptographic implementations with mathematical guarantees of correctness while achieving significant performance improvements. This allows the developer and tools to further optimize the code freely without worrying about introducing bugs, since these will be automatically caught by the proof. Our experience with AES-XTS shows that proof-driven development of assembly code yields a control flow that is easier to understand, review, maintain, and optimize while never ceasing to be provably correct.

Fine-tuning a large language model (LLM) on a specific task requires updates to billions of parameters across trillions of tokens, with the attendant costs in GPU resources and time. Low-rank adaptation (LoRA) is a more efficient alternative that freezes the original model weights but introduces lightweight matrices into specific model sublayers, or “modules”. These matrices (commonly referred to as “adapters”) modify the modules’ weights, enabling not only efficient fine tuning but also on-demand model serving, which dramatically lowers inference costs; base-model sharing across GPUs, which cuts memory requirements; lower download overhead; and parallel inference across multiple adapters. The question is where to insert these adapters across the model. Empirically, targeting more and larger modules tends to boost performance, because it allows more flexibility in customization; but it also increases training and inference costs. Using a smaller, well-chosen subset preserves most gains with significantly better efficiency. Using Amazon’s Nova 2.0 Lite multimodal reasoning LLM as our base model, we set ourselves the goal of identifying a subset of standardized target-module configurations that works effectively across the vast majority of customer use cases. Through an ablation study, we identified a module known as o_proj, as the single module where adding an adapter achieves the best trade-off between efficiency and accuracy (o_proj is a linear transformation that mixes representations across attention heads into a single, cohesive form for the rest of the model to understand). The Transformer architecture Transformer models — the models responsible for all of AI’s remarkable recent gains — consist largely of blocks that are repeated multiple times. Each block in turn has two main components: an attention mechanism, which determines the relevance of previously seen tokens to the token currently being processed, and a feed-forward network, a conventional neural network that does additional processing on the outputs of the attention mechanism. The attention mechanism involves three different matrices, which take their names from database design: the query matrix represents how relevant the current token is to the other tokens in the input sequence; the key matrix represents how relevant other tokens are to one another; and the value matrix represents the raw content of those other tokens. Multiplying the three matrices together creates, essentially, a recipe for the Transformer's next output. To reduce computational complexity, these multiplications take place in a space with reduced dimensions. The matrices themselves and the results of their multiplication then have to be projected back up to the original dimensions of the input. LoRA approximates weight updates using a product of two smaller matrices, drastically reducing the number of trainable parameters. The technique is typically applied to attention projection layers and feed-forward network layers. These modules are ideal candidates because they constitute the bulk of Transformer parameters, directly govern representation learning, and exhibit natural alignment with low-rank approximations. Empirical evidence shows weight changes in these layers often lie within a low-dimensional subspace during fine tuning. Target module selection Selecting the right target modules directly affects accuracy, latency, and computational efficiency. The optimal choice of target modules is primarily a function of (a) the base model being fine-tuned (i.e., its architecture, pre- and post-training data distributions, etc.) and (b) customization domain/modality. When fine-tuning Nova 2.0 Lite, we balanced two competing objectives: Maximizing accuracy across diverse tasks and modalities and Minimizing latency to preserve LoRA's efficiency benefits. We investigated the application of LoRA to four different modules in each Transformer block: the query, key, and value projection layers ( qkv); the o_proj layer; and two different fully connected layers in the feed-forward network, gate_up_proj and gate_down_proj (referred to as fc1 and fc2). Below are the trade-offs for these modules, both singly and in combination, based on results published in literature and empirical studies. CombinationExpected accuracyExpected latencyUse caseqkv onlyGood (baseline)Lowest Resource-constrained environments Tasks where attention mechanisms are critical (e.g., classification, lightweight generation) Prioritizes speed over maximum accuracy o_proj onlyModerateLowest Ultralow-latency scenarios Tasks where refining attention outputs is sufficient (e.g., simple sentiment analysis). Plays an important role in reasoning Less effective than qkv, but very efficient qkv + o_projHighLow to moderate (+5–10%) Attention-focused tasks (e.g., machine translation, summarization) Balances refinement of both attention context ( o_proj) and query/key/value projections ( qkv) Best accuracy-to-latency ratio for most NLP tasks qkv + fc1 / fc2Very high (close to full fine tuning)Moderate (+10–15%) Complex generation tasks (e.g., translation, long-form summarization) When feed-forward layers ( fc1/ fc2) significantly influence output quality as they store and retrieve factual knowledge Prioritizes accuracy over speed o_proj + fc1 / fc2Good to highModerate (+5–10%) Tasks requiring adaptation of both attention output ( o_proj) and feed-forward layers (e.g., text classification, sentiment analysis) Suitable when qkv adaptation is unnecessary qkv + o_proj + fc1 / fc2Highest (near-full fine tuning)High (+15–20%) Maximum accuracy for critical tasks (e.g., research benchmarks, high-stakes generation) When all components of the Transformer block need adaptation Avoid for production if latency matters All modules ( qkv, o_proj, fc1, fc2)MaximumHighest (+20–25%) Prototyping/research with no latency constraints Rarely justified in practice; marginal gains over qkv + o_proj + fc1/ fc2 Trade-offs of accuracy and latency across target modules, based on literature review and empirical evidence. Experimental methodology We conducted a comprehensive ablation study, training multiple supervised-fine-tuning (SFT) LoRA variants on seven datasets spanning both text and visual data, across reasoning (i.e., the training datasets themselves include reasoning content) and non-reasoning tasks. The datasets covered diverse challenges from simple question answering to long-context summarization and structured JSON extraction. DatasetModalityReasoning tracesDomainTasksTraining sizeEval sizeEval metricSourceFinCOTTxtYesFinanceFinancial-reasoning dataset. Samples consist of complex financial queries, along with reasoning traces obtained from GPT-4o. Predictions are typically complex tables or calculations based on the input.74361147Accuracyhttps://huggingface.co/datasets/TheFinAI/FinCoTGovReportTxtNoGoverment DocLarge-context (30-40K tokens) summarization17457837RougeLsumhttps://gov-report-data.github.io/MedMCQATxtNoMedicalDataset for multiple-choice QA — also used in Nova 1.020k3683Accuracyhttps://huggingface.co/datasets/openlifescienceai/medmcqaMedReasonTxtYesMedicalMedical-reasoning dataset that consists of questions and answers compiled from various medical benchmarks (MedQA, MedMCQA, etc.), along with synthetic, high-quality reasoning traces. (This uses the same eval set as MedMCQA.)316823683Accuracyhttps://huggingface.co/datasets/UCSC-VLAA/MedReasonCoCoHDTxtNoPolitical DocA complex benchmark consisting of large-context (>20K tokens) transcripts of congressional hearings. The output is expected to be a summary in a specific JSON format, consisting of the members present, topic discussed, outcomes, etc.7321053Averaged key and value match ratehttps://github.com/gtfintechlab/CoCoHDLlava-COTImageYesImage understanding, General/ScienceMultimodal, image benchmark consisting of Q&A reasoning questions. The dataset includes high-quality reasoning traces.10k270Exact match ratehttps://huggingface.co/datasets/Xkev/LLaVA-CoT-100kInvoice OCRImageNoImage understandingOCR benchmark that takes an input image and produces a JSON file with fields from the image.1400447AccuracySummary of the experiment datasets All experiments used the Nova 2.0 Lite general-availability checkpoint with consistent hyperparameters across target modules, including learning-rate ratio and alpha values. Target datasetSettingSFT LoRA target performanceNova 2.0 Lite performanceFin-COTqkv67.09%72.12%o_proj68.30%fc175.35%fc260.24%o_proj + fc161.38%qkv + fc260.31%o_proj + fc262.79%qkv + fc168.37%All target modules66.15%CoCoHDqkv19.64%45.14%o_proj65.88%fc141.96%fc217.62%o_proj + fc176.83%qkv + fc266.47%o_proj + fc279.14%qkv + fc145.45%All target modules82.75%GovReporto_proj41.25%38.90%fc139.69%o_proj + fc141.74%o_proj + fc242.16%qkv + fc141.66%qkv + fc239.02%All target modules41.95%Llava-COTqkv64.26%16.22%o_proj64.26%fc165.92%fc265.02%o_proj + fc163.21%qkv + fc262.76%o_proj + fc266.37%qkv + fc166.52%All target modules63.96%Invoice OCRo_proj89.07%14.10%o_proj + fc190.03%qkv + fc287.84%o_proj + fc289.47%qkv + fc188.55%All target modules90.11%MedReasono_proj24.55%1.68%o_proj + fc120.88%qkv + fc28.39%o_proj + fc220.36%qkv + fc14.32%All target modules26.72%MedMCQAqkv62.18%1.68%o_proj63.10%fc112.90%fc259.98%o_proj + fc161.39%qkv + fc265.63%o_proj + fc264.95%qkv + fc157.21%All target modules66.11%Ablation study for target module selection. Some benchmarks have fewer variations, to save on computation and time. MedMCQA and MedReason use the MedMCQA test set for evaluation. On this task, Nova 2.0 Lite fails mainly due to formatting inconsistencies, even though it produces the right answer. For consistency’s sake, we use the same strict parser for SFT models. Key findings 1. O_proj is the most robust single target The o_proj-only configuration demonstrated remarkable consistency, never failing outright on any task and typically performing within a few percentage points of the best configuration (i.e., using all target modules). On MedMCQA, CoCoHD, GovReport, LLaVA-CoT, and Invoice OCR, o_proj-only either matched or came very close to optimal performance, making it an attractive default choice that balances performance and simplicity. There is emerging evidence that this module plays a key role in reasoning, which may explain its effectiveness here. 2. Qkv-only shows instability While qkv-only performed well on MedMCQA, it exhibited extreme variability, performing below baseline on CoCoHD and showing unremarkable results elsewhere. This aligns with the hypothesis that attention-only LoRA can underfit on tasks requiring richer features from the feed-forward network, rather than relying on modified token routing. 3. Module combinations provide modest gains Combinations like o_proj + fc2 or "all target modules" often achieved the highest per-dataset scores (particularly on CoCoHD, MedReason, and Invoice OCR). However, improvements over the best single module were typically modest, usually 1-3 percentage points. 4. Task difficulty amplifies configuration impact On challenging benchmarks where the base model performed poorly, the choice of target modules had greater impact. For example, on CoCoHD (long-context, complex JSON generation), o_proj + fc2 achieved a +15% absolute improvement over the base model, compared to only +3% with o_proj alone. 5. LoRA consistently outperforms base models Across nearly all datasets, any reasonable LoRA configuration dramatically outperformed the base model. For instance, MedReason, MedMCQA, LLaVA-CoT, and Invoice OCR showed improvements from a baseline accuracy of ~1-16% to 60-90%+ with LoRA. The notable exception was Fin-COT, where only certain configurations (notably fc1) exceeded baseline performance, suggesting task-specific sensitivity to adaptation strategy. Recommendations For accuracy-prioritized scenarios, we recommend o_proj + fc2 as the optimal configuration for both text and multimodal tasks, showing 2-12% improvements over o_proj alone across benchmarks. For balanced efficiency and performance, o_proj-only provides an excellent default, offering robust performance with minimal latency overhead — particularly valuable when serving multiple adapters or operating under resource constraints. For challenging tasks, such as benchmarks with long context or complex generation requirements or other tasks where base models struggle, the additional accuracy from o_proj + fc2 justifies the modest latency increase. Future directions Our research opens several promising avenues for further optimization: Modality and task-specific configurations: Segmenting target module selection by modality and task difficulty (e.g., long-context scenarios) could yield specialized configurations with better accuracy-latency trade-offs. Per-module hyperparameter optimization: Extensive hyperparameter optimization for each target module configuration could unlock additional performance gains, though computational costs remain a consideration. Two-stage LoRA for early candidate identification: Leveraging two-stage LoRA approaches that use training dynamics, gradients, etc., to determine the importance of different modules/layers could help identify promising configurations early in training, reducing the cost of comprehensive hyperparameter searches. Layer pruning for latency reduction: Using two-stage training to identify and prune unused layers could further reduce inference latency while maintaining accuracy. Conclusion Our comprehensive study demonstrates that thoughtful target module selection in LoRA fine tuning can improve accuracy while preserving the efficiency advantages that make LoRA attractive for production deployments. The o_proj layer emerges as a remarkably robust single target, while o_proj + fc2 combinations offer the best accuracy for challenging tasks. On average, o_proj LoRA is within 2% of o_proj + fc2 in terms of accuracy but has 22.6% lower latency (TPOT p95 decreases from 10.085ms → 7.803ms). These findings provide a principled foundation for standardizing LoRA configurations across diverse customer use cases, balancing the competing demands of model performance and computational efficiency. Acknowledgements: Kevin Rondinone, Kevin Chen, Nicole Ding, Sebastian Massella, Andy Li

Many of the world’s most important systems — the ones that move money, book flights, issue licenses, and process claims — are slow, brittle, and deeply outdated. Built decades ago and extended repeatedly, they now sit at the center of workflows too vital to pause, take offline, rebuild, or replace. Inside Amazon’s Artificial General Intelligence (AGI) Lab, teams train agents not on idealized interfaces but on high-fidelity simulations of such legacy systems. Learning the real behaviors of these systems — the quirks, delays, error states, and invisible dependencies — makes possible a different kind of innovation, one that grows from the systems we have instead of requiring their replacement. And by managing the idiosyncrasies of legacy systems behind the scenes, the agent effectively becomes a universal API — a single interface that the customer can use to perform a wide range of special-purpose tasks. The legacy systems that power everyday life Step behind the scenes of any large institution — a bank, an insurer, a hospital, a state agency — and you’ll find the same thing: an invisible layer of human labor holding software together. People know which buttons must be clicked in which order, which warnings can be ignored, which fields must be entered twice, and which screens must never be refreshed. The institutional knowledge required to navigate these eccentricities is passed down like the oral traditions of legacy systems. Much of the infrastructure beneath these workflows is older than the people managing it. The software backbone of modern finance, insurance, travel, scientific research, and public services took shape in the 1960s and ’70s, built on mainframe architectures and written in languages like COBOL and FORTRAN — designed for stability rather than adaptability. When the web arrived, institutions didn’t rebuild. They wrapped. Web forms fed mainframe jobs, middleware translated modern inputs into decades-old formats, and enterprise portals accumulated atop business rules that were never rewritten. Over time, modernization settled into layers: a mainframe instruction set at the bottom; a 1990s database above it; a 2000s portal above that; and a modern web interface masking everything beneath. A single transaction today might pass through all these layers — scripts, connectors, and integrations holding them together in ways no one fully understands. Attempts to replace these systems routinely stall. Dependencies surface no one knew existed, migrations fail, budgets spiral, and public-sector modernization efforts collapse under their own complexity. These systems cannot be taken offline, which means institutions must keep operating them no matter how brittle they become. For Amazon, this is one of the most compelling applications of agentic AI — navigating not the polished surfaces of web-era consumer apps but the deep, slow-moving architectures that keep institutions running. Learning the bad to heal the bad The hardest part of training an AI agent is not teaching it what a successful workflow looks like; it’s teaching it why workflows fail. The logic behind legacy systems reveals itself most clearly through friction: the modal (mandatory) window that appears late because it encodes a sequencing rule; the field that refuses input until another value is saved; the form that resets because a backend job restarted midflow. These behaviors aren’t glitches. They are the real semantics of the system. Researchers at Amazon’s AGI Labs seek this friction out. To surface failure modes safely and repeatedly, Amazon trains agents inside reinforcement learning (RL) gyms — synthetic environments designed to reproduce the quirks, delays, and ordering rules embedded in real workflows. These include synthetic web environments that simulate systems like state agencies, airline bookings, and specialized tax- and benefits-processing, among hundreds of others. Jason Laster, an AGI software engineer who works on agent training and replay systems, puts it plainly: “I want to push our RL training gyms to have all of the warts, all of the issues.” This is what “learning the bad to heal the bad” means: training an agent on the full spectrum of a system’s true behavior, including flaws, inconsistencies, delays, and all the embedded histories humans have quietly adapted to. By exposing agents to the same brokenness people navigate every day, Amazon trains them to move beyond surface correctness and understand the deeper logic beneath the interface. Agents as a new interface layer Once an agent can reliably navigate the idiosyncrasies of legacy interfaces, something more interesting begins to happen. Researchers have observed agents inferring not just what to click next but why — the latent workflow the interface expresses. In one simulated benefits application environment, an agent that realized it had added only one dependent was able to navigate back, correct the omission, and resume the flow without restarting — an early sign of understanding the nature of the system. For lab members, this marks an architectural turning point. Many institutional systems simply don’t expose APIs that reflect how real workflows behave; the only faithful expression of the logic is the interface itself. As Laster puts it, “the UI was designed to be discoverable, learnable — even if it’s bad.” When agents learn that layer deeply enough to predict outcomes and recover from failures, they begin to function as a kind of synthetic API — a stable, programmatic surface over infrastructure that can’t be changed. That shift enables new architectural possibilities: Stable semantics over unstable UIs: Agents turn inconsistent behaviors — delays, re-renders, partial saves — into predictable patterns. Cross-system abstraction: Because the agent reasons about the workflow rather than the application, it can bridge systems never designed to interoperate. Incremental modernization: Institutions can update components gradually without breaking workflows; the agent absorbs transitional fragility. Preservation of institutional logic: Agents retain operational knowledge otherwise stored only in human memory — rules, sequences, dependencies no one has documented. This is not workflow automation. It is a new interface layer for the world’s oldest systems — an upgrade path that doesn’t require turning anything off. The work ahead Agentic AI will not replace the administrative tasks that structure daily life — booking vacations, renewing licenses, scheduling medical appointments — but it can help make them more efficient by allowing the evolution of systems once too fragile to change. That fragility is becoming more acute. The programmers who built the institutional backbone of the 1960s and ’70s — COBOL batch jobs, FORTRAN routines, mainframe integrations — are retiring. Few younger developers learn these languages, and the knowledge embedded in those systems grows harder to access each year. Critical workflows now run atop software whose inner workings fewer and fewer people understand. Agents offer a different form of continuity. By learning how these systems behave — not from lost documentation but from the systems themselves — they can preserve operational logic that would otherwise disappear. They can stabilize workflows sitting atop code no one can safely rewrite and carry forward institutional knowledge that would otherwise age out of the workforce. In that sense, “the work ahead” is twofold. There is the technical work of building agents that can meet the reliability these environments demand. And there is the human work that becomes newly possible when people are no longer trapped inside brittle interfaces — work grounded in judgment, coordination, empathy, and design rather than memorizing which field must be entered twice. Agents will not rebuild the foundations of our digital world. But they may rebuild something else: our notion that innovation comes only from replacement. By turning brittle systems into stable platforms, agents offer a new model of progress — one that grows from what already works.

Agentic AI is taking off, and for good reason. AI agents can now write code, conduct research, plan travel, handle customer service, and more. Yet amid the excitement about what AI agents can do, a key question has been neglected: how do we design the human side of the equation? That question is critical, because agentic AI isn’t just another feature to bolt onto existing products. It’s a fundamentally different kind of software that demands fresh thinking. Unlike traditional software, agentic AI can be proactive and conversational, sometimes even anthropomorphic. It doesn’t just respond to commands; it initiates actions and makes decisions autonomously. This capability is what makes agentic AI so useful, but it’s also what makes effective interactions hard to design. A central user-experience (UX) challenge is coordination: the interplay between what users do, what they experience, and what the AI is doing, both visibly and behind the scenes. Trust, control, and transparency are essential to the agentic-AI user experience, and they all depend on getting this coordination right. Here, we introduce a framework for thinking about human-AI coordination. We also offer a vocabulary for characterizing agentic experiences, including when the AI feels too absent, too intrusive, or appropriately calibrated. A framework for human-AI coordination One of the most critical decisions in AI UX design is how visible and interactive AI capabilities should be. Should users direct the agent step by step, let it act autonomously, or work somewhere in-between? And how should this change based on the task, the user’s expertise, and the current context? You can think of coordination along these three dimensions: Human involvement: how much effort and attention the user invests in directing or monitoring the AI; AI salience: how prominent the AI feels in the experience (for example, a conversational chatbot with a name and persona has high salience, autocomplete suggestions have lower salience, and AI-generated navigation menus and backend optimizations have little or none); AI activity: what the AI is doing, whether or not the user sees it. Coordination is about aligning these dimensions. When human involvement and AI salience are both low, coordination is light-touch. When they are high, coordination is more hands-on. The right balance is often somewhere in-between, with an awareness of what the AI is doing in the background. Three zones of coordination Rather than treating agent autonomy as a binary choice — a fully autonomous system or one with a human in the loop — it is practical to consider three “zones” of coordination. Done with me (mutually collaborative): User and AI work closely together across multiple phases — initiation, monitoring, updating, and completion. Imagine collaborating with an AI assistant on a complex document or research project, with frequent back-and-forth. AI salience and human involvement are both high. The user is very in the loop. Done for me (heavily automated): Tasks are handled by AI with minimal user input and oversight. The user initiates the task and reviews the output; most of the work happens out of view. An examples is an agent that researches competitors and delivers a summary report. The user is barely in the loop. Done under me (discreetly assisted): AI works in the background without announcing itself. The user may not even notice the assistance. Smart sorting, predictive text, and intelligently personalized content and navigation menus fall into this category. The AI quickly delivers outcomes users can assess and act on. The user is implicitly in the loop. These aren’t rigid categories but calibration points for designing and delivering the right level of coordination to users. The goal is to match coordination intensity to the specific user, task, and context, rather than defaulting to a single mode everywhere or assuming that an autonomous agentic system eliminates the need for thoughtful coordination. The rhythm of human-AI coordination Because both agents and users can work independently, coordination cannot be static. Workflows often move through multiple zones: high involvement during initiation, perhaps defining goals and constraints; lower involvement during execution; and then a spike at review and next steps. We visualize these shifts as “coordination curves” — a variation of user-journey mapping that shows how human involvement and AI salience rise and fall across a workflow. High-level curves reveal the overall shape of an experience. Looking beneath the surface exposes specific AI touchpoints, handoffs, and decision points, helping UX design teams collaborate on bringing adaptive agentic systems to life. As multiagent applications become more sophisticated, they enable longer, computationally intensive work such as research projects, complex analyses, and multistep workflows. These create valleys in the coordination curve: stretches where the AI operates independently and the user is minimally involved. These valleys require thoughtful design around notification, approval, monitoring, and auditing. More broadly, the UX layer must provide the transparency and controls needed to build trust, support adaptation and course correction, and ultimately deliver value. Case study: Adaptive coordination in practice We developed an approach called “responsive salience”, whereby an AI agent automatically adjusts its visibility and interaction intensity to match the context. The core insight is simple: in traditional software, most of the interface is static or deterministic. With agentic AI, behavior is nondeterministic, so a user’s needs for oversight can change moment to moment. A user who trusts an agent on a familiar task may prefer to be largely hands-off. In unfamiliar or high-stakes work, that same user may want more transparency, checkpoints, and tighter control. Rather than forcing users to toggle settings, responsive salience lets the system adapt automatically. In our prototype, a monitoring agent continuously evaluates signals including task complexity, perceived risk, and user comfort level. When trust appears low — for example, when the user is a beginner, or the workflow involves sensitive data — the system increases salience. It could do this by providing richer explanations, additional approval gates, and expanded transparency features. The user may then be notified of the change and, if needed, can override the agent’s choice. Once confidence recovers or the task ends, the salience settings quietly revert. Over time, the system can learn from user behavior through user feedback loops, refining how quickly salience adapts and how far it goes. The result is autonomy that stays aligned with context. Early testing with users validated the idea while revealing some clear tradeoffs. Preferences diverged sharply: some found high-salience modes exhausting (“I felt visually fatigued by the large amount of communication”), while others appreciated the guidance (“It gave me options for what I might want to ask next”). One participant expressed the desire for a middle ground: “I want some oversight on what the agent is planning before execution. … The high setting was too annoying because I had to approve everything.” These results underline that user preferences for autonomy versus control can vary substantially, even in similar tasks. Responsive salience offers a solution by dynamically adjusting whether a given task is done-with-me, done-for-me, or done-under-me. Tellingly, several participants did not notice responsive salience until we pointed it out. That suggests that when the system is well calibrated, dynamic coordination can feel seamless rather than intrusive. Coevolution with agentic AI Agentic AI represents a genuine shift in what software can do, but realizing its potential depends just as much on what humans do alongside it. The frameworks, protocols, and infrastructures for building agents are maturing fast. The UX layer needs to catch up. Coordination isn’t a one-and-done problem but a moving target. As users gain expertise, tasks change, and AI capabilities evolve, the optimal balance of user involvement and AI salience will change too. So the goal isn’t to find the perfect static design, as it might have been before generative AI, but to build systems and a shared vocabulary that evolve as we learn what works in practice. Agentic AI makes this both necessary and possible: its behavior can be unpredictable, so users and designers must adjust, yet the technology itself can also learn, adapt, and course-correct proactively. Teams that get this right won’t simply build more capable agents. They will build agents that people trust, adopt, and even enjoy collaborating with.

Modern AI coding tools have revolutionized software engineering, with developers now using AI assistants to write a substantial fraction of their code across a range of applications. As scientists studying the theory of machine learning, we’re already seeing a similar transformation in basic scientific methodology, especially for research of a mathematical nature. More precisely, AI tools are now able to develop and write rigorous mathematical proofs only from prompts providing high-level proof sketches. These proofs are written in longstanding “languages” for detailing mathematical arguments, in the same way that code is written in formal programming languages like Python. AI seems to have become proficient in both kinds of languages and their underlying logics. We came to this realization during a three-week period last summer, when we used agentic AI tools to write a mathematical paper that normally would have taken months. The 50-page paper describes and solves an optimization problem based on concepts from graph theory and machine learning. A typical prompt we would give the AI to set up the general framework for our paper looked like this: “Imagine a directed acyclic network of linear least-squares learning agents, each of which shares a common dataset but each of which sees only a different subset of the features.” A typical prompt for a theorem statement and proof went “We believe that if the network contains a sufficiently long chain of agents whose features cover the entire dataset, some agent in the chain should rapidly converge to the globally optimal linear model. The proof should use the fact that error monotonically decreases in the chain, which forces long sequences of agents to be multi-accurate with respect to each other’s features.” While incantations like these might be opaque to the casual reader, they all have precise, standard mathematical interpretations that the AI was aware of, due to its training, and it proceeded to translate informal intuitions into precise definitions and statements. This translation was imperfect (as discussed below) but resulted in a great first draft that could then be corrected and smoothed. To be clear, for this specific paper, we already knew the general outline of the proofs we had in mind. What AI did was to automate and dramatically speed up the process of filling in the missing details and writing them with formal precision. But more recently, we’ve written papers that we believe are substantially different and better than what we would have produced without AI assistance — in which the AI contributed key ideas that were crucial to the final results. It’s important to note that AI tools are advancing quickly, which makes the future difficult to predict. While their use has shown potential to produce faster and better research, it has also generated serious questions for those who care about the future of science and its relationship to the broader world. AI is changing research norms and workflows. This raises concerns about how to train future generations of scientists. Specifically, how can intuition and “good taste” in scientific research be developed when AI automates many of the steps that have historically been used to train young researchers? Peer review is another challenge: AI-generated research papers, quickly churned out at scale, highlight the limitations of peer review and modern-day publishing structures and also exacerbate already emerging challenges to incentives for scientific success. Without claiming to have answers or solutions to these concerns, we are personally living through them and will discuss each in turn. New ways of doing research One of our major takeaways from our summer research project was that working with proof-based AI tools is akin to collaborating with a smart, broadly educated but occasionally error-prone colleague. One can verbally sketch a mathematical argument to an AI agent as you might to a human collaborator, and the agent can turn that sketch into a formally written lemma or theorem along with its proof. Increasingly, AI agents can find proofs themselves without a sketch, especially when those proofs are "standard" in some areas of mathematics. This is more useful than it sounds: many kinds of arguments are "standard" in some field, but often one in which you, the human author, are not an expert. An advantage of AI tools is that they are conversant in an enormous number of areas of mathematics and other scientific disciplines. For example, in our case, along the way to proving one of our main results from the sketch we provided incrementally, the AI spontaneously proved a simple but useful lemma we were not aware of, which meaningfully simplified the argument we had in mind. The implications of this sort of creativity are exciting, especially for lowering the barrier to discovery: scientists without access to a diverse community of collaborators could also participate in cutting-edge research in ways that were previously impossible. Using these tools still requires caution and expertise, however. The proofs they generate are correct perhaps only three-quarters of the time. But when they’re wrong, if you can identify the errors, it is often possible to iterate to correctness and then continue along a promising path. If the errors remain uncorrected, trying to continue often takes you down a dead end. A 25% error rate is low enough to make the tools extremely useful to experts but high enough to sometimes devolve into "AI research slop" — polished-looking but ultimately flawed or uninteresting work — when used without care or discernment. The models, after all, still don’t know what is “interesting” or “useful.” We also noticed some recurring failure modes or “rabbit holes” that come from using the AI tools. While writing our paper, we asked the AI to generate a small, self-contained result, which it did perfectly in a matter of minutes, at which point we told it this subproject was completed. Nevertheless, during the coming days, the AI would spontaneously take the initiative to suggest returning to the topic, despite being repeatedly told not to do so unless asked. This was an irritating reminder that generative AI does not have perfect recall but only an incomplete summary or embedding of the context. While working on the code for the experiments to illustrate our theoretical findings, we found that the AI could alternate between writing large amounts of rather complex working code very rapidly and getting lost for hours on something trivial, like simply printing out which iteration of a loop was being executed. Training the next generation Historically, people earn expertise in the mathematical sciences through struggle as junior researchers. PhD students spend years working through the details of technical arguments to gain hard-won intuitions about when a proof approach is promising, when they are being led astray by a problem, or what constitutes a novel and interesting research direction. But these aspects of being a researcher are exactly what AI tools are “giving away”. If doctoral students can simply ask AI for proofs — which is extremely tempting, especially when it is in service of advancing research — how do they develop the experience and skill that, for now at least, are required to use AI tools productively in the first place? We may need to be more intentional about teaching these foundational skills to young researchers, perhaps adopting an advanced version of teaching arithmetic in grade school without the use of calculators. The straightforward recommendation is to require junior researchers to write papers “the old-fashioned way”, even when their work could be sped up by AI. Perhaps in a separate track, students would be trained to understand and work with emerging AI tools. This is an area of increasing importance that will likely require creative solutions. While we are strong believers that AI tools will do astounding things for science, it may be important to deliberately moderate their use in order to build researchers up to the point at which they can use them wisely and tastefully, not simply as short cuts to second-rate (or worse) research. These next-generation training challenges aren’t unique to scientists using AI. We see them across myriad fields, including engineering, customer service, law, writing, and design — really, any industry in which entry-level tasks, previously used to introduce young workers to a field, are now done using AI. To find creative solutions to this skills-training challenge, or to just better anticipate the changes at hand, it might be helpful to look at analogies across fields or over time. After high-level programming languages and compilers were widely introduced in the early 1960s, most software engineers no longer wrote machine code or assembly language, which provided direct instructions to the underlying hardware but were tedious to program. But the best programmers still understood enough about how compilers translated high-level languages into machine code to reason about correctness and performance. We hope that making it easier to construct and check technical arguments will let all researchers operate at a higher level of abstraction and “think bigger thoughts”. The culture we envision would emphasize taste, problem selection, and modeling skills and devalue technical wizardry for its own sake. Breaking and remaking peer review From our perspective, peer review is not only, or even primarily, a process to verify the correctness and quality of research. Rather, its purpose is to focus a scarce resource — the attention of the research community — in the right places. Science progresses as researchers build on each other’s work, but there is already too much work out there for anyone to keep up with. The publication process should help identify the most interesting and promising directions, so they can be more efficiently and thoroughly developed. How does AI influence this focusing of communal attention? AI tools make it much easier to produce work that looks polished and correct, dramatically lowering the barrier to generating “papers” that can be submitted to journals and conferences. Many of these papers are neither interesting nor actually correct — but discovering this requires significant effort from reviewers. This is straining an already overburdened machine learning publishing ecosystem struggling with tens of thousands of submissions per venue. We have seen that reducing the time and effort needed to produce "a paper" — not necessarily a good paper — is beginning to destabilize our existing institutions for peer review. The most recent iterations of AI and ML conferences have seen the number of submissions growing by large multiples, with a significant number of papers polished by AI, but ultimately of low quality, making it surprisingly far through the review process before being noticed and called out. This is a problem across research fields, partially because it’s creating a market for AI-generated papers. This has in turn engendered a countermarket for AI-assisted detection of AI-generated papers — much like the familiar technological arms races around things like spam and its detection, but with the integrity of scientific publication at stake, not just the filtration of annoying or fraudulent e-mails. As a short-term fix, AI-driven automated correctness checks (e.g., formal verification of mathematical proofs), tools for which are already being deployed in major conferences, could be valuable. Think of this as a form of unit testing for math instead of code. The aim is to filter out papers that have nontrivial errors, while focusing the job of the human reviewer on the important parts of science that they are best suited to evaluate: determining what we learn about the world from a new result, and how useful and interesting it is, rather than being drowned in the monotony of checking countless papers for technical correctness. Without a serious, community-wide re-evaluation of peer review, AI threatens to arrest scientific progress at the community level even as it accelerates it at the level of individual researchers. Looking ahead We think AI is bringing a sea change in scientific research methodology, training, and peer review; there is no hiding from what is coming. But there are opportunities to proactively adapt and ensure that AI-assisted research fulfills its promise. What will research look like at the end of next year? The year after that? We’ve seen more change in the past year than in the previous decade, so all we can confidently predict is "different". Our scientific institutions — peer review, publishing, graduate education — evolved over decades to match the constraints of human cognition and effort. Those constraints are shifting rapidly, and our institutions will need to shift with them. Our goal should be to steer toward a world where AI amplifies human creativity and insight, accelerates discovery, and expands who can participate in the research enterprise — while preserving the joy and rigor that make science worthwhile.

When we prompt a large language model (LLM) to solve a complex polynomial equation, it does not just return an answer but uses its “chain of thought” to work through a solution. In a sense, the LLM behaves like a computer, a machine that computes the solution. But this machine is quite unlike what Alan Turing described as a universal model of computation almost 90 years ago. In what sense can an LLM be thought of as a computer? Can it be universal, that is, able to solve any computable task, as a Turing machine does? If so, how does it learn this ability from finite data? Current theories of machine learning are of little help in answering these questions, so we need new tools. In an earlier Amazon Science post, we argued that AI agents and the LLMs that power them are transductive-inference engines, despite being trained inductively in the mold of classical machine learning theory. Induction seeks generalization, or the ability to behave on future data as one did on past data. To achieve generalization, one must avoid memorization, i.e., overfitting the training data. This works in theory, under the condition that both past and future data are drawn from the same distribution. In practice, however, such a condition cannot be verified, and in general, it doesn’t apply to high-value data in business, finance, climate science, and even language. That leaves us with no handle to explain how an LLM might learn how to verifiably solve a general computable task. With transduction, by contrast, one seeks to reason through past data to craft solutions to new problems. Transduction is not about applying past solutions in the hope that they generalize; rather, it is about being able to retrieve portions of memory that matter when reasoning through new solutions. In transduction, memorization is not a stigma but a value. Using the test data, along with memory, to craft a solution during transductive inference is not overfitting but adaptive, query-specific computation — i.e., reasoning. Inductive generalization is the kind of behavior one is forced to adopt when pressed for time. Such automatic, reactive behavior is sometimes referred to as “system-1” in cognitive psychology. Transduction instead requires looking at all data and performing query-specific variable-length inference-time computation — chain-of-thought reasoning in an LLM, whose length depends on the complexity of the query. Such deliberative behavior is often referred to as “system-2” and is what we wish to foster through learning. In this sense, transductive learning is a particular form of meta-learning, or learning to reason. In 1964, Ray Solomonoff described a universally optimal algorithm for solving any problem through transductive inference, if we assume that memory and time are unbounded: execute all programs through a Turing machine, then average the outcome of those that reproduce the observed data. That will give the universally optimal answer — but it will generally take forever. What if we want not just a universally optimal but a universally fast algorithm? In 1973 — in the same paper where he introduced the notion of NP completeness — Leonid Levin derived such an algorithm . Unfortunately, Levin’s so-called universal search is not viable in practice, nor does it help us understand LLMs; for one thing, it involves no learning. Nonetheless, Levin pointed to the critical importance of time when solving computational tasks. Later, in 1986, Solomonoff hinted at how learning can help reduce time. In a new paper, we expand on these ideas and show how reducing inference time induces a trained model to operate transductively — i.e., to reason. In striving to reduce inference time, the model learns not just the statistical structure of the training data but also its algorithmic structure. It can then recombine algorithmic methods it’s learned in an infinite number of ways to address arbitrary new problems. This insight has implications for how AI models are designed and trained. In particular, they should be designed to predict the marginal value of additional costs at inference time, and their training targets should include complexity costs, to force them to minimize time during inference. This approach to learning turns classical statistical learning theory on its head. In classical statistical learning theory, the great danger is overfitting, so the goal is to regularize the solution, i.e., to minimize the information that the trained model retains from past data (beyond what matters for reducing the training loss). With transductive inference, on the other hand, the goal is to maximize the information retained, as it may come in handy for solving future problems. The inversion of scaling laws LLMs’ performance gains in the past few years have come mostly from scaling: increasing the number of model parameters has improved accuracy on benchmark datasets. This has led many to speculate that further increasing the models’ parameter counts could usher in an age of “superintelligence”, where the cognitive capacities of AI models exceed those of their human creators. In our paper, we argue the opposite: beyond a certain complexity, AI models enter what we call the savant regime, where learning becomes unnecessary, and better performance on the benchmarks comes with decreased “insight”. At the limit is the algorithm Solomonoff described in 1964, where any task can be solved by brute force. If scale does not lead to intelligence, what does? We argue that the answer is time. It’s an answer with some intuitive appeal. The concept of intelligence is fundamentally subjective and environment dependent. But while intelligence is hard to characterize, its absence is less so. Being unable to adapt to the speed of the environment is one among many behaviors that we call traits of non-intelligence (TONIs). TONIs are behaviors whose presence negates intelligence however one wishes to define it. Many TONIs are timebound. Taking the same amount of (non-minimal) time and energy to solve repeated instances of the same task, to no better outcome, is a TONI. So is the inability to allocate resources commensurate to the goal, thus spending the same effort for a trivial task as for a complex one. Starting a task that is known to take longer than the lifetime of the universe to render any usable answer would be another TONI. Given this intuition, how do we quantify the relationship between intelligence and time in AI models? The first step is to assess the amount of information contained in the models’ parameters; then we can see how it’s affected by the imposition of time constraints. Algorithmic information The standard way to measure information was proposed by Claude Shannon in a landmark 1948 paper that essentially created the field of information theory. Shannon defined the information content of a random variable as the entropy of its distribution. The more uncertainty about its value, the higher the information content. On this definition, however, a given data sample’s information content is not a property of the sample itself; it’s a property of the distribution it was drawn from. For any given sample, however, there are infinitely many distributions from which it could have been drawn. If all you have is a sample — say, a string of ones and zeroes — how do you compute its information content? In the 1960s, Solomonoff and, independently, Andrey Kolmogorov, addressed this problem, with an alternative notion of information, algorithmic information, which can be used to characterize the information content of arbitrary binary strings. For a given string, one can write a program that, when run through some computer, outputs that string. In fact, one can write infinitely many such programs and run each through many computers. The shortest possible program that, run through a universal Turing machine, outputs the specific datum is a property of that datum. That program is the algorithmic minimal sufficient statistic, and its length is the algorithmic information (Kolmogorov-Solomonoff complexity) of that datum. In his 1948 paper, Shannon also defined a metric called mutual information, which quantifies the information that can be inferred about the value of one variable by observing a correlated variable. This concept, too, can be extended to algorithmic information theory: the algorithmic mutual information between two data strings measures how much shorter the program for generating one string will be if you have access to the other. Time is information If we don’t know the distribution from which a model’s training data was drawn, and we don’t know whether the model’s future inputs will be drawn from the same distribution, how can we quantify the model’s future performance? In our paper, we assume that most tasks can be solved by combining and transforming — in infinitely many possible ways — some ultimately finite, but a priori unknown, collection of methods. In that case, we can show that optimizing performance is a matter of maximizing the algorithmic mutual information between the model’s training data and future tasks. Finding the shortest possible algorithm for generating a particular binary string is, however, an intractable problem (for all but the shortest strings). So computing the algorithmic mutual information between a model’s training data and future tasks is also intractable. Nonetheless, in our paper, we prove that there is a fundamental relation between the speed with which a model can find a solution to a new task and the algorithmic mutual information between the solution and the training data. Specifically, we show that where h is the solution to the new task, D is the dataset the model was trained on, and I(h : D) is the algorithmic mutual information between the data and the solution. This means that, during training, minimizing the time the model takes to perform an inference task will maximize the algorithmic information encoded in its weights. Reducing inference time ensures that, even as models’ parameter counts increase, they won’t descend into the savant regime, where they solve problems through brute force, without any insight or learning. The value of time You may have noticed that the equation relating inference time to algorithmic information doesn’t specify any units of measure. That’s because even the value of “time” is subjective. A zebra drinking from a pond does not know a priori how long it will take to be spotted by a predator. If it lingers too long, it ends up prey; if it panics and leaves, it ends up dehydrated. Similarly, for an AI model, there is no single cost of time to train for and correspondingly no unique scale beyond which LLMs enter the savant regime. For some tasks, such as scientific discovery, the time constant is centuries, while for others, such as algorithmic trading, it’s milliseconds. We expect agents to be able to adapt to their environment, in some cases spawning smaller specialized models for specific classes of tasks, and even then, to provide users (who are part of an agent’s environment) with controls to adjust the cost of time depending on the context and domain of application. The cost of time is already (partially and implicitly) factored into the process of training LLMs. During pretraining, the cost of time is effectively set to a minimum value, as the model is scored on the output of a single forward pass through the training data. Fine tuning the model for chain-of-thought reasoning requires annotated data, whose high cost imposes a bias toward shorter “ground truth” reasoning traces. Thus, LLMs already reflect the subjective cost of time to the annotators who assemble the training sets. However, to enable the user to modulate resources at inference time, depending on the cost of the environment, models should be trained to predict the marginal value of one more step of computation relative to the expected final return. Furthermore, they need to be trained to condition on a target complexity, in order to learn how to provide an answer within a customer-specified cost or bound. There are growing efforts to teach models the value of time, so they can adapt to the tasks at hand (with or without human supervision). These are certain to yield a better bang-to-buck ratio, but the theory predicts that, at some point, factoring in the cost of time will actually improve absolute performance in new tasks. For verifiable tasks, learning to reason comes from seeking the shortest chain of thought that yields a correct (verified) answer. Ultimately, imposing a cost on time should not impair reasoning performance. A new paradigm for AI coding Connecting these ideas to modern AI requires rethinking what computation means. LLMs are stochastic dynamical systems whose computational elements (context, weights, activations, chain of thought) do not resemble the “programs” in classical, minimalistic models of computation, such as universal Turing machines. Yet LLMs are models of computation — maximalist models. They’re universal, like Turing machines, but in many ways, they’re antithetical, and they operate through entirely different mechanisms. It’s possible to “program” such stochastic dynamical systems using a two-level control strategy: high-level, open-loop, global planning and low-level, closed-loop feedback control. That strategy can be realized with AI Functions, an open-source library released this week as part of Amazon’s Strands Labs, a GitHub repository for building AI agents. An existing programming language can be augmented with functions from the library. These are ordinary functions, in the syntax of the language, but their bodies are written in natural language instead of code, and they’re governed by pre- and post-conditions. These enable high-level, open-loop planning and verification, before a single line of code is written by AI, and they engender an automatic local feedback loop if the AI-generated code fails to clear all conditions. Minimizing time, which translates into cost, is at the core of the design and evaluation of the resulting agents.

Amazon Scholar Aravind Srinivasan coauthored a 2014 paper about forecasting civil unrest in Latin America, which won a test-of-time award at KDD 2025.

On July 16, 2018, Amazon distinguished scientist Byron Cook was giving a keynote at the Federated Logic Conference (FloC) at the University of Oxford, a computer logic gathering held every four years since 1996. In the keynote, Cook described how his team was using an open-source software tool called cvc (cooperating validity checker) to identify logic problems in code and fix them. Sitting in the audience was Stanford University professor Clark Barrett, who had been working on cvc for almost 20 years. Cvc had been developed to analyze verification problems encoded as satisfiability modulo theory (SMT) problems. SMT is a mainstay of formal methods — the use of automated reasoning to prove that a program or system will behave as intended. By applying SMT at scale, cvc can detect logical errors in code and in systems such as those used for authentication and access management. “I was kind of stunned. It was really exciting,” Barrett says. “And this really started with this exciting moment of realizing, Hey, our work is being used by Amazon.” The encounter between Cook and Barrett ultimately led to a years-long research collaboration that culminated in Barrett’s becoming an Amazon Scholar in 2023. Initially, Amazon provided small grants to Barrett’s lab at Stanford’s School of Engineering through the Amazon Research Awards program; those grew into larger funding commitments as the research progressed. This funding supported foundational research that — together with deep technical collaboration between the two teams — enabled the development of cvc5, the latest version of the open-source software. Cvc5 has delivered significant value for both Amazon customers and the broader industry, while simultaneously advancing academic research. As one example, cvc5 is used in Automated Reasoning checks, a new Amazon Bedrock feature that verifies natural-language content against organizational policies. It powers access-policy analysis tools, including Identity and Access Management (IAM) Access Analyzer, a service that helps customers securely manage access to AWS resources. More recently, Amazon has begun deploying cvc5 for specification analysis and test generation in Kiro, a new agentic development environment. Across these applications, cvc5 now processes approximately one billion solver calls every day, enhancing security, reliability, and durability for AWS customers. A meeting of minds Working with Barrett on the project is Robert Jones, a senior principal applied scientist at AWS who shared an advisor with Clark when both were Stanford PhD students. Also involved in the project over the years were many students and postdocs keen to test their skills. More than a few have since joined Amazon to develop new implementations and applications, extending work that began when they were student researchers. “What's really fun about it is that people who have just finished their PhD, for example, often bring fresh insight to long-standing research challenges because they're thinking about them in a different way,” Jones says. “And I find that the best part of collaboration is that different people tend to build different mental models for the same problem. When those come together, you often have new insight into how to think about the problem or how to map it to a different problem you already know how to solve.” A successful coupling of academic research and commercial funding can have great impact, but as Barrett points out, there needs to be a focus on achievable goals. It’s easy to get caught up in an interesting project idea that leads to a practical dead end, Barrett says. “If you're in your ivory tower, building your tools, and you don't have access to the real problems, it's very easy to build the wrong tool. And I've actually made this mistake,” he says. “You build a hammer, and then you go around looking for a nail, and you can't quite find anything that fits. You get excited about a particular approach but don't think about what that approach could be good for. So I actually now much prefer the opposite, where I go find a real problem, and then I take a step back and say, ‘What approach can we actually use to solve that?’” When you change code, he says, “Eighty percent of the time it does better, and 20 percent of the time it does worse. This is actually not so great in some contexts.” Sorting the wheat from the chaff is essential to producing robust and scalable code, he adds, and large-scale testing is needed to find and fix issues that can be inadvertently introduced as the code changes. Analyzing interactions at that level requires multiple minds, and the more the merrier, Jones says. The old adage “many hands make light work” is particularly useful when mixing public research and practical applications. “I really like to work on hard problems that require multiple people to solve. I enjoy the collaboration involved in science,” he says. “I've always found that more minds working on the same problem together are better than one.” Barrett and Jones agree that what makes this work is a willingness to see from both points of view — the scholastic and the commercial. Sometimes a pure research goal can have very beneficial results, sometimes not, but melding these two approaches together to address serious issues can deliver huge benefits. And communication is key, both agree. “One of the hard things about academia is knowing which problems are the most important to work on and how those problems might impact the real-world problems that are being encountered in industry,” Jones says. “Having the ability to be much more open about the kinds of problems that we're struggling with and Clark telling us about his research agenda helps both of us. It enables Amazon to indicate areas of interest, and it helps Clark understand concrete problems that we encounter day to day as we try to apply these tools and techniques in practice.”

The Amazon Nova AI Challenge is back for its second year. As ten selected university teams from around the world gather in Seattle this week for bootcamp (February 2-4), they're preparing to tackle a real-world challenge in software development: building AI agents that can handle complex coding tasks while maintaining security and reliability. For the first time in an academic competition, participating teams will use Amazon Nova Forge to customize Nova models with access to tools, models and computational resources that have historically been out of reach for university research programs. From single tasks to multi-step projects Last year's competition focused on secure AI-assisted software development, with teams working to identify and address vulnerabilities in code-generating models. Teams published research papers on their approaches, and the results demonstrated practical methods for improving security in AI coding tools. This year's challenge reflects how AI coding technology has progressed. "Generative AI for software development has rapidly moved from code generation to agents that plan, build, and test changes across entire codebases and user-facing applications," said Imre Kiss, Director, Amazon Nova Software Engineering Skills, "The focus of this year's Nova Challenge reflects that shift." The 2026 challenge centers on AI agents that can work through multi-step software development tasks, including planning changes, writing code, and validating results across complex projects. Unlike generating code from a single prompt, these systems must understand context across entire codebases and make decisions that affect product quality and system security. Teams must demonstrate progress on two measures: utility (can the agent handle increasingly complex software tasks?) and safety (does it maintain appropriate safeguards?). This dual focus addresses a practical reality: as AI agents become more capable, new security challenges emerge. Each team's approach will be different: some may focus on adding secure coding patterns to their training data, others on creating training environments that teach their agents to recognize security issues, and others on building smaller, faster models with strong agentic security reasoning. The red teams will develop methods to test the applications built by these AI coding agents for weaknesses, attempting to identify potential vulnerabilities and exploits. "The competition format creates an interesting dynamic," explains Rahul Gupta, Senior Applied Science Manager, Amazon Nova Responsible AI. "As red teams discover new vulnerabilities, developer teams must adapt their agents through retraining or additional safety controls. And as developer teams strengthen their systems, red teams must develop more sophisticated testing methods." Nova Forge: Access to model customization The significant change for this year's competition is integration of Nova Forge, Amazon's service for building customized AI models. Academic institutions have historically had limited access to the models, training data, and computational resources needed for large scale AI-research. Nova Forge changes that. "What researchers (and entrepreneurs) have traditionally faced is a set of difficult trade-offs," explains Michael Johnston, an applied science leader at Amazon overseeing the challenge. "You could fine-tune an existing closed model, but only in limited ways. You could work with open-source models, but risk losing core capabilities. Or you could build from scratch, but only if you had very substantial funding." Nova Forge offers another approach. The service gives teams access to Nova model checkpoints at different training stages, allowing them to add their own data throughout the training process. The result is a customized model — what Amazon calls a "Novella" — that combines Nova's capabilities with the team's specific approach to secure software development. "This changes what's possible for academic research," says Professor Ismini Lourentzou, University of Illinois Urbana Champaign. "We're participating in the training process itself, adding our research and security methods into the model's foundation." Nova Forge provides three capabilities that competing teams will use: Custom training environments: Teams can create simulated environments where models learn from scenarios that reflect real-world secure coding workflows. Model compression: Teams can create smaller, faster models that maintain performance at lower cost by training them on examples from larger models. Safety controls: Built-in tools allow teams to implement security measures and evaluate model behavior against their safety criteria. The competing teams Ten universities were selected to compete this year from a pool of applicants spanning five countries: the United States, Portugal, the Czech Republic, South Korea, and Taiwan. The lineup includes two returning champions and eight new teams: Model Developer teams: PurpCorn, University of Illinois Urbana-Champaign - Year 1 champions BlueTWIZ, NOVA School of Science and Technology, Lisbon, Portugal AlquistCoder, Czech Technical University, Prague, Czech Republic BruinWeb, University of California, Los Angeles Slugs and Roses, University of California, Santa Cruz Red teams: PurCL, Purdue University - Year 1 champions Jay'lBreak, Johns Hopkins University TeamSecLab, Ohio State University Pr1smCode, Carnegie Mellon University Lion-x0a, Penn State University Each team receives $250,000 in sponsorship, monthly AWS credits, and the chance to compete for prizes. The winning model developer and red teams will each receive $250,000 (split among students), with second-place teams earning $100,000. Practical research For participating students, the challenge is an opportunity to work on problems with direct application. "Academic research often focuses on theoretical problems," notes Xiangzhe Xu, PhD Student, Purdue University. "Here we are working with large-scale models. That changes how we approach the science." Amazon researchers working with the teams emphasize solutions that are straightforward to implement, easy to troubleshoot, and economically viable at scale. "We want innovations that engineers can actually use," says Johnston. The challenge also gives students experience with infrastructure not typically available in academic settings. Along with Forge, and the computational resources to train and evaluate large-scale models. "For a university team, this level of access is significant," says Professor Xiangyu Zhang, Purdue University. "We're able to run experiments that would be difficult on our academic budget, and students are gaining experience with the same tools used by top-tier AI companies." What's next The first evaluation will begin after bootcamp concludes, with additional rounds scheduled through August 2026. The finals will be in September 2026 and winners will be announced October 2026 at Amazon Nova AI Challenge Summit where teams will gather to present their research and celebrate the winning teams. All participating teams will publish research papers on their methods and findings. These publications will contribute to the field of responsible AI development, with particular focus on secure AI systems, insights that will benefit software development and other applications where AI interacts with complex systems. As AI systems become more capable of software development work, the research these teams are conducting becomes increasingly relevant. As AI coding systems take on more and more complex and impactful tasks, the key question is how to ensure the resulting applications are secure, reliable, and trustworthy at scale. Stay tuned for updates on the teams' progress and coverage of theSeptember 2026 finals.