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!

View from space of a connected network around planet Earth representing the Internet of Things.
Sign up for our newsletter

Research areas

Related content

US, CA, Santa Clara
Job summaryAmazon is looking for a passionate, talented, and inventive Applied Scientist with a strong machine learning background to help build industry-leading language technology.Our mission is to provide a delightful experience to Amazon’s customers by pushing the envelope in Natural Language Processing (NLP), Natural Language Understanding (NLU), Dialog management, conversational AI and Machine Learning (ML).As part of our AI team in Amazon AWS, you will work alongside internationally recognized experts to develop novel algorithms and modeling techniques to advance the state-of-the-art in human language technology. Your work will directly impact millions of our customers in the form of products and services, as well as contributing to the wider research community. You will gain hands on experience with Amazon’s heterogeneous text and structured data sources, and large-scale computing resources to accelerate advances in language understanding.We are hiring primarily in Conversational AI / Dialog System Development areas: NLP, NLU, Dialog Management, NLG.This role can be based in NYC, Seattle or Palo Alto.Inclusive Team CultureHere at AWS, we embrace our differences. We are committed to furthering our culture of inclusion. We have ten employee-led affinity groups, reaching 40,000 employees in over 190 chapters globally. We have innovative benefit offerings, and host annual and ongoing learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences.Work/Life BalanceOur team puts a high value on work-life balance. It isn’t about how many hours you spend at home or at work; it’s about the flow you establish that brings energy to both parts of your life. We believe striking the right balance between your personal and professional life is critical to life-long happiness and fulfillment. We offer flexibility in working hours and encourage you to find your own balance between your work and personal lives.Mentorship & Career GrowthOur team is dedicated to supporting new members. We have a broad mix of experience levels and tenures, and we’re building an environment that celebrates knowledge sharing and mentorship. Our senior members enjoy one-on-one mentoring and thorough, but kind, code reviews. We care about your career growth and strive to assign projects based on what will help each team member develop into a better-rounded engineer and enable them to take on more complex tasks in the future.
US, NY, New York
Job summaryAmazon is looking for a passionate, talented, and inventive Applied Scientist with a strong machine learning background to help build industry-leading language technology.Our mission is to provide a delightful experience to Amazon’s customers by pushing the envelope in Natural Language Processing (NLP), Natural Language Understanding (NLU), Dialog management, conversational AI and Machine Learning (ML).As part of our AI team in Amazon AWS, you will work alongside internationally recognized experts to develop novel algorithms and modeling techniques to advance the state-of-the-art in human language technology. Your work will directly impact millions of our customers in the form of products and services, as well as contributing to the wider research community. You will gain hands on experience with Amazon’s heterogeneous text and structured data sources, and large-scale computing resources to accelerate advances in language understanding.We are hiring primarily in Conversational AI / Dialog System Development areas: NLP, NLU, Dialog Management, NLG.This role can be based in NYC, Seattle or Palo Alto.Inclusive Team CultureHere at AWS, we embrace our differences. We are committed to furthering our culture of inclusion. We have ten employee-led affinity groups, reaching 40,000 employees in over 190 chapters globally. We have innovative benefit offerings, and host annual and ongoing learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences.Work/Life BalanceOur team puts a high value on work-life balance. It isn’t about how many hours you spend at home or at work; it’s about the flow you establish that brings energy to both parts of your life. We believe striking the right balance between your personal and professional life is critical to life-long happiness and fulfillment. We offer flexibility in working hours and encourage you to find your own balance between your work and personal lives.Mentorship & Career GrowthOur team is dedicated to supporting new members. We have a broad mix of experience levels and tenures, and we’re building an environment that celebrates knowledge sharing and mentorship. Our senior members enjoy one-on-one mentoring and thorough, but kind, code reviews. We care about your career growth and strive to assign projects based on what will help each team member develop into a better-rounded engineer and enable them to take on more complex tasks in the future.
US, CA, Santa Clara
Job summaryAWS AI/ML is looking for world class scientists and engineers to join its AI Research and Education group working on building automated ML solutions for planetary-scale sustainability and geospatial applications. Our team's mission is to develop ready-to-use and automated solutions that solve important sustainability and geospatial problems. We live in a time wherein geospatial data, such as climate, agricultural crop yield, weather, landcover, etc., has become ubiquitous. Cloud computing has made it easy to gather and process the data that describes the earth system and are generated by satellites, mobile devices, and IoT devices. Our vision is to bring the best ML/AI algorithms to solve practical environmental and sustainability-related R&D problems at scale. Building these solutions require a solid foundation in machine learning infrastructure and deep learning technologies. The team specializes in developing popular open source software libraries like AutoGluon, GluonCV, GluonNLP, DGL, Apache/MXNet (incubating). Our strategy is to bring the best of ML based automation to the geospatial and sustainability area.We are seeking an experienced Applied Scientist for the team. This is a role that combines science knowledge (around machine learning, computer vision, earth science), technical strength, and product focus. It will be your job to develop ML system and solutions and work closely with the engineering team to ship them to our customers. You will interact closely with our customers and with the academic and research communities. You will be at the heart of a growing and exciting focus area for AWS and work with other acclaimed engineers and world famous scientists. You are also expected to work closely with other applied scientists and demonstrate Amazon Leadership Principles (https://www.amazon.jobs/en/principles). Strong technical skills and experience with machine learning and computer vision are required. Experience working with earth science, mapping, and geospatial data is a plus. Our customers are extremely technical and the solutions we build for them are strongly coupled to technical feasibility.About the teamInclusive Team CultureAt AWS, we embrace our differences. We are committed to furthering our culture of inclusion. We have ten employee-led affinity groups, reaching 40,000 employees in over 190 chapters globally. We have innovative benefit offerings, and host annual and ongoing learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences. Amazon’s culture of inclusion is reinforced within our 14 Leadership Principles, which remind team members to seek diverse perspectives, learn and be curious, and earn trust. Work/Life BalanceOur team puts a high value on work-life balance. It isn’t about how many hours you spend at home or at work; it’s about the flow you establish that brings energy to both parts of your life. We believe striking the right balance between your personal and professional life is critical to life-long happiness and fulfillment. We offer flexibility in working hours and encourage you to find your own balance between your work and personal lives.Mentorship & Career GrowthOur team is dedicated to supporting new members. We have a broad mix of experience levels and tenures, and we’re building an environment that celebrates knowledge sharing and mentorship. Our senior members enjoy one-on-one mentoring. We care about your career growth and strive to assign projects based on what will help each team member develop into a better-rounded scientist and enable them to take on more complex tasks in the future.Interested in this role? Reach out to the recruiting team with questions or apply directly via amazon.jobs.
US, CA, Santa Clara
Job summaryAWS AI/ML is looking for world class scientists and engineers to join its AI Research and Education group working on building automated ML solutions for planetary-scale sustainability and geospatial applications. Our team's mission is to develop ready-to-use and automated solutions that solve important sustainability and geospatial problems. We live in a time wherein geospatial data, such as climate, agricultural crop yield, weather, landcover, etc., has become ubiquitous. Cloud computing has made it easy to gather and process the data that describes the earth system and are generated by satellites, mobile devices, and IoT devices. Our vision is to bring the best ML/AI algorithms to solve practical environmental and sustainability-related R&D problems at scale. Building these solutions require a solid foundation in machine learning infrastructure and deep learning technologies. The team specializes in developing popular open source software libraries like AutoGluon, GluonCV, GluonNLP, DGL, Apache/MXNet (incubating). Our strategy is to bring the best of ML based automation to the geospatial and sustainability area.We are seeking an experienced Applied Scientist for the team. This is a role that combines science knowledge (around machine learning, computer vision, earth science), technical strength, and product focus. It will be your job to develop ML system and solutions and work closely with the engineering team to ship them to our customers. You will interact closely with our customers and with the academic and research communities. You will be at the heart of a growing and exciting focus area for AWS and work with other acclaimed engineers and world famous scientists. You are also expected to work closely with other applied scientists and demonstrate Amazon Leadership Principles (https://www.amazon.jobs/en/principles). Strong technical skills and experience with machine learning and computer vision are required. Experience working with earth science, mapping, and geospatial data is a plus. Our customers are extremely technical and the solutions we build for them are strongly coupled to technical feasibility.About the teamInclusive Team CultureAt AWS, we embrace our differences. We are committed to furthering our culture of inclusion. We have ten employee-led affinity groups, reaching 40,000 employees in over 190 chapters globally. We have innovative benefit offerings, and host annual and ongoing learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences. Amazon’s culture of inclusion is reinforced within our 14 Leadership Principles, which remind team members to seek diverse perspectives, learn and be curious, and earn trust. Work/Life BalanceOur team puts a high value on work-life balance. It isn’t about how many hours you spend at home or at work; it’s about the flow you establish that brings energy to both parts of your life. We believe striking the right balance between your personal and professional life is critical to life-long happiness and fulfillment. We offer flexibility in working hours and encourage you to find your own balance between your work and personal lives.Mentorship & Career GrowthOur team is dedicated to supporting new members. We have a broad mix of experience levels and tenures, and we’re building an environment that celebrates knowledge sharing and mentorship. Our senior members enjoy one-on-one mentoring. We care about your career growth and strive to assign projects based on what will help each team member develop into a better-rounded scientist and enable them to take on more complex tasks in the future.Interested in this role? Reach out to the recruiting team with questions or apply directly via amazon.jobs.
US, WA, Seattle
Job summaryHow can we create a rich, data-driven shopping experience on Amazon? How do we build data models that helps us innovate different ways to enhance customer experience? How do we combine the world's greatest online shopping dataset with Amazon's computing power to create models that deeply understand our customers? Recommendations at Amazon is a way to help customers discover products. Our team's stated mission is to "grow each customer’s relationship with Amazon by leveraging our deep understanding of them to provide relevant and timely product, program, and content recommendations". We strive to better understand how customers shop on Amazon (and elsewhere) and build recommendations models to streamline customers' shopping experience by showing the right products at the right time. Understanding the complexities of customers' shopping needs and helping them explore the depth and breadth of Amazon's catalog is a challenge we take on every day. Using Amazon’s large-scale computing resources you will ask research questions about customer behavior, build models to generate recommendations, and run these models directly on the retail website. You will participate in the Amazon ML community and mentor Applied Scientists and software development engineers with a strong interest in and knowledge of ML. Your work will directly benefit customers and the retail business and you will measure the impact using scientific tools. We are looking for passionate, hard-working, and talented Applied scientist who have experience building mission critical, high volume applications that customers love. You will have an enormous opportunity to make a large impact on the design, architecture, and implementation of cutting edge products used every day, by people you know.Key job responsibilitiesScaling state of the art techniques to Amazon-scaleWorking independently and collaborating with SDEs to deploy models to productionDeveloping long-term roadmaps for the team's scientific agendaDesigning experiments to measure business impact of the team's effortsMentoring scientists in the departmentContributing back to the machine learning science community
US, NY, New York
Job summaryAmazon Web Services is looking for world class scientists to join the Security Analytics and AI Research team within AWS Security Services. This group is entrusted with researching and developing core data mining and machine learning algorithms for various AWS security services like GuardDuty (https://aws.amazon.com/guardduty/) and Macie (https://aws.amazon.com/macie/). In this group, you will invent and implement innovative solutions for never-before-solved problems. If you have passion for security and experience with large scale machine learning problems, this will be an exciting opportunity.The AWS Security Services team builds technologies that help customers strengthen their security posture and better meet security requirements in the AWS Cloud. The team interacts with security researchers to codify our own learnings and best practices and make them available for customers. We are building massively scalable and globally distributed security systems to power next generation services.Inclusive Team Culture Here at AWS, we embrace our differences. We are committed to furthering our culture of inclusion. We have ten employee-led affinity groups, reaching 40,000 employees in over 190 chapters globally. We have innovative benefit offerings, and host annual and ongoing learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences. Amazon’s culture of inclusion is reinforced within our 14 Leadership Principles, which remind team members to seek diverse perspectives, learn and be curious, and earn trust. Work/Life Balance Our team puts a high value on work-life balance. It isn’t about how many hours you spend at home or at work; it’s about the flow you establish that brings energy to both parts of your life. We believe striking the right balance between your personal and professional life is critical to life-long happiness and fulfillment. We offer flexibility in working hours and encourage you to find your own balance between your work and personal lives. Mentorship & Career Growth Our team is dedicated to supporting new members. We have a broad mix of experience levels and tenures, and we’re building an environment that celebrates knowledge sharing and mentorship. We care about your career growth and strive to assign projects based on what will help each team member develop and enable them to take on more complex tasks in the future.A day in the lifeAbout the hiring groupJob responsibilities* Rapidly design, prototype and test many possible hypotheses in a high-ambiguity environment, making use of both quantitative and business judgment.* Collaborate with software engineering teams to integrate successful experiments into large scale, highly complex production services.* Report results in a scientifically rigorous way.* Interact with security engineers, product managers and related domain experts to dive deep into the types of challenges that we need innovative solutions for.
US, MA, Westborough
Job summaryAre you inspired by invention? Is problem solving through teamwork in your DNA? Do you like the idea of seeing how your work impacts the bigger picture? Answer yes to any of these and you’ll fit right in here at Amazon Robotics. We are a smart team of doers who work passionately to apply cutting edge advances in robotics and software to solve real-world challenges that will transform our customers’ experiences. We invent new improvements every day. We are Amazon Robotics and we will give you the tools and support you need to invent with us in ways that are rewarding, fulfilling, and fun.Amazon.com empowers a smarter, faster, more consistent customer experience through automation. Amazon Robotics automates fulfillment center operations using various methods of robotic technology including autonomous mobile robots, sophisticated control software, language perception, power management, computer vision, depth sensing, machine learning, object recognition, and semantic understanding of commands. Amazon Robotics has a dedicated focus on research and development to continuously explore new opportunities to extend its product lines into new areas.This role is a 6-month Co-Op to join AR full-time (40 hours/week) from January 9, 2023 to June 23, 2023. Amazon Robotics co-op opportunity will be Hybrid (2-3 days onsite) and based out of the Greater Boston Area in our two state-of-the-art facilities in Westborough, MA and North Reading, MA. Both campuses provide a unique opportunity to have direct access to robotics testing labs and manufacturing facilities.Key job responsibilitiesWe are seeking data scientist co-ops to help us analyze data, quantify uncertainty, and build machine learning models to make quick prediction.
US, WA, Seattle
Job summaryDo you want to join an innovative team of scientists who use machine learning and statistical techniques to help Amazon provide the best customer experience by preventing eCommerce fraud? 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? Do you like to own end-to-end business problems/metrics and directly impact the profitability of the company? Do you enjoy collaborating in a diverse team environment? If yes, then you may be a great fit to join the Amazon Buyer Risk Prevention (BRP) Machine Learning group. We are looking for a talented scientist who is passionate to build advanced algorithmic systems that help manage safety of millions of transactions every day.Major responsibilities Use statistical and machine learning techniques to create scalable risk management systemsLearning and understanding large amounts of Amazon’s historical business data for specific instances of risk or broader risk trendsDesign, development and evaluation of highly innovative models for risk managementWorking closely with software engineering teams to drive real-time model implementations and new feature creationsWorking closely with operations staff to optimize risk management operations,Establishing scalable, efficient, automated processes for large scale data analyses, model development, model validation and model implementationTracking general business activity and providing clear, compelling management reporting on a regular basisResearch and implement novel machine learning and statistical approaches
US, CA, Palo Alto
Job summaryAmazon is investing heavily in building a customer centric, world class advertising business across its many unique audio, video, and display surfaces. We are looking for an Applied Scientist who has a deep passion for building machine-learning solutions in our advertising decision system. In this role, you will be on the cutting edge of developing monetization solutions for Live TV, Connected TV and streaming Audio. These are nascent, high growth areas, where advertising monetization is an important, fully integrated part of the core strategy for each business.Key job responsibilitiesRapidly design, prototype and test machine learning algorithms for optimizing advertising reach, frequency and return on advertising spendBuild systems that extract and process volumes of disparate data using a variety of econometric and machine learning approaches. These systems should be designed to scale with exponential growth in data and run continuously.Leverage knowledge of advanced software system and algorithm development to build our measurement and optimization engine.Contribute intellectual property through patent generation.Functionally decompose complex problems into simple, straight-forward solutions.Understand system inter-dependencies and limitations as well as analytic inter-dependencies to build efficient solutions.A day in the lifeAs an Applied Scientist, you will be tasked with leading innovations in machine learning algorithms to deliver ads across platforms influencing product features and architectural choices for decision making systems. You will need to work with data scientists to invent elegant metrics and associated measurement models, and develop algorithms that help advertisers test and learn the impact of advertising strategies across channels on these metrics while ensuring a great customer experience.
US, WA, Seattle
Job summaryThe Amazon Devices Demand Science team is looking for an energetic, focused and skilled, truly innovative and technically strong research scientist with a background in data analytics, machine learning, data science, decision science and statistical modeling/analysis to help with demand forecasting and planning for the entire Amazon device family of products, services and accessories.Amazon is looking for a talented Senior Research Scientist to join the Amazon Devices team. We materially impact Amazon’s device businesses by forecasting demand, influencing promotion pricing and identifying optimal inventory allocation of all Amazon Devices using ML, operations research and big data.Key job responsibilitiesIn this role, you will have an opportunity to both develop advanced scientific solutions and drive critical customer and business impacts. You will play a key role to drive end-to-end solutions from understanding our business requirements, exploring a large amount of historical data and ML models, building prototypes and exploring conceptually new solutions, to working with partner teams for prod deployment. You will collaborate closely with scientists, engineering peers as well as business stakeholders. You will be responsible for researching, prototyping, experimenting, analyzing predictive models and developing artificial intelligence-enabled automation solutions.As a Senior Research Scientist, you will:• research and develop new methodologies for demand forecasting, alarms, alerts and automation.• apply your advanced data analytics, machine learning skills to solve complex demand planning and allocation problems.• work closely with stakeholders and translate data-driven findings into actionable insights.• improve upon existing methodologies by adding new data sources and implementing model enhancements.• create and track accuracy and performance metrics.• create, enhance, and maintain technical documentation, and present to other scientists, engineers and business leaders.• drive best practices on the team; mentor and guide junior members to achieve their career growth potential.A day in the lifeThis role will be a Problem Solver, Doer, Detail Oriented, Communicator and Influencer.Problem Solver: Ability to utilize exceptional modeling and problem-solving skills to work through different challenges in ambiguous situations.Doer: You’ve successfully delivered end-to-end operations research projects, working through conflicting viewpoints and data limitations.Detail Oriented: You have an enviable level of attention to details.Communicator: Ability to communicate analytical results to senior leaders, and peers.Influencer: Innovative scientist with the ability to identify opportunities and develop novel modeling approaches in a fast-paced and ever-changing environment, and gain support with data and storytelling.About the teamWe are a growing team continues to operate in "startup" mode to prove new business ideas, while strengthening our core ML platforms.This role is available for the following locations: Seattle/Bellevue, Washington; Arlington, Virginia (HQ2); Denver, Colorado; Bay Area/Los Angeles Metro, California; and Nashville, Tennessee. (other US Locations can be discussed further)