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
        
    




    
        

            

                
                    

                        

    

    

        
            

                Applied Scientist II, Amazon Connect
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, CA, Mountain View

            
        


        
    
Do you want to join a team of innovative scientists to research and develop generative AI technology that would disrupt the industry? Do you enjoy dealing with ambiguity and working on hard problems in a fast-paced environment? Amazon Connect is a highly disruptive cloud-based contact center from AWS that enables businesses to deliver intelligent, engaging, dynamic, and personalized customer service experiences. The Agentic Customer Experience (ACX) org is responsible for weaving native-AI across the Connect application experiences delivered to end-customers, agents, and managers/supervisors. The Interactive AI Science team, serves as the cornerstone for AI innovation across Amazon Connect, functioning as the sole science team support high impact product including Amazon Q in Connect, Contact Lens and other key initiatives. As an Applied Scientist on our team, you will work closely with senior technical and business leaders from within the team and across AWS. You distill insight from huge data sets, conduct cutting edge research, foster ML models from conception to deployment. You have deep expertise in machine learning and deep learning broadly, and extensive domain knowledge in natural language processing, generative AI and LLM Agents evaluation and optimization, etc. You are comfortable with quickly prototyping and iterating your ideas to build robust ML models using technology such as PyTorch, Tensorflow and AWS Sagemaker. The ideal candidate has the ability to understand, implement, innovate on the state-of-the-art Agentic AI based systems. We have a rapidly growing customer base and an exciting charter in front of us that includes solving highly complex engineering and scientific problems. We are looking for passionate, talented, and experienced people to join us to innovate on modern contact centers in the cloud. The position represents a rare opportunity to be a part of a fast-growing business soon after launch, and help shape the technology and product as we grow. You will be playing a crucial role in developing the next generation contact center, and get the opportunity to design and deliver scalable, resilient systems while maintaining a constant customer focus. About the team 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. 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. Inclusive Team Culture Here at AWS, it’s in our nature to learn and be curious. Our employee-led affinity groups foster a culture of inclusion that empower us to be proud of our differences. Ongoing events and learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences, inspire us to never stop embracing our uniqueness. 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.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Sr Research Scientist, Amazon Shipping
            

        

        

            
                
                    

                
            

            

            

            

            
                
IN, HR, Gurugram

            
        


        
    
Lead ML teams building large-scale forecasting and optimization systems that power Amazon’s global transportation network and directly impact customer experience and cost. As an Sr Research Scientist, you will set scientific direction, mentor applied scientists, and partner with engineering and product leaders to deliver production-grade ML solutions at massive scale. Key job responsibilities 1. Lead and grow a high-performing team of Applied Scientists, providing technical guidance, mentorship, and career development. 2. Define and own the scientific vision and roadmap for ML solutions powering large-scale transportation planning and execution. 3. Guide model and system design across a range of techniques, including tree-based models, deep learning (LSTMs, transformers), LLMs, and reinforcement learning. 4. Ensure models are production-ready, scalable, and robust through close partnership with stakeholders. Partner with Product, Operations, and Engineering leaders to enable proactive decision-making and corrective actions. 5. Own end-to-end business metrics, directly influencing customer experience, cost optimization, and network reliability. 6. Help contribute to the broader ML community through publications, conference submissions, and internal knowledge sharing. A day in the life Your day includes reviewing model performance and business metrics, guiding technical design and experimentation, mentoring scientists, and driving roadmap execution. You’ll balance near-term delivery with long-term innovation while ensuring solutions are robust, interpretable, and scalable. Ultimately, your work helps improve delivery reliability, reduce costs, and enhance the customer experience at massive scale.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Member of Technical Staff, Engineering Manager , Amazon AGI Lab
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, MA, Boston

            
        


        
    
