Neha Rungta's 2022 CAV keynote

A billion SMT queries a day

CAV keynote lecture by the director of applied science for AWS Identity explains how AWS is making the power of automated reasoning available to all customers.

At this year’s Computer-Aided Verification (CAV) conference — a leading automated-reasoning conference collocated with the Federated Logic Conferences (FLoC) — Amazon’s Neha Rungta delivered a keynote talk in which she suggested that innovations at Amazon have “ushered in the golden age of automated reasoning”. 

Amazon scientists and engineers are using automated reasoning to prove the correctness of critical internal systems and to help customers prove the security of their cloud infrastructures. Many of these innovations are being driven by powerful reasoning engines called SMT solvers.  

Satisfiability problems, or SAT, ask whether it’s possible to assign variables true/false values that satisfy a set of constraints. SMT, or satisfiability modulo theories, is a generalization of SAT to involve integers, real numbers, strings, or functions. It is a mainstay of formal methods — the use of automated reasoning to prove that a computer program will behave the way it’s supposed to.

The following is a condensed and edited version of Rungta’s talk. You can also read the accompanying invited paper.

Zelkova

At Amazon, we use automated reasoning to prove the correctness of internal systems and to provide services that allow customers to prove the correctness of their cloud systems. Today I am going to focus on a single but critical part of that work. I am going to show you how we help customers get their access controls right using an automated-reasoning engine called Zelkova. I want to show you the balancing act we do between science and engineering to make automated reasoning work at scale.

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

Zelkova takes as input an access control policy and a question about access control and returns a correct answer to the question. That sounds too good to be true: what’s the catch, you may ask?

The correctness of the answer depends on asking the right question. Our key innovation here is that, rather than require customers to ask the right questions, the way previous approaches did, we have AWS services ask Zelkova questions on behalf of customers.

For example, Amazon S3 Block Public Access asks Zelkova, “Does this S3 bucket policy grant public access?” AWS Identity and Access Management (IAM) Access Analyzer asks Zelkova, “Does this KMS key grant cross-account access?” It is easy for customers to determine the security of cloud resources by looking at the answers. This model — having AWS services ask the questions — allows us to democratize automated reasoning and make it usable by all AWS customers.

Under the hood, Zelkova translates the policy and question into an SMT query and calls a portfolio solver to get an answer, as in the figure below. A portfolio solver invokes multiple solvers in the backend — here, they include Z3, CVC4, cvc5, and a custom automaton solver — and returns the results from the solver that comes backs with an answer first, in a winner-take-all strategy. Leveraging the diversity of SMT solvers enables Zelkova to solve queries quickly — within a couple hundred milliseconds to tens of seconds.

Zelkova design.png
Zelkova is an automated-reasoning engine that helps customers make universal statements such as “There is no public access to my AWS resources”. It uses a "portfolio solver", which invokes multiple solvers in the backend — Z3, CVC4, cvc5, and so on — and returns the first answer to come back.

SMT solvers use clever algorithms and heuristics to solve problems that are computationally hard. The time it takes to solve a query depends on a wide variety of factors, including the solver configuration, the random seed picked during analysis, and the heuristics being used. The result is that two queries with small syntactic differences can have wildly different run times. Similarly, seemingly minor implementation changes in the solvers can lead to a large run-time variance.

Related content
Meet Amazon Science’s newest research area.

We turned to engineering best practices to even out the lack of predictability and monotonicity in the performance of SMT solvers. Before deploying a new version of the solver for Zelkova, we perform extensive offline testing and benchmarking.

SMT solving at cloud scale

We experienced some unexpected bumps when we wanted to upgrade CVC4 with its newer version, cvc5 (version 0.0.4). In the graph comparing the two solvers, we have approximately 15,000 SMT queries generated by Zelkova. We select a distribution of queries whose solution times range from 0.01 second to 30 seconds; after 30 seconds, the solver process is killed and a timeout reported.

Some queries that are not solved by CVC4 within the time bound are now being solved by cvc5, as is seen from the points aligned vertically at the right side of the graph. However, cvc5 times out on some queries that are solved by CVC4, as is seen from the points aligned horizontally at the top of the graph.

cvc5 0.0.4.png
Comparing the run times of queries solved by CVC4 and cvc5 (version 0.0.4).

