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
        
    




    
        

            

                
                    

                        

    

    

        
            

                Member of Technical Staff, Engineering Manager , Amazon AGI Lab
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, CA, San Francisco

            
        


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




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                 Sr. Communication Research Scientist
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, CA, Sunnyvale

            
        


        
    
Amazon Leo is an initiative to launch a constellation of Low Earth Orbit satellites that will provide low-latency, high-speed broadband connectivity to unserved and underserved communities around the world. As a Sr. Comm System Research Scientist, this role is primarily responsible for the design, development and integration of Ka band and S/C band communication payload and ground terminal systems. The Role: Be part of the team defining the overall communication system and architecture of Amazon’s broadband wireless network. This is a unique opportunity to innovate and define groundbreaking wireless technology with few legacy constraints. The team develops and designs the communication system of Amazon Leo and analyzes its overall system level performance such as for overall throughput, latency, system availability, packet loss etc. This role in particular will be responsible for leading the effort in designing and developing advanced technology and solutions for communication system. This role will also be responsible developing advanced L1/L2 proof of concept HW/SW systems to improve the performance and reliability of the Amazon Leo network. In particular this role will be responsible for using concepts from digital signal processing, information theory, wireless communications to develop novel solutions for achieving ultra-high performance LEO network. This role will also be part of a team and develop simulation tools with particular emphasis on modeling the physical layer aspects such as advanced receiver modeling and abstraction, interference cancellation techniques, FEC abstraction models etc. This role will also play a critical role in the design, integration and verification of various HW and SW sub-systems as a part of system integration and link bring-up and verification. 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. Key job responsibilities • Design advanced L1/L2 algorithms and solutions for the Amazon Leo communication system, particularly Multi-User MIMO techniques. • Develop proof-of-concepts for critical communication payload components using SDR platforms consisting of FPGAs and general-purpose processors. • Work with ASIC development teams to build power/area efficient L1/L2 HW accelerators to be integrated into Amazon Leo SoCs. • Provide specifications and work with implementation teams on the development of embedded L1/L2 HW/SW architectures. • Work with multi-disciplinary teams to develop advanced solutions for time, frequency and spatial acquisition/tracking in LEO systems, particularly under large uncertainties. • Develop link-level and system-level simulators and work closely with implementation teams to evaluate expected performance and provide quick feedback on potential improvements. • Develop testbeds consisting of digital, IF and RF components while accounting for link-budgets and RF/IF line-ups. Previous experiences with VSAs/VSGs, channel emulators, antennas (particularly phased-arrays) and anechoic chamber instrumentation are a plus. • Work with development teams on system integration and debugging from PHY to network layer, including interfacing with flight computer and SDN control subsystems. • Willing to work in fast-paced environment and take ownership that goes from algorithm specification, to HW/SW architecture definition, to proof-of-concept development, to testbed bring-up, to integration into the Amazon Leo system. • Be a team player and provide support when requested while being able to unblock themselves by reaching out to RF, ASIC, SW, Comsys and Testbed supporting teams to move forward in development, testing and integration activities. • Ability to adapt design and test activities based on current HW/SW capabilities delivered by the development teams.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist Intern, 2026 Shenzhen
            

        

        

            
                
                    

                
            

            

            

            

            
                
CN, 44, Shenzhen

            
        


        
    
