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, 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, NY, New York
Job summaryAmazon Advertising is one of Amazon's fastest growing and most profitable businesses, responsible for defining and delivering a collection of advertising products that drive discovery and sales. Our products and solutions are strategically important to enable our Retail and Marketplace businesses to drive long-term growth. We deliver billions of ad impressions and millions of clicks and break fresh ground in product and technical innovations every day!The Advertising Identity Program (AIP) identifies traffic across all devices, websites and apps. We maintain identity graphs that enable us to identify custom audiences and/or Amazon users/sessions across devices and browsers. We enable use cases for Amazon DSP like targeting, audience matching, re-marketing, attribution, frequency capping, traffic quality, regulatory and privacy compliance. As a Data Scientist on this team you will: Develop Data Science solutions from beginning to end.Deliver with independence on challenging large-scale problems with complexity and ambiguity.Write code (Python, R, Scala, SQL, etc.) to obtain, manipulate, and analyze data.Build Machine Learning and statistical models to solve specific business problems.Retrieve, synthesize, and present critical data in a format that is immediately useful to answering specific questions or improving system performance.Analyze historical data to identify trends and support optimal decision making.Apply statistical and machine learning knowledge to specific business problems and data.Formalize assumptions about how our systems should work, create statistical definitions of outliers, and develop methods to systematically identify outliers. Work out why such examples are outliers and define if any actions needed.Given anecdotes about anomalies or generate automatic scripts to define anomalies, deep dive to explain why they happen, and identify fixes.Build decision-making models and propose effective solutions for the business problems you define.Conduct written and verbal presentations to share insights to audiences of varying levels of technical sophistication.Why you will love this opportunity: Amazon has invested heavily in building a world-class advertising business. This team defines and delivers a collection of advertising products that drive discovery and sales. Our solutions generate billions in revenue and drive long-term growth for Amazon’s Retail and Marketplace businesses. We deliver billions of ad impressions, millions of clicks daily, and break fresh ground to create world-class products. We are a highly motivated, collaborative, and fun-loving team with an entrepreneurial spirit - with a broad mandate to experiment and innovate.Impact and Career Growth: You will invent new experiences and influence customer-facing shopping experiences to help suppliers grow their retail business and the auction dynamics that leverage native advertising; this is your opportunity to work within the fastest-growing businesses across all of Amazon! Define a long-term science vision for our advertising business, driven from our customers' needs, translating that direction into specific plans for research and applied scientists, as well as engineering and product teams. This role combines science leadership, organizational ability, technical strength, product focus, and business understanding.Team video ~ https://youtu.be/zD_6Lzw8raE A day in the lifeYou will work collaboratively both within and outside of the Advertising team. As a Software Engineer, you would spend most of your time architecting, designing and coding and the rest in collaboration and discussion. Since we are now working remotely, we also like to have fun by taking time to celebrate each other and to spend time with happy hours. About the teamJoining this team, you’ll experience the benefits of working in a dynamic, fast-paced environment, while leveraging the resources of Amazon.com (AMZN), one of the world's leading Internet companies. We provide a highly customer-centric, team-oriented environment.AdTech Identity Program (AIP) team is spearheading innovation for the existential challenge in AdTech today: The need for reliably establishing customer identity in a IDless world without 3P cookies or Device identifiers.
CA, BC, Vancouver
Job summary Amazon Brand Protection organization focuses on building trust with all brands by accurately representing and completely protecting their brands on Amazon. We strive to be the most trusted thought leader in the space and ensure that public perception mirrors the trustworthy experience we deliver. The Brand Protection machine learning (ML) team is responsible to provide data driven long term strategies and solutions. The team is responsible to develop the state of art ML algorithms to ensure each product is brand authentic and to ensure no abuse or infringements on any brands. The ML team faces the challenges to work with huge amount of structured and unstructured data including images and product descriptions and to develop ML solutions that can scale to protect millions of brands and billions of products worldwide. The team also faces the challenge to fast update our ML systems to stay ahead of bad actors who constantly circumvent our algorithms. If you are excited at these responsibilities and challenges and if you love data and machine learning, we have a position for you. We are looking for a strong manager to manage the ML science team in Vancouver. As the manager, you will hire and develop ML talents. You will design long terms plans and define SMART goals. You will build roadmaps to achieve team’s vision and goals. You will lead the ML directions. You will lead roadmap and plan executions. You will be able to deep dive and guide your team both in directions and in details. You understand ML cycles and advocate ML best practices. You will keep abreast with new ML technologies. Major responsibilities:Work with business/tech teams to identify opportunities, design solution, implement and monitor ML models.Understand business challenges by analyzing data and customer feedbackGuide team members on model building strategies and model experiment, implementation, measurement and continuous improvementBuild and manage team roadmapsCreate long term plans to address complicated business problems at scale using MLDeep dive to provide business insightsCreate business and analytics reports and present to the senior management teamsLead research and implement novel machine learning and statistical approaches
US, WA, Bellevue
Job summaryAre you passionate about leveraging your data science and machine learning skills to make an impact at scale? Do you enjoy developing innovative algorithms, optimization and predictive models to generate recommendations that will be used by automated systems to drive hundreds of millions of impact on Amazon Retail's cash flow? If these questions get you excited, we definitely want to hear from you. Strategic Sourcing team, as part of Amazon Supply Chain Optimization and Technology organization, is seeking an experienced and motivated Data Science leader. Strategic Sourcing team owns systems that are designed to: 1) reduce end to end costs from inbound supply chain and (2) improve vendor performance. Some of the key decisions that these systems make: when and if we should source a product (e.g. is the product obsolete or temporarily unavailable); from which vendor and at what cost we should source an ASIN; what is the ideal supply chain setup (e.g. Pallet, Truckload, Vendor Initiated PO, etc.) for an ASIN/vendor; when should vendor ship/deliver inventory to Amazon FCs; which inbound lanes – vendor warehouse to Amazon FC – should have pre-allocated transportation with how many shipments; when should we penalize vendors for defects/infractions through chargebacks and by how much. Together these set of decisions and systems work together to ensure Amazon’s inventory needs are met on time and in the most efficient way. We develop sophisticated algorithms that involve learning from large amounts of data from diverse sources such Vendors, Transportation carriers, Amazon warehouses etc. Key job responsibilitiesAs the Data Science Senior Manager on this team, you will: • Lead of team of scientists on solving science problems with a high degree of complexity and ambiguity • Develop science roadmaps, run annual planning, and foster cross-team collaboration to execute complex projects • Perform hands-on data analysis, build machine-learning models, run regular A/B tests, and communicate the impact to senior management • Hire and develop top talent, provide technical and career development guidance to scientists and engineers in the organization • Analyze historical data to identify trends and support optimal decision making • Apply statistical and machine learning knowledge to specific business problems and data • Formalize assumptions about how our systems should work, create statistical definitions of outliers, and develop methods to systematically identify outliers. Work out why such examples are outliers and define if any actions needed
CA, ON, Toronto
Job summaryThe Customer Behavior Analytics (CBA) organization owns Amazon’s insights pipeline from data collection to deep analytics. We aspire to be the place where Amazon teams come for answers, a trusted source for data and insights that empower our systems and business leaders to make better decisions. Our outputs shape Amazons marketing teams’ decisions and thus how Amazon customers see, use, and value their experience.CMO (Campaign measurement and Optimization) team within CBA org's mission is to make Amazon’s marketing the most measurably effective in the world. Our long-term objective is to measure the incremental impact of all Amazon’s marketing investments on consumer perceptions, actions, and sales. This requires measuring Amazon’s marketing comparably and consistently across channels, business teams and countries using a comprehensive approach that integrates all Paid, Owned and Earned marketing activity. As the experts on marketing performance, we will lead the Amazon worldwide marketing community by providing critical global insights that can power marketing best practices and tenets globally.Are you passionate about Deep Learning, Causal Inference, and Big Data Systems? Interested in building new state-of-the-art measurement products at petabyte scale? Be part of a team of industry leading experts that operates one of the largest big data and machine learning stacks at Amazon. Amazon is leveraging its highly unique data and applying the latest machine learning and big data technologies to change the way marketers optimize their advertising spend. Our campaign measurement and reporting systems apply these technologies on many billions of events in near real time.You'll be one of the lead scientists tackling some of the hardest problems in advertising; measuring ads incrementality, providing estimated counterfactuals and predicting the success of advertising strategies for omni-channel campaign measurement. Working with a cross-functional team of product managers, program managers, economists and engineers you will develop state of the art causal learning, deep learning, and predictive techniques to help marketers understand the performance of their omni-channel campaigns and optimize their spends.Some things you'll do in this role:Lead full life-cycle Data Science solutions from beginning to end.Deliver with independence on challenging large-scale problems with complexity and ambiguity.Write code (Python, R, Scala, SQL, etc.) to obtain, manipulate, and analyze data.Build Machine Learning and statistical models to solve specific business problems.Retrieve, synthesize, and present critical data in a format that is immediately useful to answering specific questions or improving system performance.Analyze historical data to identify trends and support optimal decision making.Apply statistical and machine learning knowledge to specific business problems and data.Formalize assumptions about how our systems should work, create statistical definitions of outliers, and develop methods to systematically identify outliers. Work out why such examples are outliers and define if any actions needed.Given anecdotes about anomalies or generate automatic scripts to define anomalies, deep dive to explain why they happen, and identify fixes.Build decision-making models and propose effective solutions for the business problems you define.Conduct written and verbal presentations to share insights to audiences of varying levels of technical sophistication.Impact and Career Growth: You will invent solutions that can make billion dollar impact for Amazon as an advertiser. Define a long-term science vision for our business, driven from our customers' needs, translating that direction into specific plans for research and applied scientists, as well as engineering and product teams. This role combines science leadership, organizational ability, technical strength, product focus, and business understanding.This position is based in Irvine, San Francisco, Sunnyvale, San Jose or Seattle. Key job responsibilitiesDive deep into petabyte-scale data to drive insights, identify machine-learning modeling gaps and business opportunitiesEstablish scalable, efficient, automated processes for large-scale data analysisRun regular A/B experiments, gather data, and perform statistical analysisWork with scientists, engineers and product partners to develop new machine learning approaches, and monetization strategiesConduct written and verbal presentation to share insights and recommendations to audiences of varying levels of technical sophistication