Social
Automated reasoning

A gentle introduction to automated reasoning

Meet Amazon Science’s newest research area.

By Byron Cook
December 1, 2021
18 min read
Share

This week, Amazon Science added automated reasoning to its list of research areas. We made this change because of the impact that automated reasoning is having here at Amazon. For example, Amazon Web Services’ customers now have direct access to automated-reasoning-based features such as IAM Access Analyzer, S3 Block Public Access, or VPC Reachability Analyzer. We also see Amazon development teams integrating automated-reasoning tools into their development processes, raising the bar on the security, durability, availability, and quality of our products.

The goal of this article is to provide a gentle introduction to automated reasoning for the industry professional who knows nothing about the area but is curious to learn more. All you will need to make sense of this article is to be able to read a few small C and Python code fragments. I will refer to a few specialist concepts along the way, but only with the goal of introducing them in an informal manner. I close with links to some of our favorite publicly available tools, videos, books, and articles for those looking to go more in-depth.

Let’s start with a simple example. Consider the following C function:

bool f(unsigned int x, unsigned int y) {
   return (x+y == y+x);
}



        
Take a few moments to answer the question “Could f ever return false?” This is not a trick question: I’ve purposefully used a simple example to make a point.
To check the answer with exhaustive testing, we could try executing the following doubly nested test loop, which calls f on all possible pairs of values of the type unsigned int:

            

    
#include<stdio.h>
#include<stdbool.h>
#include<limits.h>

bool f(unsigned int x, unsigned int y) {
   return (x+y == y+x);
}

void main() {
   for (unsigned int x=0;1;x++) {
      for (unsigned int y=0;1;y++) {
         if (!f(x,y)) printf("Error!\n");
         if (y==UINT_MAX) break;
      }
      if (x==UINT_MAX) break;
   }
}



        
Unfortunately, even on modern hardware, this doubly nested loop will run for a very long time. I compiled it and ran it on a 2.6 GHz Intel processor for over 48 hours before giving up.
Why does testing take so long? Because UINT_MAX is typically 4,294,967,295, there are 18,446,744,065,119,617,025 separate f calls to consider. On my 2.6 GHz machine, the compiled test loop called f approximately 430 million times a second. But to test all 18 quintillion cases at this performance, we would need over 1,360 years.
When we show the above code to industry professionals, they almost immediately work out that f can't return false as long as the underlying compiler/interpreter and hardware are correct. How do they do that? They reason about it. They remember from their school days that x + y can be rewritten as y + x and conclude that f always returns true.

            

    
        






    
    

        
            
Re:Invent 2021 keynote address by Peter DeSantis, senior vice president for utility computing at Amazon Web Services

        
        
            
Skip to 15:49 for a discussion of Amazon Web Services' work on automated reasoning.

        
    



        
An automated reasoning tool does this work for us: it attempts to answer questions about a program (or a logic formula) by using known techniques from mathematics. In this case, the tool would use algebra to deduce that x + y == y + x can be replaced with the simple expression true.
Automated-reasoning tools can be incredibly fast, even when the domains are infinite (e.g., unbounded mathematical integers rather than finite C ints). Unfortunately, the tools may answer “Don’t know” in some instances. We'll see a famous example of that below.
The science of automated reasoning is essentially focused on driving the frequency of these “Don’t know” answers down as far as possible: the less often the tools report "Don't know" (or time out while trying), the more useful they are.
Today’s tools are able to give answers for programs and queries where yesterday’s tools could not. Tomorrow’s tools will be even more powerful. We are seeing rapid progress in this field, which is why at Amazon, we are increasingly getting so much value from it. In fact, we see automated reasoning forming its own Amazon-style virtuous cycle, where more input problems to our tools drive improvements to the tools, which encourages more use of the tools.
A slightly more complex example. Now that we know the rough outlines of what automated reasoning is, the next small example gives a slightly more realistic taste of the sort of complexity that the tools are managing for us.

            

    
void g(int x, int y) {
   if (y > 0)
      while (x > y)
         x = x - y;
}



        
Or, alternatively, consider a similar Python program over unbounded integers:

            

    
def g(x, y):
   assert isinstance(x, int) and isinstance(y, int)
   if y > 0:
      while x > y:
         x = x - y



        
