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, VA, Arlington
Are you looking to work at the forefront of Machine Learning and AI? Would you be excited to apply cutting edge Generative AI algorithms to solve real world problems with significant impact? The Generative AI Innovation Center at AWS is a new strategic team that helps AWS customers implement Generative AI solutions and realize transformational business opportunities. This is a team of strategists, data scientists, engineers, and solution architects working step-by-step with customers to build bespoke solutions that harness the power of generative AI. The team helps customers imagine and scope the use cases that will create the greatest value for their businesses, select and train and fine tune the right models, define paths to navigate technical or business challenges, develop proof-of-concepts, and make plans for launching solutions at scale. The GenAI Innovation Center team provides guidance on best practices for applying generative AI responsibly and cost efficiently. You will work directly with customers and innovate in a fast-paced organization that contributes to game-changing projects and technologies. You will design and run experiments, research new algorithms, and find new ways of optimizing risk, profitability, and customer experience. We’re looking for Data Scientists capable of using GenAI and other techniques to design, evangelize, and implement state-of-the-art solutions for never-before-solved problems. A key focus of this role is GenAI model customization using techniques such as fine-tuning and continued pre-training to help customers build differentiating solutions with their unique data. Key job responsibilities As a Data Scientist, you will: Collaborate with AI/ML scientists and architects to research, design, develop, and evaluate cutting-edge generative AI algorithms to address real-world challenges Interact with customers directly to understand the business problem, help and aid them in implementation of generative AI solutions, deliver briefing and deep dive sessions to customers and guide customer on adoption patterns and paths to production Create and deliver best practice recommendations, tutorials, blog posts, sample code, and presentations adapted to technical, business, and executive stakeholder Provide customer and market feedback to Product and Engineering teams to help define product direction About the team Sales, Marketing and Global Services (SMGS) AWS Sales, Marketing, and Global Services (SMGS) is responsible for driving revenue, adoption, and growth from the largest and fastest-growing small- and mid-market accounts to enterprise-level customers, including the public sector. The AWS Global Support team interacts with leading companies and believes that world-class support is critical to customer success. AWS Support also partners with a global list of customers that are building mission-critical applications on top of AWS services. The Professional Services team is part of Global Services. About AWS Diverse Experiences AWS values diverse experiences. Even if you do not meet all of the qualifications and skills listed in the job description, we encourage candidates to apply. If your career is just starting, hasn’t followed a traditional path, or includes alternative experiences, don’t let it stop you from applying. Why AWS? Amazon Web Services (AWS) is the world’s most comprehensive and broadly adopted cloud platform. We pioneered cloud computing and never stopped innovating — that’s why customers from the most successful startups to Global 500 companies trust our robust suite of products and services to power their businesses. Inclusive Team Culture Here at AWS, it’s in our nature to learn and be curious. Our employee-led affinity groups foster a culture of inclusion that empower us to be proud of our differences. Ongoing events and learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences, inspire us to never stop embracing our uniqueness. Mentorship & Career Growth We’re continuously raising our performance bar as we strive to become Earth’s Best Employer. That’s why you’ll find endless knowledge-sharing, mentorship and other career-advancing resources here to help you develop into a better-rounded professional. Work/Life Balance We value work-life harmony. Achieving success at work should never come at the expense of sacrifices at home, which is why we strive for flexibility as part of our working culture. When we feel supported in the workplace and at home, there’s nothing we can’t achieve in the cloud. We are open to hiring candidates to work out of one of the following locations: Arlington, VA, USA | Denver, CO, USA | Herndon, VA, USA | New York, NY, USA | Santa Clara, CA, USA | Seattle, WA, USA | Washington Dc, DC, USA
CN, 11, Beijing
Amazon Search JP builds features powering product search on the Amazon JP shopping site and expands the innovations to world wide. As an Applied Scientist on this growing team, you will take on a key role in improving the NLP and ranking capabilities of the Amazon product search service. Our ultimate goal is to help customers find the products they are searching for, and discover new products they would be interested in. We do so by developing NLP components that cover a wide range of languages and systems. As an Applied Scientist for Search JP, you will design, implement and deliver search features on Amazon site, helping millions of customers every day to find quickly what they are looking for. You will propose innovation in NLP and IR to build ML models trained on terabytes of product and traffic data, which are evaluated using both offline metrics as well as online metrics from A/B testing. You will then integrate these models into the production search engine that serves customers, closing the loop through data, modeling, application, and customer feedback. The chosen approaches for model architecture will balance business-defined performance metrics with the needs of millisecond response times. Key job responsibilities - Designing and implementing new features and machine learned models, including the application of state-of-art deep learning to solve search matching, ranking and Search suggestion problems. - Analyzing data and metrics relevant to the search experiences. - Working with teams worldwide on global projects. Your benefits include: - Working on a high-impact, high-visibility product, with your work improving the experience of millions of customers - The opportunity to use (and innovate) state-of-the-art ML methods to solve real-world problems with tangible customer impact - Being part of a growing team where you can influence the team's mission, direction, and how we achieve our goals We are open to hiring candidates to work out of one of the following locations: Beijing, 11, CHN | Shanghai, 31, CHN
US, VA, Arlington
Device Economics is looking for an economist experienced in causal inference, empirical industrial organization, forecasting, and scaled systems to work on business problems to advance critical resource allocation and pricing decisions in the Amazon Devices org. Output will be included in scaled systems to automate existing processes and to maximize business and customer objectives. Amazon Devices designs and builds Amazon first-party consumer electronics products to delight and engage customers. Amazon Devices represents a highly complex space with 100+ products across several product categories (e-readers [Kindle], tablets [Fire Tablets], smart speakers and audio assistants [Echo], wifi routers [eero], and video doorbells and cameras [Ring and Blink]), for sale both online and in offline retailers in several regions. The space becomes more complex with dynamic product offering with new product launches and new marketplace launches. The Device Economics team leads in analyzing these complex marketplace dynamics to enable science-driven decision making in the Devices org. Device Economics achieves this by combining economic expertise with macroeconomic trends, and including both in scientific applications for use by internal analysts, to provide deep understanding of customer preferences. Our team’s outputs inform product development decisions, investments in future product categories, product pricing and promotion, and bundling across complementary product lines. We have achieved substantial impact on the Devices business, and will achieve more. Device Economics seeks an economist adept in measuring customer preferences and behaviors with proven capacity to innovate, scale measurement, and drive rigor. The candidate will work with Amazon Devices science leadership to refine science roadmaps, models, and priorities for innovation and simplification, and advance adoption of insights to influence important resource allocation and prioritization decisions. Effective communication skills (verbal and written) are required to ensure success of this collaboration. The candidate must be passionate about advancing science for business and customer impact. We are open to hiring candidates to work out of one of the following locations: Arlington, VA, USA | Seattle, WA, USA
US, TX, Austin
Passionate about helping customers simplify and accelerate their workloads on AWS? Are you fascinated by the power of Large Language Models (LLM), and applying ML and AI to solve complex challenges within one of Amazon's most significant businesses. Come join the AWS Marketplace team and help us build the future of partnerships and marketplace through ML. You will be a part of a team consisting of experienced Applied Scientists working on a new set of initiatives, building models and delivering them into the Amazon production ecosystem. Your efforts will build a robust ensemble of LLM artifacts and ML systems that can achieve high precision and recall, and scale to new marketplaces and languages. This problem is challenging due to sheer scale (billions of dollars of AWS revenue impact), diversity (hundreds of AWS services) and multitude of input sources (thousands of Partners and millions of Partner activity). We are looking for an experienced Scientist who can develop best in class solutions. Your primary customers are AWS customers and AWS Partners who would thank you for accelerating their migration to the AWS cloud across countries and industries. Inclusive Team Culture Our team is intentional about attracting, developing, and retaining amazing talent from diverse backgrounds. We’re looking for a new teammate who is enthusiastic, empathetic, curious, motivated, reliable, and able to work effectively with a diverse team of peers; someone who will help us amplify the positive & inclusive team culture we’ve been building. 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 we 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 We understand that sometimes you need to work from home. Outside of quarantine, our team is co-located across our New York and Seattle offices. We work from home as needed for doctors appointments, to take our kids to school, pick them up, and do the things that can’t be done from the office. Mentorship & Career Growth We are dedicated to supporting new team members. Our team has a broad mix of experience levels and Amazon tenures, and we’re building an environment that celebrates knowledge sharing and mentorship. You'll have an opportunity to learn from people with and without engineering and science backgrounds through one-on-one mentoring, and helpful code/design reviews. As a Senior Applied Scientist, you'll actively mentor others on the team on the art of what's possible with Machine Learning. Key job responsibilities The ideal Applied Scientist candidate has deep expertise in one or several of the following fields: Web search, Applied/Theoretical Machine Learning, Large Language Models, Deep Neural Networks, Classification Systems, Clustering, Label Propagation, Natural Language Processing, Computer Vision, Active learning, and Artificial Intelligence. S/he has a strong publication record at top relevant academic venues and experience in launching products/features in the industry. Do you want the excitement of experimenting with cutting edge Large Language Models (LLMs), machine learning, natural language processing, computer vision, and active learning models to solve real world problems at scale? Imagine experimenting with LLMs, with Deep Neural Networks as your daily job and imagine using your model outputs to affect the adoption of AWS cloud at scale through Partners. Imagine doing research inside of an Amazon team that is always looking to deploy creative solutions to real world problems in Cloud migration. Our scientists continue to publish, teach, and engage with the academic community, in addition to utilizing our working backwards method to enrich the way we live and work. About the team The AWS Partner Organization (APO) supports tens of thousands of consulting and technology partners who in turn serve AWS customers across nearly every industry, segment, and geography. The APO Engineering team is driven by the mission to provide best partner experience worldwide and create a better future for our customers and communities through a culture of Customer obsession, innovation and a relentless pursuit of excellence. Our team is responsible for both internal and external support for Partner Sales, the APN, and other key elements that drive the AWS partner engagement. Our commitment is to serve three primary stakeholder groups: the partners who collaborate with us to develop, promote, and sell AWS, the customers who rely on AWS services, and our internal users responsible for fostering AWS sales and partner-based adoption. This position is a critical enabler driving intelligence and science roadmaps for this entire organization. We are open to hiring candidates to work out of one of the following locations: Austin, TX, USA | Denver, CO, USA | New York City, NY, USA | Seattle, WA, USA
US, MA, North Reading
Working at Amazon Robotics Are 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, collaborative 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 imagine 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. Position Overview The Amazon Robotics (AR) Software Research and Science team builds and runs simulation experiments and delivers analyses that are central to understanding the performance of the entire AR system. This includes operational and software scaling characteristics, bottlenecks, and robustness to “chaos monkey” stresses -- we inform critical engineering and business decisions about Amazon’s approach to robotic fulfillment. We are seeking an enthusiastic Data Scientist to design and implement state-of-the-art solutions for never-before-solved problems. The DS will collaborate closely with other research and robotics experts to design and run experiments, research new algorithms, and find new ways to improve Amazon Robotics analytics to optimize the Customer experience. They will partner with technology and product leaders to solve business problems using scientific approaches. They will build new tools and invent business insights that surprise and delight our customers. They will work to quantify system performance at scale, and to expand the breadth and depth of our analysis to increase the ability of software components and warehouse processes. They will work to evolve our library of key performance indicators and construct experiments that efficiently root cause emergent behaviors. They will engage with software development teams and warehouse design engineers to drive the evolution of the AR system, as well as the simulation engine that supports our work. Inclusive Team Culture Here at Amazon, we embrace our differences. We are committed to furthering our culture of inclusion. We have 12 affinity groups (employee resource groups) with more than 87,000 employees across hundreds of chapters around the world. 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 reminds team members to seek diverse perspectives, learn and be curious, and earn trust. Flexibility It isn’t about which 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 offer flexibility and encourage you to find your own balance between your work and personal lives. Mentorship & Career Growth We care about your career growth too. Whether your goals are to explore new technologies, take on bigger opportunities, or get to the next level, we'll help you get there. Our business is growing fast and our people will grow with it. A day in the life Amazon offers a full range of benefits that support you and eligible family members, including domestic partners and their children. Benefits can vary by location, the number of regularly scheduled hours you work, length of employment, and job status such as seasonal or temporary employment. The benefits that generally apply to regular, full-time employees include: 1. Medical, Dental, and Vision Coverage 2. Maternity and Parental Leave Options 3. Paid Time Off (PTO) 4. 401(k) Plan If you are not sure that every qualification on the list above describes you exactly, we'd still love to hear from you! At Amazon, we value people with unique backgrounds, experiences, and skillsets. If you’re passionate about this role and want to make an impact on a global scale, please apply! A day in the life Amazon offers a full range of benefits that support you and eligible family members, including domestic partners and their children. Benefits can vary by location, the number of regularly scheduled hours you work, length of employment, and job status such as seasonal or temporary employment. The benefits that generally apply to regular, full-time employees include: 1. Medical, Dental, and Vision Coverage 2. Maternity and Parental Leave Options 3. Paid Time Off (PTO) 4. 401(k) Plan If you are not sure that every qualification on the list above describes you exactly, we'd still love to hear from you! At Amazon, we value people with unique backgrounds, experiences, and skillsets. If you’re passionate about this role and want to make an impact on a global scale, please apply! We are open to hiring candidates to work out of one of the following locations: North Reading, MA, USA
US, NY, New York
We are looking for a motivated and experienced Data Scientist with experience in Machine Learning (ML), Artificial Intelligence (AI), Big Data, and Service Oriented Architecture with deep understanding in advertising businesses, to be part of a team of talented scientists and engineers to innovate, iterate, and solve real world problem with cutting-edge AWS technologies. In this role, you will take a leading role in defining the problem, innovating the ML/AI solutions, and information the tech roadmap. You will join a cross-functional, fun-loving team, working closely with scientists and engineers on a daily basis. You will innovate on behalf of our customers by prototyping, delivering functional proofs of concept (POCs), and partnering with our engineers to productize and scale successful POCs. If you are passionate about creating the future, come join us as we have fun, and make history. Key job responsibilities - Define and execute a research & development roadmap that drives data-informed decision making for marketers and advertisers - Establish and drive data hygiene best practices to ensure coherence and integrity of data feeding into production ML/AI solutions - Collaborate with colleagues across science and engineering disciplines for fast turnaround proof-of-concept prototyping at scale - Partner with product managers and stakeholders to define forward-looking product visions and prospective business use cases - Drive and lead of culture of data-driven innovations within and outside across Amazon Ads Marketing orgs About the team Marketing Decision Science provides science products to enable Amazon Ads Marketing to deliver relevant and compelling guidance across marketing channels to prospective and active advertisers for success on Amazon. We own the product, technology and deployment roadmap for AI- and analytics-powered products across Amazon Ads Marketing. We analyze the needs, experiences, and behaviors of Amazon advertisers at petabytes scale, to deliver the right marketing communications to the right advertiser at the right team to help them make the data-informed advertising decisions. Our science-based products enable applications and synergies across Ads organization, spanning marketing, product, and sales use cases. We are open to hiring candidates to work out of one of the following locations: New York, NY, USA
DE, Berlin
AWS AI is looking for passionate, talented, and inventive Applied Scientists with a strong machine learning background to help build industry-leading Conversational AI Systems. Our mission is to provide a delightful experience to Amazon’s customers by pushing the envelope in Natural Language Understanding (NLU), Dialog Systems including Generative AI with Large Language Models (LLMs) and Applied 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 that make use language technology. You will gain hands on experience with Amazon’s heterogeneous text, structured data sources, and large-scale computing resources to accelerate advances in language understanding. We are hiring in all areas of human language technology and code generation. We are open to hiring candidates to work out of one of the following locations: Berlin, DEU
US, VA, Arlington
Amazon launched the Generative AI Innovation Center (GenAIIC) in Jun 2023 to help AWS customers accelerate the use of Generative AI to solve business and operational problems and promote innovation in their organization (https://press.aboutamazon.com/2023/6/aws-announces-generative-ai-innovation-center). GenAIIC provides opportunities to innovate in a fast-paced organization that contributes to game-changing projects and technologies that get deployed on devices and in the cloud. As an Applied Science Manager in GenAIIC, you'll partner with technology and business teams to build new GenAI solutions that delight our customers. You will be responsible for directing a team of data/research/applied scientists, deep learning architects, and ML engineers to build generative AI models and pipelines, and deliver state-of-the-art solutions to customer’s business and mission problems. Your team will be working with terabytes of text, images, and other types of data to address real-world problems. The successful candidate will possess both technical and customer-facing skills that will allow you to be the technical “face” of AWS within our solution providers’ ecosystem/environment as well as directly to end customers. You will be able to drive discussions with senior technical and management personnel within customers and partners, as well as the technical background that enables them to interact with and give guidance to data/research/applied scientists and software developers. The ideal candidate will also have a demonstrated ability to think strategically about business, product, and technical issues. Finally, and of critical importance, the candidate will be an excellent technical team manager, someone who knows how to hire, develop, and retain high quality technical talent. About the team About AWS Diverse Experiences AWS values diverse experiences. Even if you do not meet all of the preferred qualifications and skills listed in the job description, we encourage candidates to apply. If your career is just starting, hasn’t followed a traditional path, or includes alternative experiences, don’t let it stop you from applying. Why AWS? Amazon Web Services (AWS) is the world’s most comprehensive and broadly adopted cloud platform. We pioneered cloud computing and never stopped innovating — that’s why customers from the most successful startups to Global 500 companies trust our robust suite of products and services to power their businesses. Inclusive Team Culture Here at AWS, it’s in our nature to learn and be curious. Our employee-led affinity groups foster a culture of inclusion that empower us to be proud of our differences. Ongoing events and learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences, inspire us to never stop embracing our uniqueness. Mentorship & Career Growth We’re continuously raising our performance bar as we strive to become Earth’s Best Employer. That’s why you’ll find endless knowledge-sharing, mentorship and other career-advancing resources here to help you develop into a better-rounded professional. Work/Life Balance We value work-life harmony. Achieving success at work should never come at the expense of sacrifices at home, which is why we strive for flexibility as part of our working culture. When we feel supported in the workplace and at home, there’s nothing we can’t achieve in the cloud. Sales, Marketing and Global Services (SMGS) AWS Sales, Marketing, and Global Services (SMGS) is responsible for driving revenue, adoption, and growth from the largest and fastest growing small- and mid-market accounts to enterprise-level customers including public sector. The AWS Global Support team interacts with leading companies and believes that world-class support is critical to customer success. AWS Support also partners with a global list of customers that are building mission-critical applications on top of AWS services. We are open to hiring candidates to work out of one of the following locations: Arlington, VA, USA | Atlanta, GA, USA | Austin, TX, USA | Houston, TX, USA | New York, NY, USA | San Francisco, CA, USA | San Jose, CA, USA | Santa Clara, CA, USA | Seattle, WA, USA
US, VA, Arlington
Machine learning (ML) has been strategic to Amazon from the early years. We are pioneers in areas such as recommendation engines, product search, eCommerce fraud detection, and large-scale optimization of fulfillment center operations. The Generative AI team helps AWS customers accelerate the use of Generative AI to solve business and operational challenges and promote innovation in their organization. As an applied scientist, you are proficient in designing and developing advanced ML models to solve diverse challenges and opportunities. You will be working with terabytes of text, images, and other types of data to solve real-world problems. You'll design and run experiments, research new algorithms, and find new ways of optimizing risk, profitability, and customer experience. We’re looking for talented scientists capable of applying ML algorithms and cutting-edge deep learning (DL) and reinforcement learning approaches to areas such as drug discovery, customer segmentation, fraud prevention, capacity planning, predictive maintenance, pricing optimization, call center analytics, player pose estimation, event detection, and virtual assistant among others. AWS Sales, Marketing, and Global Services (SMGS) is responsible for driving revenue, adoption, and growth from the largest and fastest growing small- and mid-market accounts to enterprise-level customers including public sector. The AWS Global Support team interacts with leading companies and believes that world-class support is critical to customer success. AWS Support also partners with a global list of customers that are building mission-critical applications on top of AWS services. Key job responsibilities The primary responsibilities of this role are to: - Design, develop, and evaluate innovative ML models to solve diverse challenges and opportunities across industries - Interact with customer directly to understand their business problems, and help them with defining and implementing scalable Generative AI solutions to solve them - Work closely with account teams, research scientist teams, and product engineering teams to drive model implementations and new solution About the team About AWS Diverse Experiences AWS values diverse experiences. Even if you do not meet all of the preferred qualifications and skills listed in the job description, we encourage candidates to apply. If your career is just starting, hasn’t followed a traditional path, or includes alternative experiences, don’t let it stop you from applying. Why AWS? Amazon Web Services (AWS) is the world’s most comprehensive and broadly adopted cloud platform. We pioneered cloud computing and never stopped innovating — that’s why customers from the most successful startups to Global 500 companies trust our robust suite of products and services to power their businesses. Inclusive Team Culture Here at AWS, it’s in our nature to learn and be curious. Our employee-led affinity groups foster a culture of inclusion that empower us to be proud of our differences. Ongoing events and learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences, inspire us to never stop embracing our uniqueness. Mentorship & Career Growth We’re continuously raising our performance bar as we strive to become Earth’s Best Employer. That’s why you’ll find endless knowledge-sharing, mentorship and other career-advancing resources here to help you develop into a better-rounded professional. Work/Life Balance We value work-life harmony. Achieving success at work should never come at the expense of sacrifices at home, which is why we strive for flexibility as part of our working culture. When we feel supported in the workplace and at home, there’s nothing we can’t achieve in the cloud. We are open to hiring candidates to work out of one of the following locations: Arlington, VA, USA | Atlanta, GA, USA | Austin, TX, USA | Houston, TX, USA | New York, NJ, USA | New York, NY, USA | San Francisco, CA, USA | Santa Clara, CA, USA | Seattle, WA, USA
CN, Shanghai
亚马逊云科技上海人工智能实验室OpenSearch 研发团队正在招募应用科学实习生-多模态检索与生成方向实习生。OpenSearch是一个开源的搜索和数据分析套件, 它旨在为数据密集型应用构建解决方案,内置高性能、开发者友好的工具,并集成了强大的机器学习、数据处理功能,可以为客户提供灵活的数据探索、丰富和可视化功能,帮助客户从复杂的数据中发现有价值的信息。OpenSearch是现有AWS托管服务(AWS OpenSearch)的基础,OpenSearch核心团队负责维护OpenSearch代码库,他们的目标是使OpenSearch安全、高效、可扩展、可扩展并永远开源。 点击下方链接查看申请手册获得更多信息: https://amazonexteu.qualtrics.com/CP/File.php?F=F_55YI0e7rNdeoB6e Key job responsibilities 在这个实习期间,你将有机会: 1. 研究最新的搜索相关性人工智能算法。 2. 探索大模型技术在数据分析与可视化上的应用。 3. 了解主流搜索引擎Lucene的原理和应用。深入了解前沿自然语言处理技术和底层索引性能调优的结合。 4. 学习亚马逊云上的各种云服务。 5. 参与产品需求讨论,提出技术实现方案。 6. 与国内外杰出的开发团队紧密合作,学习代码开发和审查的流程。 We are open to hiring candidates to work out of one of the following locations: Shanghai, CHN