Automated reasoning at Amazon: A conversation

To mark the occasion of the eighth Federated Logic Conference (FloC), Amazon’s Byron Cook, Daniel Kröning, and Marijn Heule discussed automated reasoning’s prospects.

The Federated Logic Conference (FLoC) is a superconference that, like the Olympics, happens every four years. FLoC draws together 12 distinct conferences on logic-related topics, most of which meet annually. The individual conferences have their own invited speakers, but FLoC as a whole has several plenary speakers as well.

At the last FLoC, in 2018, one of those plenary speakers was Byron Cook, who leads Amazon’s automated-reasoning group, and he was introduced by Daniel Kröning, then a professor of computer science at the University of Oxford

Byron Cook's keynote at FLoC 2018
With introduction by Daniel Kröning.

“What makes me so proud that Byron is here,” Kröning said, is “he’s now at Amazon, and he’s going to run the next Bell Labs, he’s going to run the next Microsoft Research, from within Amazon. My prediction is that — not 10 years but 16 years; remember, it’s multiples of four — 16 years from now you’ll be at a FLoC, and you’ll hear these stories about the great thing that Byron Cook built up at Amazon Web Services. And we’ll speak about it in the same tone as we’re now talking about Bell Labs and Microsoft Research.”

In the audience at the talk was Marijn Heule, a highly cited automated-reasoning researcher who was then at the University of Texas.

“I hadn't met Marijn, though I had heard about him from a couple other people and thought I should talk to him,” Cook says. “And then Marijn found me at the banquet after the talk and was like, ‘I want a job.’”

AR scientists.png
L to R: Amazon vice president and distinguished scientist Byron Cook; Amazon Scholar Marijn Heule; Amazon senior principal scientist Daniel Kröning.

Heule is now an Amazon Scholar who divides his time between Amazon and his new appointment at Carnegie Mellon University. Kröning, too, has joined Amazon as a senior principal scientist, working closely with Cook’s group.

As 2022’s FLoC approached, Cook, Kröning, and Heule took some time to talk with Amazon Science about the current state of automated-reasoning research and its implications for Amazon customers.

Related content
Meet Amazon Science’s newest research area.

Amazon Science: The conference name has the word “logic” in it. Does FLoC deal with other aspects of logic, or is logic coextensive with automated reasoning now?

Byron Cook: It’s about the intersection of logic and computer science. Automated reasoning is one dimension of that intersection.

Daniel Kröning: Traditionally, FLoC is split into two halves, with the first half more theoretical and the second half more applied.

Cook: One of the things about automated reasoning is you're on the bleeding edge of what is even computable. We're often working on intractable or undecidable problems. So people automating reasoning are really paying attention to both the applied and the theoretical.

AS: I know Marijn is concentrating on SAT solvers, and SAT is an intractable problem, right? It’s NP-complete?

Marijn Heule: Yes, but you can also use these techniques to solve problems that go beyond NP. For example, solvers for SAT modulo theories, called SMT. I even have a project with one student trying to solve the famous Collatz conjecture with these tools.

Collatz-27.png
The Collatz conjecture posits that any integer will be transformed into the integer 1 through iterative application of two operations: n/2 and 3n+1. This figure shows a "Collatz cascade" of possible transitions from 27 to 1 using a set of seven symbols, which can be interpreted as simple calculations, and 11 rules for transforming those symbols into symbols consistent with the Collatz operations. At top right are the symbol rewrite rules; at bottom left is a blowup of part of the cascade, illustrating sequences of rewrites that yield the number 425 and its transformation through Collatz operations.

Kröning: SAT is now the inexpensive, easy-to-solve workhorse for really hard problems. People still have it in their heads that SAT equals NP hard, therefore difficult to solve or impossible to solve. But for us, it's the lowest entry point. On top of SAT, we build algorithms for solving problems that are way harder.

Cook: One of the tricks of the trade is abstraction, where you take a problem that's much, much bigger but represent it with something smaller, where classes of questions you might ask about the smaller problem imply that the answer also holds for the bigger problem. We also have techniques for refining the abstractions on demand when the abstraction is losing too much information to answer the question. Often we can represent these abstractions in tools for SAT.

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

Marijn’s work on the Collatz conjecture is a great example of this. He has done this amazing reduction of Collatz to a series of SAT questions, and he's tantalizingly close to solving it because he's got one decidable problem to go — and he's the world expert on solving those problems. [Laughs]

Heule: Tantalizingly close but also so far away, right? Because this problem might not be solvable even with a million cores.

