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, Structural Design Integrity, Hardware - Product Integrity
            

        

        

            
                
                    

                
            

            

            

            

            
                
CN, 31, Shanghai

            
        


        
    
As an Applied Scientist, you will be responsible for bringing new product designs through to manufacturing. You will work closely with multi-disciplinary groups including Product Design, Industrial Design, Hardware Engineering, and Operations, to drive key aspects of engineering of consumer electronics products. In this role, you will use expertise in physical sciences, theoretical, numerical or empirical techniques to create scalable models representing response of physical systems or devices, including: * Applying domain scientific expertise towards developing innovative analysis and tests to study viability of new materials, designs or processes * Working closely with engineering teams to drive validation, optimization and implementation of hardware design or software algorithmic solutions to improve product and customer risks * Establishing scalable, efficient, automated processes to handle large scale design and data analysis * Conducting research into use conditions, materials and analysis techniques * Tracking general business activity including device health in field and providing clear, compelling reports to management on a regular basis * Developing, implementing guidelines to continually optimize design processes * Using simulation tools like LS-DYNA, and Abaqus for analysis and optimization of product design * Using of programming languages like Python and Matlab for analytical/statistical analyses and automation * Demonstrating strong understanding across multiple physical science domains, e.g. structural, thermal, fluid dynamics, and materials * Developing, analyzing and testing structural solutions from concept design, feature development, product architecture, through system validation * Supporting product development and optimization through application of analysis and testing of complex electronic assemblies using advanced simulation and experimentation tools and techniques




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist, Personalization, Personalization
            

        

        

            
                
                    

                
            

            

            

            

            
                
IL, Haifa

            
        


        
    
We are seeking an Applied Scientist to help build Amazon’s next-generation customer memory and personalization systems. Are you interested in building systems that move beyond reacting to customer behavior, to actually understanding and remembering it over time? Our team is building Amazon’s customer memory layer – a system that extracts, curates, and reasons over customer knowledge to power next-generation personalization. This includes transforming noisy, unstructured signals into durable, high-quality representations of customer preferences, intents, and life events, and using them in real time to improve customer experiences. We are part of Amazon’s Personalization organization, a high-performing group that leverages large-scale machine learning, generative AI, and distributed systems to deliver highly relevant customer experiences. We tackle challenging problems at the intersection of information extraction, knowledge representation, LLM reasoning, and recommendation systems. Our systems operate under real-world constraints of scale, latency, and quality, requiring careful tradeoffs between precision, recall, and responsiveness. This team plays a central role in defining how Amazon understands its customers, and how that understanding is applied across the shopping experience. As an Applied Scientist, you will design and build ML and LLM-powered solutions for Amazon's customer memory and personalization systems. You will work on how customer knowledge is extracted, validated, and applied in production systems. You will own the end-to-end delivery of ML solutions, from problem formulation and modeling to offline and online experimentation, and production deployment at scale. You will deliver high-quality, scalable systems that power customer-facing experiences. You will drive work across areas such as fact extraction, memory quality and lifecycle, temporal reasoning, and grounded personalization, while navigating tradeoffs between quality, latency, and coverage. You will collaborate closely with engineering and product teams to translate research into measurable customer impact. Please visit https://www.amazon.science for more information.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Sr Data Scientist, Amazon - Vertical Ads
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Seattle

            
        


        
    
Are you passionate about solving big problems from ground-up? Do you enjoy building new state-of-the-art products at internet scale? Come lead the innovation in this startup team, vertical ad products. This is a green field problem without a known answer or a pattern to follow. We have ambitious vision to simplify full funnel advertising solutions, at scale, with specialized agentic AI-powered models and diversify the demand to strategic verticals including finserv, autos, locals.. etc. We are seeking an experienced Sr Data Scientist to drive innovation in our Ads Foundational Model. In this individual contributor role, you will apply advanced machine learning techniques to improve advertiser performance and customer experience. Key job responsibilities As a Data Scientist on this team, you will: 1. Develop and drive the science strategy for Ads Foundational Model (Ads-FM), aligning it with the program's objectives and overall business goals. 2. Identify high-impact opportunities within Ads-FM program and lead the ideation, planning, and execution of science initiatives to address them. 3. Build and deploy machine learning models using computer vision, natural language processing, and deep learning to evaluate and enhance ad effectiveness. 4. Develop algorithms that extract meaningful signals from image, video, and audio content to predict and improve customer engagement 5. Leverage Amazon's extensive data repository to create predictive models that generate actionable recommendations for more compelling ad creative 6. Collaborate with business leaders and cross-functional teams to implement ML-powered solutions 7. Contribute to the ML roadmap for the Ads-FM program through innovation and research.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Director, Economist - Head of Experimentation & Value, Devices Science Optimization (DSO)
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Seattle

            
        


        
    
