Actions you can handle: dependent types for AI plans
Authors: 
Alasdair Hill, Ekaterina Komendantskaya, Matthew L. Daggitt, Ronald P. A. PetrickAuthors Info & Claims
Pages 1 - 13
Abstract
Verification of AI is a challenge that has engineering, algorithmic and programming language components. For example, AI planners are deployed to model actions of autonomous agents. They comprise a number of searching algorithms that, given a set of specified properties, find a sequence of actions that satisfy these properties. Although AI planners are mature tools from the algorithmic and engineering points of view, they have limitations as programming languages. Decidable and efficient automated search entails restrictions on the syntax of the language, prohibiting use of higher-order properties or recursion. This paper proposes a methodology for embedding plans produced by AI planners into the dependently-typed language Agda, which enables users to reason about and verify more general and abstract properties of plans, and also provides a more holistic programming language infrastructure for modelling plan execution.
References
[1]
Mohammad Abdulaziz and Dominik Berger. 2021. Computing Plan-Length Bounds Using Lengths of Longest Paths. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021. 11709–11717.
[2]
Mohammad Abdulaziz and Peter Lammich. 2018. A formally verified validator for classical planning problems and solutions. In 2018 IEEE 30th International Conference on Tools with Artificial Intelligence (ICTAI). 474–479.
[3]
Mohammad Abdulaziz and Peter Lammich. 2020. AI Planning Languages Semantics. Arch. Formal Proofs, 2020 (2020).
[4]
David W. Albrecht, John N. Crossley, and John S. Jeavons. 1997. New Curry-Howard Terms for Full Linear Logic. Theor. Comput. Sci., 185, 2 (1997), 217–235.
[5]
Ana Bove, Peter Dybjer, and Ulf Norell. 2009. A brief overview of Agda–a functional language with dependent types. In International Conference on Theorem Proving in Higher Order Logics. 73–78.
[6]
Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter O’Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. 2015. Moving fast with software verification. In NASA Formal Methods Symposium. 3–11.
[7]
Michael Cashmore, Anna Collins, Benjamin Krarup, Senka Krivic, Daniele Magazzeni, and David Smith. 2019. Towards explainable AI planning as a service. arXiv preprint arXiv:1908.05059.
[8]
Iliano Cervesato and Frank Pfenning. 2002. A Linear Logical Framework. Inf. Comput., 179, 1 (2002), 19–75.
[9]
Lukáš Chrpa, Pavel Surynek, and Jiří Vyskočil. 2007. Encoding of planning problems and their optimizations in linear logic. In Applications of Declarative Programming and Knowledge Management. Springer, 54–68.
[10]
Daniel C Dennett. 2006. Cognitive wheels: The frame problem of AI.
[11]
Lucas Dixon, Alan Smaill, and Tracy Tsang. 2009. Plans, Actions and Dialogues Using Linear Logic. Journal of Logic, Language and Information, 18, 2 (2009), 251–289.
[12]
Rebecca Eifler, Michael Cashmore, Jörg Hoffmann, Daniele Magazzeni, and Marcel Steinmetz. 2020. A new approach to plan-space explanation: Analyzing plan-property dependencies in oversubscription planning. In Proceedings of the AAAI Conference on Artificial Intelligence. 34, 9818–9826.
[13]
Rebecca Eifler, Marcel Steinmetz, Alvaro Torralba, and Jörg Hoffmann. 2020. Plan-space explanation via plan-property dependencies: Faster algorithms & more powerful properties. In 29th International Joint Conference on Artificial Intelligence, IJCAI 2020. 4091–4097.
[14]
George W Ernst and Allen Newell. 1969. GPS: A case study in generality and problem solving. Academic Pr.
[15]
Richard Fikes and Nils J. Nilsson. 1971. STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving. Artificial Intelligence, 2, 3/4 (1971), 189–208.
[16]
Peng Fu and Ekaterina Komendantskaya. 2017. Operational semantics of resolution and productivity in Horn clause logic. Formal Asp. Comput., 29, 3 (2017), 453–474.
[17]
Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, and Andrew Pond. 2016. Proof Relevant Corecursive Resolution. In Functional and Logic Programming - 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings (Lecture Notes in Computer Science, Vol. 9613). Springer, 126–143.
[18]
Alfonso Gerevini and Derek Long. 2005. Plan constraints and preferences in PDDL3. Technical Report 2005-08-07, Department of Electronics for Automation ….
[19]
Cordell Green. 1969. Theorem proving by resolution as a basis for question-answering systems. Machine intelligence, 4 (1969), 183–205.
[20]
Patrick J Hayes. 1981. The frame problem and related problems in artificial intelligence. In Readings in Artificial Intelligence. Elsevier, 223–230.
[21]
A. Hill, M. Daggitt, F. Farka, K. Komendantskaya, and C. Schwaab. 2021. Agda Code for Proof Carrying Plans, 2018 – 2021. https://github.com/PDTypes
[22]
Alasdair Hill, Ekaterina Komendantskaya, and Ronald P. A. Petrick. 2020. Proof-Carrying Plans: a Resource Logic for AI Planning. In PPDP ’20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020. ACM, 14:1–14:13.
[23]
Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM, 12, 10 (1969), 576–580.
[24]
Joshua S. Hodas and Dale Miller. 1994. Logic Programming in a Fragment of Intuitionistic Linear Logic. Inf. Comput., 110, 2 (1994), 327–365.
[25]
Samin S Ishtiaq and Peter W O’Hearn. 2001. BI as an assertion language for mutable data structures. In Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 14–26.
[26]
Eric Jacopin. 1993. Classical AI planning as theorem proving: The case of a fragment of linear logic. In AAAI Fall Symposium on Automated Deduction in Nonstandard Logics. 62–66.
[27]
John McCarthy and Patrick J Hayes. 1981. Some philosophical problems from the standpoint of artificial intelligence. In Readings in artificial intelligence. Elsevier, 431–450.
[28]
Drew McDermott, Malik Ghallab, Adele Howe, Craig Knoblock, Ashwin Ram, Manuela Veloso, Daniel Weld, and David Wilkins. 1998. PDDL-the planning domain definition language.
[29]
Cathy O’neil. 2016. Weapons of math destruction: How big data increases inequality and threatens democracy. Crown.
[30]
Peter O’Hearn, John Reynolds, and Hongseok Yang. 2001. Local reasoning about programs that alter data structures. In International Workshop on Computer Science Logic. 1–19.
[31]
Peter W O’hearn. 2007. Resources, concurrency, and local reasoning. Theoretical computer science, 375, 1-3 (2007), 271–307.
[32]
Jeff Polakow and Frank Pfenning. 2001. Ordered linear logic and applications. Carnegie Mellon University Pittsburgh.
[33]
David Pym. 2019. Resource semantics: logic as a modelling technology. ACM SIGLOG News, 6, 2 (2019), 5–41.
[34]
Anders Schack-Nielsen and Carsten Schürmann. 2008. Celf - A Logical Framework for Deductive and Concurrent Systems (System Description). In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, Alessandro Armando, Peter Baumgartner, and Gilles Dowek (Eds.) (Lecture Notes in Computer Science, Vol. 5195). Springer, 320–326.
[35]
Christopher Schwaab, Ekaterina Komendantskaya, Alasdair Hill, Frantisek Farka, Ronald P. A. Petrick, Joe B. Wells, and Kevin Hammond. 2019. Proof-Carrying Plans. In Practical Aspects of Declarative Languages - 21th International Symposium, PADL 2019, Lisbon, Portugal, January 14-15, 2019, Proceedings, José Júlio Alferes and Moa Johansson (Eds.) (Lecture Notes in Computer Science, Vol. 11372). Springer, 204–220.
[36]
Mark Steedman. 2002. Plans, affordances, and combinatory grammar. Linguistics and Philosophy, 25, 5-6 (2002), 723–753.
Recommendations
Proof-Carrying Plans
Practical Aspects of Declarative LanguagesAbstractIt is becoming increasingly important to verify safety and security of AI applications. While declarative languages (of the kind found in automated planners and model checkers) are traditionally used for verifying AI systems, a big challenge is to ...
Dependent Types for Safe and Secure Web Programming
IFL '13: Proceedings of the 25th symposium on Implementation and Application of Functional LanguagesDependently-typed languages allow precise types to be used during development, facilitating static reasoning about program behaviour. However, with the use of more specific types comes the disadvantage that it becomes increasingly difficult to write ...
A specification for dependent types in Haskell
We propose a core semantics for Dependent Haskell, an extension of Haskell with full-spectrum dependent types. Our semantics consists of two related languages. The first is a Curry-style dependently-typed language with nontermination, irrelevant ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2021
22 pages
Copyright © 2021 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 18 August 2021
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
ICFP '21
Sponsor:
ICFP '21: 26th ACM SIGPLAN International Conference on Functional Programming
August 22, 2021
Virtual, Republic of Korea
Upcoming Conference
ICFP '25
- Sponsor:
- sigplan
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 89Total Downloads
- Downloads (Last 12 months)24
- Downloads (Last 6 weeks)14
Reflects downloads up to 20 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in