CoChat
Sign Up
Cited by 215Formal Methods in VerificationSafety Systems Engineering in AutonomyLogic, programming, and type systems

Toward verified artificial intelligence

Open access
Seshia, Sanjit A., Sadigh, Dorsa, Sastry, S. Shankar·2022·Communications of the ACM
DOI 10.1145/3503914
Open this paper in CoChat — free accountOpen PDF

Abstract

Making AI more trustworthy with a formal methods-based approach to AI system verification and validation.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1145/3503914

Cites

1 of 1 references verified0 citation errors · 0 not checkable

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Seshia et al. (2022) propose techniques to automatically infer a decomposition of the system into components along with interface contracts between them.

    “Seshia et al. (2022) tackle this by proposing techniques to automatically infer a decomposition of the system into components along with interface contracts between them.”

    From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Seshia et al. (2022)

    In “Compositional reasoning for AI/ML” (page unavailable), the paper describes splitting a system into components and using assume-guarantee contracts. In “Bridging design time and runtime for resilient AI” (page unavailable), it calls for techniques to generate those contracts algorithmically. It does not say that the decomposition into components is automatically inferred, so that part of the claim is unsupported. (LLM, conf=0.87)

    Experimental — accuracy not yet measured

  • Even when individual AI components perform tasks that are hard to formalise, the relevant notion of safety can still be formalised at the full system level.

    “even when individual AI components perform tasks that are hard to formalise, it can still be the case that the relevant notion of safety can be formalised at the full system level.”

    From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Seshia et al. (2022)

  • The task of formalising specifications can be easier with a system-level approach.

    “It is also important to note that the task of formalising specifications can be easier with a system-level approach.”

    From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Seshia et al. (2022)

  • Seshia et al. (2022) presents 15 principles for providing provable guarantees of safety for AI systems.

    “Seshia et al. (2022), who presents 15 principles for providing provable guarantees of safety for AI systems.”

    From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Seshia et al. (2022)

  • One important piece is devising suitable abstractions of AI components such as neural networks.

    “First of all, one important piece is devising suitable abstractions of AI components such as neural networks.”

    From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Seshia et al. (2022)

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

Flagged first, then by citations

