Automated reasoning's scientific frontiers

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

Automated reasoning is the algorithmic search through the infinite set of theorems in mathematical logic. We can use automated reasoning to answer questions about what systems such as biological models and computer programs can and cannot do in the wild.

In the 1990s, AMD, IBM, Intel, and other companies invested in automated reasoning for circuit and microprocessor design, leading to today’s widely used and industry-standard hardware formal-verification tools (e.g., JasperGold). In the 2000s, automated reasoning expanded to niche software domains such as device drivers (e.g., Static Driver Verifier) or transportation systems (e.g., Prover technology). In the 2010s, we saw automated reasoning increasingly applied to our foundational computing infrastructure, such as cryptography, networking, storage, and virtualization.

Related content
Meet Amazon Science’s newest research area.

With recently launched cloud services such as IAM Access Analyzer and VPC Network Access Analyzer, automated reasoning is now beginning to change how computer systems built on top of the cloud are developed and operated.

All these applications of automated reasoning rest on a common foundation: automated and semi-automated mechanical theorem provers. ACL2, CVC5, HOL-light’s Meson_tac, MiniSat, and Vampire are a few examples, but there are many more we could name. They are all, in outline, working on the same problem: the search for proofs in mathematical logic.

Over the past 30 years, slowly but surely, a virtuous cycle has formed: automated reasoning in specific and critical application areas drives more investment in foundational tools, while improvements in the foundational tools drive further applications. Around and around.

SAT graph comparison.png
The propositional-satisfiability problem (a.k.a. SAT) is NP-complete, and in the case of unstructured decision graphs (left), the problem instances can be prohibitively time consuming to solve. But when the decision graphs have some inherent structure (right), automatic solvers can exploit that structure to find solutions efficiently.
Visualizations produced by Carsten Sinz, using his 3DVis visualization tool