Cook: But it's still decidable. And one of the thresholds is that NP, PSpace, all these things, they're actually decidable. There are questions that are undecidable — and we work on those, too. When a problem is undecidable, it means that your tool will sometimes fail to find an answer, and that's just fundamental: there are no extra computers you could use ever to solve that. The halting problem is a great example of that.

Heule: For these kinds of problems, you're asking the question “Is there a termination argument of this kind of shape?” And if there is one, you have your termination argument. If there is no termination argument of that shape, there could be one of another shape. So if the answer is SAT [satisfiable], then you're happy because you’ve solved the problem. If the answer is no, you try something else.

Cook: It's really, really exciting. In Amazon, we're building these increasingly powerful SAT solvers, using the power of the cloud and distributed systems. So there's no better place for Marijn to be than at Amazon.

Related content
ICSE paper presents techniques piloted by Amazon Web Services’ Automated Reasoning team.

AS: Daniel, could we talk a little bit about your research?

Kröning: What I'm looking at right now is reasoning about the cloud infrastructure that performs remote management of EC2 instances — how to secure that in a way that is provable. You also want to do that in a way that is economical.

Cook: One of the things that Daniel's focusing on is agents. We have pieces of software that run on other machines, like EC2 instances, agents for telemetry or for control, and you give them power to take action on your behalf on your machine. But you want to make sure that an adversary doesn't trick those agents into doing bad things.

Correct software

AS: I know that, commercially, formal methods have been used in hardware design and transportation systems for some time. But it seems that they’re really starting to make inroads in software development, too.

The storage team is able to write code that otherwise they might not want to deploy because they wouldn't be as confident about it, and they're deploying four times as fast. It was an investment in agility that's really paid off.
Byron Cook

Cook: The thing we've seen is it's really by need. The storage team, for example, is able to be much more agile and be much more aggressive in the programs that they write because of the formal methods. They're able to write code that otherwise they might not want to deploy because they wouldn't be as confident about it, and they're deploying four times as fast. It was an investment in agility that's really paid off.

Kröning: There are actually a good number of stories wherein engineering teams didn't dare to roll out a particular feature or design revision or design variant that offers clear benefits — like being faster, using less power — because they just couldn't gain the confidence that it's actually right under all circumstances.

Heule: The interesting thing is that you even see this now in tools. Now we have produced proofs from the tools, and people start implementing features that they wouldn't dare have in the past because they were not clear that they were correct. So the solvers get faster and more complex because we now can check the results from the tools and to have confidence in their correctness.

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

Cook: Yeah, I wanted to double down on that point. There’s a distinction in automated reasoning between finding a proof and checking your proof, and the checking is actually relatively easy. It's an accounting thing. Whereas finding the proof is an incredibly creative activity, and the algorithms that find proofs are mind-blowing. But how do you know that the tool that found the proof is correct? Well, you produce an auditable artifact that you can check with the easy tool.

SAT in the cloud

AS: What are you all most excited about at this year’s FLoC?

Cook: The SAT conference is at FLoC, and there will be the SAT competition results, and one of the things I'm really excited about is the cloud track. Automated reasoning has really moved into the cloud, and the past couple years running the cloud track has really blown the doors off what's possible. I'm expecting that that will be true again this year.

SAT results.png
The results of the top-performing cloud-based, parallel, and sequential SAT solvers in this year's SAT competition, whose results were presented at FLoC. The curves show the number of problems (y-axis) in the SAT competition's anniversary problem set — which aggregates all 5,355 problems presented in the competition's 20-year history — that a given solver could solve in the allotted time (x-axis).

Heule: This is the first year that Amazon is running both the parallel track and the cloud track, and the cloud track was only possible because of Amazon. Before that, there was no way we had the resources to run a cloud track. In the cloud track, every solver-benchmark combination is run on 1,600 cores. And this year is extra special because it's 20 years of SAT, and we have a single anniversary track and all the competitions that were run in the past are in there. That is 5,355 problems, and all the solvers are running on this.

Cook: Wow.

Heule: I'm also excited to see the results. We have seen in the last year and the year before that the cloud solver can, say, solve in 100 seconds as much as the sequential solvers can do in 5,000 seconds. The user doesn't have to wait for four hours but just for four minutes

Cook: And that raises all boats because, as we mentioned earlier, everything is reduced to SAT. If the SAT solvers go from one hour to one minute, that's really game changing. That means a whole other set of things you can do.

What has been clear for a while but continues to be true is there's some sort of Moore's-law thing happening with SAT. You fix the same hardware, the same benchmarks, and then run all the tools from the past 20 years, and you see every year they're getting dramatically better. What's also really amazing is that in many ways the tools are getting simpler.