You will build and lead the economics research agenda for measurement, experimentation, and value attribution for Amazon's Devices & Services organization. Your team is the "truth layer" of the Intelligence Core — the shared economics and causal inference capability that serves all Devices product lines, marketing pods, and Finance leadership with causal evidence of what Devices are worth and whether our investments are working. This is not a traditional analytics or measurement role. You will own an active research program in experimentation design — identifying and executing the causal studies that produce the causal inputs for pricing decisions, marketing optimization, and portfolio strategy. Your outputs provide the causal evidence base that L8 peers and senior leadership consume to make billions of dollars in investment decisions across the D&S portfolio. You will also own the economic models that validate and drive execution across the full surface area of marketing spend for devices and services. Key job responsibilities Economic Value: • Downstream value attribution for all Devices product lines — Impact on Prime, subscription lift, consumer spending, advertising value • Alexa+ value isolation and cross-PL attribution • Causal frameworks connecting device sales to Prime acquisition, subscription retention, and ecosystem engagement Marketing Science & Measurement: • Build the marketing science function from scratch • Incrementality measurement for marketing spend across all channels • Attribution methodology, measurement standards, and cross-pod governance • Marketing ROI frameworks for use by category marketers • CCM certification methodology and scenario planning models for optimal investment allocation Experimentation: • Owning the estimation methodology, identification strategies, data inputs/outputs, and refresh cadence • You will build this team's analytics function with AI at its core from day one • Experimentation governance — managing interference across teams, setting standards for causal validity • Evaluation framework for AI agents and autonomous optimization systems




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Quality Assurance Manager, Special Projects
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Seattle

            
        


        
    
Innovators wanted! Are you an entrepreneur? A builder? A dreamer? This role is part of an Amazon Special Projects team that takes the company’s Think Big leadership principle to the extreme. We focus on creating entirely new products and services with a goal of positively impacting the lives of our customers. No industries or subject areas are out of bounds. If you’re interested in innovating at scale to address big challenges in the world, this is the team for you. Here at Amazon, we embrace our differences. We are committed to furthering our culture of inclusion. We have thirteen employee-led affinity groups, reaching 40,000 employees in over 190 chapters globally. We are constantly learning through programs that are local, regional, and global. Amazon’s culture of inclusion is reinforced within our 16 Leadership Principles, which remind team members to seek diverse perspectives, learn and be curious, and earn trust. Our team highly values work-life balance, mentorship and career growth. We believe striking the right balance between your personal and professional life is critical to life-long happiness and fulfillment. We care about your career growth and strive to assign projects and offer training that will challenge you to become your best.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Manager Research Science, Last Mile Science and Analytics
            

        

        

            
                
                    

                
            

            

            

            

            
                
IN, KA, Bengaluru

            
        


        
    
Have you ever wondered how that Amazon box with the smile arrives so quickly, where it came from, and how much it cost Amazon to deliver? The WW Amazon Logistics, Business Analytics team manages the delivery of tens of millions of products every week to Amazon's customers, achieving on-time delivery in a cost-effective manner. We are seeking an enthusiastic, customer-obsessed Manager Research Science with strong analytical skills to join our team. This role is crucial in optimizing Amazon's vast delivery network and will have significant impact on the customer experience, particularly in the final phase of delivery. As a Manager Research Science, you will: 1. Address business challenges through building compelling cases and using data to influence change across the organization 2. Develop input and assumptions based on preexisting models to estimate costs and savings opportunities associated with varying levels of network growth and operations 3. Create metrics to measure business performance, identify root causes and trends, and prescribe action plans 4. Manage multiple high-impact projects simultaneously 5. Work with technology teams and product managers to develop new tools and systems supporting business growth 6. Communicate with and support various internal stakeholders and external audiences 7. Implement scheduling solutions, improve metrics, and develop scalable processes and tools The ideal candidate will have: - Extensive experience in operations research and data-driven decision making - Strong analytical and problem-solving skills - Robust program management and research science skills - Ability to work with a team and make independent decisions in ambiguous environments - Customer-obsessed mindset with a focus on improving the Amazon delivery experience This role offers the autonomy to think strategically and make data-driven decisions from day one. Join us in shaping the future of e-commerce delivery and addressing the core challenges in our world-class operations space! Key job responsibilities 1. Advanced Modeling and Algorithm Development: - Design and implement sophisticated machine learning models for logistics optimization - Develop complex time series forecasting algorithms for demand prediction and resource allocation 2. AI and Machine Learning Integration: - Architect and deploy AI-powered systems to enhance decision-making in logistics operations - Implement deep learning techniques for image recognition in package sorting and handling - Develop reinforcement learning algorithms for adaptive scheduling and resource management 3. Big Data Analytics and Processing: - Design and implement distributed computing solutions for processing massive logistics datasets - Utilize cloud computing platforms (e.g., AWS) for scalable data processing and analysis 4. AI-Driven Workflow Optimization: - Design and implement AI agents for autonomous decision-making in logistics processes - Create machine learning models for customer behavior analysis and personalized delivery options 5. Software Development and System Architecture: - Write efficient, scalable code in languages such as Python, Java, or C++ - Develop and maintain complex software systems for logistics optimization - Stay at the forefront of AI and ML research - Publish research findings in top-tier conferences and journals About the team We are Amazon's Last Mile Science and Analytics team, dedicated to improving e-commerce delivery. We work to optimize our vast network, forecast demand using machine learning, and enhance route efficiency. Our efforts focus on developing innovative delivery methods, applying AI to solve complex problems, and conducting geospatial analysis. We create simulations to refine processes and plan capacity effectively. Operating globally, we strive to develop adaptable solutions for diverse markets. We aim to advance logistics science, continually improving speed, efficiency, and customer satisfaction, in support of Amazon's mission to be Earth's most customer-centric company.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist - LLM, Alexa Conversational Modelling Intelligence
            

        

        

            
                
                    

                
            

            

            

            

            
                
