Reference. Towards Verified Artificial Intelligence
Verified artificial intelligence (AI) is the goal of designing AI-based systems that have strong, ideally provable, assurances of correctness with respect to mathematically-specified requirements. This paper considers Verified AI from a formal methods perspective. We describe five challenges for achieving Verified AI, and five corresponding principles for addressing these challenges.
Cite
Cites 100 works (0 here)
External (100)
- Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI (2020)
- Formal Scenario-Based Testing of Autonomous Vehicles: From Simulation to the Real World (2020)
- Liability, Ethics, and Culture-Aware Behavior Specification using Rulebooks (2019)
- SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems (2019)
- VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems (2019)
- A formalization of robustness for deep neural networks (2019)
- Scenic: a language for scenario specification and scene generation (2019)
- Explaining AI Decisions Using Efficient Methods for Learning Sparse Boolean Formulae (2019)
- Stochastic assume-guarantee contracts for cyber-physical system design (2019)
- The seven tools of causal inference, with reflections on machine learning (2019)
- Introspective Environment Modeling (2019)
- A General Safety Framework for Learning-Based Control in Uncertain Robotic Systems (2018)
- Semantic Adversarial Deep Learning (2018)
- AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018)
- Making machine learning robust against adversarial inputs (2018)
- Differentiable Monte Carlo ray tracing through edge sampling (2018)
- Formal Specification for Deep Neural Networks (2018)
- A semantic loss function for deep learning with symbolic knowledge (2018)
- An overview of machine teaching (2018)
- Analysis of classifiers’ robustness to adversarial perturbations (2017)
- A theory of formal synthesis via inductive learning (2017)
- Safety Verification of Deep Neural Networks (2017)
- A Storm is Coming: A Modern Probabilistic Model Checker (2017)
- Compositional Falsification of Cyber-Physical Systems with Machine Learning Components (2017)
- Combining Model Checking and Runtime Verification for Safe Robotics (2017)
- SMC (2017)
- Logical Clustering and Learning for Time-Series Data (2017)
- Learning Task Specifications from Demonstrations (2017)
- Developing Bug-Free Machine Learning Systems With Formal Mathematics (2017)
- Systematic Testing of Convolutional Neural Networks for Autonomous Driving (2017)
- Information technology and the U.S. workforce: Where are we and where do we go from here? (2017)
- Compositional verification without compositional specification for learning-based systems (UCB/EECS-2017-164) (2017)
- Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications (2016)
- Planning for Autonomous Cars that Leverage Effects on Human Actions (2016)
- Information gathering actions over human internal state (2016)
- Safe Control under Uncertainty with Probabilistic Signal Temporal Logic (2016)
- Combining requirement mining, software model checking and simulation-based verification for industrial automotive systems (2016)
- Constrained Sampling and Counting: Universal Hashing Meets SAT Solving (2016)
- Concrete problems in AI safety (2016)
- Deep neural networks are easily fooled: High confidence predictions for unrecognizable images (2015)
- A comprehensive survey on safe reinforcement learning (2015)
- νZ - An Optimizing SMT Solver (2015)
- On Parallel Scalable Uniform SAT Witness Generation (2015)
- Rise of concerns about AI (2015)
- Combining Induction, Deduction, and Structure for Verification and Synthesis (2015)
- System Design Automation: Challenges and Limitations (2015)
- Automotive control design bug-finding with the S-TaLiRo tool (2015)
- Research priorities for robust and beneficial artificial intelligence: An open letter (2015)
- Safe Platooning of Unmanned Aerial Vehicles via Reachability (2015)
- Automotive systems requirement mining using breach (2015)
- Mining Requirements From Closed-Loop Control Models (2015)
- Safe sequential path planning of multi-vehicle systems via double-obstacle Hamilton-Jacobi-Isaacs variational inequality (2015)
- DeepFool: a simple and accurate method to fool deep neural networks (2015)
- Runtime Assurance Framework Development for Highly Adaptive Flight Control Systems (2015)
- Control Improvisation (2015)
- Automatic exploit generation (2014)
- Reachability-based safe learning with Gaussian processes (2014)
- Synthesis for Human-in-the-Loop Control Systems (2014)
- Distribution-Aware Sampling and Weighted Model Counting for SAT (2014)
- Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior (2014)
- Specification Mining: New Formalisms, Algorithms and Applications (2013)
- Polynomial-time verification of PCTL properties of MDPs with convex uncertainties (2013)
- Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems* (2012)
- Sciduction (2012)
- PRISM 4.0: Verification of Probabilistic Real-Time Systems (2011)
- Mining assumptions for synthesis (2011)
- Artificial Intelligence: A Modern Approach (2010)
- Quantitative languages (2010)
- Satisfiability Modulo Theories (2009)
- Boolean satisfiability from theoretical hardness to practical success (2009)
- Maximum Entropy Inverse Reinforcement Learning (2008)
- Stimulus generation for constrained random simulation (2007)
- Applied Assertion-Based Verification: An Industry Perspective (2007)
- BLOG: Probabilistic models with unknown objects (2007)
- Combinatorial sketching for finite programs (2006)
- Robust Control of Markov Decision Processes with Uncertain Transition Matrices (2005)
- Monitoring Temporal Properties of Continuous Signals (2004)
- Apprenticeship learning via inverse reinforcement learning (2004)
- Computational techniques for the verification of hybrid systems (2003)
- Using model checking to help discover mode confusions and other automation surprises (2002)
- Using simplicity to control complexity (2001)
- Computer-Aided Reasoning: An Approach (2000)
- Dynamically discovering likely program invariants (2000)
- Model Checking (Clarke, Grumberg, Peled) (2000)
- Algorithms for inverse reinforcement learning (2000)
- Rationality and intelligence (1997)
- Efficient detection of vacuity in ACTL formulas (1997)
- Machine Learning (Mitchell) (1997)
- Formal Methods: State of the Art and Future Directions (1995)
- Introduction to HOL: a theorem proving environment for higher order logic (1993)
- PVS: A prototype verification system (1992)
- A specifier's introduction to formal methods (1990)
- Bounded Rationality (1990)
- On the synthesis of a reactive module (1989)
- Graph-Based Algorithms for Boolean Function Manipulation (1986)
- Explanation-Based Generalization: A Unifying View (1986)
- Specification and verification of concurrent systems in CESAR (1982)
- Design and synthesis of synchronization skeletons using branching time temporal logic (1981)
- Scenic Environment Modeling and Scenario Description Language (GitHub BerkeleyLearnVerify/Scenic)
- VerifAI: A toolkit for design and verification of AI-based systems (GitHub BerkeleyLearnVerify/VerifAI)