The change in run times for SMT queries can have an impact on the customer experience. For example, in Amazon S3 Block Public Access, when analyzing a bucket policy, if the solver times out, it classifies the bucket as “public”.

Suppose that, with the previous solver version, there was a bucket marked “not public” based on the results of a query. Further suppose that, with the current solver version, if the same query times out, then the bucket is marked as “public”. This will lock down the bucket, and the intended users will not be able to access it. This is unexpected for the user, who made no configuration changes. Hence, we need to ensure that all queries that were previously getting solved within the max time bound are still getting solved.

cvc5 0.0.7.png
Comparing the run times of queries solved by CVC4 and cvc5 (version 0.0.7).

We dug into the root causes of the discrepancy, and it turned out that a rewrite rule had been disabled in cvc5. We worked with the cvc5 developers to get it re-enabled (in version 0.0.7), but the story doesn’t end there. It turns out that even with the fix, CVC4 was twice as fast as cvc5 on many easier problems, solving them in one second instead of two.

Run-time comparison.png
Run-time data that led us to add cvc5 to the Zelkova portfolio solver.

This slowdown was significant because Zelkova is called in the request path of security controls such as Amazon S3 Block Public Access. When a user attempts to attach a new access control policy to an S3 bucket or to update an existing one, a synchronous call is made to Zelkova and the corresponding portfolio solver to determine if the policy grants unrestricted public access or not. The bulk of the analysis time is spent on the SMT solvers, so doubling the analysis time for queries can potentially degrade the user experience. This is why we decided to add cvc5 to the Zelkova portfolio solver rather than replace CVC4 with it.

Democratizing automated reasoning

What does this mean for our customers? Instead of focusing on the technology, they can think about its value to them. We tell customers they can make universal statements about the security of their cloud infrastructure. A universal statement holds over the entire universe of possibilities, not just what we’ve tested or fuzzed or observed or thought about. Services such as Amazon S3 Block Public Access, IAM Access Analyzer, Amazon VPC Network Access Analyzer, and Amazon Inspector allow customers to make universal statements such as “there is no public access to my S3 bucket”.

High assurance with provable security
Neha Rungta and Andrew Gacek's talk at the AWS re:Inforce security conference.

I believe that these services would be useful to all our customers. To learn how to use them, watch the talk on high assurance with provable security that my colleague Andrew Gacek and I gave earlier this summer at the AWS re:Inforce security conference. Automated reasoning is transforming the landscape of cloud security, and its power is available to all AWS customers through a few clicks.

Related content