DE, BE, Berlin

            
        


        
    
As an Applied Scientist II in the Alexa Conversational Modelling Intelligence team within Alexa AI, you will drive model post-training for Large Language Models that power Alexa+. You'll adopt and adapt state-of-the-art techniques — including supervised fine-tuning, RLHF, and preference optimization — running rigorous experiments and translating findings into production-ready solutions that directly improve the customer experience for millions of users worldwide. You will own the full model development cycle from data curation through training, evaluation, and deployment. Your day-to-day will involve developing evaluation methods and metrics, diagnosing model defects, and iterating on recipes to move concrete quality and efficiency benchmarks. You'll write clean, reproducible code, contribute to shared tooling, and collaborate closely with scientists and engineers to bring models from experimentation to scale. You are technically curious, experiment-driven, and motivated by real customer impact. You will also advance the state of the art by publishing at top-tier NLP/ML conferences (ACL, EMNLP, NeurIPS, ICML, ICLR) — contributing to the broader research community while grounding your work in measurable outcomes. Key job responsibilities As an Applied Scientist II in the Alexa Conversational Modelling Intelligence team, you will own the end-to-end model development lifecycle for LLMs that power Alexa+. You'll design and execute training recipes — including supervised fine-tuning, reinforcement learning from human feedback, and preference optimization — iterating rapidly on data, hyperparameters, and architectures to move quality and efficiency metrics. Your work will directly shape how millions of customers interact with Alexa daily. You will build robust evaluation frameworks to measure model performance, diagnose failure modes, and quantify improvements. This includes developing benchmarks, implementing LLM-as-a-judge pipelines, and conducting rigorous defect analysis to identify where models fall short and why. You'll translate these insights into targeted improvements that close gaps in conversational quality, safety, and fluency. You will collaborate closely with research scientists and engineers to bring models from experimentation to production at scale. You'll contribute to shared tooling and infrastructure, write clean and reproducible code, and document your methods so the team can build on your work. You are also expected to advance the state of the art by publishing findings at top-tier NLP/ML venues (ACL, EMNLP, NeurIPS, ICML, ICLR), ensuring your research drives both customer impact and scientific contribution. A day in the life As an Applied Scientist II, your day will involve launching and monitoring training runs, analyzing experiment results, and iterating on model recipes based on evaluation data. You'll participate in science reviews with fellow researchers, sync with engineering partners on deployment readiness, and deep-dive into model outputs to understand behavioral patterns. You'll balance hands-on experimentation with collaborative problem-solving — working across the Alexa AI organization to align model improvements with customer-facing goals and product priorities. About the team The Alexa Conversational Modelling Intelligence team builds industry-leading LLM-based conversational technologies that customers love. Our mission is to push the envelope in LLMs for Alexa to deliver the best-possible customer experience. As an Applied Scientist, you'll contribute directly to that mission through model development and experimentation.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Manager III, Economist - AMZ9803624
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, CA, Sunnyvale

            
        


        
    
MULTIPLE POSITIONS AVAILABLE Employer: AMAZON.COM SERVICES LLC Offered Position: Manager III, Economist Job Location: Sunnyvale, California Job Number: AMZ9803624 Position Responsibilities: Independently manage a team of economists and/or scientists in developing strategic economic analyses and demand estimation models. Translate business questions into econometric methodologies and causal inference analyses. Communicate economic insights to non-technical audiences to guide strategic-level, high-impact business decisions. Scale economic models through cross-functional collaboration with engineering teams. Establish scientific quality standards and research priorities. Drive operational efficiency and research excellence across the team. 40 hours / week, 8:00am-5:00pm, Salary Range: $201,300/year to $272,400/year. Amazon is a total compensation company. Dependent on the position offered, equity, sign-on payments, and other forms of compensation may be provided as part of a total compensation package, in addition to a full range of medical, financial, and/or other benefits. For more information, visit: https://www.aboutamazon.com/workplace/employee-benefits. Amazon.com is an Equal Opportunity-Affirmative Action Employer – Minority / Female / Disability / Veteran / Gender Identity / Sexual Orientation.#0000




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Economist, Prime Video
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Seattle

            
        


        
    