LH: Are the simplicity and efficiency two sides of the same coin? Understanding the problems better helps you find a simpler solution, which is more efficient?

Cook: Yeah, but it’s also the point that Marijn made that because the tools produce auditable proofs that you can check independently, you can do aggressive things that we were scared to do before. Often, aggressive is much simpler.

Related content
Automated-reasoning method enables the calculation of tight bounds on the use of resources — such as computation or memory — that results from code changes.

Heule: It's also the case that we now understand there are different kinds of problems, and they need different kinds of heuristics. Solvers are combining different heuristics and have phases: “Let's first try this. Let's also try that.” And the code involved in changing the heuristics is very small. It's just changing a couple of parameters. But if you notice, okay, this set of heuristics works well for this problem, then you kind of focus more on that.

Cook: One of the things a SAT solver does is make decisions fast. It just makes a bunch of choices, and those choices won't work out, and then it spends some time to learn lessons why. And then it has a very efficient internal database for managing what has been learned, what not to do in the future. And that prunes the search space a lot.

One of the really exciting things that's happening in the cloud is that you have, say, 1,000 SAT solvers all running on the same problem, and they're learning different things and can share that information amongst them. So by adding 5,000 more solvers, if you can make the communication and the lookup efficient between them, you're really off to the races.

The other thing that's quite neat about that is the point that Marijn is making: it's becoming increasingly clear that there are these fundamental building blocks, and for different kinds of problems, you would want to use one kind of Lego brick versus a different kind of Lego brick. And the cloud allows you to run them all but then to share the information between them.

Iterated SAT solver.png
In "Migrating solver state", Heule and his colleagues show that passing modified versions of a problem between different solvers can accelerate convergence on a solution.

Heule: We have an Amazon paper at FLoC with some very cool ideas. If you run things in the cloud, you sometimes have a limited time window where you have to solve them, and otherwise it stops. You started with a certain problem, the solver did some modifications, and now we have a different problem. Initially we just tested, Okay, can we stop the solver and then store the modified problem somewhere and continue later, in case we need more time than we allocated initially? And then we can continue solving it.

But the interesting thing is that if you give the modified problem to another solver, and you give it, say, a couple of minutes, and then it stores the modified problem, and you give it to another solver, it actually really speeds things up. It turns out to solve the most instances from everything that we tried.

AS: Do you do that in a principled way, or do you just pick a new solver randomly?

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

Heule: The thing that turned out to work really well is to take two top-tier solvers and just Ping-Pong the problem among them. This functionality of storing and continuing search requires some work, so that implementing it in, say, a dozen solvers would require quite some work. But it would be a very interesting experiment.

AS: I’m sure our readers would love to know the result of that experiment!

Well, thank you all very much for your time. Does anyone have any last thoughts?

Cook: I think I speak for the thousands of others who are attending FLoC: we are ready to having our minds blown, just as we did in 2018. Many of the tools and theories presented by our scientific colleagues at this year’s FLoC will challenge our current assumptions or spark that next big insight in our brains. We will also get to catch up with old friends that we’ve known for around 20 years and meet new ones. I’m particularly excited to meet the new generation of scientists who have entered the field, to see the world afresh through their eyes. This is such an amazing time to be in the field of automated reasoning.

Research areas

Related content