职位：Applied scientist 应用科学家实习生 毕业时间：2026年10月 - 2027年7月之间毕业的应届毕业生 · 入职日期：2026年6月及之前 · 实习时间：保证一周实习4-5天全职实习，至少持续3个月 · 工作地点：深圳福田区 投递须知： 1 填写简历申请时，请把必填和非必填项都填写完整。提交简历之后就无法修改了哦！ 2 学校的英文全称请准确填写。中英文对应表请查这里（无法浏览请登录后浏览）https://docs.qq.com/sheet/DVmdaa1BCV0RBbnlR?tab=BB08J2 关于职位 Amazon Device &Services Asia团队正在寻找一位充满好奇心、善于沟通的应用科学家实习生，成为连接前沿AI研究与现实世界认知的桥梁。这是一个独特的角色——既需要动手参与机器学习项目，又要接受将复杂AI概念转化为通俗易懂内容的创意挑战。D&S Asia是亚马逊设备与服务业务在亚洲的支柱组织，自2009年支持Kindle制造起步，现已发展为横跨软硬件、AI（Alexa）及智能家居（Ring/Blink）的综合性团队，持续驱动区域业务创新与人才发展。 你将做什么 • 解密AI： 将复杂的技术发现转化为直观的解释、博客文章、教程或互动演示，让非技术背景的业务方和更广泛的社区都能理解 • 技术叙事： 与工程团队协作，以清晰、引人入胜的方式记录AI的能力与局限性 • 知识共享： 协助开发内部工作坊或"AI入门"课程，提升跨职能团队（产品、设计、商务）的AI素养 • 保持前沿： 持续学习并整合最新突破（如大语言模型、扩散模型、智能体），为团队输出简明易懂的趋势简报 • 研究与应用： 参与端到端的应用研究项目，从文献综述到原型开发，涵盖自然语言处理、计算机视觉或多模态AI领域




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist, Books Reading & Discovery Experiences
            

        

        

            
                
                    

                
            

            

            

            

            
                
IN, KA, Bengaluru

            
        


        
    
Passionate about books? The Amazon Books team is looking for a talented Applied Scientist II to help invent, design, and deliver science solutions to make it easier for millions of customers to find the next book they will love. In this role, you will - Be a part of a growing team of scientists, economists, engineers, analysts, and business partners. - Use Amazon’s large-scale computing and data resources to generate deep understandings of our customers and products. - Build highly accurate models (and/or agentic systems) to enhance the book reading & discovery experiences. - Design, implement, and deliver novel solutions to some of Amazon’s oldest problems. Key job responsibilities - Inspect science initiatives across Amazon to identify opportunities for application and scaling within book reading and discovery experiences. - Participate in team design, scoping, and prioritization discussions while mapping business goals to scientific problems and aligning business metrics with technical metrics. - Spearhead the design and implementation of new features through thorough research and collaboration with cross-functional teams. - Initiate the design, development, execution, and implementation of project components with input and guidance from team members. - Work with Software Development Engineers (SDEs) to deliver production-ready solutions that benefit customers and business operations. - Invent, refine, and develop solutions to ensure they meet customer needs and team objectives. - Demonstrate ability to use reasonable assumptions, data analysis, and customer requirements to solve complex problems. - Write secure, stable, testable, and maintainable code with minimal defects while taking full responsibility for your components. - Possess strong understanding of data structures, algorithms, model evaluation techniques, performance optimization, and trade-off analysis. - Follow engineering and scientific method best practices, including design reviews, model validation, and comprehensive testing. - Maintain current knowledge of research trends in your field and apply rigorous scrutiny to results and methodologies. A day in the life In this role, you will address complex Books customer challenges by developing innovative solutions that leverage the advancements in science. Working alongside a talented team of scientists, you will conduct research and execute experiments designed to enhance the Books reading and shopping experience. Your responsibilities will encompass close collaboration with cross-functional partner teams, including engineering, product management, and fellow scientists, to ensure optimal data quality, robust model development, and successful productionization of scientific solutions. Additionally, you will provide mentorship to other scientists, conduct reviews of their work, and contribute to the development of team roadmaps. About the team The team consists of a collaborative group of scientists, product leaders, and dedicated engineering teams. We work with multiple partner teams to leverage our systems to drive a diverse array of customer experiences, owned both by ourselves and others, that enable shoppers to easily find their perfect next read and enable delightful reading experiences that would make Kindle the best place to read.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist, Central Machine Learning
            

        

        

            
                
                    

                
            

            

            

            

            
                
IN, KA, Bengaluru

            
        


        
    