Amazon launched the AGI Lab to develop foundational capabilities for useful AI agents. We built Nova Act - a new AI model trained to perform actions within a web browser. The team builds AI/ML infrastructure that powers our production systems to run performantly at high scale. We’re also enabling practical AI to make our customers more productive, empowered, and fulfilled. In particular, our work combines large language models (LLMs) with reinforcement learning (RL) to solve reasoning, planning, and world modeling in both virtual and physical environments. Our lab is a small, talent-dense team with the resources and scale of Amazon. Each team in the lab has the autonomy to move fast and the long-term commitment to pursue high-risk, high-payoff research. We’re entering an exciting new era where agents can redefine what AI makes possible. We’d love for you to join our lab and build it from the ground up! Key job responsibilities This role will lead a team of SDEs building AI agents infrastructure from launch to scale. The role requires the ability to span across ML/AI system architecture and infrastructure. You will work closely with application developers and scientists to have a impact on the Agentic AI industry. We're looking for a Software Development Manager who is energized by building high performance systems, making an impact and thrives in fast-paced, collaborative environments. About the team Check out the Nova Act tools our team built on on nova.amazon.com/act




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Instrument Control Engineer, Software, Center for Quantum Computing
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, CA, Pasadena

            
        


        
    
The Amazon Center for Quantum Computing (CQC) is a multi-disciplinary team of scientists, engineers, and technicians, on a mission to develop a fault-tolerant quantum computer. We are looking to hire an Instrument Control Engineer to join our growing software team. You will work closely with our experimental physics and control hardware development teams to enable their work characterizing, calibrating, and operating novel quantum devices. The ideal candidate should be able to translate high-level science requirements into software implementations (e.g. Python APIs/frameworks, compiler passes, embedded SW, instrument drivers) that are performant, scalable, and intuitive. This requires someone who (1) has a strong desire to work within a team of scientists and engineers, and (2) demonstrates ownership in initiating and driving projects to completion. This role has a particular emphasis on working directly with our control hardware designers and vendors to develop instrument software for test and measurement. Inclusive Team Culture Here at Amazon, it’s in our nature to learn and be curious. Our employee-led affinity groups foster a culture of inclusion that empower us to be proud of our differences. Ongoing events and learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon conferences, inspire us to never stop embracing our uniqueness. Diverse Experiences Amazon 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. Key job responsibilities - Work with control hardware developers, as a “subject matter expert” on the software interfaces around our control hardware - Collaborate with external control hardware vendors to understand and refine integration strategies - Implement instrument drivers and control logic in Python and/or a low-level languages, including C++ or Rust - Contribute to our compiler backend to enable the efficient execution of OpenQASM-based experiments on our next-generation control hardware - Benchmark system performance and help define key performance metrics - Ensure new features are successfully integrated into our Python-based experimental software stack - Partner with scientists to actively contribute to the codebase through mentorship and documentation We are looking for candidates with strong engineering principles, a bias for action, superior problem-solving, and excellent communication skills. Working effectively within a team environment is essential. As an Instrument Control Engineer embedded in a broader science organization, you will have the opportunity to work on new ideas and stay abreast of the field of experimental quantum computation. A day in the life Your time will be spent on projects that extend functional capabilities or performance of our internal research software stack. This requires working backwards from the needs of science staff in the context of our larger experimental roadmap. You will translate science and software requirements into design proposals balancing implementation complexity against time-to-delivery. Once a design proposal has been reviewed and accepted, you’ll drive implementation and coordinate with internal stakeholders to ensure a smooth roll out. Because many high-level experimental goals have cross-cutting requirements, you’ll often work closely with other engineers or scientists or on the team. About the team You will be joining the Software group within the Amazon Center of Quantum Computing. Our team is comprised of scientists and software engineers who are building scalable software that enables quantum computing technologies.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist, Workplace Health & Safety 
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Bellevue

            
        


        
    