Research works printed but not linked: 38

  1. falsification of temporal properties of non-linear hybrid systems. In Proceedings of the 13 th ACM Intern. Conf. on Hybrid Systems: Computation and Control (2010), 211-220.
  2. Nuzzo, P., Li, J., Sangiovanni-Vincentelli, A.L., Xi, Y., and Li, D. Stochastic assume-guarantee contracts for cyber-physical system design. ACM Transactions on Embedded Computing Systems 18, 1, (Jan. 2019).
  3. Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., and Seshia, S.A. Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In Proceedings of the 25 th Intern. Conf. on Computer- Aided Verification (2013).
  4. Russell, S.J. and Norvig, P. Artificial Intelligence: A Modern Approach. Prentice Hall (2010).
  5. Sadigh, D. et al. Data-driven probabilistic modeling and verification of human driver behavior. In Formal Verification and Modeling in Human-Machine Systems, AAAI Spring Symposium (2014).
  6. Sadigh, D., Sastry, S., Seshia, S.A., and Dragan, A.D. Information gathering actions over human internal state. In Proceedings of the IEEE/RSJ Intern. Conf. on Intelligent Robots and Systems (2016).
  7. Selsam, D., Liang, P., and Dill, D.L. Developing bug-free machine learning systems with formal mathematics. In Proceedings of the 34 th Intern. Conf. on Machine Learning 70 (2017), 3047-3056.
  8. Seshia, S.A. Combining induction, deduction, and structure for verification and synthesis. In Proceedings of the IEEE 103, 11 (2015), 2036-2051.
  9. Seshia, S.A. Introspective environment modeling. 19 th Intern. Conf. on Runtime Verification (2019), 15-26.
  10. Seshia, S.A. et al. Formal specification for deep neural networks. In Proceedings of the Intern. Symp. on Automated Technology for Verification and Analysis (2018), 20-34.
  11. Sha, L. Using simplicity to control complexity. IEEE Software 18, 4 (2001), 20-28.
  12. Shoukry, Y., et al. SMC: Satisfiability modulo convex optimization. In Proceedings of the 10 th Intern. Conf. on Hybrid Systems: Computation and Control (2017).
  13. Tomlin, C., Mitchell, I., Bayen, A.M., and Oishi, M. Computational techniques for the verification of hybrid systems. In Proceedings of the IEEE 91, 7 (2003), 986-1001.
  14. Tran, H-D., Xiang, W., and Johnson, T.T. Verification approaches for learning-enabled autonomous cyber- physical systems. IEEE Design & Test (Aug. 2020). https://doi.org/10.1109/MDAT.2020.3015712. · DOI
  15. Vazquez-Chanlatte, M., Jha, S., Tiwari, A., Ho, M.K., and Seshia, S.A. Learning task Specifications from demonstrations. In Advances in Neural Information Processing Systems 31 (2018), 5372-5382.
  16. Wing, J.M. A specifier's introduction to formal methods. IEEE Computer 23, 9 (Sept. 1990), 8-24.
  17. Wing, J.M. Trustworthy AI. Communications of the ACM 64, 10 (2021), 64-71.
  18. Xu, J., Zhang, Z., Friedman, T., Liang, Y., and Van den Broeck, G. A semantic loss function for deep learning with symbolic knowledge. In Proceedings of the 35 th Intern. Conf. on Machine Learning (2018), 5498-5507.
  19. Censi, A., Slutsky, K., Wongpiromsarn, T., Yershov, D., Pendleton, S., Fu, J., and Frazzoli, E. Liability, ethics, and culture-aware behavior specification using rulebooks. In 2019 Intern. Conf. on Robotics and Automation (ICRA), IEEE, 8536-8542.
  20. Cohen, J.M., Rosenfeld, E., and Kolter, J.Z. Certified adversarial robustness via randomized smoothing. In Proceedings of the 36 th Intern. Conf. on Machine Learning 97 (2019), 1310-1320.
  21. Desai, A., Ghosh, S., Seshia, S.A., Shankar, N., and Tiwari, A. SOTER: A runtime assurance framework for programming safe robotics systems. In IEEE/IFIP Intern. Conf. on Dependable Systems and Networks (2019), 138-150.
  22. Dietterich, T.G. and Horvitz, E.J. Rise of concerns about AI: Reflections and directions. Communications of the ACM 58, 10 (2015), 38-40.
  23. Dreossi, T., Donze, A., and Seshia, S.A. Compositional falsification of cyber-physical systems with machine learning components. In Proceedings of the NASA Formal Methods Conf. (Lecture Notes in Computer Science) 10227 (2017), 357-372.
  24. Dreossi, T., Fremont, D.J., Ghosh, S., Kim, E., Ravanbakhsh, H., Vazquez-Chanlatte, M., and Seshia, S.A. VerifAI: A toolkit for the formal design and analysis of artificial intelligence-based systems. In 31 st Intern. Conf. on Computer Aided Verification (Lecture Notes in Computer Science) 11561 (2017), 432-442.
  25. Dreossi, T., Jha, S., and Seshia, S.A. Semantic adversarial deep learning. In 30 th Intern. Conf. on Computer Aided Verification (Lecture Notes in Computer Science) 10981 (2018), 3-26.
  26. Fisac, J.F. et al. A general safety framework for learning-based control in uncertain robotic systems. IEEE Transactions on Automatic Control 64, 7 (2018), 2737-2752.
  27. Fremont, D.J., Donzé, A., Seshia, S.A., and Wessel, D. Control improvisation. In 35 th IARCS Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (2015), 463-474.
  28. Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., and Seshia, S.A. Scenic: A language for scenario specification and scene generation. In Proceedings of the 40 th annual ACM SIGPLAN Conf. on Programming Language Design and Implementation (2019).
  29. Garcıa, J. and Fernández, F. A comprehensive survey on safe reinforcement learning. J. of Machine Learning Research 16, 1 (2015), 1437-1480.
  30. Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., and Vechev, M. AI2: Safety and robustness certification of neural networks with abstract interpretation. In IEEE Symposium on Security and Privacy (2018), 3-18.
  31. Goodfellow, I., McDaniel, P., and Papernot, N. Making machine learning robust against adversarial inputs. Communications of the ACM 61, 7 (2018), 56-66.
  32. Huang, X., Kwiatkowska, M., Wang, S., and Wu, M. Safety verification of deep neural networks. In Intern. Conf. on Computer Aided Verification, Springer, (2017), 3-29.
  33. Icarte, R.T., Klassen, T., Valenzano, R., and McIlraith, S. Using reward machines for high-level task specification and decomposition in reinforcement learning. Intern. Conf. on Machine Learning (2018), 2107-2116.
  34. Jha, S., Sahai, T., Raman, V., Pinto, A., and Francis, M. Explaining AI decisions using efficient methods for learning sparse Boolean formulae. J. of Automated Reasoning 63, 4 (2019), 1055-1075.
  35. Li, W., Sadigh, D., Sastry, S.S., and Seshia, S.A. Synthesis for human-in-the-loop control systems. In Proceedings of the 20 th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (2014), 470-484.
  36. Liu, C. et al. Algorithms for verifying deep neural networks. Foundations and Trends in Optimization 4, 3-4 (2021), 244-404.
  37. Meel, K.S. et al. Constrained sampling and counting: Universal hashing meets SAT solving. In Beyond NP, Papers from the 2016 AAAI Workshop, (Feb. 12, 2016).
  38. Mitchell, T.M., Keller, R.M., and Kedar-Cabelli, S.T. Explanation-based generalization: A unifying view. Machine Learning 1, 1 (1986), 47-80.

Cited by

Sorted by citations

Authors
Seshia, S. A., Sadigh, D., & Sastry, S. S.
Affiliations
  • University of California, Berkeley (US)
  • Stanford University (US)
ORCID
Venue
Communications of the ACM
Publisher
Association for Computing Machinery (ACM)
Published
2022-06-21
Volume
65
Issue
7
Pages
46-55
ISSN
  • 0001-0782 (ISSN-L)
  • 1557-7317
DOI
10.1145/3503914
OpenAlex
W4283212640
Cited by
215
References
1
Citations by year
2026: 50 · 2025: 47 · 2024: 34 · 2023: 61 · 2022: 13 · 2021: 1 · 2020: 3 · 2019: 1 · 2018: 5
FWCI
20.96
Type
journal article
Language
en
Open access
Licence
Locations
  • Communications of the ACM (publishedVersion, cc-by)
  • eScholarship (California Digital Library) (submittedVersion)
Funders
  • NSF (1545126,1646208,1837132)
  • Defense Advanced Research Projects Agency (FA8750-16-C0043,FA8750-20-C-0156)
Topics
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
  • Physical Sciences › Engineering › Safety, Risk, Reliability and Quality › Safety Systems Engineering in Autonomy
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
Keywords
formal methods, trustworthy AI, AI safety

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review