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?

Conclusion

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, 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.
IN, TS, Hyderabad
Job summaryAre you excited about driving business growth for millions of sellers by applying Machine Learning? Do you thrive in a fast-moving, large-scale environment that values data-driven decision making and sound scientific practices? We are looking for experienced data scientists to build sophisticated decision making systems that help Amazon Marketplace Sellers to grow their businesses.Amazon Marketplace enables sellers to reach hundreds of millions of customers and provides sellers the tools and services needed to make e-commerce simple, efficient and successful. Our team builds the core intelligence, insights, and algorithms that power a range of products used by millions of sellers. We are tackling large-scale, challenging problems such as helping sellers to prioritise business tasks by bringing together petabytes of data from sources across Amazon.You will be proficient with creating value out of data by formulating questions, analysing vast amounts of data, and communicating insights effectively to audience of varied backgrounds. In addition, you'll contribute to online experiments, build machine learning pipelines and personalised data products.To know more about Amazon science, Please visit https://www.amazon.scienceKey job responsibilities· Collaborate with domain experts, formulate questions, gather, process and analyse petabytes of data to unearth reliable insights· Design & execute experiments and analyze experimental results· Communicate insights effectively to audience of a wide range of backgrounds· Formulate relevant prediction problems and solve them by developing machine learning models· Partner with data engineering teams to improve quality of data assets, metrics and insights· Leverage industry best practices to establish repeatable science practices, principles & processes
US, WA, Seattle
Job summaryAmazon Sub-Same-Day Supply Chain team is looking for an experienced and motivated Senior Data Scientist to generate data-driven insights influencing the long term SSD supply chain strategy, build the necessary predictive models, optimization algorithms and customer behavioral segments allowing us to discover and build the roadmap for SSD to enable operational efficiency and scale.Key job responsibilitiesWork with product managers, engineers, other scientists, and leadership to identify and prioritize complex problems.Translate business problems into specific analytical questions and form hypotheses that can be answered with available data using scientific methods or identify additional data needed in the master datasets to fill any gapsDesign, develop, and evaluate highly innovative statistics and ML modelsGuide and establish scalable, efficient, automated processes for large scale data analyses, model development, model validation and model implementationProactively seek to identify business opportunities and insights and provide solutions to shape key business processes and policies based on a broad and deep knowledge of Amazon data, industry best-practices, and work done by other teams.A day in the lifeIn this role, you will be a technical expert with significant scope and impact. You will work with Product Managers, Business Engineers, and other Scientists, to deeply understand SSDs current optimization strategy while benchmarking against industry best practices and standards to gain insights that will drive our roadmap. A successful Data Scientist will have extreme bias for action needed in a startup environment, with outstanding leadership skills, proven ability to build and manage medium-scale modeling projects, identify data requirements, build methodology and tools that are statistically grounded. It will be a person who enjoys diving deep into data, doing analysis, discovering root causes, and designing long-term scientific solutions. We are seeking someone who can thrive in a fast-paced, high-energy and fun work environment where we deliver value incrementally and frequently. We value highly technical people who know their subject matter deeply and are willing to learn new areas. We look for individuals who know how to deliver results and show a desire to develop themselves, their colleagues, and their career.About the teamAmazon's Sub-Same Day (SSD) delivery program is designed to get customers their items as fast as possible – currently in as quickly as five hours. With ultra-fast delivery becoming increasingly important, we are looking for an experienced Senior Data Scientist to help us benchmark against industry standards to uncover insights to improve and optimize the long term supply chain strategy for Amazons Sub-Same-Day business.
US, NY, New York
Job summaryJob 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, VA, Arlington
Job summaryAmazon is investing heavily in building a world class advertising business and we are responsible for defining and delivering a collection of self-service performance advertising products that drive discovery and sales. Our products are strategically important to our Retail and Marketplace businesses driving long term growth. We deliver billions of ad impressions and millions of clicks daily and are breaking fresh ground to create world-class products. We are highly motivated, collaborative and fun-loving with an entrepreneurial spirit and bias for action. With a broad mandate to experiment and innovate, we are growing at an unprecedented rate with a seemingly endless range of new opportunities.Sponsored Products helps merchants, retail vendors, and brand owners succeed via native advertising that grows incremental sales of their products sold through Amazon. The Sponsored Products Ad Marketplace organization optimizes the systems and ad placements to match advertiser demand with publisher supply using a combination of machine learning, big data analytics, ultra-low latency high-volume engineering systems, and quantitative product focus. Our goals are to help buyers discover new products they love, be the most efficient way for advertisers to meet their business objectives, and to build a major, sustainable business that helps Amazon continuously innovate on behalf of all customers.We are seeking a Sr. Applied Science Manager who has a solid background in applied Machine Learning and AI, deep passion for building data-driven products, ability to communicate data insights and scientific vision, and has a proven track record of leading both applied scientists and software engineers to execute complex projects and deliver business impacts.In this team, Machine Learning and Deep Learning technologies including Semantic Retrieval, Natural Language Processing (NLP), Information Extraction, Image Understanding, Learning to Rank are used to match shoppers' search queries to ads with per impression prediction models that run in real-time with tight latency budgets. Models are trained using self-supervised techniques, transfer learning, and supervised training using labeled datasets. Knowledge distillation and model compression techniques are used to optimize model performance for production serving.The Senior Manager role will lead science and engineering efforts in these areas for Amazon Search pages WW. The person in this role is responsible for: maintaining the consistent and long term reliability for the models and the delivery services that power them, managing diverse teams across multiple domains, and collaborating cross-functional with other senior decision makers. Our critical LPs for this role are Think Big, Are Right A lot, and Earns Trust. What is key is that the leader will need a dynamic mindset to build systems that are flexible and will scale.In this role, you will:· Lead a group of both applied scientists and software engineers to deliver machine-learning and AI solutions to production.· Advance team's engineering craftsmanship and drive continued scientific innovation as a thought leader and practitioner.· Develop science and engineering roadmap, run Sprint/quarter and 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 talents, provide technical and career development guidance to both scientists and engineers in the organization.Locations: Seattle, WA; New York, NY; Arlington, VA
US, WA, Seattle
Job summaryWorkforce Staffing (WFS) brings together the workforce powering Amazon’s ability to delight customers: the Amazon Associate. With over 1M hires, WFS supports sourcing, hiring, and developing the best talent to work in our fulfillment centers, sortation centers, delivery stations, shopping sites, Prime Air locations, and more.WFS' Funnel Science and Analytics team is looking for a Research Scientist. This individual will be responsible for conducting experiments and evaluating the impact of interventions when conducting experiments is not feasible. The perfect candidate will have the applied experience and the theoretical knowledge of policy evaluation and conducting field studies.Key job responsibilitiesAs a Research Scientist (RS), you will do causal inference, design studies and experiments, leverage data science workflows, build predictive models, conduct simulations, create visualizations, and influence science and analytics practice across the organization.Provide insights by analyzing historical data from databases (Redshift, SQL Server, Oracle DW, and Salesforce).Identify useful research avenues for increasing candidate conversion, test, and create well written documents to communicate to technical and non-technical audiences.About the teamFunnel Science and Analytics team finds ways to maximize the conversion and early retention of every candidate who wants to be an Amazon Associate. By focusing on our candidates, we improve candidate and business outcomes, and Amazon takes a step closer to being Earth’s Best Employer.
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, WA, Seattle
Job summaryAmazon's Weblab team enables experimentation at massive scale to help Amazon build better products for customers. A/B testing is in Amazon's DNA and we're at the core of how Amazon innovates on behalf of customers. We are seeking a skilled Applied Scientist to help us build the future of experimentation systems at Amazon.About you:You have an entrepreneurial spirit and want to make a big impact on Amazon and its customers. You are excited about cutting-edge research on unsupervised learning, graph algorithms, and causal inference in the intersection between Machine Learning, Statistics, and Econometrics. You enjoy building massive scale and high performance systems but also have a bias for delivering simple solutions to complex problems. You're looking for a career where you'll be able to build, to deliver, and to impress. You challenge yourself and others to come up with better solutions. You develop strong working relationships and thrive in a collaborative team environment.About us together:We're going to help Amazon make better long term decisions by designing and delivering A/B-testing systems for long-term experiments, and by using these systems to figure out how near term behavior impacts long term growth and profitability. Our work will inform some of the biggest decisions at Amazon. Along the way, we're going to face seemingly insurmountable challenges. We're going to argue about how to solve them, and we'll work together to find a solution that is better than each of the proposals we came in with. We'll make tough decisions, but we'll all understand why. We'll be the dream team.We have decades of combined experience on the team in many areas science and engineering so it's a great environment in which to learn and grow. A/B testing is one of the hottest areas of research and development in the world today and this is a chance to learn how it works in the company known for pioneering its use.
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.