Do you want to join an innovative team of scientists who use machine learning and statistical techniques to create state-of-the-art solutions for providing better value to Amazon’s customers? Do you want to build and deploy advanced algorithmic systems that help optimize millions of transactions every day? Are you excited by the prospect of analyzing and modeling terabytes of data to solve real world problems? Do you like to own end-to-end business problems/metrics and directly impact the profitability of the company? Do you like to innovate and simplify? If yes, then you may be a great fit to join the Machine Learning and Data Sciences team for India Consumer Businesses. If you have an entrepreneurial spirit, know how to deliver, love to work with data, are deeply technical, highly innovative and long for the opportunity to build solutions to challenging problems that directly impact the company's bottom-line, we want to talk to you. Major responsibilities - Use machine learning and analytical techniques to create scalable solutions for business problems - Analyze and extract relevant information from large amounts of Amazon’s historical business data to help automate and optimize key processes - Design, development, evaluate and deploy innovative and highly scalable models for predictive learning - Research and implement novel machine learning and statistical approaches - Work closely with software engineering teams to drive real-time model implementations and new feature creations - Work closely with business owners and operations staff to optimize various business operations - Establish scalable, efficient, automated processes for large scale data analyses, model development, model validation and model implementation - Mentor other scientists and engineers in the use of ML techniques A day in the life You will solve real-world problems by getting and analyzing large amounts of data, generate insights and opportunities, design simulations and experiments, and develop statistical and ML models. The team is driven by business needs, which requires collaboration with other Scientists, Engineers, and Product Managers across the International Emerging Stores organization. You will prepare written and verbal presentations to share insights to audiences of varying levels of technical sophistication. About the team Central Machine Learning team works closely with the IES business and engineering teams in building ML solutions that create an impact for Emerging Marketplaces. This is a great opportunity to leverage your machine learning and data mining skills to create a direct impact on millions of consumers and end users.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Language Data Scientist, Alexa AI
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Seattle

            
        


        
    
Amazon is seeking a Language Data Scientist to join the Alexa Artificial Intelligence (AI) team as domain expert. This role focuses on expanding analysis and evaluation of speech and interaction data deliverables. The Language Data Scientist is an expert in dialog evaluation processes, working closely with a team of skilled analysts and machine learning scientists and engineers, and is a key member in developing new conventions for relevant annotation workflows. The Language Data Scientist will be asked to handle unique data analysis and research requests that support the training and evaluation of machine learning models and the overall processing of a data collection. Key job responsibilities To be successful in this role, you must have a passion for data, efficiency, and accuracy. Specifically, you will: - Own data analyses for customer-facing features, including launch go/no-go metrics for new features and accuracy metrics for existing features - Handle unique data analysis requests from a range of stakeholders, including quantitative and qualitative analyses to elevate customer experience with speech interfaces - Lead and evaluate changing dialog evaluation conventions, test tooling developments, and pilot processes to support expansion to new data areas - Continuously evaluate workflow tools and processes and offer solutions to ensure they are efficient, high quality, and scalable - Provide expert support for a large and growing team of data analysts - Provide support for ongoing and new data collection efforts as a subject matter expert on conventions and use of the data - Conduct research studies to understand speech and customer-Alexa interactions - Assist scientists, program and product managers, and other stakeholders in defining and validating customer experience metrics




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist II, Amazon Connect
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, CA, Mountain View

            
        


        
    