Try to answer this question: “Does g always eventually return control back to its caller?”
When we show this program to industry professionals, they usually figure out the right answer quickly. A few, especially those who are aware of results in theoretical computer science, sometimes mistakenly think that we can't answer this question, with the rationale “This is an example of the halting problem, which has been proved insoluble”. In fact, we can reason about the halting behavior for specific programs, including this one. We’ll talk more about that later.
Here’s the reasoning that most industry professionals use when looking at this problem:
  1. In the case where y is not positive, execution jumps to the end of the function g. That’s the easy case.
  2. If, in every iteration of the loop, the value of the variable x decreases, then eventually, the loop condition x > y will fail, and the end of g will be reached.
  3. The value of x always decreases only if y is always positive, because only then does the update to x (i.e., x = x - y) decrease x. But y’s positivity is established by the conditional expression, so x always decreases.
The experienced programmer will usually worry about underflow in the x = x - y command of the C program but will then notice that x > y before the update to x and thus cannot underflow.
If you carried out the three steps above yourself, you now have a very intuitive view of the type of thinking an automated-reasoning tool is performing on our behalf when reasoning about a computer program. There are many nitty-gritty details that the tools have to face (e.g., heaps, stacks, strings, pointer arithmetic, recursion, concurrency, callbacks, etc.), but there’s also decades of research papers on techniques for handling these and other topics, along with various practical tools that put these ideas to work.

            

    

        
    
        Policy-code.gif
    


        

        
    


    
        
Automated reasoning can be applied to both policies (top) and code (bottom). In both cases, an essential step is reasoning about what's always true.

    


        
The main takeaway is that automated-reasoning tools are usually working through the three steps above on our behalf: Item 1 is reasoning about the program’s control structure. Item 2 is reasoning about what is eventually true within the program. Item 3 is reasoning about what is always true in the program.
Note that configuration artifacts such as AWS resource policies, VPC network descriptions, or even makefiles can be thought of as code. This viewpoint allows us to use the same techniques we use to reason about C or Python code to answer questions about the interpretation of configurations. It’s this insight that gives us tools like IAM Access Analyzer or VPC Reachability Analyzer.
An end to testing?
As we saw above when looking at f and g, automated reasoning can be dramatically faster than exhaustive testing. With tools available today, we can show properties of f or g in milliseconds, rather than waiting lifetimes with exhaustive testing.
Can we throw away our testing tools now and just move to automated reasoning? Not quite. Yes, we can dramatically reduce our dependency on testing, but we will not be completely eliminating it any time soon, if ever. Consider our first example:

            

    
bool f(unsigned int x, unsigned int y) {
   return (x + y == y + x);
}



        
Recall the worry that a buggy compiler or microprocessor could in fact cause an executable program constructed from this source code to return false. We might also need to worry about the language runtime. For example, the C math library or the Python garbage collector might have bugs that cause a program to misbehave.
What’s interesting about testing, and something we often forget, is that it’s doing much more than just telling us about the C or Python source code. It’s also testing the compiler, the runtime, the interpreter, the microprocessor, etc. A test failure could be rooted in any of those tools in the stack.
Automated reasoning, in contrast, is usually applied to just one layer of that stack — the source code itself, or sometimes the compiler or the microprocessor. What we find so valuable about reasoning is it allows us to clearly define both what we do know and what we do not know about the layer under inspection.
Furthermore, the models of the surrounding environment (e.g., the compiler or the procedure calling our procedure) used by the automated-reasoning tool make our assumptions very precise. Separating the layers of the computational stack helps make better use of our time, energy, and money and the capabilities of the tools today and tomorrow.
Unfortunately, we will almost always need to make assumptions about something when using automated reasoning — for example, the principles of physics that govern our silicon chips. Thus, testing will never be fully replaced. We will want to perform end-to-end testing to try and validate our assumptions as best we can.
An impossible program
I previously mentioned that automated-reasoning tools sometimes return “Don’t know” rather than “yes” or “no”. They also sometimes run forever (or time out), thus never returning an answer. Let’s look at the famous "halting problem" program, in which we know tools cannot return “yes” or “no”.
Imagine that we have an automated-reasoning API, called terminates, that returns “yes” if a C function always terminates or “no” when the function could execute forever. As an example, we could build such an API using the tool described here (shameless self-promotion of author’s previous work). To get the idea of what a termination tool can do for us, consider two basic C functions, g (from above),

            

    
void g(int x, int y) {
   if (y > 0)
      while (x > y)
         x = x - y;
}



        
and g2:

            

    
void g2(int x, int y) {
   while (x > y)
      x = x - y;
}



        
For the reasons we have already discussed, the function g always returns control back to its caller, so terminates(g) should return true. Meanwhile, terminates(g2) should return false because, for example, g2(5, 0) will never terminate.
Now comes the difficult function. Consider h:

            

    
void h() {
   if terminates(h) while(1){}
}



        
Notice that it's recursive. What’s the right answer for terminates(h)? The answer cannot be "yes". It also cannot be "no". Why?
Imagine that terminates(h) were to return "yes". If you read the code of h, you’ll see that in this case, the function does not terminate because of the conditional statement in the code of h that will execute the infinite loop while(1){}. Thus, in this case, the terminates(h) answer would be wrong, because h is defined recursively, calling terminates on itself.
Similarly, if terminates(h) were to return "no", then h would in fact terminate and return control to its caller, because the if case of the conditional statement is not met, and there is no else branch. Again, the answer would be wrong. This is why the “Don’t know” answer is actually unavoidable in this case.
The program h is a variation of examples given in Turing’s famous 1936 paper on decidability and Gödel’s incompleteness theorems from 1931. These papers tell us that problems like the halting problem cannot be “solved”, if by“solved” we mean that the solution procedure itself always terminates and answers either “yes” or “no” but never “Don’t know”. But that is not the definition of “solved” that many of us have in mind. For many of us, a tool that sometimes times out or occasionally returns “Don’t know” but, when it gives an answer, always gives the right answer is good enough.
This problem is analogous to airline travel: we know it’s not 100% safe, because crashes have happened in the past, and we are sure that they will happen in the future. But when you land safely, you know it worked that time. The goal of the airline industry is to reduce failure as much as possible, even though it’s in principle unavoidable.
To put that in the context of automated reasoning: for some programs, like h, we can never improve the tool enough to replace the "Don't know" answer. But there are many other cases where today's tools answer "Don't know", but future tools may be able to answer "yes" or "no". The modern scientific challenge for automated-reasoning subject-matter experts is to get the practical tools to return “yes” or “no” as often as possible. As an example of current work, check out CMU professor and Amazon Scholar Marijn Heule and his quest to solve the Collatz termination problem.
Another thing to keep in mind is that automated-reasoning tools are regularly trying to solve “intractable” problems, e.g., problems in the NP complexity class. Here, the same thinking applies that we saw in the case of the halting problem: automated-reasoning tools have powerful heuristics that often work around the intractability problem for specific cases, but those heuristics can (and sometimes do) fail, resulting in “Don’t know” answers or impractically long execution time. The science is to improve the heuristics to minimize that problem.
Nomenclature
A host of names are used in the scientific literature to describe interrelated topics, of which automated reasoning is just one. Here’s a quick glossary:
  • A logic is a formal and mechanical system for defining what is true and untrue. Examples: propositional logic or first-order logic.
  • A theorem is a true statement in logic. Example: the four-color theorem.
  • A proof is a valid argument in logic of a theorem. Example: Gonthier's proof of the four-color theorem. 
  • A mechanical theorem prover is a semi-automated-reasoning tool that checks a machine-readable expression of a proof often written down by a human. These tools often require human guidance. Example: HOL-light, from Amazon researcher John Harrison. 
  • Formal verification is the use of theorem proving when applied to models of computer systems to prove desired properties of the systems. Example: the CompCert verified C compiler. 
  • Formal methods is the broadest term, meaning simply the use of logic to reason formally about models of systems. 
  • Automated reasoning focuses on the automation of formal methods. 
  • A semi-automated-reasoning tool is one that requires hints from the user but still finds valid proofs in logic. 
