A gentle introduction to automated reasoning

Meet Amazon Science’s newest research area.

The new automated-reasoning icon

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 bysolved” 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:

  • logic is a formal and mechanical system for defining what is true and untrue. Examples: propositional logic or first-order logic.
  • theorem is a true statement in logic. Example: the four-color theorem.
  • proof is a valid argument in logic of a theorem. Example: Gonthier's proof of the four-color theorem
  • 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. 
  • 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

Related content

US, WA, Seattle
Job summaryPrime Video is an industry leading, high-growth business and a critical driver of Amazon Prime subscriptions, which contribute to customer loyalty and lifetime value. Prime Video is a digital video streaming and download service that offers Amazon customers the ability to rent, purchase or subscribe to a huge catalog of videos. The Prime Video Economist team works on disruptive ideas in the Prime Video space.We are looking for a truly innovative Data Scientist to work on disruptive ideas within the Prime Video space. Examples of problem spaces you may be working on include video product pricing, ecosystem effects (how streaming affects rentals or purchases), and forecasting demand for new content on the platform.On our team you will work with a diverse scientific team including engineers and economists as well as other data scientist to build statistical models using world-class data systems and partner directly with the business to implement the solutions.Key job responsibilities· Implement code (Python, R, Scala, etc.) for analyzing data and building machine learning/econometric models to solve specific business problems. Work with software engineering teams to productionize algorithms where appropriate.· Lead the development of the scientific roadmap, guide and develop junior engineers in designing and implementing scientific solutions.· Translate analytic insights into concrete, actionable recommendations for business or product improvement. Develop and present these as reports to senior stakeholders with ranging levels of technical knowledge.· Create, enhance, and maintain technical documentation, and present to other scientists, engineers and business leaders.· Demonstrate thorough technical knowledge on feature engineering of massive datasets, effective exploratory data analysis, and model building to deliver accurate and effective business insights.· Innovate by researching, learning, and adapting new modeling techniques and procedures to existing business problems.· Manage and execute entire project from start to finish including problem solving, data gathering and manipulation, predictive modeling, and stakeholder engagement.
US, WA, Bellevue
Job summaryDo you enjoy solving challenging problems and driving innovations in research? Are you seeking for an environment with a group of motivated and talented scientists like yourself? Do you want to create scalable optimization models and apply machine learning techniques to guide real-world decisions? Do you want to play a key role in the future of Amazon transportation and operations? Come and join us at Amazon's Modeling and Optimization team (MOP).Key job responsibilitiesAn Applied Scientist in the Modeling and Optimization (MOP) team· provides analytical decision support to Amazon planning teams via applying advanced mathematical and statistical techniques.· collaborates effectively with Amazon internal business customers, and is their trusted partner· is proactive and autonomous in discovering and resolving business pain-points within a given scope· is able to identify a suitable level of sophistication in resolving the different business needs· is confident in leveraging existing solutions to new problems where appropriate and is independent in designing and implementing new solutions where needed· is aware of the limitations of his/her proposed solutions and is proactive in communicating them to the business, and advances the application of sciences towards Amazon business problems by bringing new methods, ideas, and practices to the team and scientific community.A day in the life· Your will be developing model-based optimization, simulation, and/or predictive tools to identify and evaluate opportunities to improve customer experience, network speed, cost, and efficiency of capital investment.· You will quantify the improvements resulting from the application of these tools and you will evaluate the trade-offs between potentially competing objectives.· You will develop good communication skills and ability to speak at a level appropriate for the audience, will collaborate effectively with fellow scientists, software development engineers, and product managers, and will deliver business value in a close partnership with many stakeholders from operations, finance, IT, and business leadership.About the team· At the Modeling and Optimization (MOP) team, we use mathematical optimization, algorithm design, statistics, and machine learning to improve decision-making capabilities across WW Operations and Amazon Logistics.· We focus on transportation topology, labor and resource planning for fulfillment centers (FC), routing science, visualization research, data science and development, and process optimization.· We create models to simulate, optimize, and control the fulfillment network with the objective of reducing cost while improving speed and reliability.· We support multiple business lanes, therefore maintain a comprehensive and objective view, coordinating solutions across organizational lines where possible.
US, WA, Seattle
Job summaryAt Amazon, we're working to be the most customer-centric company on earth. To get there, we need exceptionally talented, bright, result oriented, and driven people. Amazon is seeking a Data Scientist - Simulation to assist in designing and optimizing the fulfillment network concepts and process improvements using discrete event simulations for our World Wide Design Engineering Team. Successful candidates will be natural self-starters who have the drive to design, model, and simulate new fulfillment center concepts and processes. The Simulation Data Scientist will be expected to deep dive problems and drive relentlessly towards creative solutions. This individual needs to be comfortable interfacing and driving various functional teams and individuals at all levels of the organization in order to be successful. Perform process modelling and simulation using discrete event simulation software’s, process optimization, statistical data analysis, and Design of Experiments (DOE) etc. to drive decisions on process and designs. Need based remote work option is available.Responsibilities:· Lead system level complex Discrete Event Simulation (DES) projects to build , simulate, and optimize the fulfillment center operational process flow models using FlexSim, Demo 3D, AnyLogic or any other Discrete Event Simulation (DES) software packages· Understand process flows , analyze data, perform Design of Experiments and effectively represent in simulation model to achieve better correlation and process improvements· Manage multiple DES simulation projects and tasks simultaneously and effectively influence, negotiate, and communicate with internal and external business partners, contractors and vendors.· Facilitate process improvement initiatives among site operations, engineering, and corporate systems groups.· Utilize code (python or another object oriented language) for data analysis and modeling algorithms· Analyze historical data to identify trends and support decision making using Statistical Techniques· Lead and coordinate simulation efforts between internal teams and outside vendors to develop optimal solutions for the network, including equipment specification, material flow, process design, and site layout.· Deliver results according to project schedules and quality· Provide written and verbal presentations to share insights and recommendations to audiences of varying levels of technical sophistication.· Make technical trade-offs for long term/short-term needs considering challenges in business area by applying relevant data science disciplines, and interactions among systems.
US, WA, Seattle
Job summaryAmazon is seeking an outstanding Data Scientist to uncover key insights on how customers engage with live sports events on Prime Video globally. With prestigious US sporting matches on Prime Video from NFL’s Thursday Night Football, the WNBA, AVP, the New York Yankees, and the Seattle Sounders, as well as global events like the English Premiere League (UK), UEFA Champions League (Italy, Germany), Ligue 1 (France), US Open Tennis (UK), Roland Garros (France), Autumn Nations Cup Rugby (UK) and more, live sports are an integral and growing component of Prime Video. As our selection of events expands, the Prime Video Content Analytics team is looking to enable agile decision making on live sports by developing key insights into customer engagement with live sport and translating these insights into large scale predictive modeling and analytics solutions.Key job responsibilitiesYou will have the following responsibilities within the scope of our global Prime Video business:· Drive analytics in an uncharted field that is not only developing at a fast pace but also becoming increasingly important to the Prime Video business· Support the analytical needs of stakeholders in the sports, advertising, finance, and live events teams, inclusive of statistical inference, demand modeling, and feature engineering· Build profitability models for new sports rights and partner with finance on business use cases· Think outside the box to use novel data and methodological approaches· Create new metrics that effectively guide the business and deploy dashboards to surface them to senior leadership· Ensure that the quality and timeliness of analytic deliverables meet business expectationsAbout the teamThe Prime Video Content Analytics team uses machine learning, econometrics, and data science to optimize Amazon’s streaming-video catalogue, driving customer engagement and Prime member acquisition. We generate insights to guide Amazon’s digital-video strategy, and we provide direct support to the content-acquisition process. We use detailed customer behavioral data (e.g. streaming history) and detailed information about content (e.g. IMDb-sourced characteristics) to predict and understand what customers like to watch.
ES, M, Madrid
Job summaryAmazon is looking for creative Applied Scientists to tackle some of the most interesting problems on the leading edge of machine learning (ML), search, natural language processing (NLP), and related areas with our Amazon Books team. At Amazon Books we believe that books are not only needed to work, education and entertainment, but are also required for a healthy society. As such, we aim to create an unmatched book discovery experience for our customers worldwide. We enable customers to discover new books, authors and genres through sophisticated recommendation engines, smart search tools and through social interaction, and we need your help to keep innovating in this space.If you are looking for an opportunity to solve deep technical problems and build innovative solutions in a fast-paced environment working within a smart and passionate team, this might be the role for you. You will develop and implement novel algorithms and modeling techniques to advance the state-of-the-art in technology areas at the intersection of ML, search, NLP, and deep learning. You will innovate, help move the needle for applied research in these exciting areas and build cutting-edge and scalable technologies that enable delightful experiences for hundreds of millions of people.In this role you will:· Work collaboratively with other scientists and developers to design and implement scalable models for improving our customers' experience discovering and getting the most out of their books;· Have the opportunity to work with a variety of technologies in a variety of use cases;· Drive scalable solutions from the business to prototyping, production testing and through engineering directly to production;· Drive best practices on the team, deal with ambiguity and competing objectives, and mentor and guide other members to achieve their career growth potential.About the teamWe aspire to be experts at the forefront of AI, machine learning and data science and their application to books e-commerce to help engineering teams innovate for readers, authors and publishers.As an Applied Scientist, you'll help us translate customer problems into tractable technical problems, and find ways to solve them by combining your expertise and that of other scientists and team members. You will work with partner engineering and business teams to ensure solutions have a real impact.
US, WA, Seattle
Job summaryAre you inspired by building new technologies to benefit customers? Do you dream of being at the forefront of robotics and autonomous system technology? Would you enjoy working in a fast paced, highly collaborative, start-up like environment? If you answered yes to any of these then you've got to check out the Amazon Scout team.We’ve been hard at work developing a new, fully-electric delivery system – Amazon Scout – designed to get packages to customers using autonomous delivery devices. These devices were created by Amazon, are the size of a small cooler, and roll along sidewalks at a walking pace. We developed Amazon Scout at our research and development lab in Seattle, ensuring the devices can safely and efficiently navigate around pets, pedestrians and anything else in their path.The Amazon Scout team shares a passion for innovation using advanced technologies, a love of solving complex challenges, and a desire to delight customers. We're looking for people who like dealing with ambiguity, solving hard, large scale problems, and working in a startup like environment. To learn more about Amazon Scout, check out our Amazon Day One Blog here: http://amazon.com/scoutAs a part of the localization team you will:· Collaborate closely with engineers, applied researchers and hardware teams to develop computer vision and machine learning algorithms and software for robots.· Take responsibility for technical problem solving, including creatively meeting product objectives and developing best practices.· Interact with teammates in variety of roles to accomplish your goals· Identify and initiate investigations of new technologies, prototype and test solutions for product features, and design and validate designs that deliver an exceptional user experience.· Recruit, hire and develop other applied scientists.
US, WA, Bellevue
Job summaryThe People eXperience and Technology Central Science Team (PXTCS) uses economics, behavioral science, statistics, and machine learning to proactively identify mechanisms and process improvements which simultaneously improve Amazon and the lives, wellbeing, and the value of work to Amazonians. We are an interdisciplinary team that combines the talents of science and engineering to develop and deliver solutions that measurably achieve this goal.We are looking for economists who are able to work with business partners to hone complex problems into specific, scientific questions, and test those questions to generate insights. The ideal candidate will work with engineers and computer scientists to estimate models and algorithms on large scale data, design pilots and measure their impact, and transform successful prototypes into improved policies and programs at scale. We are looking for creative thinkers who can combine a strong technical economic toolbox with a desire to learn from other disciplines, and who know how to execute and deliver on big ideas as part of an interdisciplinary technical team.Ideal candidates will work closely with business partners to develop science that solves the most important business challenges. They will work in a team setting with individuals from diverse disciplines and backgrounds. They will serve as an ambassador for science and a scientific resource for business teams, so that scientific processes permeate throughout the HR organization to the benefit of Amazonians and Amazon. Ideal candidates will own the data analysis, modeling, and experimentation that is necessary for estimating and validating models. They will work closely with engineering teams to develop scalable data resources to support rapid insights, and take successful models and findings into production as new products and services. They will be customer-centric and will communicate scientific approaches and findings to business leaders, listening to and incorporate their feedback, and delivering successful scientific solutions.Key job responsibilitiesUse causal inference methods to evaluate the impact of policies on employee outcomes. Examine how external labor market and economic conditions impact Amazon's ability to hire and retain talent. Use scientifically rigorous methods to develop and recommend career paths for employees.A day in the lifeWork with teammates to apply economic methods to business problems. This might include identifying the appropriate research questions, writing code to implement a DID analysis or estimate a structural model, or writing and presenting a document with findings to business leaders. Our economists also collaborate with partner teams throughout the process, from understanding their challenges, to developing a research agenda that will address those challenges, to help them implement solutions.About the teamWe are a multidisciplinary team that combines the talents of science and engineering to develop innovative solutions to make Amazon Earth's Best Employer.
US, Virtual
Job summaryAmazon’s Global Reliability Team is seeking a Principal Research Scientist to help envision, design and build the next generation of predictive maintenance capabilities and inventory management optimization behind Amazon’s Fulfillment Centers, Transportation Services, and Global Specialty Fulfillment.Key job responsibilitiesThe Principal Research Scientist will partner with senior leadership to develop long term strategic products/solutions and will represent and advocate them to leaders in our organization and other partner organizations such as Amazon Fulfillment Technologies, Workplace Health and Safety, amongst others. They will interact with Amazon scholars and universities among other research institutions to ensure that our team and our senior executives are up to speed on important trends, tools and technologies and how they can be used to impact the business.A day in the lifeIn this role, you will participate and lead the brainstorming sessions and review other scientists’ research. They will actively participate in the science community through presenting their research at the internal and external conference. They will mentor senior scientists for their career development and growth and help the company to identify and acquire scientists with the right skillset.About the teamWe are seeking high-energy individuals that are passionate about working with real-time machine and sensor data to build automated systems aimed to improve equipment availability.This position is perfect for someone who has a deep and broad analytic background and is passionate about using mathematical modeling and statistical analysis to make a real difference. Experience in applied analytics is essential, and they should be familiar with modern tools for data science and business analysis. We are particularly interested in candidates with research background in reliability engineering, econometrics, statistical inference, and time series modeling.
US, MA, Cambridge
Job summaryAmazon Lab126 is an inventive research and development company that designs and engineers high-profile consumer electronics. Lab126 began in 2004 as a subsidiary of Amazon.com, Inc., originally creating the best-selling Kindle family of products. Since then, we have produced groundbreaking devices like Fire tablets, Fire TV and Amazon Echo. What will you help us create?The Role:We are looking for a high caliber Applied Scientist Lead to join our team. As part of the larger technology team working on new consumer technology, your work will have a large impact to hardware, internal software developers, ecosystem, and ultimately the lives of Amazon customers. In this role, you will:• Lead a team of talented audio scientists and SW developers to bring a new and innovative audio products and services to delight customers• Propose new research projects, get buy-in from stakeholders, plan and budget the project and lead the team for successful execution• Work closely with an inter-disciplinary product development team including outside partners to bring the prototype algorithm into commercialization• Mentor team on music/speech/acoustic processing technology development• Manage small team of world class scientists and SW engineers in audio• Take a big part in the mission to create earth's best employerBe a respectable team leader in an open and collaborative environment
US, MA, Boston
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 that work passionately to apply cutting edge advances in robotics and software to solve real-world challenges that will transform our customers’ experiences in ways we can’t even image yet. 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.We seek a talented and motivated engineer to tackle broad challenges in system-level analysis. You will work in a small team to quantify system performance at scale and to expand the breadth and depth of our analysis (e.g. increase the range of software components and warehouse processes covered by our models, develop our library of key performance indicators, construct experiments that efficiently root cause emergent behaviors). You will engage with growing teams of software development and warehouse design engineers to drive evolution of the AR system and of the simulation engine that supports our work.This role is a 6 month co-op to join AR full time (40 hours/week) from July-December 2022. Come join us in North Reading, MA, or in our newly expanded innovation hub in Westborough, MA!Both campuses provide a unique opportunity for co-ops to have direct access to robotics testing labs and manufacturing facilities. Remote and hybrid flexibility is available for this role.