Automated reasoning's scientific frontiers

Distributing proof search, reasoning about distributed systems, and automating regulatory compliance are just three fruitful research areas.

Automated reasoning is the algorithmic search through the infinite set of theorems in mathematical logic. We can use automated reasoning to answer questions about what systems such as biological models and computer programs can and cannot do in the wild.

In the 1990s, AMD, IBM, Intel, and other companies invested in automated reasoning for circuit and microprocessor design, leading to today’s widely used and industry-standard hardware formal-verification tools (e.g., JasperGold). In the 2000s, automated reasoning expanded to niche software domains such as device drivers (e.g., Static Driver Verifier) or transportation systems (e.g., Prover technology). In the 2010s, we saw automated reasoning increasingly applied to our foundational computing infrastructure, such as cryptography, networking, storage, and virtualization.

Related content
Meet Amazon Science’s newest research area.

With recently launched cloud services such as IAM Access Analyzer and VPC Network Access Analyzer, automated reasoning is now beginning to change how computer systems built on top of the cloud are developed and operated.

All these applications of automated reasoning rest on a common foundation: automated and semi-automated mechanical theorem provers. ACL2, CVC5, HOL-light’s Meson_tac, MiniSat, and Vampire are a few examples, but there are many more we could name. They are all, in outline, working on the same problem: the search for proofs in mathematical logic.

Over the past 30 years, slowly but surely, a virtuous cycle has formed: automated reasoning in specific and critical application areas drives more investment in foundational tools, while improvements in the foundational tools drive further applications. Around and around.

SAT graph comparison.png
The propositional-satisfiability problem (a.k.a. SAT) is NP-complete, and in the case of unstructured decision graphs (left), the problem instances can be prohibitively time consuming to solve. But when the decision graphs have some inherent structure (right), automatic solvers can exploit that structure to find solutions efficiently.
Visualizations produced by Carsten Sinz, using his 3DVis visualization tool