As you can see, we have a choice of monikers when working in this space. At Amazon, we’ve chosen to use automated reasoning, as we think it best captures our ambition for automation and scale. In practice, some of our internal teams use both automated and semi-automated reasoning tools, because the scientists we've hired can often get semi-automated reasoning tools to succeed where the heuristics in fully automated reasoning might fail. For our externally facing customer features, we currently use only fully automated approaches.
Next steps
In this essay, I’ve introduced the idea of automated reasoning, with the smallest of toy programs. I haven’t described how to handle realistic programs, with heap or concurrency. In fact, there are a wide variety of automated-reasoning tools and techniques, solving problems in all kinds of different domains, some of them quite narrow. To describe them all and the many branches and sub-disciplines of the field (e.g. “SMT solving”, “higher-order logic theorem proving”, “separation logic”) would take thousands of blogs posts and books.
Automated reasoning goes back to the early inventors of computers. And logic itself (which automated reasoning attempts to solve) is thousands of years old. In order to keep this post brief, I’ll stop here and suggest further reading. Note that it’s very easy to get lost in the weeds reading depth-first into this area, and you could emerge more confused than when you started. I encourage you to use a bounded depth-first search approach, looking sequentially at a wide variety of tools and techniques in only some detail and then moving on, rather than learning only one aspect deeply.
Suggested books:
International conferences/workshops:
Tool competitions:
Some tools:
Interviews of Amazon staff about their use of automated reasoning:
AWS Lectures aimed at customers and industry:
AWS talks aimed at the automated-reasoning science community:
AWS blog posts and informational videos:
Some course notes by Amazon Scholars who are also university professors:
A fun deep track:
Some algorithms found in the automated theorem provers we use today date as far back as 1959, when Hao Wang used automated reasoning to prove the theorems from Principia Mathematica.

    



                            
                        

                    
                


                
                    

                        

    

    

        Research areas
    


    
        
    



                    

                

                
                    

                        

    

    

        Tags
    


    
        
    



                    

                

                

                
                    
