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
        
    




    
        

            

                
                    

                        

    

    

        
            

                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.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                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




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                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




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                2027 Applied Science Intern (Computer Vision), Amazon International Machine Learning
            

        

        

            
                
                    

                
            

            

            

            

            
                
AU, VIC, Melbourne

            
        


        
    
Are you excited about leveraging state-of-the-art Computer Vision algorithms and large datasets to solve real-world problems? Join Amazon as an Applied Scientist Intern and be at the forefront of AI innovation! As an Applied Scientist Intern, you'll work in a fast-paced, cross-disciplinary team of pioneering researchers. You'll tackle complex problems, developing solutions that either build on existing academic and industrial research or stem from your own innovative thinking. Your work may even find its way into customer-facing products, making a real-world impact. Please note: This internship is a duration of 6 months full time with a start date in Jan-March 2027. The successful intern is required to be based in Melbourne and relocation allowance will be provided if you are based outside of Melbourne. Key job responsibilities - Develop novel solutions and build prototypes - Work on complex problems in Computer Vision and Machine Learning - Contribute to research that could significantly impact Amazon's operations - Collaborate with a diverse team of experts in a fast-paced environment - Collaborate with scientists on writing and submitting papers to Tier-1 conferences (e.g., CVPR, ICCV, NeurIPS, ICML) - Present your research findings to both technical and non-technical audiences Key Opportunities - Collaborate with leading machine learning researchers - Access Amazon tools and hardware (large GPU clusters) - Address challenges at an unparalleled scale - Become a disruptor, innovator, and problem solver in the field of computer vision - Potentially deliver solutions to production in customer-facing applications - Opportunities to become an FTE after the internship Join us in shaping the future of AI at Amazon. Apply now and turn your research into real-world solutions!




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist, Trustworthy Shopping Experience (TSE)
            

        

        

            
                
                    

                
            

            

            

            

            
                
IN, KA, Bengaluru

            
        


        
    