Ever wish you could use your quantitative and critical thinking skills to influence business decisions? Economists at Amazon partner closely with senior management, business stakeholders, scientist and engineers, and economist leadership to solve key business problems. As part of the Content Discovery and Experimentation Science team within Prime Video, you will leverage your expertise in causal inference and experimental design to make Prime Video the best-in-class digital video experience. Key job responsibilities - Build causal models and metrics that capture trade-off decisions when business and customer outcomes do not align - Partner with data scientists and product managers to integrate these metrics into Prime Video's experimentation tooling - Work with finance partners to ensure that the team's product metrics contribute to Prime Video's strategic business and financial objectives - Contribute to technical and business documents to communicate ideas and proposals to various audiences - Educate and advocate for best practices in experimentation and how to use it for decision-making




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Senior Data Scientist, Enterprise Security Products
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, TX, Austin

            
        


        
    
What happens when you combine startup speed with Amazon-scale impact? You get this team. Amazon Enterprise Security Products is a newly launched group building intelligent, cloud-agnostic security tools using AI-first development practices. Here, you build AI and you build with AI at the same time. This role is a chance to define and lead the science strategy for the future of security tooling with a small, fast team that ships like a startup but deploys at Amazon scale. We're looking for a Senior Data Scientist who operates at the intersection of applied ML, agentic AI, and security; and who can set technical direction across ambiguous, undefined problem spaces. You won't just build models; you'll decide which problems are worth solving, architect the scientific approach for an entire product area, and raise the bar for how the team applies science. You'll partner with senior and principal engineers, applied scientists, security researchers, and PMs, and your judgment will shape roadmaps, not just deliverables. This is a role for someone who thrives in ambiguity, influences without authority, and turns "too ambitious" into shipped reality. Key job responsibilities - Set the science direction for a product area: Define the modeling strategy, scientific approach, and success metrics for entire categories of AI-first security capabilities, agentic systems, anomaly detection, threat classification, and automated response across multi-cloud environments. Decide where science can move the needle and where it can't. - Own the hardest, most ambiguous problems: Take on undefined, open-ended challenges where the path isn't clear, the data is messy or scarce, and the stakes are high. Frame the problem, choose the approach, and bring others along. - Build with AI to build AI and define how the team does it: Drive adoption of agentic coding tools, LLM-powered workflows, and experimental AI tooling across the science org. Establish the practices that multiply velocity for every scientist, not just yourself. - Architect agentic intelligence: Lead the design of models, embeddings, RAG pipelines, evaluation frameworks, and feedback loops that make multi-agent security systems smart, safe, and customer-ready at scale. Own the science architecture decisions others build on. - Drive technical strategy across teams: Influence roadmaps, dive deep with senior and principal scientists and engineers, and align cross-functional partners around a shared scientific vision. Your recommendations shape what the team invests in next. - Prototype, validate, and scale: Turn ambiguous hypotheses into prototypes in days, validate with real customer signal, and chart the path from prototype to production system that runs reliably at Amazon scale. - Communicate to influence at the executive level: Translate complex modeling results and scientific trade-offs into clear recommendations for engineers, product leaders, and senior executives. Drive organizational decisions with data and earn trust across the company. - Raise the bar and grow others: Mentor data scientists and applied scientists, lead technical and science reviews, and champion AI-first development practices. Shape the science culture and hiring bar of a fast-growing team from the ground floor. A day in the life No two days look the same on this fast-growing, AI-first team. You might start your morning setting direction in a roadmap review; making the call on which science investments will have the biggest customer impact and then dive into architecting an evaluation framework that the whole team will build on. Before lunch, you're pair-prompting with an agentic coding assistant to validate a new approach, then unblocking a teammate stuck on a thorny modeling problem. In the afternoon, you lead a design session with senior and principal scientists and engineers, then distill it into a crisp recommendation for senior leadership. You own ambiguous problems end to end, define how the team works, and see your decisions ripple across the product. This is where builders who want to lead with science come to do their best work. 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. 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 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. Hybrid Work We value innovation and recognize this sometimes requires uninterrupted time to focus on a build. We also value in-person collaboration and time spent face-to-face. Our team affords employees options to work in the office every day or in a flexible, hybrid work model near one of our U.S. Amazon offices.




        

        

        

        
    


    



                    

                
            

        

    

    

        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