About the Author

                    

                        
                            
    

        

            
                

                    Byron Cook
                

            
            
            
                

                    Amazon vice president and distinguished scientist Byron Cook is a leader in the field of formal verification, known for his contributions to SAT, SMT, and symbolic model checking, with applications to biological systems, computer operating systems, programming languages, and security. Byron’s work on automated reasoning at Amazon has led to higher levels of assurance in the cloud as well as new customer features.
                

            
        

    



                        
                    

                
            

        


        
    

    
    



    

        
Related content

        
    




    
        
    

    



    
    



    

        
Work with us
See more jobs
        
            See more jobs
        
    




    
        

            

                
                    

                        

    

    

        
            

                Research Scientist, AMX Research
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, NY, New York

            
        


        
    
The PXT (People Experience and Technology) AMX Research is seeking a highly skilled and motivated Research Scientist to join our team. You will be leading manager experience research space to support the PXT talent evaluation/talent management initiatives. If you enjoy innovating, thinking big and want to contribute directly to the success of a growing team, you may be a prime candidate for this position. Key job responsibilities Design experiments, test hypotheses, and build actionable models Conduct quantitative analyses of talent management data and trends Conduct qualitative data collection and analysis Partner closely and drive effective collaborations across multi-disciplinary research and product teams Consult on appropriate analytic methodologies and scope research requests




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Principal Applied Scientist, Neuro-Symbolic AI Labs
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, MA, Boston

            
        


        
    
We are looking for researchers who aim to build super-intelligent AI systems that leverage proof assistants to guide learning and reasoning. Our neuro-symbolic AI technology is applied across a wide range of science and engineering domains within Amazon, and you will join the team at the forefront of this research. As a Principal Applied Scientist, you will play a pivotal role in shaping the definition, vision, and development of product features from beginning to end. You will: - Define and implement new neuro-symbolic applications that employ scalable and efficient approaches to solve complex problems. - Work in an agile, startup-like development environment, where you are always working on the most important stuff. - Deliver high-quality scientific artifacts. About the team We work closely with academia. Our team includes an Amazon Scholar in mathematics, and we maintain active research collaborations with faculty at leading CS departments (MIT, Berkeley, CMU).




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist II
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, MA, N.reading

            
        


        
    
Amazon is on a mission to redefine the future of automation — and we're looking for exceptional talent to help lead the way. We are building the next generation of advanced robotic systems that seamlessly blend cutting-edge AI, sophisticated control systems, and novel mechanical design to create adaptable, intelligent automation solutions capable of operating safely alongside humans in dynamic, real-world environments. At Amazon, we leverage the power of machine learning, artificial intelligence, and advanced robotics to solve some of the most complex operational challenges at a scale unlike anywhere else in the world. Our fleet of robots spans hundreds of facilities globally, working in sophisticated coordination to deliver on our promise of customer excellence — and we're just getting started. As an Applied Scientist in Robot Perception, you will be at the forefront of this transformation. You will develop and deploy state-of-the-art perception algorithms that enable robots to truly understand and interact with the physical world — bridging the gap between theoretical research and real-world impact. Bringing deep expertise in Computer Vision and a nuanced understanding of the capabilities and limitations of modern Vision-Language Models (VLMs), you will innovate boldly and push the boundaries of what's possible. Our vision for the Perception layer is ambitious: to enable seamless, intelligent interaction between the user, the robot, and its environment. This is a rare opportunity to work at the intersection of deep learning, large language models, and robotics — contributing to research that doesn't just advance the field, but reshapes it. You will collaborate with world-class teams pioneering breakthroughs in dexterous manipulation, locomotion, and human-robot interaction, all at an unprecedented scale. Join us in building intelligent robotic systems that will define the future of automation and human-robot collaboration. Key job responsibilities - Design, develop, and deploy perception algorithms for robotics systems, including object detection, segmentation, tracking, depth estimation, and scene understanding - Contribute to research initiatives in computer vision, sensor fusion and 3D perception - Collaborate with cross-functional teams including robotics engineers, software engineers, and product managers to define and deliver perception capabilities - Drive end-to-end ownership of ML models — from data collection and labeling strategy to training, evaluation, and deployment - Define and track key metrics to measure perception system performance in real-world environments - Publish research findings in top-tier venues (CVPR, ICCV, ECCV, ICRA, NeurIPS, etc.) and contribute to patents A day in the life - Train ML models for deployment in simulation and real-world robots, identify and document their limitations post-deployment - Contribute to technical discussions within your team and with key stakeholders to develop innovative solutions to address identified limitations - Actively contribute to brainstorming sessions on adjacent topics, bringing fresh perspectives that help peers grow and succeed — and in doing so, build lasting trust across the team




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist, AMXL Worldwide Science
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Bellevue

            
        


        
    