US, WA, Seattle
Amazon is seeking an experienced, self-directed data scientist to support the research and analytical needs of Amazon Web Services' Sales teams. This is a unique opportunity to invent new ways of leveraging our large, complex data streams to automate sales efforts and to accelerate our customers' journey to the cloud. This is a high-visibility role with significant impact potential. You, as the right candidate, are adept at executing every stage of the machine learning development life cycle in a business setting; from initial requirements gathering to through final model deployment, including adoption measurement and improvement. You will be working with large volumes of structured and unstructured data spread across multiple databases and can design and implement data pipelines to clean and merge these data for research and modeling. Beyond mathematical understanding, you have a deep intuition for machine learning algorithms that allows you to translate business problems into the right machine learning, data science, and/or statistical solutions. You’re able to pick up and grasp new research and identify applications or extensions within the team. You’re talented at communicating your results clearly to business owners in concise, non-technical language. Key job responsibilities • Work with a team of analytics & insights leads, data scientists and engineers to define business problems. • Research, develop, and deliver machine learning & statistical solutions in close partnership with end users, other science and engineering teams, and business stakeholders. • Use AWS services like SageMaker to deploy scalable ML models in the cloud. • Examples of projects include modeling usage of AWS services to optimize sales planning, recommending sales plays based on historical patterns, and building a sales-facing alert system using anomaly detection.
US, WA, Seattle
We are a team of doers working passionately to apply cutting-edge advances in deep learning in the life sciences to solve real-world problems. As a Senior Applied Science Manager you will participate in developing exciting products for customers. Our team rewards curiosity while maintaining a laser-focus in bringing products to market. Competitive candidates are responsive, flexible, and able to succeed within an open, collaborative, entrepreneurial, startup-like environment. At the leading edge of both academic and applied research in this product area, you have the opportunity to work together with a diverse and talented team of scientists, engineers, and product managers and collaborate with others teams. Location is in Seattle, US Embrace Diversity Here at Amazon, 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 Balance Work and Life 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 Mentor & Grow Careers 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. 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. Key job responsibilities • Manage high performing engineering and science teams • Hire and develop top-performing engineers, scientists, and other managers • Develop and execute on project plans and delivery commitments • Work with business, data science, software engineer, biological, and product leaders to help define product requirements and with managers, scientists, and engineers to execute on them • Build and maintain world-class customer experience and operational excellence for your deliverables
US, Virtual
The Amazon Economics Team is hiring Interns in Economics. We are looking for detail-oriented, organized, and responsible individuals who are eager to learn how to work with large and complicated data sets. Some knowledge of econometrics, as well as basic familiarity with Stata, R, or Python is necessary. Experience with SQL, UNIX, Sawtooth, and Spark would be a plus. These are full-time positions at 40 hours per week, with compensation being awarded on an hourly basis. You will learn how to build data sets and perform applied econometric analysis at Internet speed collaborating with economists, data scientists and MBAʼs. These skills will translate well into writing applied chapters in your dissertation and provide you with work experience that may help you with placement. Roughly 85% of interns from previous cohorts have converted to full time economics employment at Amazon. If you are interested, please send your CV to our mailing list at econ-internship@amazon.com.
US, WA, Seattle
Amazon internships are full-time (40 hours/week) for 12 consecutive weeks with start dates in May - July 2023. Our internship program provides hands-on learning and building experiences for students who are interested in a career in hardware engineering. This role will be based in Seattle, and candidates must be willing to work in-person. Corporate Projects (CPT) is a team that sits within the broader Corporate Development organization at Amazon. We seek to bring net-new, strategic projects to life by working together with customers and evolving projects from ZERO-to-ONE. To do so, we deploy our resources towards proofs-of-concept (POCs) and pilot programs and develop them from high-level ideas (the ZERO) to tangible short-term results that provide validating signal and a path to scale (the ONE). We work with our customers to develop and create net-new opportunities by relentlessly scouring all of Amazon and finding new and innovative ways to strengthen and/or accelerate the Amazon Flywheel. CPT seeks an Applied Science intern to work with a diverse, cross-functional team to build new, innovative customer experiences. Within CPT, you will apply both traditional and novel scientific approaches to solve and scale problems and solutions. We are a team where science meets application. A successful candidate will be a self-starter comfortable with ambiguity, strong attention to detail, and the ability to work in a fast-paced, ever-changing environment. As an Applied Science Intern, you will own the design and development of end-to-end systems. You’ll have the opportunity to create technical roadmaps, and drive production level projects that will support Amazon Science. You will work closely with Amazon scientists, and other science interns to develop solutions and deploy them into production. The ideal scientist must have the ability to work with diverse groups of people and cross-functional teams to solve complex business problems.
US, WA, Seattle
Amazon internships are full-time (40 hours/week) for 12 consecutive weeks with start dates in May - July 2023. Our internship program provides hands-on learning and building experiences for students who are interested in a career in hardware engineering. This role will be based in Seattle, and candidates must be willing to work in-person. Corporate Projects (CPT) is a team that sits within the broader Corporate Development organization at Amazon. We seek to bring net-new, strategic projects to life by working together with customers and evolving projects from ZERO-to-ONE. To do so, we deploy our resources towards proofs-of-concept (POCs) and pilot programs and develop them from high-level ideas (the ZERO) to tangible short-term results that provide validating signal and a path to scale (the ONE). We work with our customers to develop and create net-new opportunities by relentlessly scouring all of Amazon and finding new and innovative ways to strengthen and/or accelerate the Amazon Flywheel. CPT seeks an Applied Science intern to work with a diverse, cross-functional team to build new, innovative customer experiences. Within CPT, you will apply both traditional and novel scientific approaches to solve and scale problems and solutions. We are a team where science meets application. A successful candidate will be a self-starter comfortable with ambiguity, strong attention to detail, and the ability to work in a fast-paced, ever-changing environment. As an Applied Science Intern, you will own the design and development of end-to-end systems. You’ll have the opportunity to create technical roadmaps, and drive production level projects that will support Amazon Science. You will work closely with Amazon scientists, and other science interns to develop solutions and deploy them into production. The ideal scientist must have the ability to work with diverse groups of people and cross-functional teams to solve complex business problems.
US, CA, Palo Alto
The Amazon Search team creates powerful, customer-focused search solutions and technologies. Whenever a customer visits an Amazon site worldwide and types in a query or browses through product categories, Amazon Search services go to work. We design, develop, and deploy high performance, fault-tolerant distributed search systems used by millions of Amazon customers every day. We’re seeking a Principal Scientist with a deep expertise in Search Science. Your responsibilities will include everything from developing and prototyping innovative machine learning, and deep learning algorithms to implementing, testing, and supporting full solutions in a production environment. We are looking for innovators who can contribute to advancing search technology on what’s scientifically possible while remaining committed to creating world-class products. Joining this team, you’ll experience the benefits of working in a dynamic, entrepreneurial environment, while leveraging the resources of Amazon.com (AMZN), Earth's most customer-centric company one of the world's leading internet companies. We provide a highly customer-centric, team-oriented environment in our offices located in Palo Alto, California. Key job responsibilities As a hands-on leader of this team, you’ll be responsible for defining key research questions, identifying relevant data, adopting or proposing innovative machine learning solutions conducting rigorous experiments, publishing results and working with the engineering team to deploy these solutions. As a strategic leader, you will identify investment opportunities, develop long term strategies, and propose, prioritize and deliver on goals. You’ll also participate in organizational planning, hiring, mentorship and leadership development. You will be technically fearless and with a passion for building scalable science and engineering solutions. You will serve as a key scientific resource in full-cycle development (conception, design, implementation, testing to documentation, delivery, and maintenance). About the team Starting in 2009, the Visual Search & Augmented Reality team has thus far launched many visual search solutions on the Amazon App that use computer vision and machine learning/deep learning to help customers complete their shopping missions more easily; multiple internal teams at Amazon (devices, Kindle, Seller services, etc.) also use our libraries and APIs to deliver solutions to their own customers. We are a full stack shop, and our team capabilities cover the whole solution spectrum, ranging across applied science, large scale engineering services, product management, UX design, and mobile app development for iOS and Android.
LU, Luxembourg
&ltHire Relocation Requisition - not for posting> Provides insights to leadership on improving Supply Chain cost and Speed by using Data Science and Analytics techniques. Build Dashboards and models to industrialize these findings at scale.
US, VA, Arlington
The 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 responsibilities Use 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 life Work 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 team We are a multidisciplinary team that combines the talents of science and engineering to develop innovative solutions to make Amazon Earth's Best Employer.
US, WA, Seattle
The 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 apply economic methods to address business problems. 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 in a team setting with individuals from diverse disciplines and backgrounds. They will work with teammates to develop scientific models and conduct 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 responsibilities Use 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 life Work 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 team We are a multidisciplinary team that combines the talents of science and engineering to develop innovative solutions to make Amazon Earth's Best Employer.
US, WA, Seattle
Amazon is looking for talented Postdoctoral Scientists to join our global Science teams for a one-year, full-time research position. Postdoctoral Scientists will innovate as members of Amazon’s key global Science teams, including: AWS, Alexa AI, Alexa Shopping, Amazon Style, CoreAI, Last Mile, and Supply Chain Optimization Technologies. Postdoctoral Scientists will join one of may central, global science teams focused on solving research-intense business problems by leveraging Machine Learning, Econometrics, Statistics, and Data Science. Postdoctoral Scientists will work at the intersection of ML and systems to solve practical data driven optimization problems at Amazon scale. Postdocs will raise the scientific bar across Amazon by diving deep into exploratory areas of research to enhance the customer experience and improve efficiencies. Please note: This posting is one of several Amazon Postdoctoral Scientist postings. Please only apply to a maximum of 2 Amazon Postdoctoral Scientist postings that are relevant to your technical field and subject matter expertise. Key job responsibilities * Work closely with a senior science advisor, collaborate with other scientists and engineers, and be part of Amazon’s vibrant and diverse global science community. * Publish your innovation in top-tier academic venues and hone your presentation skills. * Be inspired by challenges and opportunities to invent cutting-edge techniques in your area(s) of expertise.