US, WA, Seattle
We are designing the future. If you are in quest of an iterative fast-paced environment, where you can drive innovation through scientific inquiry, and provide tangible benefit to hundreds of thousands of our associates worldwide, this is your opportunity. Come work on the Amazon Worldwide Fulfillment Design & Engineering Team! We are looking for an experienced and Research Scientist with background in Ergonomics and Industrial Human Factors, someone that is excited to work on complex real-world challenges for which a comprehensive scientific approach is necessary to drive solutions. Your investigations will define human factor / ergonomic thresholds resulting in design and implementation of safe and efficient workspaces and processes for our associates. Your role will entail assessment and design of manual material handling tasks throughout the entire Amazon network. You will identify fundamental questions pertaining to the human capabilities and tolerances in a myriad of work environments, and will initiate and lead studies that will drive decision making on an extreme scale. .You will provide definitive human factors/ ergonomics input and participate in design with every single design group in our network, including Amazon Robotics, Engineering R&D, and Operations Engineering. You will work closely with our Worldwide Health and Safety organization to gain feedback on designs and work tenaciously to continuously improve our associate’s experience. Key job responsibilities - Collaborating and designing work processes and workspaces that adhere to human factors/ ergonomics standards worldwide. - Producing comprehensive and assessments of workstations and processes covering biomechanical, physiological, and psychophysical demands. - Effectively communicate your design rationale to multiple engineering and operations entities. - Identifying gaps in current human factors standards and guidelines, and lead comprehensive studies to redefine “industry best practices” based on solid scientific foundations. - Continuously strive to gain in-depth knowledge of your profession, as well as branch out to learn about intersecting fields, such as robotics and mechatronics. - Travelling to our various sites to perform thorough assessments and gain in-depth operational feedback, approximately 25%-50% of the time. We are open to hiring candidates to work out of one of the following locations: Seattle, WA, USA
DE, BE, Berlin
Have you ever wondered how Amazon delivers timely and reliably hundreds of millions of packages to customer’s doorsteps? Are you passionate about data and mathematics, and hope to impact the experience of millions of customers? Are you obsessed with designing simple algorithmic solutions to very challenging problems? If so, we look forward to hearing from you! Amazon Transportation Services is seeking Applied (or Research) Scientists. As a key member of the central Research Science Team of ATS operations, these persons will be responsible for designing algorithmic solutions based on data and mathematics for optimizing the middle-mile Amazon transportation network. The job is opened in the EU Headquarters in Luxembourg (alternatively: Barcelona, Berlin or London), designed to maximize interaction with the team and stakeholders, but we will consider applicants with remote work requirements as well. Basic qualifications * PhD in Operations Research, Machine Learning, Statistics, Applied Mathematics, Computer Science or other field related to algorithms and data (or equivalent experience). * Excellent written and verbal communication skills. * Experience with some programming language (Java/python/C++) * Research experience in one or more: *Combinatorial optimization problems (e.g., scheduling, vehicle routing, facility location). *Continuous optimization problems (e.g., linear programming, convex programming, non-convex programming). *Predictive analytics (e.g., forecasting, time-series, neural networks) *Prescriptive analytics (e.g., stochastic optimization, bandits, reinforcement learning). Preferred qualifications * Experience from working in a fast-paced applied research environment. * Ability to handle ambiguity. * Top tier publications pertinent to the field of study. Amazon is an equal opportunities employer. We believe passionately that employing a diverse workforce is central to our success. We make recruiting decisions based on your experience and skills. We value your passion to discover, invent, simplify and build. Protecting your privacy and the security of your data is a longstanding top priority for Amazon. Please consult our Privacy Notice (https://www.amazon.jobs/en/privacy_page) to know more about how we collect, use and transfer the personal data of our candidates. Key job responsibilities Solve complex optimization and machine learning problems using scalable algorithmic techniques. Design and develop efficient research prototypes that address real-world problems in the middle-mile operations of Amazon. Lead complex time-bound, long-term as well as ad-hoc analyses to assist decision making. Communicate to leadership results from business analysis, strategies and tactics. A day in the life You will be brainstorming algorithmic approaches with team-mates to solve challenging problems for the middle-mile operations of Amazon. You will be developing and testing prototype solutions with above algorithmic techniques. You will be scavenging information from the sea of Amazon data to improve these solutions. You will be meeting with other scientists, engineers, stakeholders and customers to enhance the solutions and get them adopted. About the team The Science and Tech team of ATS EU is looking for candidates who are looking to impact the world with their mathematical and data-driven skills. ATS stands for Amazon Transportation Service, we are the middle-mile planners: we carry the packages from the warehouses to the cities in a limited amount of time to enable the “Amazon experience”. As the core research team, we grow with ATS business to support decision making in an increasingly complex ecosystem of a data-driven supply chain and e-commerce giant. We schedule more than 1 million trucks with Amazon shipments annually; our algorithms are key to reducing CO2 emissions, protecting sites from being overwhelmed during peak days, and ensuring a smile on Amazon’s customer lips. Our mathematical algorithms provide confidence in leadership to invest in programs of several hundreds millions euros every year. Above all, we are having fun solving real-world problems, in real-world speed, while failing & learning along the way. We use modular algorithmic designs in the domain of combinatorial optimization, solving complicated generalizations of core OR problems with the right level of decomposition, employing parallelization and approximation algorithms. We use deep learning, bandits, and reinforcement learning to put data into the loop of decision making. We like to learn new techniques to surprise business stakeholders by making possible what they cannot anticipate. For this reason, we work closely with Amazon scholars and experts from Academic institutions. We code our prototypes to be production-ready We prefer provably optimal solutions than heuristics, though we settle for heuristics when performance dictates it. Overall, we appreciate the value of correct modeling. We are open to hiring candidates to work out of one of the following locations: Berlin, BE, DEU
US, WA, Seattle
Have you ever wanted to solve a mystery or be part of solving a case? Are you fascinated by detective stories or crime shows on TV? Do you love to catch bad actors, build ML models and solve complex problems. If so, working on the Loss Prevention Tech team as a Sr Applied Scientist is the place for you! We detect theft, fraud and organized crime happening across our global supply chain and operations for millions of items, for hundreds of product lines worth billions of dollars of inventory world-wide. We foster new game-changing ideas, creating ever more intelligent and self-learning systems to maximize the cost savings of Amazon's inventory losses. The primary role of a Sr Applied Scientist within Amazon is to address business challenges through building a compelling case, and using data to influence change across the organization. This individual will be given responsibility on their first day to own those business challenges and the autonomy to think strategically and make data driven decisions. Decisions and tools made in this role will have significant impact to the customer experience, as it will have a major impact on all the fraud investigations happening across Amazon operations. Ideal candidates will be a high potential, strategic and analytic graduate with a PhD in ( Research, Statistics, Engineering, and Supply Chain) ready for challenging opportunities in the core of our world class operations space. Great candidates have a history of building fraud detections, detecting organized crime and the ability to use data and research to make changes. This individual will need to be able to work with a team, but also be comfortable making decisions independently, in what is often times an ambiguous environment. Key job responsibilities - Own KPIs that measure fraud management performance and efficiencies. - Detect and automate theft, fraud MOs - Detect organized crime rings and bad actor clusters - Build data or computer vision based ML models - Perform end to end evaluation of operational defects, system gaps, and scaling challenges (both system and operational). - Contribute to the overall fraud management and product development strategies. - Present key learnings and vision to stakeholders and leadership. - Integrate ML detection models via software applications About the team We believe that building a culture that is welcoming and inclusive is integral to people doing their best work and is essential to what we can achieve as a company. We actively recruit people from diverse backgrounds to build a supportive and inclusive workplace. Our team puts a high value on work-live 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 are open to hiring candidates to work out of one of the following locations: Seattle, WA, USA
US, WA, Seattle
Are you interested in working with top talent in Optimization, Operations Research and Supply Chain to help Amazon to efficiently match our Devices with worldwide customers? We have challenging problems and need your innovative solutions to make tremendous financial impacts! The Amazon Devices Science team is looking for a Research Scientist with background in Operations Research, Optimization, Supply Chain and/or Simulation to support science efforts to integrate across inventory management functionalities. Our team is responsible for science models (both deterministic and stochastic) that power world-wide inventory allocation for Amazon Devices business that includes Echo, Kindle, Fire Tablets, Amazon TVs, Amazon Fire TV sticks, Ring, and other smart home devices. We formulate and solve challenging large-scale financially-based optimization problems which ingest demand forecasts and produce optimal procurement, production, distribution, and inventory management plans. In addition, we also work closely with demand forecasting, material procurement, production planning, finance, and logistics teams to co-optimize the inventory management and supply chain for Amazon Devices given operational constraints. Key job responsibilities The successful candidate will be a self-starter, comfortable with ambiguity, with strong attention to detail, and ability to work in a fast-paced and ever-changing environment and a desire to help shape the overall business. Job responsibilities include: - Design and develop advanced mathematical, simulation, and optimization models and apply them to define strategic and tactical needs and drive appropriate business and technical solutions in the areas of inventory management and distribution, network flow, supply chain optimization, and demand planning - Apply mathematical optimization techniques (linear, quadratic, SOCP, robust, stochastic, dynamic, mixed-integer programming, network flows, nonlinear, nonconvex programming) and algorithms to design optimal or near optimal solution methodologies to be used by in-house decision support tools and software - Research, prototype and experiment with these models by using modeling languages such as Python; participate in the production level deployment - Create, enhance, and maintain technical documentation, and present to other Scientists, Product, and Engineering teams - Support project plans from a scientific perspective by managing product features, technical risks, milestones and launch plans - Influence organization's long-term roadmap and resourcing, and onboard new technologies onto the Science team's toolbox We are open to hiring candidates to work out of one of the following locations: Seattle, WA, USA
US, VA, Arlington
Amazon's Global Hiring Science team ensures we match the right people to the right roles, quickly, fairly, and with an amazing experience. To achieve this, we design, implement, and optimize hiring systems experienced by millions of candidates annually. We work in a data-rich, global environment solving complex problems with deep thought, large-sample research, and advanced quantitative methods to deliver practical solutions that make all aspects of hiring more fair, accurate, efficient, and enjoyable. Key job responsibilities We’re developing a new approach to hiring via a multi-year initiative to evolve how we define jobs and candidate qualifications, how we recommend and promote jobs to candidates, and how we help candidates find the roles in which they will be most successful, satisfied, and engaged. To accomplish this, we’ve created a specialized team of experienced industrial-organizational psychologists, applied scientists, engineers, and UX designers. We're looking for an experienced senior research science manager to lead a team of scientists working on this initiative who is equal parts researcher, consultant, and thought leader, with strong expertise in psychometrics, research methodology, and data analysis. In this role, you will collaborate with cross-functional teams to drive research, development, and implementation of innovative hiring technology, evaluation tools, approaches, and methods. The impact of your work will be global and applicable across all of Amazon’s businesses (e.g., AWS, Retail, Logistics, Kindle, and Business Development) and roles (e.g., hourly, technical, professional). A day in the life What you’ll do: • Manage the development and execution of large-scale, highly-visible global research, validation, and hiring optimization projects. • Solve complex, ambiguous measurement, legal defensibility, and experimental design challenges. • Lead the development and research of new content and approaches to assessment (e.g., high fidelity simulation, interactive item types, constructed response). • Apply the scientific method to answer novel research questions. • Influence executive project sponsors and stakeholders across the company. • Drive effective teamwork, communication, collaboration, and commitment across cross-functional groups with competing priorities. • Oversee complex statistical/quantitative analyses with large datasets. About the team We are a team of scientists, and this is an important part of our professional identities. We take our continuing education as well as our contributions to the continuing education of others seriously. To this end, we regularly look for opportunities to engage in reading groups with our peers, present at internal and external conferences, publish our work, and engage in other professional activities in support of our or others development. Learn more about being a scientist at Amazon: https://www.amazon.science. We embrace differences and are committed to furthering our culture of inclusion. 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. We are open to hiring candidates to work out of one of the following locations: Arlington, VA, USA | Seattle, WA, USA
US, WA, Seattle
The Bad Actor Disincentives (BAD) team is responsible for removing the incentive for Bad Actors while accurately and fairly paying millions of third-party sellers along with disrupting the bad actor flywheel and change the economics of abuse within our store. The team works to ensure that bad actors cannot profit from using our services to abuse customers, selling partners and Amazon. While we obsess over customers, we specialize in obsessing over bad actors to identify their friction points and multiply them exponentially in ways that don’t impact good sellers. Our vision is to ensure Bad Actors do not receive a dollar from selling on Amazon and abusing our policies. If we successfully achieve our vision, then Bad Actors will stop committing misconduct on Amazon. This role requires outstanding technical skills, a deep understanding of machine learning approaches, and a passion for melding ML with great user experience/design. You must have a demonstrated ability for optimizing, developing, launching, and maintaining large-scale production systems. As a key member of the team, you will oversee all aspects of the software lifecycle: design, experimentation, implementation, and testing. You should be willing to dive deep when needed, move rapidly with a bias for action, and get things done. You should have an entrepreneurial spirit, love autonomy, know how to deliver, and long for the opportunity to build pioneering solutions to challenging problems. This role will demand resourcefulness and willingness to learn on both the technical and business side. The challenges we take on can involve a mix of large-scale distributed systems, big data technologies, machine learning science, and require a keen sense of customer obsession and long-term strategic thinking. Key job responsibilities You're a former engineer or scientist who can see the bigger picture. While your career is full of individual wins, it is now more fulfilling when your team is able to build, deliver, and impress. You enjoy leading and mentoring others, and want to work on projects that require innovative and creative thinking alongside deep technical problem solving. You challenge yourself and others to constantly come up with better solutions, and can deliver on a technical roadmap that serves our customers and the business optimally. You communicate clearly, and hold yourself and your team to a high bar. We are open to hiring candidates to work out of one of the following locations: Seattle, WA, USA
US, WA, Seattle
Are you passionate about solving unique customer-facing problem in the Amazon scale? Are you excited by developing and productizing machine learning, deep learning algorithms and leverage tons of Amazon data to learn and infer customer shopping patterns? Do you enjoy working with a diversity of engineers, machine learning scientists, product managers and user-experience designers? If so, you have found the right match! Fashion is extremely fast-moving, visual, subjective, and it presents numerous unique problem domains such as product recommendations, product discovery and evaluation. The vision for Amazon Fashion is to make Amazon the number one online shopping destination for Fashion customers by providing large selections, inspiring and accurate recommendations and customer experience. The mission of Fit science team as part of Fashion Tech is to innovate and develop scalable ML solutions to provide personalized fit and size recommendation when Amazon Fashion customers evaluate apparels or shoes online. The team is hiring Applied Scientist who has a solid background in applied Machine Learning and a proven record of solving customer-facing problems via scalable ML solutions, and is motivated to grow professionally as an ML scientist. Key job responsibilities Tackle ambiguous problems in Machine Learning and drive full life-cycle Machine Learning projects. Build machine learning models, perform proof-of-concept, experiment, optimize, and deploy your models into production. Run A/B experiments, gather data, and perform statistical tests. Establish scalable, efficient, automated processes for large-scale data mining, machine-learning model development, model validation and serving. Work closely with software engineers and product managers to assist in productizing your ML models. We are open to hiring candidates to work out of one of the following locations: San Diego, CA, USA | San Francisco, CA, USA | Santa Monica, CA, USA | Seattle, WA, USA | Sunnyvale, CA, USA
US, NY, New York
Amazon Advertising is one of Amazon's fastest growing and most profitable businesses, responsible for defining and delivering a collection of advertising products that drive discovery and sales. As a core product offering within our advertising portfolio, Sponsored Products (SP) helps merchants, retail vendors, and brand owners succeed via native advertising, which grows incremental sales of their products sold through Amazon. We deliver billions of ad impressions and millions of clicks and break fresh ground in product and technical innovations every day! The Books Advertising team owns the worldwide advertising business for books, including advertiser and shopper experiences. They develop long-term vision and drive improvements for category relevance, auction dynamics, and ad serving. Additionally, they drive advertiser engagement, represent advertisers' voice, and provide operational support for our programs. This means the team owns all book-specific experiences for Sponsored Products, Sponsored Brands, Sponsored Display, Lock Screen Advertising, the Ads Console, and the Public API. As an Senior Applied Scientist on this team, you will: - Drive end-to-end Machine Learning projects that have a high degree of ambiguity, scale, complexity. - Perform hands-on analysis and modeling of enormous data sets to develop insights that increase traffic monetization and merchandise sales, without compromising the shopper experience. - Build machine learning models, perform proof-of-concept, experiment, optimize, and deploy your models into production; work closely with software engineers to assist in productionizing your ML models. - Run A/B experiments, gather data, and perform statistical analysis. - Establish scalable, efficient, automated processes for large-scale data analysis, machine-learning model development, model validation and serving. - Research new and innovative machine learning approaches. - Recruit Applied Scientists to the team and provide mentorship. Why you will love this opportunity: Amazon is investing heavily in building a world-class advertising business. This team defines and delivers a collection of advertising products that drive discovery and sales. Our solutions generate billions in revenue and drive long-term growth for Amazon’s Retail and Marketplace businesses. We deliver billions of ad impressions, millions of clicks daily, and break fresh ground to create world-class products. We are a highly motivated, collaborative, and fun-loving team with an entrepreneurial spirit - with a broad mandate to experiment and innovate. Impact and Career Growth: You will invent new experiences and influence customer-facing shopping experiences to help suppliers grow their retail business and the auction dynamics that leverage native advertising; this is your opportunity to work within the fastest-growing businesses across all of Amazon! Define a long-term science vision for our advertising business, driven from our customers' needs, translating that direction into specific plans for research and applied scientists, as well as engineering and product teams. This role combines science leadership, organizational ability, technical strength, product focus, and business understanding. Team video https://youtu.be/zD_6Lzw8raE ** Candidates can be based within proximity of NYC, Seattle, Toronto, Arlington County/Virginia (HQ2), or Santa Monica ** We are open to hiring candidates to work out of one of the following locations: Arlington, VA, USA | New York, NY, USA | Santa Monica, CA, USA
US, WA, Seattle
Amazon Prime is looking for an ambitious Economist to help create econometric insights for world-wide Prime. Prime is Amazon's premiere membership program, with over 200M members world-wide. This role is at the center of many major company decisions that impact Amazon's customers. These decisions span a variety of industries, each reflecting the diversity of Prime benefits. These range from fast-free e-commerce shipping, digital content (e.g., exclusive streaming video, music, gaming, photos), and grocery offerings. Prime Science creates insights that power these decisions. As an economist in this role, you will create statistical tools that embed causal interpretations. You will utilize massive data, state-of-the-art scientific computing, econometrics (causal, counterfactual/structural, time-series forecasting, experimentation), and machine-learning, to do so. Some of the science you create will be publishable in internal or external scientific journals and conferences. You will work closely with a team of economists, applied scientists, data professionals (business analysts, business intelligence engineers), product managers, and software engineers. You will create insights from descriptive statistics, as well as from novel statistical and econometric models. You will create internal-to-Amazon-facing automated scientific data products to power company decisions. You will write strategic documents explaining how senior company leaders should utilize these insights to create sustainable value for customers. These leaders will often include the senior-most leaders at Amazon. The team is unique in its exposure to company-wide strategies as well as senior leadership. It operates at the cutting-edge of utilizing data, econometrics, artificial intelligence, and machine-learning to form business strategies. A successful candidate will have demonstrated a capacity for building, estimating, and defending statistical models (e.g., causal, counterfactual, time-series, machine-learning) using software such as R, Python, or STATA. They will have a willingness to learn and apply a broad set of statistical and computational techniques to supplement deep-training in one area of econometrics. For example, many applications on the team use structural econometrics, machine-learning, and time-series forecasting. They rely on building scalable production software, which involves a broad set of world-class software-building skills often learned on-the-job. As a consequence, already-obtained knowledge of SQL, machine learning, and large-scale scientific computing using distributed computing infrastructures such as Spark-Scala or PySpark would be a plus. Additionally, this candidate will show a track-record of delivering projects well and on-time, preferably in collaboration with other team members (e.g. co-authors). Candidates must have very strong writing and emotional intelligence skills (for collaborative teamwork, often with colleagues in different functional roles), a growth mindset, and a capacity for dealing with a high-level of ambiguity. Endowed with these traits and on-the-job-growth, the role will provide the opportunity to have a large strategic, world-wide impact on the customer experiences of Prime members. Amazon is committed to a diverse and inclusive workplace. Amazon is an equal opportunity employer and does not discriminate on the basis of race, national origin, gender, gender identity, sexual orientation, protected veteran status, disability, age, or other legally protected status. For individuals with disabilities who would like to request an accommodation, visit https://www.amazon.jobs/en/disability/us We are open to hiring candidates to work out of one of the following locations: Arlington, VA, USA | Chicago, IL, USA | Seattle, WA, USA
US, MA, North Reading
Are you excited about developing generative AI and foundation models to revolutionize automation, robotics and computer vision? Are you looking for opportunities to build and deploy them on real problems at truly vast scale? At Amazon Fulfillment Technologies and Robotics we are on a mission to build high-performance autonomous systems that perceive and act to further improve our world-class customer experience - at Amazon scale. We are looking for scientists, engineers and program managers for a variety of roles. The Research team at Amazon Robotics is seeking a passionate, hands-on Sr. Applied Scientist to help create the world’s first foundation model for a many-robot system. The focus of this position is how to predict the future state of our warehouses that feature a thousand or more mobile robots in constant motion making deliveries around the building. It includes designing, training, and deploying large-scale models using data from hundreds of warehouses under different operating conditions. This work spans from research such as alternative state representations of the many-robot system for training, to experimenting using simulation tools, to running large-scale A/B tests on robots in our facilities. Key job responsibilities * Research vision - Where should we be focusing our efforts * Research delivery - Proving/dis-proving strategies in offline data or in simulation * Production studies - Insights from production data or ad-hoc experimentation * Production implementation - Building key parts of deployed algorithms or models About the team You would join our multi-disciplinary science team that includes scientists with backgrounds in planning and scheduling, grasping and manipulation, machine learning, and operations research. We develop novel planning algorithms and machine learning methods and apply them to real-word robotic warehouses, including: - Planning and coordinating the paths of thousands of robots - Dynamic allocation and scheduling of tasks to thousands of robots - Learning how to adapt system behavior to varying operating conditions - Co-design of robotic logistics processes and the algorithms to optimize them Our team also serves as a hub to foster innovation and support scientists across Amazon Robotics. We also coordinate research engagements with academia, such as the Robotics section of the Amazon Research Awards. We are open to hiring candidates to work out of one of the following locations: North Reading, MA, USA | Westborough, MA, USA