Do you want to join an innovative team applying machine learning, advanced optimization techniques, and Large Language Models (LLMs) to transform the delivery of heavy and bulky items for Amazon customers? Are you excited about working with large-scale operational data and developing models that solve real-world logistics and fulfillment challenges? If so, the Amazon Extra Large (AMXL) Science team may be the right fit for you. AMXL is Amazon's specialized business for delivering heavy and bulky items, including appliances, furniture, fitness equipment, and mattresses, with a premium customer experience that includes room-of-choice delivery, at-home installations, and assembly services. We are seeking an Applied Scientist to help develop scalable machine learning and optimization solutions that improve delivery efficiency, capacity planning, network design, and customer experience across our rapidly growing network. In this role, you will partner with senior scientists and engineers to translate complex operational problems into data-driven solutions, build and evaluate models, and contribute to next-generation fulfillment and logistics systems. Key job responsibilities Apply machine learning, statistical techniques, time series modeling, and operations research to build and improve models for delivery routing, capacity planning, demand forecasting, workforce scheduling, and network optimization Analyze large-scale historical and real-time operational data to identify efficiency patterns, bottlenecks, and emerging trends across the AMXL network Develop, validate, and deploy innovative models under the guidance of senior scientists to improve cost-to-serve and customer experience Experiment with emerging technologies, including Generative AI and LLMs, to enhance automation, scheduling, and operational decision-making Collaborate closely with software engineers to implement models in real-time production systems Partner with operations, product, and business teams to translate operational insights into actionable improvements Build scalable, automated pipelines for data analysis, model training, and validation Monitor model performance and provide clear reporting on key operational and business metrics Research and prototype new modeling approaches to improve system performance and delivery quality A day in the life You will be working within a dynamic, diverse, and supportive group of scientists who share your passion for innovation and excellence in logistics and fulfillment science. You will work closely with business partners, operations teams, and engineering teams to create end-to-end scalable machine learning solutions that address real-world challenges across AMXL's heavy and bulky delivery network, including demand forecasting, capacity planning, routing optimization, and customer experience improvement. You will build scalable, efficient, and automated processes for large-scale data analyses, model development, model validation, and model implementation in production systems. You will also provide clear and compelling reports on your solutions to both technical and non-technical stakeholders, and contribute to the ongoing innovation and knowledge-sharing that are central to the team's success. About the team The AMXL (Amazon Extra Large) Worldwide Science team is a multidisciplinary organization of data scientists, applied scientists, and product managers dedicated to solving some of the most complex supply chain and logistics challenges in Amazon's heavy bulky business. The team's mission is to leverage advanced analytics, machine learning, and optimization science to drive measurable improvements across the AMXL end-to-end supply chain — from inbound fulfillment and middle-mile transportation to last-mile delivery of heavy and bulky items. The science team transforms complex operational data into actionable intelligence that directly impacts customer experience, cost efficiency, and delivery performance at a worldwide scale.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist, WW Promotions Science
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Seattle

            
        


        
    