Are you driven by the challenge of solving complex problems that directly impact the safety and well-being of millions of Amazon Associates worldwide? Do you want to push the boundaries of AI to build innovative solutions that make workplaces safer and more efficient? If so, we invite you to join our WHS DataTech team as an Applied Scientist and take your career to the next level! At WHS DataTech, we leverage Large Language Models (LLMs), Computer Vision, and AI-driven innovations to develop industry-leading solutions that proactively enhance workplace safety. Our work spans real-time risk assessment, predictive analytics, and AI-powered insights, all aimed at creating a safer work environment at scale. As an Applied Scientist specializing in LLMs and Computer Vision, you will play a pivotal role in shaping our next-generation safety solutions. You’ll be at the forefront of innovation, designing and implementing AI-powered features that redefine workplace safety. Your work will drive strategic decisions, optimize system architecture, and influence best practices, ensuring our technology remains industry-leading. Key job responsibilities - Apply LLM model to analyze complex unstructured datasets and extract meaningful insights. - Collaborate with software engineers to implement and deploy machine learning (LLM or CV) solutions. - Conduct experiments and evaluate model performance, iterating and improving as needed. - Stay up-to-date with the latest advancements in machine learning and related fields. - Collaborate with cross-functional teams to understand business needs and identify areas for application of machine learning. - Present findings and recommendations to stakeholders and contribute to the overall research and development strategy. A day in the life Amazon offers a full range of benefits that support you and eligible family members, including domestic partners and their children. Benefits can vary by location, the number of regularly scheduled hours you work, length of employment, and job status such as seasonal or temporary employment. The benefits that generally apply to regular, full-time employees include: 1. Medical, Dental, and Vision Coverage 2. Maternity and Parental Leave Options 3. Paid Time Off (PTO) 4. 401(k) Plan If you are not sure that every qualification on the list above describes you exactly, we'd still love to hear from you! At Amazon, we value people with unique backgrounds, experiences, and skillsets. If you’re passionate about this role and want to make an impact on a global scale, please apply! About the team WHS DataTech is a multidisciplinary team of scientists and engineers dedicated to building AI-powered solutions that improve workplace safety across Amazon. We work at the intersection of large-scale data, advanced machine learning, and computer vision, delivering innovations that enhance decision-making, streamline operations, and protect millions of associates worldwide. Our collaborative culture emphasizes scientific rigor, engineering excellence, and a strong mission focus on creating safer, more efficient workplaces.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist II, AERO Agentic AI Team
            

        

        

            
                
                    

                
            

            

            

            

            
                
IN, KA, Bengaluru

            
        


        
    
Amazon is seeking passionate, talented and inventive Applied Scientists with a strong machine learning background to help build Agentic AI solutions for Selling Partners and Retail users. Our mission is to elevate their experience through intelligent, collaborative Agentic AI solution powered by specialized agents that deliver seamless, personalized support at scale. Key job responsibilities As part of our AERO team in Amazon PGX, you will work alongside internationally recognized experts to develop novel solutions and modeling techniques to advance the state-of-the-art in Generative and Agentic AI. Your work will directly impact millions of our users in the form of products and services that improves their experience. You will gain hands on experience with Amazon’s native/partnered Large Language Models (LLMs), technologies like AgentCore, AgentMemory, Strands and Model Context Protocol (MCPs). We are also looking for talents with experiences/expertise in building large-scale and high-performing systems.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Machine Learning Scientist / Applied Scientist, EU Prime and Marketing Analytics & Science (PRIMAS)
            

        

        

            
                
                    

                
            

            

            

            

            
                
ES, B, Barcelona

            
        


        
    