Are you passionate about solving complex business problems at scale through Generative AI? Do you want to help build intelligent systems that reason, act, and learn from minimal supervision? If so, we have an exciting opportunity for you on Amazon's Trustworthy Shopping Experience (TSE) team. At TSE, our vision is to guarantee customers a worry-free shopping experience by earning their trust that the products they buy are safe, authentic, and compliant with regulations and policy. We do this in close partnership with our selling partners, empowering them with best-in-class tools and expertise to offer a high-quality, compliant selection that customers trust. As an Applied Scientist I, you will bring subject matter expertise in at least one relevant discipline (e.g., NLP, computer vision, representation learning, agentic architecture) to contribute to next-generation agentic AI solutions that automate complex manual investigation processes at Amazon scale. Working alongside senior scientists, you will map business goals—such as reducing cost-of-serving while maintaining trust and safety standards—to well-defined scientific problems and metrics. You will invent, refine, and experiment with solutions spanning agentic reasoning, self-supervised representation learning, few-shot adaptation, multimodal understanding, and model compression. With guidance from senior scientists, you will stay current on research trends and benchmark your results against the state of the art. You will help design and execute experiments to identify optimal solutions, initiating the development and implementation of small components with team guidance. You will write secure, stable, testable, and well-documented production code at the level of an SDE I, rigorously evaluating models and quantifying performance. You will handle data in accordance with Amazon policies, troubleshoot issues to root cause, and ensure your work does not put the company at risk. Your scope of influence will typically be at the self-level, with the possibility of mentoring interns. You will participate in team design and prioritization discussions, learn the business context behind TSE's products, and escalate problems with proposed solutions. You will publish internal technical reports and may contribute to peer-reviewed publications and external review activities when aligned with business needs. This role offers a unique opportunity to contribute to end-to-end AI development—from research through production—with your contributions serving hundreds of millions of customers within months, not years. Key job responsibilities • Contribute to the design and development of agentic AI systems with multi-step reasoning, autonomous task execution, and multimodal intelligence, including feedback and memory mechanisms, leveraging reinforcement learning techniques for agent decision-making and policy optimization, with input and guidance from senior scientists • Help productionize models built on top of SFT (Supervised Fine-tuning) and RFT (Reinforced Fine-tuning) approaches, as well as few-shot approaches based on multimodal datasets spanning text, images, and structured data, applying mathematical optimization techniques to improve efficiency, resource allocation, and decision-making in complex workflows, working alongside senior scientists to identify optimal solutions • Contribute to building production-ready deep learning and conventional ML solutions, including multimodal fusion and cross-modal alignment techniques that seamlessly connect visual, textual, and relational understanding, to support automation requirements within your team's scope • Help identify customer and business problems; use reasonable assumptions, data, and customer requirements to solve well-defined scientific problems involving multimodal inputs such as unstructured text, documents, product images, and relational data, developing representations that capture complementary signals across modalities and mapping business goals to scientific metrics • May co-author research papers for peer-reviewed internal and/or external venues, including contributions in areas such as multimodal representation learning and vision-language modeling, and contribute to the wider scientific community by reviewing research submissions, when aligned with business needs • Prototype rapidly, iterate based on feedback, and deliver small components at SDE I level—including multimodal data pipelines and inference modules—that integrate into production-scale systems • Write secure, stable, testable, maintainable, and well-documented code, balancing model capability, deployment cost, and resource usage across multimodal architectures while understanding state-of-the-art data structures, algorithms, and performance tradeoffs • Rigorously test code and evaluate models across individual and combined modalities, quantifying their performance; troubleshoot issues, research root causes, and thoroughly resolve defects, leaving systems more maintainable • Participate in team design, scoping, and prioritization discussions through clear verbal and written communication; seek to learn the business context, science, and engineering behind your team's products, including how multimodal signals contribute to trust and safety decisions • Participate in engineering best practices with peer reviews; clearly document approaches and communicate design decisions; publish internal technical reports to institutionalize scientific learning • Help train and mentor scientist interns; identify and escalate problems with proposed solutions, taking ownership or ensuring clear hand-off to the right owner About the team Trustworthy Shopping Experience Product team in TSE is responsible for the human-in-the-loop products and technology used in the risk investigations at Amazon. The team is also responsible for reducing the cost of performing the investigations, by automating wherever possible and optimizing the experience where manual interventions are needed. The team leverages state-of-the art technology and GenAI to deliver the products and associated goals.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Flight Dynamics Engineer, FD Research
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Redmond

            
        


        
    
We are searching for a talented candidate with expertise in orbital mechanics and spaceflight navigation, including LEO Satellite Orbit Determination. This position requires experience in simulation and analysis of spacecraft orbital mechanics and sequential orbit determination methods, including Extended Kalman Filters (EKF) and/or Unscented Kalman Filter (UKF). Strong analysis skills are required to develop engineering studies of complex large-scale dynamical systems. This position requires demonstrated expertise in computational analysis automation and tool development. Key job responsibilities - Perform spacecraft maneuver or navigation analysis in support of multi-disciplinary trades within the Amazon Leo team. - Contribute to prototype software development of flight algorithms. - Test and assess navigation software for integration into flight systems. - Assess and trouble-shoot the performance of Leo on-board GNSS hardware and software systems. - Work closely with GNC engineers to manage on-orbit performance and develop flight dynamics operations processes. Export Control Requirement: Due to applicable export control laws and regulations, candidates must be 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. A day in the life - Interacting with GNC teams to evaluate and troubleshoot satellite issues. - Working within the Flight Dynamics Research team to prioritize tasks. - Performing analysis, simulation, testing and documentation to address assigned tasks.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                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.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist, Trust CX Innovations&AI Policy
            

        

        

            
                
                    

                
            

            

            

            

            
                
IN, KA, Bengaluru

            
        


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




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Quantum Research Scientist, AWS Center for Quantum Computing
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, CA, Pasadena

            
        


        
    