Amazon's Worldwide Pricing & Promotions organization is seeking a strong Applied Scientist to help solve complex business problems involving promotional strategies at a global scale. This Applied Scientist will operate in a team of other scientists and economists. Our team applies causal inference, statistics, machine learning, forecasting, optimization, economics, and experimentation to drive actionable insights and to improve strategic business decision-making. This is an individual contributor role that requires collaboration across teams and functions to solve core business problems for the company around setting promotional strategies. The work is part of significant scientific investments in promotions intelligence systems that forecast customer demand and optimize promotions strategies across different surfaces. Key job responsibilities * Invent or adapt new scientific approaches, models, or algorithms inspired and driven by customers' needs and benefits * Produce research papers and reports that have the same level of correctness, scholarship, usefulness, completeness, depth, rigor, and originality as a top-tier external publication * Implement solutions that will be deployed into production or directly support production systems * Write clear, useful documentation describing algorithms and design choices in your components to make it possible for others to understand and reproduce your work * Contribute to operational excellence in the team's deliverable * Analyze the performance of your methods and models to understand the gaps, and iteratively propose solutions to improve * Champion the adoption of scientific advancements in the team * Help new teammates ramp up and understand who our customers are, what their needs are, how the team's solutions work, and how scientific components fit in those solutions A day in the life As an Applied Scientist on the WW Promotions Science team, you invent or adapt new scientific approaches, models, or algorithms to solve real-world business problems. Your work uses the latest (or the most appropriate) techniques from academic literature. You work semi-autonomously to successfully deliver solutions that are consistently of high quality (efficient, reproducible, testable code). You work collaboratively with teammates, partners, and stakeholders. You recognize discordant views and take part in constructive dialogue to resolve them. You adopt and identify opportunities to refine mechanisms to raise the general scientific knowledge in the team. About the team The WW Promotions Science team is responsible for driving scientific innovation to support pricing and promotions programs across Amazon's businesses. We specialize in experimental and observational causal methods, forecasting, and optimization. We apply these tools to drive business decision making at scale, leading to launch decisions of new pricing algorithms and new promotion strategies, understanding short- and long-term value of different programs, and the prioritization of budget allocations. We also develop models to set optimal prices and promotions, and define innovative price guardrails and incentives to optimize for long-term program health.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Quantum Applied Scientist, Processor Test & Measurement, Amazon Center for Quantum Computing
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, CA, Pasadena

            
        


        
    
The Amazon Web Services (AWS) Center for Quantum Computing in Pasadena, CA, is looking to hire a Quantum Research Scientist in the Processor Test and Measurement group. You will join a multi-disciplinary team of theoretical and experimental physicists, materials scientists, and hardware and software engineers working at the forefront of quantum computing. You should have a deep and broad knowledge of experimental measurement techniques. Candidates with a track record of original scientific contributions will be preferred. We are looking for candidates with strong engineering principles, resourcefulness and a bias for action, superior problem solving, and excellent communication skills. Working effectively within a team environment is essential. As a research scientist you will be expected to work on new ideas and stay abreast of the field of experimental quantum computation. Key job responsibilities We are looking to hire a Research Scientist to develop and test novel calibration and optimization tools for Quantum Error Correction on large scale quantum processors. You will be on a team of engineers and scientists at the frontier of quantum processor control and error correction. You are expected to take part in high-impact research projects that intersect with our engineering roadmap. We are looking for candidates with strong engineering principles and resourcefulness. Organization and communication skills are essential. A day in the life About the team Why AWS? Amazon Web Services (AWS) is the world’s most comprehensive and broadly adopted cloud platform. We pioneered cloud computing and never stopped innovating — that’s why customers from the most successful startups to Global 500 companies trust our robust suite of products and services to power their businesses. AWS Utility Computing (UC) provides product innovations — from foundational services such as Amazon’s Simple Storage Service (S3) and Amazon Elastic Compute Cloud (EC2), to consistently released new product innovations that continue to set AWS’s services and features apart in the industry. As a member of the UC organization, you’ll support the development and management of Compute, Database, Storage, Internet of Things (Iot), Platform, and Productivity Apps services in AWS. Within AWS UC, Amazon Dedicated Cloud (ADC) roles engage with AWS customers who require specialized security solutions for their cloud services. Inclusive Team Culture AWS values curiosity and connection. Our employee-led and company-sponsored affinity groups promote inclusion and empower our people to take pride in what makes us unique. Our inclusion events foster stronger, more collaborative teams. Our continual innovation is fueled by the bold ideas, fresh perspectives, and passionate voices our teams bring to everything we do. Diverse Experiences AWS values diverse experiences. Even if you do not meet all of the qualifications and skills listed in the job description, we encourage candidates to apply. If your career is just starting, hasn’t followed a traditional path, or includes alternative experiences, don’t let it stop you from applying. Mentorship & Career Growth We’re continuously raising our performance bar as we strive to become Earth’s Best Employer. That’s why you’ll find endless knowledge-sharing, mentorship and other career-advancing resources here to help you develop into a better-rounded professional. Work/Life Balance We value work-life harmony. Achieving success at work should never come at the expense of sacrifices at home, which is why we strive for flexibility as part of our working culture. When we feel supported in the workplace and at home, there’s nothing we can’t achieve in the cloud. Export Control Requirement: Due to applicable export control laws and regulations, candidates must be either a U.S. citizen or national, U.S. permanent resident (i.e., current Green Card holder), or lawfully admitted into the U.S. as a refugee or granted asylum, or be able to obtain a US export license. If you are unsure if you meet these requirements, please apply and Amazon will review your application for eligibility.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist, Trust CX Innovations&AI Policy
            

        

        

            
                
                    

                
            

            

            

            

            
                