Are you interested in building the measurement foundation that proves whether targeted, cohort-based marketing actually changes customer behavior at Amazon scale? We are seeking an Applied Scientist to own measurement and experimentation for our Lifecycle Marketing Experimentation roadmap within the PRIMAS (Prime & Marketing Analytics and Science) team. In this role, you will design and execute rigorous experiments that measure the effectiveness of audience-based marketing campaigns across multiple channels, providing the evidence that guides marketing strategy and investment decisions. This is a high-impact role where you will build measurement frameworks from scratch, design experiments that isolate causal effects, and establish the experimental standards for lifecycle marketing across EU. You will work closely with business leaders and the senior science lead to answer critical questions: does targeting specific cohorts (Bargain hunters, Young adults) improve efficiency vs. broad campaigns? Which creative strategies drive behavior change? How should we optimize marketing spend across channels? Key job responsibilities Measurement & Experimentation Ownership: 1. Own measurement end-to-end for lifecycle marketing campaigns – design experiments (RCTs, geo-tests, audience holdouts) that measure campaign effectiveness across marketing channels 2. Build measurement frameworks and experimental best practices that work across different activation platforms and can scale to multiple campaigns 3. Establish experimental standards and tooling for lifecycle marketing, ensuring statistical rigor while balancing business constraints Causal Inference & Analysis: 1. Apply causal inference methods to measure incremental impact of marketing campaigns vs. counterfactual 2. Navigate measurement challenges across different platforms (Meta attribution, LiveRamp, clean rooms, onsite tracking) 3. Analyze experiment results and provide optimization recommendations based on statistical evidence 4. Establish guardrails and success criteria for campaign evaluation About the team The PRIMAS team, is part of a larger tech tech team of 100+ people called WIMSI (WW Integrated Marketing Systems and Intelligence). WIMSI core mission is to accelerate marketing technology capabilities that enable de-averaged customer experiences across the marketing funnel: awareness, consideration, and conversion.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Principal Applied Scientist, Amazon - Sponsored Products and Brands 
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Seattle

            
        


        
    
The Sponsored Products and Brands (SPB) team at Amazon Ads is re-imagining the advertising landscape through generative and agentic 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 to transform every aspect of the advertising lifecycle; from ad creation, delivery, optimization, performance management, and beyond. We are a passionate group of innovators dedicated to developing state-of-the-art AI technologies that balance the needs of advertisers and enhance the shopping experience. Within SPB, the SPB Offsite (SPBO) team builds solutions to extend campaigns to reach customers off the store and extend shopping experiences on third-party sites where shoppers search and discover products. We use industry-leading machine learning, high-scale low-latency systems, and gen AI technologies to create better sponsored customer experiences off the store. The Principal Applied Scientist for SPBO leads the technical vision and scientific strategy for extending Amazon Advertising's sponsored experiences to the broader web—meeting shoppers wherever they search, browse, and discover products. This is a multi-disciplinary scientific space spanning machine learning, large-scale optimization, causal inference, NLP, information retrieval, and generative AI. You will define and drive the science roadmap for how Amazon connects advertisers with high-intent customers across third-party environments at massive scale and with low latency. As a GenAI-first organization, we build foundational and agentic models that power advertiser use cases across Ads, while empowering our Applied Scientists to directly build and ship products. You will be a hands-on technical leader who architects novel solutions end-to-end—from research through production—while mentoring a team of scientists across diverse domains. The problems you will tackle are among the hardest in ad tech. You will develop models that leverage Amazon's first-party shopping signals to reach high-value audiences in third-party environments where signal density differs fundamentally from on-Amazon contexts. You will innovate on real-time bidding, auction dynamics, and ranking models across heterogeneous supply sources with distinct inventory characteristics, latency constraints, and auction mechanics. You will design ML approaches that maintain effectiveness amid an evolving privacy landscape—turning constraints from cookie deprecation, regulation, and platform restrictions into innovation opportunities. You will influence attribution models that capture the incremental value of offsite advertising on shopping outcomes, bridging measurement gaps between offsite touchpoints and on-Amazon conversions. You will pioneer generative and agentic AI to personalize ad creatives and shopping experiences for offsite contexts, and develop scientific frameworks to optimize spend allocation across supply partners and channels. You will partner with engineering, product, and business leaders as well as external partners to shape product strategy with scientific insight and drive results at scale. You will represent Amazon Advertising's offsite science externally through patents and industry engagement. Key job responsibilities - Driving the scientific vision of the teams in your organization and advising and influencing its technical leadership on ad serving, bidding, ranking, and offsite advertising models and products. - Identifying, tackling, and proposing innovative solutions to intrinsically hard, previously unsolved problems in offsite ad tech. - Bringing clarity to complex problems, probing assumptions, illuminating pitfalls, fostering shared understanding, and guiding towards effective solutions. - Serving and being recognized by internal and external peers as a thought leader in offsite advertising science, including real-time bidding, personalization, privacy-preserving ML, and generative AI for ad experiences. - Influencing your team's science and business strategy by driving one or more team roadmaps contributing to the organization's roadmap and taking responsibility for some organizational goals. You drive multiple new product features from inception to production launch. - Guiding the career development of others, actively mentoring and educating the larger applied science community on trends, technologies, and best practices.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist II, Industrial Robotics Group
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, MA, N.reading

            
        


        
    