Do you want to join a team of innovative scientists to research and develop generative AI technology that would disrupt the industry? Do you enjoy dealing with ambiguity and working on hard problems in a fast-paced environment? Amazon Connect is a highly disruptive cloud-based contact center from AWS that enables businesses to deliver intelligent, engaging, dynamic, and personalized customer service experiences. The Agentic Customer Experience (ACX) org is responsible for weaving native-AI across the Connect application experiences delivered to end-customers, agents, and managers/supervisors. The Interactive AI Science team, serves as the cornerstone for AI innovation across Amazon Connect, functioning as the sole science team support high impact product including Amazon Q in Connect, Contact Lens and other key initiatives. As an Applied Scientist on our team, you will work closely with senior technical and business leaders from within the team and across AWS. You distill insight from huge data sets, conduct cutting edge research, foster ML models from conception to deployment. You have deep expertise in machine learning and deep learning broadly, and extensive domain knowledge in natural language processing, generative AI and LLM Agents evaluation and optimization, etc. You are comfortable with quickly prototyping and iterating your ideas to build robust ML models using technology such as PyTorch, Tensorflow and AWS Sagemaker. The ideal candidate has the ability to understand, implement, innovate on the state-of-the-art Agentic AI based systems. We have a rapidly growing customer base and an exciting charter in front of us that includes solving highly complex engineering and scientific problems. We are looking for passionate, talented, and experienced people to join us to innovate on modern contact centers in the cloud. The position represents a rare opportunity to be a part of a fast-growing business soon after launch, and help shape the technology and product as we grow. You will be playing a crucial role in developing the next generation contact center, and get the opportunity to design and deliver scalable, resilient systems while maintaining a constant customer focus. About the team Diverse Experiences AWS values diverse experiences. Even if you do not meet all of the qualifications and skills listed in the job description, we encourage candidates to apply. If your career is just starting, hasn’t followed a traditional path, or includes alternative experiences, don’t let it stop you from applying. Why AWS? Amazon Web Services (AWS) is the world’s most comprehensive and broadly adopted cloud platform. We pioneered cloud computing and never stopped innovating — that’s why customers from the most successful startups to Global 500 companies trust our robust suite of products and services to power their businesses. Inclusive Team Culture Here at AWS, it’s in our nature to learn and be curious. Our employee-led affinity groups foster a culture of inclusion that empower us to be proud of our differences. Ongoing events and learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences, inspire us to never stop embracing our uniqueness. Mentorship & Career Growth We’re continuously raising our performance bar as we strive to become Earth’s Best Employer. That’s why you’ll find endless knowledge-sharing, mentorship and other career-advancing resources here to help you develop into a better-rounded professional. Work/Life Balance We value work-life harmony. Achieving success at work should never come at the expense of sacrifices at home, which is why we strive for flexibility as part of our working culture. When we feel supported in the workplace and at home, there’s nothing we can’t achieve in the cloud.




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist - Agentic AI, Amazon Fulfillment Technology
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Bellevue

            
        


        
    
As an Applied Scientist in Amazon Fullfilment Technology, you will lead the development of agentic systems to assist with operational decision making and orchestration. You will work building full agentic systems leveraging multi-agent orchestration, tool use, memory, and action execution. You will train LLMs using a combination of rejection sampling approaches, SFT, continual post-training, and Reinforcement Learning (RL). These systems are deployed to Amazon buildings, and you will also work on rigorous offline and online evaluations. Your work will leverage the latest LLMs to develop capabilities for agentic reasoning, coding and analytics. You will also lead research projects to tackle unsolved problems, mentor interns, and author academic papers to summarize your findings for external publication. Key job responsibilities - Generating training and preference data for specific use cases (reasoning trajectories, tool traces) - Reward modeling and policy optimization for LLMs: DPO, IPO, RLHF/RLAIF with PPO/GRPO, rejection sampling. - Supervised fine-tuning on step-by-step trajectories and tool-use traces - Verbal Reinforcement Learning and Continual Learning - RL for LLMs, Offline RL and off-policy evaluation - Agentic memory/state management; episodic and semantic memory; vector search; grounding with RAG. - Evaluation: developing decision quality metrics, scaling LLM-based evaluations. About the team Amazon Fulfillment Technologies (AFT) powers Amazon’s global fulfillment network. We invent and deliver software, hardware, and data science solutions that orchestrate processes, robots, machines, and people. We harmonize the physical and virtual world so Amazon customers can get what they want, when they want it. Learn more about AFT: https://tinyurl.com/AFTOverview




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Applied Scientist, Workplace Health & Safety 
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, WA, Bellevue

            
        


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




        

        

        

        
    


    



                    

                
                    

                        

    

    

        
            

                Instrument Control Engineer, Software, Center for Quantum Computing
            

        

        

            
                
                    

                
            

            

            

            

            
                