IN, KA, Bengaluru

            
        


        
    
Alexa+ is Amazon’s next-generation, AI-powered assistant. Building on the original Alexa, it uses generative AI to deliver a more conversational, personalized, and effective experience. The Trust CX Innovations team is looking for an Applied Scientist with strong background in Generative AI space to build solutions that help in upholding customer trust for Alexa+. As an Applied Scientist in Trust CX innovations, you will be at the forefront of developing innovative solutions to critical challenges in AI trust and privacy. You'll lead research in trust-preserving machine learning techniques. We are working on revolutionizing the way Amazonians work and collaborate. You will help us achieve new heights of productivity through the power of advanced generative AI technologies. Key job responsibilities - Lead research initiatives in generative AI, focusing on LLMs, multimodal models, and frontier AI capabilities - Develop innovative approaches for model optimization, including prompt engineering, few-shot learning, and efficient fine-tuning - Pioneer new methods for AI safety, alignment, and responsible AI development - Design and execute sophisticated experiments to evaluate model performance and behavior - Lead the development of production-ready AI solutions that scale efficiently - Collaborate with product teams to translate research innovations into practical applications - Guide engineering teams in implementing AI models and systems at scale - Author technical papers for top-tier conferences - File patents for novel AI technologies and applications A day in the life You will be working with a group of talented scientists on researching algorithm and running experiments to test scientific proposal/solutions to improve our trust-preserving experiences. This will involve collaboration with partner teams including engineering, PMs, data annotators, and other scientists to discuss data quality, policy, and model development. You work closely with partner teams across Alexa to deliver platform features that require cross-team leadership. About the team Who We Are: Trust CX Innovations is a strategic innovation team within Amazon Devices & Services that focuses on advancing AI technology while prioritizing customer trust and experience. Our team operates at the intersection of artificial intelligence, privacy engineering and customer-centric design. Our Mission: To pioneer trustworthy AI innovations that delight customers while setting new standards for privacy and responsible technology development. We aim to transform how Amazon builds AI products by creating solutions that balance innovation with customer trust.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Sr. Applied Scientist, Amazon Publisher Monetization - Ads
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Seattle

            
        


        
    
Advertising is a complex, multi-sided market with many technologies at play within the industry. The industry is rapidly growing and evolving as viewers are shifting from traditional TV viewing to streaming video and publishers are increasingly adding video content to their online experiences. Amazon’s video advertising is a rising competitor in this industry. Amazon’s service has differentiated assets in our customer & audience insights, exclusive video content, and associated inventory that position us well as an end-to-end service for advertisers and agencies. We are innovating at the intersection of advertising, e-commerce, and entertainment. Amazon Publisher Monetization (APM) is looking for a a passionate and experienced scientist who is adept at a variety of skills; especially in generative AI, computer vision, and large language models that will accelerate our plans to maximize yield via AI-driven contextual targeting, Ads syndication and more. The ideal candidate will be an inventor at heart, they will provide science expertise, rapidly prototype, iterate, and launch, foster the spirit of collaboration and innovation within our larger sister teams and their scientists, and execute against a compelling product roadmap designed to bring AI-led science innovation to solve one of the most challenging problems in advertising. Key job responsibilities This role is focused on shaping our approach to the solving the trifecta of advertising - serving the right ad to the right viewer at the right moment - delivering engaging ads for viewers, improved performance for advertisers, and maximizing the yield of our supply inventory. Responsibilities include: * Partner deeply with Product and Engineering to develop AI-based solutions to generating contextual signals across both video (VOD and Live) and display ads. * Drive end-to-end applied science projects that have a high degree of ambiguity, scale, complexity. * Provide technical/science leadership related to computer vision, large language models and contextual targeting. * Research new and innovative machine learning approaches. * Partner with Applied Scientists across the broader org to make the most of prior art and contribute back to this community the innovation that you come up with.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist II, Alexa International
            

        

        

            
                
                    

                
            

            

            

            

            
                
IN, KA, Bengaluru

            
        


        
    