The Amazon Web Services (AWS) Center for Quantum Computing in Pasadena, CA, is looking to hire a Research Scientist with experience in semiconductor process development who will aid in AWS’s effort to bring cloud quantum computing services to its worldwide customer base. You will join a multi-disciplinary team of scientists, and hardware and software engineers working at the forefront of quantum computing. Through your work inside and outside of the cleanroom environment in the fabrication research and development group, you will solve problems related to developing next-generation quantum processors. Candidates must have a demonstrated background in sound scientific and engineering principles, and must have excellent data analysis, bias for action, problem solving, and communication skills, and be highly motivated and curious to research and learn new technical topics as needed. As a research scientist you will be expected to work on new ideas and stay abreast of novel approaches in fabricating and packaging superconducting quantum processors. Working effectively within a team environment is critical. Key job responsibilities Responsibilities include developing novel processes to fabricate high-coherence superconducting qubits; developing advanced 3DI interconnect and routing technologies for integrating superconducting quantum technologies; analyzing inline metrology and electrical test data; writing production standard operating procedures to transfer newly-developed processes to production teams; interacting with project leads to provide feedback that continuously improves different processes. A day in the life The candidate will develop novel technologies using micro-/nano-fabrication techniques inside the cleanroom (independently or in collaboration with other scientists and engineers) for next-generation quantum computing. Outside the cleanroom, the candidate will plan experiments, analyze data, and conceive future innovations. About the team AWS Utility Computing (UC) provides product innovations — from foundational services such as Amazon’s Simple Storage Service (S3) and Amazon Elastic Compute Cloud (EC2), to consistently released new product innovations that continue to set AWS’s services and features apart in the industry. As a member of the UC organization, you’ll support the development and management of Compute, Database, Storage, Internet of Things (Iot), Platform, and Productivity Apps services in AWS, including support for customers who require specialized security solutions for their cloud services. 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 (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. 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.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Data Scientist II, FinAuto
            

        

        

            
                
                    

                
            

            

            

            

            
                
IN, KA, Bengaluru

            
        


        
    
Interested to build the next generation Financial systems that can handle billions of dollars in transactions? Interested to build highly scalable next generation systems that could utilize Amazon Cloud? Massive data volume + complex business rules in a highly distributed and service oriented architecture, a world class information collection and delivery challenge. Our challenge is to deliver the software systems which accurately capture, process, and report on the huge volume of financial transactions that are generated each day as millions of customers make purchases, as thousands of Vendors and Partners are paid, as inventory moves in and out of warehouses, as commissions are calculated, and as taxes are collected in hundreds of jurisdictions worldwide. Key job responsibilities • Understand the business and discover actionable insights from large volumes of data through application of machine learning, statistics or causal inference. • Analyse and extract relevant information from large amounts of Amazon’s historical transactions data to help automate and optimize key processes • Research, develop and implement novel machine learning and statistical approaches for anomaly, theft, fraud, abusive and wasteful transactions detection. • Use machine learning and analytical techniques to create scalable solutions for business problems. • Identify new areas where machine learning can be applied for solving business problems. • Partner with developers and business teams to put your models in production. • Mentor other scientists and engineers in the use of ML techniques. A day in the life • Understand the business and discover actionable insights from large volumes of data through application of machine learning, statistics or causal inference. • Analyse and extract relevant information from large amounts of Amazon’s historical transactions data to help automate and optimize key processes • Research, develop and implement novel machine learning and statistical approaches for anomaly, theft, fraud, abusive and wasteful transactions detection. • Use machine learning and analytical techniques to create scalable solutions for business problems. • Identify new areas where machine learning can be applied for solving business problems. • Partner with developers and business teams to put your models in production. • Mentor other scientists and engineers in the use of ML techniques. About the team The FinAuto TFAW(theft, fraud, abuse, waste) team is part of FGBS Org and focuses on building applications utilizing machine learning models to identify and prevent theft, fraud, abusive and wasteful(TFAW) financial transactions across Amazon. Our mission is to prevent every single TFAW transaction. As a Machine Learning Scientist in the team, you will be driving the TFAW Sciences roadmap, conduct research to develop state-of-the-art solutions through a combination of data mining, statistical and machine learning techniques, and coordinate with Engineering team to put these models into production. You will need to collaborate effectively with internal stakeholders, cross-functional teams to solve problems, create operational efficiencies, and deliver successfully against high organizational standards.




        

        

        

        
    


    



                    

                
            

        

    

    

        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