The increasingly difficult benchmarks driving the development of these tools present new science opportunities. International competitions such as CASC, SAT-COMP, SMT-COMP, SV-COMP, and the Termination competition have accelerated this virtuous cycle. On the application side, with increasing power from the tools come new research opportunities in the design of customer-intuitive tools (such as models of cellular signaling pathways or Amazon's abstraction of control policies for cloud computing).

As an example of the virtuous cycle at work, consider the following graph, which shows the results for all of the winners of SAT-COMP from 2002 to 2021, compared apples-to-apples in a competition with the same hardware and same benchmarks:

Winners 2021.png

This graph plots the number of benchmarks that each solver can solve in 200 seconds, 400 seconds, etc. The higher the line, the more benchmarks the solver could solve. By looking at the plot we can see, for example, that the 2010 winner (cryptominisat) solved approximately 50 benchmarks within the allotted 1,000 seconds, whereas the 2021 winner (kissat) can solve nearly four times as many benchmarks in the same time, using the same hardware. Why did the tools get better? Because members of the scientific community pushing on the application submitted benchmarks to the competitions, which helped tool developers take the tools to new heights of performance and scale.

At Amazon we see the velocity of the virtuous cycle dramatically increasing. Our automated-reasoning tools are now called billions of times daily, with growth rates exceeding 100% year-over-year. For example, AWS customers now have 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 using tools such as Dafny, P, and SAW.

Related content
In a pilot study, an automated code checker found about 100 possible errors, 80% of which turned out to require correction.

What’s most exciting to me as an automated-reasoning scientist is that our research area seems to be entering a golden era. I think we are beginning to witness a transformation in automated reasoning that is similar to what happened in virtualized computing as the cloud’s virtuous cycle spun up. As described in Werner Vogels’s 2019 re:Invent keynote, AWS’s EC2 team was driven by unprecedented customer adoption to reinvent its hypervisor, microprocessor, and networking stack, capturing significant improvements in security, cost, and team agility made possible by economies of scale.

There are parallels in automated reasoning today. Dramatic new infrastructure is needed for viable business reasons, putting a spotlight on research questions that were previously obscure and unsolved. Below I outline three examples of open research areas driven by the increasing scale of automated-reasoning tools and our underlying computing infrastructure.

Example: Distributed proof search

For over two decades the automated-reasoning scientific community has postulated that distributed-systems-based proof search could be faster than sequential proof search. But we didn’t have the economic scale to justify serious investigation of the question.

At Amazon, with our increased reliance on automated reasoning, we now have that kind of scale. For example, we sponsored the new cloud-based-tool tracks in several international competitions.

Compare the mallob-mono solver, the winner of SAT-COMP’s new cloud-solver track, to the single-microprocessor solvers:

2 Mallob-mono.png

Mallob-mono is now, by a wide margin, the most powerful SAT solver on the planet. And like the sequential solvers, the distributed solvers are improving.

As described in Kuhn’s seminal book <i>The Structure of Scientific Revolutions</i>, major perspective shifts like this tend to trigger scientific revolutions. The success of distributed proof search raises the possibility of similar revolutions. For example, we may need to re-evaluate our assumptions about when to use eager vs. lazy reduction techniques when converting between formalisms.

Related content
Rungta had a promising career with NASA, but decided the stars aligned for her at Amazon.

Here at Amazon, we recently reconsidered the PhD dissertation of University of California, Berkeley, professor Sanjit Seshia in light of mallob-mono and were able to quickly (in about 2,000 lines of Rust) develop a new eager-reduction-based solver that outperforms today’s leading lazy-reduction tools on the notoriously difficult SMT-COMP bcnscheduling and job_shop benchmarks. Here we are solving SAT problems that go beyond Booleans, to involve integers, real numbers, strings, or functions. We call this SAT modulo theories, or SMT.

In the graph below we compare the performance of leading lazy SMT solvers CVC5 and Z3 to a Seshia-style eager solver based on the SAT solvers Kissat and mallob-mono on those benchmarks:

Solver performance.png

We’ve published the code for our Seshia-style eager solver on GitHub.

There are many other open questions driven by distributed proof search. For example, is there an effective lookahead-solver strategy for SMT that would facilitate cube-and-conquer? Or as the Zoncolan service does when analyzing programs for security vulnerabilities, can we memoize intermediate lemmas in a cloud database and reuse them, rather than recomputing for each query? Can Monte Carlo tree search in the cloud on past proofs be used to synthesize more-effective proof search strategies?

Another example: Reasoning about distributed systems

Recent examples of formal reasoning within AWS at the level of distributed-protocol design include a proof of S3’s recently announced strong consistency and the protocol-level proof of secrecy in AWS's KMS service. The problem with these proofs is that they apply to the protocols that power the distributed services, not necessarily to the code running on the servers that use those protocols.

Related content
SOSP paper describes lightweight formal methods for validating new S3 data storage service.

Here at Amazon, we believe that automated reasoning at the level of protocol design has the greatest long-term value when the investment cost is amortized and protected via continuous integration/continuous delivery (CI/CD) integrations with the code that implements the protocols. That is, the benefit of upfront effort is often seen later, when protocol compliance proofs fail on buggy changes to implementation source code. The code doesn’t make it to production until the developers have fixed it.

Again: major perspective shifts like those resulting from successful proofs about S3 and KMS could trigger a revolution, à la Kuhn. For years, we have had tools for reasoning about distributed systems, such as TLA+ and P. But with the success of the work with S3 and KMS, it’s now clear that protocol design should be a first-class concept for engineering, with tools that support it, proactively finding errors and proving properties.

These tools should also connect to the source code that speaks the protocols by (i) constructing specifications that can be proved with existing code-level tools and (ii) synthesizing implementation code in languages such as C, Go, Rust, or Java. The tools would facilitate integration into our CI/CD, code review, and ticketing systems, allowing service teams to (iii) synthesize “runtime monitors” to exploit enterprise-level operations strength by providing telemetry about the status of a service’s conformance to a proved protocol.

Final example: Automating regulatory compliance

At the recent Computer-Aided Verification (CAV ’21) workshop called Formal Approaches to Certifying Compliance (talks recorded and available), we heard from NIST, Coalfire, Collins Aerospace, DARPA, and Amazon about the use of automated reasoning to lower the cost and the time-to-market added by regulatory compliance.

Karthik Amrutesh of the AWS security assurance team reported that automated reasoning enabled a 91% reduction in the time it took for our third-party auditor to produce evidence for checking controls. For perhaps the first time in the more than 2,500-year history of mathematical logic, we see a business use case that exploits the difference between finding proofs and checking proofs. What's the difference? Finding is usually the hard part, the creative part, the part that requires sophisticated algorithms. Finding is usually undecidable or NP-complete, depending on the context.

Meanwhile, not only is checking proofs decidable in most cases, but it’s often linear in the size of the proof. To check proofs, compliance auditors can use well-understood and trusted small solvers such as HOL-light.

Using cloud-scale automation to find the proofs lowers cost. That lets the auditor offer its services for less, saving the customer money. It also reduces the latency of audits, a major pain point for developers looking to go to market quickly.

An audit check involves constraints on the form that valid text strings can take. The set of constraints is known as a string theory, and the imposition of that theory means that audit checks are SMT problems.

From the perspective of automated-reasoning science, it becomes important to build string theory solvers that can efficiently construct easily checkable proof artifacts. In the realm of propositional satisfiability — SAT problems — the DRAT proof checker is now the standard methodology for communicating proofs. But in SMT, no such standard exists. What would a general-purpose theory-agnostic SMT format and checker look like?

Conclusion

We've come a long way from days when automated reasoning was the exclusive domain of circuit designers or aerospace engineers. Success in these early domains kicked off a virtuous cycle for the makers of the theorem provers that power automated reasoning. With applications for mainstream applications such as cloud computing, the automated-reasoning virtuous cycle is now radically accelerating. After 2,500 years of mathematical-logic research and 70+ years of automated-reasoning science, we live in a heady time. With wider adoption of and investment in automated reasoning, we are seeing economies of scale where what we can do now would have been unimaginable even two or three years ago. Welcome to the future!

Research areas

Related content

US, CA, San Diego
Do you want to join an innovative team of scientists who use deep learning, natural language processing, large language models to help Amazon provide the best seller experience across the entire Seller life cycle, including recruitment, growth, support and provide the best customer and seller experience by automatically mitigating risk? Do you want to build advanced algorithmic systems that help manage the trust and safety of millions of customer interactions every day? Are you excited by the prospect of analyzing and modeling terabytes of data and creating state-of-the-art algorithms to solve real world problems? Are you excited by the opportunity to leverage GenAI and innovate on top of the state-of-the-art large language models to improve customer and seller experience? Do you like to build end-to-end business solutions and directly impact the profitability of the company? Do you like to innovate and simplify processes? If yes, then you may be a great fit to join the Machine Learning Accelerator team in the Amazon Selling Partner Services (SPS) group. Key job responsibilities The scope of an Applied Scientist III in the Selling Partner Services (SPS) Machine Learning Accelerator (MLA) team is to research and prototype Machine Learning applications that solve strategic business problems across SPS domains. Additionally, the scientist collaborates with engineers and business partners to design and implement solutions at scale when they are determined to be of broad benefit to SPS organizations. They develop large-scale solutions for high impact projects, introduce tools and other techniques that can be used to solve problems from various perspectives, and show depth and competence in more than one area. They influence the team’s technical strategy by making insightful contributions to the team’s priorities, approach and planning. They develop and introduce tools and practices that streamline the work of the team, and they mentor junior team members and participate in hiring. We are open to hiring candidates to work out of one of the following locations: San Diego, CA, USA
US, WA, Seattle
Amazon is looking for a strategic, innovative science leader within the Global Talent and Compensation (GTMC) organization to lead an interdisciplinary team charged with developing data-driven solutions to model, automate, and inform high judgement decision making by bringing together science and technology in consumer grade internal talent products. GTMC delivers employee-focused experiences by providing scalable and responsive mechanisms for employees, as well as listening and signaling mechanisms for managers and leaders. They do this through intelligent, flexible, and extensible products and scalable data and science services. They set out to deliver a singular experience supporting multiple employee talent journeys (e.g., onboarding, evaluation, compensation, movement, promotion, exit), to generate and capture signals from product data, surface outliers, increase personalization, and improve the efficacy of “next best action” recommendations, for 1.6 million Amazonians around the world. In this role you will lead multiple research teams across the disciplines of Talent Management, Diversity Equity and Inclusion, and Compensation. You will interface with the most senior leaders at Amazon to develop and deliver on a strategic research roadmap that crosses all lines of Amazon businesses (e.g., Consumer, AWS, Devices, Advertising). This role will then partner with engineering and product management leader to deliver the outcomes of this research in production environments. Successful candidates will have an established background expertise in machine learning with some experience in applying this expertise to the fields of talent management, product management and/or software development. We are open to hiring candidates to work out of one of the following locations: Seattle, WA, USA
IN, KA, Bangalore
Are you interested in changing the Digital Reading Experience? We are from Kindle Books Team looking for a set of Scientists to take the reading experience in Kindle to next level with a set of innovations! We envision Kindle as the place where readers find the best manifestation of all written content optimized with features that enable them to get the most out of reading, and creators are able to realize their vision to customers quickly and at scale. Every time customers open their content, regardless of surface, they start or restart their reading in a familiar, useful and engaging place. We achieve this by building a strong foundation of core experiences and act as a force multiplier and partner for content creators (directly or indirectly) to easily innovate on top of Kindle's purpose built content experience stack in a simple and extensible way. We will achieve this by providing a best-in-class reading experience, unique content experiences, and remaining agile in meeting the evolving needs and preferences of our users. Our goal is to foster long-lasting reading habits and make us the preferred destination for enriching literary experiences. We are building a In The Book Science team and looking for Scientists, who are passionate about Reading and are willing to take Reading to the next level. Every Book is a complex structure with different entities, layout, format and semantics, with more than 17MM eBooks in our catalog. We are looking for experts in all domains like core NLP, Generative AI, CV and Deep Learning Techniques for unlocking capabilities like analysis, enhancement, curation, moderation, translation, transformation and generation in Books based on Content structure, features, Intent & Synthesis. Scientists will focus on Inside the book content and semantically learn the different entities to enhance the Reading experience overall (Kindle & beyond). They have an opportunity to influence in 2 major phases of life-cycle - Publishing (Creation of Books process) and Reading experience (building engaging features & representation in the book thereby driving reading engagement). Key job responsibilities - 5+ years of building machine learning models for business application experience - PhD, or Master's degree and 6+ years of applied research experience - Knowledge of programming languages such as C/C++, Python, Java or Perl - Experience programming in Java, C++, Python or related language - You have expertise in one of the applied science disciplines, such as machine learning, natural language processing, computer vision, Deep learning - You are able to use reasonable assumptions, data, and customer requirements to solve problems. - You initiate the design, development, execution, and implementation of smaller components with input and guidance from team members. - You work with SDEs to deliver solutions into production to benefit customers or an area of the business. - You assume responsibility for the code in your components. You write secure, stable, testable, maintainable code with minimal defects. - You understand basic data structures, algorithms, model evaluation techniques, performance, and optimality tradeoffs. - You follow engineering and scientific method best practices. You get your designs, models, and code reviewed. You test your code and models thoroughly - You participate in team design, scoping and prioritization discussions. You are able to map a business goal to a scientific problem and map business metrics to technical metrics. - You invent, refine and develop your solutions to ensure they are meeting customer needs and team goals. You keep current with research trends in your area of expertise and scrutinize your results. - Experience in mentoring junior scientists A day in the life You will be working with a group of talented scientists on researching algorithm and running experiments to test solutions to improve our experience. This will involve collaboration with partner teams including engineering, PMs, data annotators, and other scientists to discuss data quality, model development and productionizing the same. You will mentor other scientists, review and guide their work, help develop roadmaps for the team. We are open to hiring candidates to work out of one of the following locations: Banagalore, KA, IND | Bangalore, IND | Bangalore, KA, IND
IN, KA, Bangalore
Are you interested in changing the Digital Reading Experience? We are from Kindle Books Team looking for a set of Scientists to take the reading experience in Kindle to next level with a set of innovations! We envision Kindle as the place where readers find the best manifestation of all written content optimized with features that enable them to get the most out of reading, and creators are able to realize their vision to customers quickly and at scale. Every time customers open their content, regardless of surface, they start or restart their reading in a familiar, useful and engaging place. We achieve this by building a strong foundation of core experiences and act as a force multiplier and partner for content creators (directly or indirectly) to easily innovate on top of Kindle's purpose built content experience stack in a simple and extensible way. We will achieve this by providing a best-in-class reading experience, unique content experiences, and remaining agile in meeting the evolving needs and preferences of our users. Our goal is to foster long-lasting reading habits and make us the preferred destination for enriching literary experiences. We are building a In The Book Science team and looking for Scientists, who are passionate about Reading and are willing to take Reading to the next level. Every Book is a complex structure with different entities, layout, format and semantics, with more than 17MM eBooks in our catalog. We are looking for experts in all domains like core NLP, Generative AI, CV and Deep Learning Techniques for unlocking capabilities like analysis, enhancement, curation, moderation, translation, transformation and generation in Books based on Content structure, features, Intent & Synthesis. Scientists will focus on Inside the book content and semantically learn the different entities to enhance the Reading experience overall (Kindle & beyond). They have an opportunity to influence in 2 major phases of life-cycle - Publishing (Creation of Books process) and Reading experience (building engaging features & representation in the book thereby driving reading engagement). Key job responsibilities - 3+ years of building machine learning models for business application experience - PhD, or Master's degree and 2+ years of applied research experience - Knowledge of programming languages such as C/C++, Python, Java or Perl - Experience programming in Java, C++, Python or related language - You have expertise in one of the applied science disciplines, such as machine learning, natural language processing, computer vision, Deep learning - You are able to use reasonable assumptions, data, and customer requirements to solve problems. - You initiate the design, development, execution, and implementation of smaller components with input and guidance from team members. - You work with SDEs to deliver solutions into production to benefit customers or an area of the business. - You assume responsibility for the code in your components. You write secure, stable, testable, maintainable code with minimal defects. - You understand basic data structures, algorithms, model evaluation techniques, performance, and optimality tradeoffs. - You follow engineering and scientific method best practices. You get your designs, models, and code reviewed. You test your code and models thoroughly - You participate in team design, scoping and prioritization discussions. You are able to map a business goal to a scientific problem and map business metrics to technical metrics. - You invent, refine and develop your solutions to ensure they are meeting customer needs and team goals. You keep current with research trends in your area of expertise and scrutinize your results. A day in the life You will be working with a group of talented scientists on researching algorithm and running experiments to test solutions to improve our experience. This will involve collaboration with partner teams including engineering, PMs, data annotators, and other scientists to discuss data quality, model development and productionizing the same. You will mentor other scientists, review and guide their work, help develop roadmaps for the team. We are open to hiring candidates to work out of one of the following locations: Bangalore, IND | Bangalore, KA, IND
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 We are open to hiring candidates to work out of one of the following locations: Bengaluru, KA, IND
IN, KA, Bengaluru
How to use the world’s richest collection of e-commerce data to improve payments experience for our customers? Amazon Payments Global Data Science team seeks a Senior Data Scientist for building analytical and scientific solutions that will address increasingly complex business questions in the Gift-Cards space. Amazon.com has a culture of data-driven decision-making and demands intelligence that is timely, accurate, and actionable. This team operates at WW level and provides a fast-paced environment where every day brings new challenges and opportunities. As a Senior Data Scientist in this team, you will be driving the Data Science/ML roadmap for business continuity & growth. You will develop statistical and machine learning models to solve for complex business problems in Gift-Cards space, design and run global experiments, and find new ways to optimize the customer experience. 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. You will explore GenAI use-cases within Gift-Cards space and also work on cross-disciplinary efforts with other scientists within Amazon. Key job responsibilities - You should be detail-oriented and must have an aptitude for solving unstructured and ambiguous problems. You should work in a self-directed environment, own tasks and drive them to completion - You should be passionate about working with huge data sets and be someone who loves to bring datasets together to answer business questions - You should demonstrate thorough technical expertise on feature engineering of massive datasets, exploratory data analysis, and model building using state-of-art ML algorithms - Random Forest, Gradient Boosting, SVM, Neural Nets, DL, Reinforcement Learning etc. You should be aware of automating feedback loops for algorithms in production - You should work closely with internal stakeholders like the business teams, engineering teams and partner teams and align them with respect to your focus areas - You should have excellent business and communication skills to be able to work with business owners to develop and define key business questions and build mechanisms that answer those questions We are open to hiring candidates to work out of one of the following locations: Bengaluru, KA, IND
US, NY, New York
The Automated Reasoning Group in AWS Platform is looking for an Applied Scientist with experience in building scalable solver solutions that delight customers. You will be part of a world-class team building the next generation of automated reasoning tools and services. AWS has the most services and more features within those services, than any other cloud provider–from infrastructure technologies like compute, storage, and databases–to emerging technologies, such as machine learning and artificial intelligence, data lakes and analytics, and Internet of Things. You will apply your knowledge to propose solutions, create software prototypes, and move prototypes into production systems using modern software development tools and methodologies. In addition, you will support and scale your solutions to meet the ever-growing demand of customer use. You will use your strong verbal and written communication skills, are self-driven and own the delivery of high quality results in a fast-paced environment. Each day, hundreds of thousands of developers make billions of transactions worldwide on AWS. They harness the power of the cloud to enable innovative applications, websites, and businesses. Using automated reasoning technology and mathematical proofs, AWS allows customers to answer questions about security, availability, durability, and functional correctness. We call this provable security, absolute assurance in security of the cloud and in the cloud. See https://aws.amazon.com/security/provable-security/ As an Applied Scientist in AWS Platform, you will play a pivotal role in shaping the definition, vision, design, roadmap and development of product features from beginning to end. You will: - Define and implement new solver applications that are scalable and efficient approaches to difficult problems - Apply software engineering best practices to ensure a high standard of quality for all team deliverables - Work in an agile, startup-like development environment, where you are always working on the most important stuff - Deliver high-quality scientific artifacts - Work with the team to define new interfaces that lower the barrier of adoption for automated reasoning solvers - Work with the team to help drive business decisions The AWS Platform is the glue that holds the AWS ecosystem together. From identity features such as access management and sign on, cryptography, console, builder & developer tools, to projects like automating all of our contractual billing systems, AWS Platform is always innovating with the customer in mind. The AWS Platform team sustains over 750 million transactions per second. Learn and Be Curious. We have a formal mentor search application that lets you find a mentor that works best for you based on location, job family, job level etc. Your manager can also help you find a mentor or two, because two is better than one. In addition to formal mentors, we work and train together so that we are always learning from one another, and we celebrate and support the career progression of our team members. Inclusion and Diversity. Our team is diverse! We drive towards an inclusive culture and work environment. We are intentional about attracting, developing, and retaining amazing talent from diverse backgrounds. Team members are active in Amazon’s 10+ affinity groups, sometimes known as employee resource groups, which bring employees together across businesses and locations around the world. These range from groups such as the Black Employee Network, Latinos at Amazon, Indigenous at Amazon, Families at Amazon, Amazon Women and Engineering, LGBTQ+, Warriors at Amazon (Military), Amazon People With Disabilities, and more. Key job responsibilities Work closely with internal and external users on defining and extending application domains. Tune solver performance for application-specific demands. Identify new opportunities for solver deployment. About the team Solver science is a talented team of scientists from around the world. Expertise areas include solver theory, performance, implementation, and applications. 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. 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. We are open to hiring candidates to work out of one of the following locations: New York, NY, USA
US, WA, Bellevue
Amazon’s Automated Inventory Management (AIM) Planning Organization is looking for a Data Scientist to help invent the next generation of Amazon's Capacity and Constraint Management system - Automated Planning System (APS). APS will herald a a new era in Sales and Operations Planning (S&OP). APS emerges as a next-generation decision-making framework for Amazon's Worldwide (WW) fulfillment networks. In an industry first, APS seamlessly aligns Amazon's business controls by uniting cutting-edge supply and demand forecasts with a state-of-the-art coordination framework – respecting the distributed ownership of business logic and outcomes. As the centralized planning system, APS takes charge of coordinating all fulfillment, inventory, and operational decisions, maximizing WW Long Term Free Cash Flow (LTFCF) over a 1-year horizon The AIM team is part of the Supply Chain Optimization Technology (SCOT) Team within the Operations Organization. The charter of the SCOT team is to maximize Amazon’s return on our inventory investment in terms of Free Cash Flow and customer satisfaction. The planning organization within Amazon leads the S&OP, IPE and Capacity Planning functions. As a Data Scientist on the this team, you will build a deep understanding of Amazon's supply chain systems, lead innovation in our forecasting capabilities and build principled solutions to identify improvement opportunities in our supply chain using the latest machine learning techniques. You will also work with a team of Product Managers, Business Intelligence Engineers and Software Engineers to research and build accurate predictive models and deploy automated software solutions to provide insights to business leaders at the most senior levels throughout the company. You will build models that make our data more actionable and help us make complex business decisions at scale. To help describe some of our challenges, we created a short video about Supply Chain Optimization at Amazon - http://bit.ly/amazon-scot Key job responsibilities - Implement statistical and machine learning methods to solve complex business problems - Research new ways to improve predictive and explanatory models - Directly contribute to the design and development of automated prediction systems and ML infrastructure - Build models that can detect supply chain defects and explain variance to the optimal state - Collaborate with other researchers, software developers, and business leaders to define the scientific roadmap for this team We are open to hiring candidates to work out of one of the following locations: Bellevue, WA, USA
US, WA, Seattle
Do you want to join an innovative team of scientists who use machine learning to help Amazon provide the best experience to our Selling Partners by automatically understanding and addressing their challenges, needs and opportunities? Do you want to build advanced algorithmic systems that are powered by state-of-art ML, such as Natural Language Processing, Large Language Models, Deep Learning, Computer Vision and Causal Modeling, to seamlessly engage with Sellers? Are you excited by the prospect of analyzing and modeling terabytes of data and creating cutting edge algorithms to solve real world problems? Do you like to build end-to-end business solutions and directly impact the profitability of the company and experience of our customers? Do you like to innovate and simplify? If yes, then you may be a great fit to join the Selling Partner Experience Science team. Key job responsibilities - Use statistical and machine learning techniques to create the next generation of the tools that empower Amazon's Selling Partners to succeed. - Design, develop and deploy highly innovative models to interact with Sellers and delight them with solutions. - Work closely with teams of scientists and software engineers to drive real-time model implementations and deliver novel and highly impactful features. - Establish scalable, efficient, automated processes for large scale data analyses, model development, model validation and model implementation. - Research and implement novel machine learning and statistical approaches. - Participate in strategic initiatives to employ the most recent advances in ML in a fast-paced, experimental environment. About the team Selling Partner Experience Science is a growing team of scientists, engineers and product leaders engaged in the research and development of the next generation of ML-driven technology to empower Amazon's Selling Partners to succeed. We draw from many science domains, from Natural Language Processing to Computer Vision to Optimization to Economics, to create solutions that seamlessly and automatically engage with Sellers, solve their problems, and help them grow. Focused on collaboration, innovation and strategic impact, we work closely with other science and technology teams, product and operations organizations, and with senior leadership, to transform the Selling Partner experience. We are open to hiring candidates to work out of one of the following locations: Denver, CO, USA | Seattle, WA, USA
US, WA, Seattle
Amazon is investing heavily in building a world class advertising business and developing a collection of self-service performance advertising products that drive discovery and sales. Our products are strategically important to our Retail and Marketplace businesses for driving long-term growth. We deliver billions of ad impressions and millions of clicks daily and are breaking fresh ground to create world-class products. We are highly motivated, collaborative and fun-loving with an entrepreneurial spirit and bias for action. With a broad mandate to experiment and innovate, we are growing at an unprecedented rate with a seemingly endless range of new opportunities. Key job responsibilities Search Supply and Experiences, within Sponsored Products, is seeking a Senior Data Scientist to join a fast growing team with the mandate of creating new ads experience that elevates the shopping experience for our hundreds of millions customers worldwide. We are looking for a top analytical mind capable of understanding our complex ecosystem of advertisers participating in a pay-per-click model– and leveraging this knowledge to help turn the flywheel of the business. As a Senior Data Scientist on this team you will: - Lead Data Science solutions from beginning to end. - Deliver with independence on challenging large-scale problems with ambiguity. - Manage and drive the technical and analytical aspects of Advertiser segmentation; continually advance approach and methods. - Write code (Python, R, Scala, etc.) to analyze data and build statistical models to solve specific business problems - Retrieve, synthesize, and present critical data in a format that is immediately useful to answering specific questions or improving system performance. - Analyze historical data to identify trends and support decision making. - Improve upon existing methodologies by developing new data sources, testing model enhancements, and fine-tuning model parameters. - Provide requirements to develop analytic capabilities, platforms, and pipelines. - Apply statistical and machine learning knowledge to specific business problems and data. - Formalize assumptions about how our systems should work, create statistical definitions of outliers, and develop methods to systematically identify outliers. Work out why such examples are outliers and define if any actions needed. - Given anecdotes about anomalies or generate automatic scripts to define anomalies, deep dive to explain why they happen, and identify fixes. - Build decision-making models and propose solution for the business problem you defined - Conduct written and verbal presentation to share insights and recommendations to audiences of varying levels of technical sophistication. - Write code (python or another object-oriented language) for data analyzing and modeling algorithms. A day in the life The Senior Data Scientist will have the opportunity to use one of the world's largest eCommerce and advertising data sets to influence the evolution of our products. This role requires an individual with excellent business, communication, and technical skills, enabling collaboration with various functions, including product managers, software engineers, economists and data scientists, as well as senior leadership. This role will create and enhance performance monitoring reports to find insights that product and business team should focus on. The successful candidate will be a self-starter comfortable with ambiguity, with strong attention to detail, and with an ability to work in a fast-paced, high-energy and ever-changing environment. The drive and capability to shape the direction is a must. This role will influence the direction of the business by leveraging our data to deliver insights that drive decisions and actions. The role will involve translating broad business problems into specific analytics projects, conducting deep quantitative analyses, and communicating results effectively. The role will help the organization identify, evaluate, and evangelize new techniques and tools to continue to improve our ability to deliver value to Amazon’s customers. About the team We are a customer-obsessed team of engineers, technologists, product leaders, and scientists. We are focused on continuous exploration of contexts and creatives where advertising delivers value to customers and advertisers. We specifically work on new ads experiences globally with the goal of helping shoppers make the most informed purchase decision. We obsess about our customers and we are continuously innovating on their behalf to enrich their shopping experience on Amazon We are open to hiring candidates to work out of one of the following locations: Seattle, WA, USA