Industrial Robotics Group is seeking exceptional talent to help develop the next generation of advanced robotics systems that will transform automation at Amazon's scale. We're building revolutionary robotic systems that combine cutting-edge AI, sophisticated control systems, and advanced mechanical design to create adaptable automation solutions capable of working safely alongside humans in dynamic environments. This is a unique opportunity to shape the future of robotics and automation at an unprecedented scale, working with world-class teams pushing the boundaries of what's possible in robotic manipulation, locomotion, and human-robot interaction. We're seeking an Applied Scientist to join our Robotics team. This role focuses on developing innovative machine learning solutions that enable robots to perform complex manipulation tasks in real-world environments. You will work on creating adaptive learning approaches that combine traditional robotics with modern ML techniques to improve robot performance and reliability. In this role, you will collaborate with multidisciplinary teams to advance the state-of-the-art in robotic manipulation, contributing to the development of next-generation autonomous systems that can operate safely and efficiently within Amazon fulfillment centers. Key job responsibilities - Lead design, adapt, and implement novel machine learning solutions for manipulation robots - Create hybrid approaches combining classical methods with learning-based solutions - Design learning algorithms for automated parameter tuning and adaptation - Develop data collection pipelines and methodologies for capturing high-quality demonstrations of dexterous tasks - Build and test prototype robotic workcell setups to validate the performance of the solution - Partner with cross-functional teams to rapidly create new concepts and prototypes - Work with Amazon's robotics engineering and operations teams to grasp their requirements and develop tailored solutions - Document the architecture, performance, and validation of the final system




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist, EU INTech Consumer Selection, Tamale
            

        

        

            
                
                    

                
            

            

            

            

            
                
ES, M, Madrid

            
        


        
    
At Amazon, we are committed to being the Earth's most customer-centric company. The European International Technology group (EU INTech) owns the enhancement and delivery of Amazon's engineering to all the varied customers and cultures of the world. We do this through a combination of partnerships with other Amazon technical teams and our own innovative new projects. You will be joining the Tamale team to work on Haul. As part of EU INTech and Haul, Tamale strives to create a discovery-driven shopping experience using challenging machine learning and ranking solutions. You will be exposed to large-scale recommendation systems, multi-objective optimization, and state-of-the-art deep learning architectures, and you'll be part of a key effort to improve our customers' browsing experience by building next-generation ranking models for Amazon Haul's endless scroll experience. We are looking for a passionate, talented, and inventive Scientist with a strong machine learning background to help build industry-leading ranking solutions. We strongly value your hard work and obsession to solve complex problems on behalf of Amazon customers. Key job responsibilities We look for applied scientists who possess a wide variety of skills. As the successful applicant for this role, you will work closely with your business partners to identify opportunities for innovation. You will apply machine learning solutions to optimize multi-objective ranking, improve discovery engagement through contextual signals, and scale ranking systems across multiple marketplaces. You will work with business leaders, scientists, and product managers to translate business and functional requirements into concrete deliverables, including the design, development, testing, and deployment of highly scalable distributed ranking services. You will be part of a team of scientists and engineers working on solving ranking and personalization challenges at scale. You will be able to influence the scientific roadmap of the team, setting the standards for scientific excellence. You will be working with state-of-the-art architectures and real-time feature serving systems. Your work will improve the experience of millions of daily customers using Amazon Haul worldwide. You will have the chance to have great customer impact and continue growing in one of the most innovative companies in the world. You will learn a huge amount - and have a lot of fun - in the process!




        

        

        

        
    


    



                    

                
            

        

    

    

        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 monthly newsletter



        

        
          
        
      

  



                    

                

            
        

    


    

        

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

        
        
            

    
Social