US, CA, Pasadena

            
        


        
    
The Amazon Center for Quantum Computing (CQC) is a multi-disciplinary team of scientists, engineers, and technicians, on a mission to develop a fault-tolerant quantum computer. We are looking to hire an Instrument Control Engineer to join our growing software team. You will work closely with our experimental physics and control hardware development teams to enable their work characterizing, calibrating, and operating novel quantum devices. The ideal candidate should be able to translate high-level science requirements into software implementations (e.g. Python APIs/frameworks, compiler passes, embedded SW, instrument drivers) that are performant, scalable, and intuitive. This requires someone who (1) has a strong desire to work within a team of scientists and engineers, and (2) demonstrates ownership in initiating and driving projects to completion. This role has a particular emphasis on working directly with our control hardware designers and vendors to develop instrument software for test and measurement. Inclusive Team Culture Here at Amazon, it’s in our nature to learn and be curious. Our employee-led affinity groups foster a culture of inclusion that empower us to be proud of our differences. Ongoing events and learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon conferences, inspire us to never stop embracing our uniqueness. Diverse Experiences Amazon values diverse experiences. Even if you do not meet all of the qualifications and skills listed in the job description, we encourage candidates to apply. If your career is just starting, hasn’t followed a traditional path, or includes alternative experiences, don’t let it stop you from applying. Mentorship & Career Growth We’re continuously raising our performance bar as we strive to become Earth’s Best Employer. That’s why you’ll find endless knowledge-sharing, mentorship and other career-advancing resources here to help you develop into a better-rounded professional. Work/Life Balance We value work-life harmony. Achieving success at work should never come at the expense of sacrifices at home, which is why we strive for flexibility as part of our working culture. When we feel supported in the workplace and at home, there’s nothing we can’t achieve in the cloud. Export Control Requirement Due to applicable export control laws and regulations, candidates must be either a U.S. citizen or national, U.S. permanent resident (i.e., current Green Card holder), or lawfully admitted into the U.S. as a refugee or granted asylum, or be able to obtain a US export license. If you are unsure if you meet these requirements, please apply and Amazon will review your application for eligibility. Key job responsibilities - Work with control hardware developers, as a “subject matter expert” on the software interfaces around our control hardware - Collaborate with external control hardware vendors to understand and refine integration strategies - Implement instrument drivers and control logic in Python and/or a low-level languages, including C++ or Rust - Contribute to our compiler backend to enable the efficient execution of OpenQASM-based experiments on our next-generation control hardware - Benchmark system performance and help define key performance metrics - Ensure new features are successfully integrated into our Python-based experimental software stack - Partner with scientists to actively contribute to the codebase through mentorship and documentation We are looking for candidates with strong engineering principles, a bias for action, superior problem-solving, and excellent communication skills. Working effectively within a team environment is essential. As an Instrument Control Engineer embedded in a broader science organization, you will have the opportunity to work on new ideas and stay abreast of the field of experimental quantum computation. A day in the life Your time will be spent on projects that extend functional capabilities or performance of our internal research software stack. This requires working backwards from the needs of science staff in the context of our larger experimental roadmap. You will translate science and software requirements into design proposals balancing implementation complexity against time-to-delivery. Once a design proposal has been reviewed and accepted, you’ll drive implementation and coordinate with internal stakeholders to ensure a smooth roll out. Because many high-level experimental goals have cross-cutting requirements, you’ll often work closely with other engineers or scientists or on the team. About the team You will be joining the Software group within the Amazon Center of Quantum Computing. Our team is comprised of scientists and software engineers who are building scalable software that enables quantum computing technologies.




        

        

        

        
    


    



                    

                
            

        

    

    

        See more jobs
    






        




    

        
            
        
        

            

                
                    

                        

                    

                
            

            
                

                    

                        

  

      
          

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

              
          

      

      

        

          
              
Get more from Amazon Science

          

          
    
Subscribe to our monthly newsletter



        

        
          
        
      

  



                    

                

            
        

    


    

        

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

        
        
            

    
Social