The increasingly difficult benchmarks driving the development of these tools present new science opportunities. International competitions such as CASC, SAT-COMP, SMT-COMP, SV-COMP, and the Termination competition have accelerated this virtuous cycle. On the application side, with increasing power from the tools come new research opportunities in the design of customer-intuitive tools (such as models of cellular signaling pathways or Amazon's abstraction of control policies for cloud computing).

As an example of the virtuous cycle at work, consider the following graph, which shows the results for all of the winners of SAT-COMP from 2002 to 2021, compared apples-to-apples in a competition with the same hardware and same benchmarks:

Winners 2021.png

This graph plots the number of benchmarks that each solver can solve in 200 seconds, 400 seconds, etc. The higher the line, the more benchmarks the solver could solve. By looking at the plot we can see, for example, that the 2010 winner (cryptominisat) solved approximately 50 benchmarks within the allotted 1,000 seconds, whereas the 2021 winner (kissat) can solve nearly four times as many benchmarks in the same time, using the same hardware. Why did the tools get better? Because members of the scientific community pushing on the application submitted benchmarks to the competitions, which helped tool developers take the tools to new heights of performance and scale.

At Amazon we see the velocity of the virtuous cycle dramatically increasing. Our automated-reasoning tools are now called billions of times daily, with growth rates exceeding 100% year-over-year. For example, AWS customers now have access to automated-reasoning-based features such as IAM Access Analyzer, S3 Block Public Access, or VPC Reachability Analyzer. We also see Amazon development teams using tools such as Dafny, P, and SAW.

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

What’s most exciting to me as an automated-reasoning scientist is that our research area seems to be entering a golden era. I think we are beginning to witness a transformation in automated reasoning that is similar to what happened in virtualized computing as the cloud’s virtuous cycle spun up. As described in Werner Vogels’s 2019 re:Invent keynote, AWS’s EC2 team was driven by unprecedented customer adoption to reinvent its hypervisor, microprocessor, and networking stack, capturing significant improvements in security, cost, and team agility made possible by economies of scale.

There are parallels in automated reasoning today. Dramatic new infrastructure is needed for viable business reasons, putting a spotlight on research questions that were previously obscure and unsolved. Below I outline three examples of open research areas driven by the increasing scale of automated-reasoning tools and our underlying computing infrastructure.

Example: Distributed proof search

For over two decades the automated-reasoning scientific community has postulated that distributed-systems-based proof search could be faster than sequential proof search. But we didn’t have the economic scale to justify serious investigation of the question.

At Amazon, with our increased reliance on automated reasoning, we now have that kind of scale. For example, we sponsored the new cloud-based-tool tracks in several international competitions.

Compare the mallob-mono solver, the winner of SAT-COMP’s new cloud-solver track, to the single-microprocessor solvers:

2 Mallob-mono.png

Mallob-mono is now, by a wide margin, the most powerful SAT solver on the planet. And like the sequential solvers, the distributed solvers are improving.

As described in Kuhn’s seminal book <i>The Structure of Scientific Revolutions</i>, major perspective shifts like this tend to trigger scientific revolutions. The success of distributed proof search raises the possibility of similar revolutions. For example, we may need to re-evaluate our assumptions about when to use eager vs. lazy reduction techniques when converting between formalisms.

Related content
Rungta had a promising career with NASA, but decided the stars aligned for her at Amazon.

Here at Amazon, we recently reconsidered the PhD dissertation of University of California, Berkeley, professor Sanjit Seshia in light of mallob-mono and were able to quickly (in about 2,000 lines of Rust) develop a new eager-reduction-based solver that outperforms today’s leading lazy-reduction tools on the notoriously difficult SMT-COMP bcnscheduling and job_shop benchmarks. Here we are solving SAT problems that go beyond Booleans, to involve integers, real numbers, strings, or functions. We call this SAT modulo theories, or SMT.

In the graph below we compare the performance of leading lazy SMT solvers CVC5 and Z3 to a Seshia-style eager solver based on the SAT solvers Kissat and mallob-mono on those benchmarks:

Solver performance.png

We’ve published the code for our Seshia-style eager solver on GitHub.

There are many other open questions driven by distributed proof search. For example, is there an effective lookahead-solver strategy for SMT that would facilitate cube-and-conquer? Or as the Zoncolan service does when analyzing programs for security vulnerabilities, can we memoize intermediate lemmas in a cloud database and reuse them, rather than recomputing for each query? Can Monte Carlo tree search in the cloud on past proofs be used to synthesize more-effective proof search strategies?

Another example: Reasoning about distributed systems

Recent examples of formal reasoning within AWS at the level of distributed-protocol design include a proof of S3’s recently announced strong consistency and the protocol-level proof of secrecy in AWS's KMS service. The problem with these proofs is that they apply to the protocols that power the distributed services, not necessarily to the code running on the servers that use those protocols.

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

Here at Amazon, we believe that automated reasoning at the level of protocol design has the greatest long-term value when the investment cost is amortized and protected via continuous integration/continuous delivery (CI/CD) integrations with the code that implements the protocols. That is, the benefit of upfront effort is often seen later, when protocol compliance proofs fail on buggy changes to implementation source code. The code doesn’t make it to production until the developers have fixed it.

Again: major perspective shifts like those resulting from successful proofs about S3 and KMS could trigger a revolution, à la Kuhn. For years, we have had tools for reasoning about distributed systems, such as TLA+ and P. But with the success of the work with S3 and KMS, it’s now clear that protocol design should be a first-class concept for engineering, with tools that support it, proactively finding errors and proving properties.

These tools should also connect to the source code that speaks the protocols by (i) constructing specifications that can be proved with existing code-level tools and (ii) synthesizing implementation code in languages such as C, Go, Rust, or Java. The tools would facilitate integration into our CI/CD, code review, and ticketing systems, allowing service teams to (iii) synthesize “runtime monitors” to exploit enterprise-level operations strength by providing telemetry about the status of a service’s conformance to a proved protocol.

Final example: Automating regulatory compliance

At the recent Computer-Aided Verification (CAV ’21) workshop called Formal Approaches to Certifying Compliance (talks recorded and available), we heard from NIST, Coalfire, Collins Aerospace, DARPA, and Amazon about the use of automated reasoning to lower the cost and the time-to-market added by regulatory compliance.

Karthik Amrutesh of the AWS security assurance team reported that automated reasoning enabled a 91% reduction in the time it took for our third-party auditor to produce evidence for checking controls. For perhaps the first time in the more than 2,500-year history of mathematical logic, we see a business use case that exploits the difference between finding proofs and checking proofs. What's the difference? Finding is usually the hard part, the creative part, the part that requires sophisticated algorithms. Finding is usually undecidable or NP-complete, depending on the context.

Meanwhile, not only is checking proofs decidable in most cases, but it’s often linear in the size of the proof. To check proofs, compliance auditors can use well-understood and trusted small solvers such as HOL-light.

Using cloud-scale automation to find the proofs lowers cost. That lets the auditor offer its services for less, saving the customer money. It also reduces the latency of audits, a major pain point for developers looking to go to market quickly.

An audit check involves constraints on the form that valid text strings can take. The set of constraints is known as a string theory, and the imposition of that theory means that audit checks are SMT problems.

From the perspective of automated-reasoning science, it becomes important to build string theory solvers that can efficiently construct easily checkable proof artifacts. In the realm of propositional satisfiability — SAT problems — the DRAT proof checker is now the standard methodology for communicating proofs. But in SMT, no such standard exists. What would a general-purpose theory-agnostic SMT format and checker look like?


We've come a long way from days when automated reasoning was the exclusive domain of circuit designers or aerospace engineers. Success in these early domains kicked off a virtuous cycle for the makers of the theorem provers that power automated reasoning. With applications for mainstream applications such as cloud computing, the automated-reasoning virtuous cycle is now radically accelerating. After 2,500 years of mathematical-logic research and 70+ years of automated-reasoning science, we live in a heady time. With wider adoption of and investment in automated reasoning, we are seeing economies of scale where what we can do now would have been unimaginable even two or three years ago. Welcome to the future!

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

Research areas

Related content

US, CA, Palo Alto
We’re working to improve shopping on Amazon using the conversational capabilities of large language models, and are searching for pioneers who are passionate about technology, innovation, and customer experience, and are ready to make a lasting impact on the industry. You'll be working with talented scientists, engineers, and technical program managers (TPM) to innovate on behalf of our customers. If you're fired up about being part of a dynamic, driven team, then this is your moment to join us on this exciting journey!"?
US, CA, Santa Clara
AWS AI/ML is looking for world class scientists and engineers to join its AI Research and Education group working on foundation models, large-scale representation learning, and distributed learning methods and systems. At AWS AI/ML you will invent, implement, and deploy state of the art machine learning algorithms and systems. You will build prototypes and innovate on new representation learning solutions. 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. Large-scale foundation models have been the powerhouse in many of the recent advancements in computer vision, natural language processing, automatic speech recognition, recommendation systems, and time series modeling. Developing such models requires not only skillful modeling in individual modalities, but also understanding of how to synergistically combine them, and how to scale the modeling methods to learn with huge models and on large datasets. Join us to work as an integral part of a team that has diverse experiences in this space. We actively work on these areas: * Hardware-informed efficient model architecture, training objective and curriculum design * Distributed training, accelerated optimization methods * Continual learning, multi-task/meta learning * Reasoning, interactive learning, reinforcement learning * Robustness, privacy, model watermarking * Model compression, distillation, pruning, sparsification, quantization About Us 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. 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, WA, Bellevue
We are looking for detail-oriented, organized, and responsible individuals who are eager to learn how to work with large and complicated data sets. Knowledge of econometrics, (Bayesian) time series, macroeconomic, as well as basic familiarity with Matlab, R, or Python is necessary, and experience with SQL would be a plus. These are full-time positions at 40 hours per week, with compensation being awarded on an hourly basis. You will learn how to build data sets and perform applied econometric analysis at Internet speed collaborating with economists, scientists, and product managers. These skills will translate well into writing applied chapters in your dissertation and provide you with work experience that may help you with placement. Roughly 85% of previous cohorts have converted to full time economics employment at Amazon. If you are interested, please send your CV to our mailing list at
US, WA, Seattle
The AWS AI Labs team has a world-leading team of researchers and academics, and we are looking for world-class colleagues to join us and make the AI revolution happen. Our team of scientists have developed the algorithms and models that power AWS computer vision services such as Amazon Rekognition and Amazon Textract. As part of the team, we expect that you will develop innovative solutions to hard problems, and publish your findings at peer reviewed conferences and workshops. AWS is the world-leading provider of cloud services, has fostered the creation and growth of countless new businesses, and is a positive force for good. Our customers bring problems which will give Applied Scientists like you endless opportunities to see your research have a positive and immediate impact in the world. You will have the opportunity to partner with technology and business teams to solve real-world problems, have access to virtually endless data and computational resources, and to world-class engineers and developers that can help bring your ideas into the world. Our research themes include, but are not limited to: few-shot learning, transfer learning, unsupervised and semi-supervised methods, active learning and semi-automated data annotation, large scale image and video detection and recognition, face detection and recognition, OCR and scene text recognition, document understanding, 3D scene and layout understanding, and geometric computer vision. For this role, we are looking for scientist who have experience working in the intersection of vision and language. We are located in Seattle, Pasadena, Palo Alto (USA) and in Haifa and Tel Aviv (Israel).
US, WA, Seattle
Do you want to join an innovative team of scientists who use machine learning to help Amazon provide the best experience to our Selling Partners by automatically understanding and addressing their challenges, needs and opportunities? Do you want to build advanced algorithmic systems that are powered by state-of-art ML, such as Natural Language Processing, Large Language Models, Deep Learning, Computer Vision and Causal Modeling, to seamlessly engage with Sellers? Are you excited by the prospect of analyzing and modeling terabytes of data and creating cutting edge algorithms to solve real world problems? Do you like to build end-to-end business solutions and directly impact the profitability of the company and experience of our customers? Do you like to innovate and simplify? If yes, then you may be a great fit to join the Selling Partner Experience Science team. Key job responsibilities Use statistical and machine learning techniques to create the next generation of the tools that empower Amazon's Selling Partners to succeed. Design, develop and deploy highly innovative models to interact with Sellers and delight them with solutions. Work closely with teams of scientists and software engineers to drive real-time model implementations and deliver novel and highly impactful features. Establish scalable, efficient, automated processes for large scale data analyses, model development, model validation and model implementation. Research and implement novel machine learning and statistical approaches. Lead strategic initiatives to employ the most recent advances in ML in a fast-paced, experimental environment. Drive the vision and roadmap for how ML can continually improve Selling Partner experience. About the team Selling Partner Experience Science (SPeXSci) is a growing team of scientists, engineers and product leaders engaged in the research and development of the next generation of ML-driven technology to empower Amazon's Selling Partners to succeed. We draw from many science domains, from Natural Language Processing to Computer Vision to Optimization to Economics, to create solutions that seamlessly and automatically engage with Sellers, solve their problems, and help them grow. Focused on collaboration, innovation and strategic impact, we work closely with other science and technology teams, product and operations organizations, and with senior leadership, to transform the Selling Partner experience.
US, CA, Cupertino
We're looking for an Applied Scientist to help us secure Amazon's most critical data. In this role, you'll work closely with internal security teams to design and build AR-powered systems that protect our customers' data. You will build on top of existing formal verification tools developed by AWS and develop new methods to apply those tools at scale. You will need to be innovative, entrepreneurial, and adaptable. We move fast, experiment, iterate and then scale quickly, thoughtfully balancing speed and quality. 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. 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. Our senior members enjoy one-on-one mentoring and thorough, but kind, code reviews. We care about your career growth and strive to assign projects based on what will help each team member develop into a better-rounded engineer and enable them to take on more complex tasks in the future. Key job responsibilities Deeply understand AR techniques for analyzing programs and other systems, and keep up with emerging ideas from the research community. Engage with our customers to develop understanding of their needs. Propose and develop solutions that leverage symbolic reasoning services and concepts from programming languages, theorem proving, formal verification and constraint solving. Implement these solutions as services and work with others to deploy them at scale across Payments and Healthcare. Author papers and present your work internally and externally. Train new teammates, mentor others, participate in recruiting and interviewing, and participate in our tactical and strategic planning. About the team Our small team of applied scientists works within a larger security group, supporting thousands of engineers who are developing Amazon's payments and healthcare services. Security is a rich area for automated reasoning. Most other approaches are quite ad-hoc and take a lot of human effort. AR can help us to reason deliberately and systematically, and the dream of provable security is incredibly compelling. We are working to make this happen at scale. We partner closely with our larger security group and with other automated reasoning teams in AWS that develop core reasoning services.
GB, London
Are you excited about applying economic models and methods using large data sets to solve real world business problems? Then join the Economic Decision Science (EDS) team. EDS is an economic science team based in the EU Stores business. The teams goal is to optimize and automate business decision making in the EU business and beyond. An internship at Amazon is an opportunity to work with leading economic researchers on influencing needle-moving business decisions using incomparable datasets and tools. It is an opportunity for PhD students and recent PhD graduates in Economics or related fields. We are looking for detail-oriented, organized, and responsible individuals who are eager to learn how to work with large and complicated data sets. Knowledge of econometrics, as well as basic familiarity with Stata, R, or Python is necessary. Experience with SQL would be a plus. As an Economics Intern, you will be working in a fast-paced, cross-disciplinary team of researchers who are pioneers in the field. You will take on complex problems, and work on solutions that either leverage existing academic and industrial research, or utilize your own out-of-the-box pragmatic thinking. In addition to coming up with novel solutions and prototypes, you may even need to deliver these to production in customer facing products. Roughly 85% of previous intern cohorts have converted to full time economics employment at Amazon.
US, NY, New York
Search Thematic Ad Experience (STAX) team within Sponsored Products is looking for a leader to lead a team of talented applied scientists working on cutting-edge science to innovate on ad experiences for Amazon shoppers!. You will manage a team of scientists, engineers, and PMs to innovate new widgets on Amazon Search page to improve shopper experience using state-of-the-art NLP and computer vision models. You will be leading some industry first experiences that has the potential to revolutionize how shopping looks and feels like on Amazon, and e-commerce marketplaces in general. You will have the opportunity to design the vision on how ad experiences look on Amazon search page, and use the combination of advanced techniques and continuous experimentation to realize this vision. Your work will be core to Amazon’s advertising business. You will be a significant contributor in building the future of sponsored advertising, directly impacting the shopper experience for our hundreds of millions of shoppers worldwide, while delivering significant value for hundreds of thousands of advertisers across the purchase journey with ads on Amazon. Key job responsibilities * Be the technical leader in Machine Learning; lead efforts within the team, and collaborate and influence across the organization. * Be a critic, visionary, and execution leader. Invent and test new product ideas that are powered by science that addresses key product gaps or shopper needs. * Set, plan, and execute on a roadmap that strikes the optimal balance between short term delivery and long term exploration. You will influence what we invest in today and tomorrow. * Evangelize the team’s science innovation within the organization, company, and in key conferences (internal and external). * Be ruthless with prioritization. You will be managing a team which is highly sought after. But not all can be done. Have a deep understanding of the tradeoffs involved and be fierce in prioritizing. * Bring clarity, direction, and guidance to help teams navigate through unsolved problems with the goal to elevate the shopper experience. We work on ambiguous problems and the right approach is often unknown. You will bring your rich experience to help guide the team through these ambiguities, while working with product and engineering in crisply defining the science scope and opportunities. * Have strong product and business acumen to drive both shopper improvements and business outcomes. A day in the life * Lead a multidisciplinary team that embodies “customer obsessed science”: inventing brand new approaches to solve Amazon’s unique problems, and using those inventions in software that affects hundreds of millions of customers * Dive deep into our metrics, ongoing experiments to understand how and why they are benefitting our shoppers (or not) * Design, prototype and validate new widgets, techniques, and ideas. Take end-to-end ownership of moving from prototype to final implementation. * Be an advocate and expert for STAX science to leaders and stakeholders inside and outside advertising. About the team We are the Search thematic ads experience team within Sponsored products - a fast growing team of customer-obsessed engineers, technologists, product leaders, and scientists. We are focused on continuous exploration of contexts and creatives to drive value for both our customers and advertisers, through continuous innovation. We focus on new ads experiences globally to help shoppers make the most informed purchase decision while helping shortcut the time to discovery that shoppers are highly likely to engage with. We also harvest rich contextual and behavioral signals that are used to optimize our backend models to continually improve the shopper experience. We obsess about our customers and are continuously seeking opportunities to delight them.
US, CA, Palo Alto
Amazon is the 4th most popular site in the US. Our product search engine, one of the most heavily used services in the world, indexes billions of products and serves hundreds of millions of customers world-wide. We are working on a new initiative to transform our search engine into a shopping engine that assists customers with their shopping missions. We look at all aspects of search CX, query understanding, Ranking, Indexing and ask how we can make big step improvements by applying advanced Machine Learning (ML) and Deep Learning (DL) techniques. We’re seeking a thought leader to direct science initiatives for the Search Relevance and Ranking at Amazon. This person will also be a deep learning practitioner/thinker and guide the research in these three areas. They’ll also have the ability to drive cutting edge, product oriented research and should have a notable publication record. This intellectual thought leader will help enhance the science in addition to developing the thinking of our team. This leader will direct and shape the science philosophy, planning and strategy for the team, as we explore multi-modal, multi lingual search through the use of deep learning . We’re seeking an individual that can enhance the science thinking of our team: The org is made of 60+ applied scientists, (2 Principal scientists and 5 Senior ASMs). This person will lead and shape the science philosophy, planning and strategy for the team, as we push into Deep Learning to solve problems like cold start, discovery and personalization in the Search domain. Joining this team, you’ll experience the benefits of working in a dynamic, entrepreneurial environment, while leveraging the resources of Amazon [Earth's most customer-centric internet company]. We provide a highly customer-centric, team-oriented environment in our offices located in Palo Alto, California.
JP, 13, Tokyo
Our mission is to help every vendor drive the most significant impact selling on Amazon. Our team invent, test and launch some of the most innovative services, technology, processes for our global vendors. Our new AVS Professional Services (ProServe) team will go deep with our largest and most sophisticated vendor customers, combining elite client-service skills with cutting edge applied science techniques, backed up by Amazon’s 20+ years of experience in Japan. We start from the customer’s problem and work backwards to apply distinctive results that “only Amazon” can deliver. Amazon is looking for a talented and passionate Applied Science Manager to manage our growing team of Applied Scientists and Business Intelligence Engineers to build world class statistical and machine learning models to be delivered directly to our largest vendors, and working closely with the vendors' senior leaders. The Applied Science Manager will set the strategy for the services to invent, collaborating with the AVS business consultants team to determine customer needs and translating them to a science and development roadmap, and finally coordinating its execution through the team. In this position, you will be part of a larger team touching all areas of science-based development in the vendor domain, not limited to Japan-only products, but collaborating with worldwide science and business leaders. Our current projects touch on the areas of causal inference, reinforcement learning, representation learning, anomaly detection, NLP and forecasting. As the AVS ProServe Applied Science Manager, you will be empowered to expand your scope of influence, and use ProServe as an incubator for products that can be expanded to all Amazon vendors, worldwide. We place strong emphasis on talent growth. As the Applied Science Manager, you will be expected in actively growing future Amazon science leaders, and providing mentoring inside and outside of your team. Key job responsibilities The Applied Science Manager is accountable for: (1) Creating a vision, a strategy, and a roadmap tackling the most challenging business questions from our leading vendors, assess quantitatively their feasibility and entitlement, and scale their scope beyond the ProServe team. (2) Coordinate execution of the roadmap, through direct reports, consisting of scientists and business intelligence engineers. (3) Grow and manage a technical team, actively mentoring, developing, and promoting team members. (4) Work closely with other science managers, program/product managers, and business leadership worldwide to scope new areas of growth, creating new partnerships, and proposing new business initiatives. (5) Act as a technical supervisor, able to assess scientific direction, technical design documents, and steer development efforts to maximize project delivery.