Alexa International is looking for passionate, talented, and inventive Senior Applied Scientists to help build industry-leading technology with Large Language Models (LLMs) and multimodal systems, requiring strong deep learning and generative models knowledge. Senior applied scientists will drive cross-team scientific strategy, influence partner teams, and deliver solutions that have broad impact across Alexa's international products and services. Key job responsibilities As a Applied Scientist with II the Alexa International team, you will work with talented peers to develop novel algorithms and modeling techniques to advance the state of the art with LLMs, particularly delivering industry-leading scientific research and applied AI for multi-lingual applications — a challenging area for the industry globally. Your work will directly impact our global customers in the form of products and services that support Alexa+. You will leverage Amazon's heterogeneous data sources and large-scale computing resources to accelerate advances in text, speech, and vision domains. The ideal candidate possesses a solid understanding of machine learning, speech and/or natural language processing, modern LLM architectures, LLM evaluation & tooling, and a passion for pushing boundaries in this vast and quickly evolving field. They thrive in fast-paced environment, like to tackle complex challenges, excel at swiftly delivering impactful solutions while iterating based on user feedback, and are able to influence and align multiple teams around a shared scientific vision. A day in the life * Analyze, understand, and model customer behavior and the customer experience based on large-scale data. * Build novel online & offline evaluation metrics and methodologies for multimodal personal digital assistants. * Fine-tune/post-train LLMs using advanced and innovative techniques like SFT, DPO, Reinforcement Learning (RLHF and RLAIF) for supporting model performance specific to a customer’s location and language. * Quickly experiment and set up experimentation framework for agile model and data analysis or A/B testing. * Contribute through industry-first research to drive innovation forward. * Drive cross-team scientific strategy and influence partner teams on LLM evaluation frameworks, post-training methodologies, and best practices for international speech and language systems. * Lead end-to-end delivery of scientifically complex solutions from research to production, including reusable science components and services that resolve architecture deficiencies across teams. * Serve as a scientific thought leader, communicating solutions clearly to partners, stakeholders, and senior leadership. * Actively mentor junior scientists and contribute to the broader internal and external scientific community through publications and community engagement.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Senior Applied Scientist, Sponsored Products and Brands
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, NY, New York

            
        


        
    
The Sponsored Products and Brands team at Amazon Ads is re-imagining the advertising landscape through novel generative AI technologies, revolutionizing how millions of customers discover products and engage with brands across Amazon.com and beyond. We are at the forefront of re-inventing advertising experiences, bridging human creativity with artificial intelligence to transform every aspect of the advertising lifecycle from ad creation and optimization to performance analysis and customer insights. We are a passionate group of innovators dedicated to developing responsible and intelligent AI technologies that balance the needs of advertisers, enhance the shopping experience, and strengthen the marketplace ecosystem. If you're energized by solving complex challenges and pushing the boundaries of what's possible with AI, join us in shaping the future of advertising. Key job responsibilities As an applied scientist on our team, you will * Develop AI solutions for Sponsored Products and Brands advertiser and shopper experiences powered by video. You will build recommendation systems that leverage computer vision to develop and improve video performance and outcomes * You invent and design new solutions for scientifically-complex problem areas and/or opportunities in new business initiatives. * You drive or heavily influence the design of scientifically-complex software solutions or systems, for which you personally write significant parts of the critical scientific novelty. You take ownership of these components, providing a system-wide view and design guidance. These systems or solutions can be brand new or evolve from existing ones. * Define a long-term science vision and roadmap for our Sponsored Products and Brands advertising business, driven from our customers' needs, translating that direction into specific plans for applied scientists and engineering teams. This role combines science leadership, organizational ability, technical strength, product focus, and business understanding. * Work closely with engineers and product managers to design, implement and launch AI solutions end-to-end; * Design and conduct A/B experiments to evaluate proposed solutions based on in-depth data analyses; * Think big about the arc of development of Gen AI over a multi-year horizon, and identify new opportunities to apply these technologies to solve real-world problems * Effectively communicate technical and non-technical ideas with teammates and stakeholders; * Translate complex scientific challenges into clear and impactful solutions for business stakeholders. * Mentor and guide junior scientists, fostering a collaborative and high-performing team culture. * Stay up-to-date with advancements and the latest modeling techniques in the field About the team The Sponsored Videos team is responsible for the design, development, and implementation of Sponsored Products and Sponsored Brands Video experiences worldwide. We design and launch video based experiences, aiming to delight shoppers and advertisers worldwide.




        

        

        

        
    


    



                    

                
            

        

    

    

        See more jobs
    






        




    

        
            
        
        

            

                
                    

                        

                    

                
            

            
                

                    

                        

  

      
          

              
                  
    
        View from space of a connected network around planet Earth representing the Internet of Things.
    

              
          

      

      

        

          
              
Get more from Amazon Science

          

          
    
Subscribe to our newsletter



        

        
          
        
      

  



                    

                

            
        

    


    

        

        
            
Amazon.com | Conditions of Use | Privacy | © 1996-2026 Amazon.com, Inc. or its affiliates

        
        
            

    
Social