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

Towards Verified Artificial Intelligence

Open access
Seshia, Sanjit A., Sadigh, Dorsa, Sastry, S. Shankar·2016·arXiv
DOI 10.48550/arxiv.1606.08514arXiv 1606.08514
Open this paper in CoChat — free accountOpen PDF

Abstract

Verified artificial intelligence (AI) is the goal of designing AI-based systems that 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.

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

DataCite · 10.48550/arxiv.1606.08514

Cites

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?

  • Formal verification is often hard to produce, even for relatively simple computer programs, and traditional formal methods face unique challenges for AI systems.

    “Of course, such formal verification is often hard to produce, even for relatively simple computer programs, and traditional formal methods face unique challenges for AI systems (Seshia et al., 2016).”

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

    Section 3.2 (p. 4) says that producing a high-quality formal specification is challenging even in domains where formal verification has succeeded, and that AI systems exacerbate the challenge. The Conclusion (p. 12) identifies five challenges for applying formal methods to AI systems. Our copy does not establish the more specific claim that formal verification is often hard to produce even for relatively simple computer programs. (LLM, conf=0.86)

    Experimental — accuracy not yet measured

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

No references could be resolved yet.

Research works printed but not linked: 78

  1. [3][3] Anayo K Akametalu, Jaime F Fisac, Jeremy H Gillula, Shahab Kaynama, Melanie N Zeilinger, and Claire J Tomlin. Reachability-based safe learning with Gaussian processes. In 53rd IEEE Conference on Decision and Control , pages 1424-1431, 2014. -
  2. [4][4] Dario Amodei, Chris Olah, Jacob Steinhardt, Paul Christiano, John Schulman, and Dan Man´ e. Concrete problems in AI safety. arXiv preprint arXiv:1606.06565 , 2016. - · arXiv
  3. [5][5] Thanassis Avgerinos, Sang Kil Cha, Alexandre Rebert, Edward J. Schwartz, Maverick Woo, and David Brumley. Automatic exploit generation. Commun. ACM , 57(2):74-84, 2014. -
  4. [6][6] Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability , volume 4, chapter 8. IOS Press, 2009. -
  5. [7][7] I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh. Efficient detection of vacuity in ACTL formulas. Formal Methods in System Design , 18(2):141-162, 2001. -
  6. [8][8] Nikolaj Bjørner, Anh-Dung Phan, and Lars Fleckenstein. n z-an optimizing SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages 194-199. Springer, 2015. -
  7. [9][9] Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers , C-35(8):677-691, August 1986. -
  8. [10][10] Andrea Censi, Konstantin Slutsky, Tichakorn Wongpiromsarn, Dmitry Yershov, Scott Pendleton, James Fu, and Emilio Frazzoli. Liability, ethics, and culture-aware behavior specification using rulebooks. In 2019 International Conference on Robotics and Automation (ICRA) , pages 8536-8542. IEEE, 2019. -
  9. [11][11] Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi. Distribution-aware sampling and weighted model counting for SAT. In Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI) , pages 1722-1730, July 2014. -
  10. [12][12] Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi. On parallel scalable uniform sat witness generation. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , pages 304-319, April 2015. -
  11. [13][13] Krishnendu Chatterjee, Laurent Doyen, and Thomas A Henzinger. Quantitative languages. ACM Transactions on Computational Logic (TOCL) , 11(4):23, 2010. -
  12. [14][14] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs , pages 52-71, 1981. -
  13. [15][15] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking . MIT Press, 2000. -
  14. [16][16] Edmund M Clarke and Jeannette M Wing. Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR) , 28(4):626-643, 1996. -
  15. [18][18] Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A storm is coming: A modern probabilistic model checker. In International Conference on Computer Aided Verification (CAV) , pages 592-600. Springer, 2017. -
  16. [19][19] Ankush Desai, Tommaso Dreossi, and Sanjit A. Seshia. Combining model checking and runtime verification for safe robotics. In Runtime Verification - 17th International Conference, RV 2017, Seattle, WA, USA, September 13-16, 2017, Proceedings , pages 172-189, 2017. -
  17. [20][20] Ankush Desai, Shromona Ghosh, Sanjit A. Seshia, Natarajan Shankar, and Ashish Tiwari. A runtime assurance framework for programming safe robotics systems. In IEEE/IFIP International Conference on Dependable Systems and Networks (DSN) , June 2019. -
  18. [21][21] Thomas G Dietterich and Eric J Horvitz. Rise of concerns about AI: reflections and directions. Communications of the ACM , 58(10):38-40, 2015. -
  19. [22][22] Tommaso Dreossi, Alexandre Donze, and Sanjit A. Seshia. Compositional falsification of cyberphysical systems with machine learning components. In Proceedings of the NASA Formal Methods Conference (NFM) , May 2017. -
  20. [23][23] Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia. VerifAI: A toolkit for the formal design and analysis of artificial intelligence-based systems. In 31st International Conference on Computer Aided Verification (CAV) , July 2019. -
  21. [24][24] Tommaso Dreossi, Shromona Ghosh, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia. A formalization of robustness for deep neural networks. In Proceedings of the AAAI Spring Symposium Workshop on Verification of Neural Networks (VNN) , March 2019. -
  22. [25][25] Tommaso Dreossi, Somesh Jha, and Sanjit A. Seshia. Semantic adversarial deep learning. In 30th International Conference on Computer Aided Verification (CAV) , 2018. -
  23. [26][26] Michael Ernst. Dynamically Discovering Likely Program Invariants . PhD thesis, University of Washington, Seattle, 2000. -
  24. [27][27] Georgios E. Fainekos. Automotive control design bug-finding with the S-TaLiRo tool. In American Control Conference (ACC) , page 4096, 2015. -
  25. [28][28] Jaime F Fisac, Anayo K Akametalu, Melanie N Zeilinger, Shahab Kaynama, Jeremy Gillula, and Claire J Tomlin. A general safety framework for learning-based control in uncertain robotic systems. IEEE Transactions on Automatic Control , 64(7):2737-2752, 2018. -
  26. [30][30] Daniel J. Fremont, Johnathan Chiu, Dragos D. Margineantu, Denis Osipychev, and Sanjit A. Seshia. Formal analysis and redesign of a neural network-based aircraft taxiing system with verifai. In 32nd International Conference on Computer-Aided Verification (CAV) , pages 122-134, 2020. -
  27. [31][31] Daniel J. Fremont, Alexandre Donz´ e, Sanjit A. Seshia, and David Wessel. Control improvisation. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015) , pages 463-474, 2015. -
  28. [32][32] Daniel J. Fremont, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. SangiovanniVincentelli, and Sanjit A. Seshia. Scenic: A language for scenario specification and scene generation. In Proceedings of the 40th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI) , June 2019. -
  29. [33][33] Daniel J. Fremont, Edward Kim, Yash Vardhan Pant, Sanjit A. Seshia, Atul Acharya, Xantha Bruso, Paul Wells, Steve Lemke, Qiang Lu, and Shalin Mehta. Formal scenario-based testing of autonomous vehicles: From simulation to the real world. In IEEE Intelligent Transportation Systems Conference (ITSC) , 2020. -
  30. [34][34] Javier Garcıa and Fernando Fern´ andez. A comprehensive survey on safe reinforcement learning. Journal of Machine Learning Research , 16(1):1437-1480, 2015. -
  31. [35][35] Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. AI2: Safety and robustness certification of neural networks with abstract interpretation. In IEEE Symposium on Security and Privacy (SP) , pages 3-18. IEEE, 2018. -
  32. [36][36] Ian Goodfellow, Patrick McDaniel, and Nicolas Papernot. Making machine learning robust against adversarial inputs. Communications of the ACM , 61(7):56-66, 2018. -
  33. [37][37] M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for HigherOrder Logic . Cambridge University Press, 1993. -
  34. [38][38] Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In International Conference on Computer Aided Verification , pages 3-29. Springer, 2017. -
  35. [39][39] S. Jha and S. A. Seshia. A Theory of Formal Synthesis via Inductive Learning. ArXiv e-prints , May 2015. -
  36. [40][40] Susmit Jha, Tuhin Sahai, Vasumathi Raman, Alessandro Pinto, and Michael Francis. Explaining AI decisions using efficient methods for learning sparse boolean formulae. J. Autom. Reasoning , 63(4):1055-1075, 2019. -
  37. [42][42] Xiaoqing Jin, Alexandre Donz´ e, Jyotirmoy Deshmukh, and Sanjit A. Seshia. Mining requirements from closed-loop control models. IEEE Transactions on Computer-Aided Design of Circuits and Systems , 34(11):1704-1717, 2015. -
  38. [44][44] Nathan Kitchen and Andreas Kuehlmann. Stimulus generation for constrained random simulation. In Proceedings of the 2007 IEEE/ACM International Conference on Computer-Aided Design (ICCAD) , pages 258-265. IEEE Press, 2007. -
  39. [45][45] Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic realtime systems. In International Conference on Computer Aided Verification (CAV) , pages 585-591. Springer, 2011. -
  40. [46][46] Tzu-Mao Li, Miika Aittala, Fr´ edo Durand, and Jaakko Lehtinen. Differentiable monte carlo ray tracing through edge sampling. ACM Trans. Graph. (Proc. SIGGRAPH Asia) , 37(6):222:1-222:11, 2018. -
  41. [47][47] Wenchao Li. Specification Mining: New Formalisms, Algorithms and Applications . PhD thesis, EECS Department, University of California, Berkeley, Mar 2014. -
  42. [48][48] Wenchao Li, Dorsa Sadigh, S. Shankar Sastry, and Sanjit A. Seshia. Synthesis for human-in-the-loop control systems. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , pages 470-484, April 2014. -
  43. [49][49] Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In FORMATS/FTRTFT , pages 152-166, 2004. -
  44. [50][50] Sharad Malik and Lintao Zhang. Boolean satisfiability: From theoretical hardness to practical success. Communications of the ACM (CACM) , 52(8):76-82, 2009. -
  45. [51][51] Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii, and Sharad Malik. Constrained sampling and counting: Universal hashing meets SAT solving. In Beyond NP, Papers from the 2016 AAAI Workshop, Phoenix, Arizona, USA, February 12, 2016. , 2016. -
  46. [53][53] Tom M. Mitchell. Machine Learning . McGraw-Hill, 1997. -
  47. [54][54] Tom M Mitchell, Richard M Keller, and Smadar T Kedar-Cabelli. Explanation-based generalization: A unifying view. Machine learning , 1(1):47-80, 1986. -
  48. [55][55] Andrew Y. Ng and Stuart J. Russell. Algorithms for inverse reinforcement learning. In Proceedings of the Seventeenth International Conference on Machine Learning (ICML) , pages 663-670, 2000. -
  49. [56][56] A. Nilim and L. El Ghaoui. Robust Control of Markov Decision Processes with Uncertain Transition Matrices. Journal of Operations Research , pages 780-798, 2005. -
  50. [57][57] Pierluigi Nuzzo, Jiwei Li, Alberto L. Sangiovanni-Vincentelli, Yugeng Xi, and Dewei Li. Stochastic assume-guarantee contracts for cyber-physical system design. ACM Trans. Embed. Comput. Syst. , 18(1), January 2019. -
  51. [58][58] S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE) , volume 607 of Lecture Notes in Artificial Intelligence , pages 748-752. Springer-Verlag, June 1992. -
  52. [59][59] Judea Pearl. The seven tools of causal inference, with reflections on machine learning. Communications of the ACM , 62(3):54-60, 2019. -
  53. [60][60] Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989 , pages 179-190, 1989. -
  54. [61][61] Alberto Puggelli, Wenchao Li, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia. Polynomialtime verification of PCTL properties of MDPs with convex uncertainties. In Proceedings of the 25th International Conference on Computer-Aided Verification (CAV) , July 2013. -
  55. [62][62] Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in CESAR. In Symposium on Programming , number 137 in LNCS, pages 337-351, 1982. -
  56. [63][63] John Rushby. Using model checking to help discover mode confusions and other automation surprises. Reliability Engineering & System Safety , 75(2):167-177, 2002. -
  57. [64][64] Stuart Russell, Tom Dietterich, Eric Horvitz, Bart Selman, Francesca Rossi, Demis Hassabis, Shane Legg, Mustafa Suleyman, Dileep George, and Scott Phoenix. Letter to the editor: Research priorities for robust and beneficial artificial intelligence: An open letter. AI Magazine , 36(4), 2015. -
  58. [65][65] Stuart J Russell. Rationality and intelligence. Artificial Intelligence , 94(1-2):57-77, 1997. -
  59. [67][67] Dorsa Sadigh, Katherine Driggs-Campbell, Alberto Puggelli, Wenchao Li, Victor Shia, Ruzena Bajcsy, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry, and Sanjit A. Seshia. Data-driven probabilistic modeling and verification of human driver behavior. In Formal Verification and Modeling in HumanMachine Systems, AAAI Spring Symposium , March 2014. -
  60. [68][68] Dorsa Sadigh and Ashish Kapoor. Safe control under uncertainty with probabilistic signal temporal logic. In Proceedings of Robotics: Science and Systems , AnnArbor, Michigan, June 2016. -
  61. [69][69] Dorsa Sadigh, Shankar Sastry, Sanjit A. Seshia, and Anca D. Dragan. Information gathering actions over human internal state. In Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) , October 2016. -
  62. [70][70] Alberto Sangiovanni-Vincentelli, Werner Damm, and Roberto Passerone. Taming Dr. Frankenstein: Contract-based design for cyber-physical systems. European journal of control , 18(3):217-238, 2012. -
  63. [72][72] Daniel Selsam, Percy Liang, and David L. Dill. Developing bug-free machine learning systems with formal mathematics. In Proceedings of the 34th International Conference on Machine Learning, (ICML) , volume 70 of Proceedings of Machine Learning Research , pages 3047-3056. PMLR, 2017. -
  64. [73][73] Sanjit A. Seshia. Sciduction: Combining induction, deduction, and structure for verification and synthesis. In Proceedings of the Design Automation Conference (DAC) , pages 356-365, June 2012. -
  65. [74][74] Sanjit A. Seshia. Combining induction, deduction, and structure for verification and synthesis. Proceedings of the IEEE , 103(11):2036-2051, 2015. -
  66. [76][76] Sanjit A. Seshia. Introspective environment modeling. In 19th International Conference on Runtime Verification (RV) , pages 15-26, 2019. -
  67. [77][77] Sanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xiangyu Yue. Formal specification for deep neural networks. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis (ATVA) , pages 20-34, October 2018. -
  68. [78][78] Lui Sha. Using simplicity to control complexity. IEEE Software , 18(4):20-28, 2001. -
  69. [79][79] Yasser Shoukry, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, and Paulo Tabuada. Smc: Satisfiability modulo convex optimization. In Proceedings of the 10th International Conference on Hybrid Systems: Computation and Control (HSCC) , April 2017. -
  70. [80][80] Joseph Sifakis. System design automation: Challenges and limitations. Proceedings of the IEEE , 103(11):2093-2103, 2015. -
  71. [81][81] Herbert A Simon. Bounded rationality. In Utility and Probability , pages 15-18. Springer, 1990. -
  72. [82][82] Armando Solar-Lezama, Liviu Tancau, Rastislav Bod´ ık, Sanjit A. Seshia, and Vijay A. Saraswat. Combinatorial sketching for finite programs. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) , pages 404-415. ACM Press, October 2006. -
  73. [83][83] Claire Tomlin, Ian Mitchell, Alexandre M. Bayen, and Meeko Oishi. Computational techniques for the verification of hybrid systems. Proceedings of the IEEE , 91(7):986-1001, 2003. -
  74. [84][84] Marcell Vazquez-Chanlatte, Jyotirmoy V. Deshmukh, Xiaoqing Jin, and Sanjit A. Seshia. Logical clustering and learning for time-series data. In 29th International Conference on Computer Aided Verification (CAV) , pages 305-325, 2017. -
  75. [85][85] Marcell Vazquez-Chanlatte, Susmit Jha, Ashish Tiwari, Mark K. Ho, and Sanjit A. Seshia. Learning task specifications from demonstrations. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems (NeurIPS) , pages 5372-5382, December 2018. -
  76. [86][86] Jeannette M Wing. A specifier's introduction to formal methods. IEEE Computer , 23(9):8-24, September 1990. -
  77. [87][87] Jingyi Xu, Zilu Zhang, Tal Friedman, Yitao Liang, and Guy Van den Broeck. A semantic loss function for deep learning with symbolic knowledge. In Proceedings of the 35th International Conference on Machine Learning, (ICML) , volume 80 of Proceedings of Machine Learning Research , pages 54985507. PMLR, 2018. -
  78. [89][89] Xiaojin Zhu, Adish Singla, Sandra Zilles, and Anna N Rafferty. An overview of machine teaching. arXiv preprint arXiv:1801.05927 , 2018. · arXiv

Cited by

Sorted by citations

Authors
Seshia, S. A., Sadigh, D., & Sastry, S. S.
Affiliations
University of California, Berkeley (US)
ORCID
Venue
arXiv
Publisher
arXiv
Published
2016
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.1606.08514
arXiv
1606.08514
OpenAlex
W2467659428
Cited by
142
References
0
Citations by year
2026: 1 · 2025: 4 · 2024: 3 · 2023: 10 · 2022: 22 · 2021: 18 · 2020: 29 · 2019: 33 · 2018: 16 · 2017: 5 · 2016: 1
Type
posted content
Language
en
Open access
Licence
arxiv.org/licenses/nonexclusive-distrib/1.0/
Locations
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Funders
  • National Science Foundation (1646208, 1545126, 1116993, 1139138, 1837132)
  • Semiconductor Research Corporation
  • Defense Advanced Research Projects Agency
  • National Defense Science and Engineering Graduate
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, AI system design, requirements specification

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