Actions You Can Handle: Dependent Types for AI Plans

• URL: http://arxiv.org/abs/2105.11267v1
• Date: Mon, 24 May 2021 13:33:56 GMT
• Title: Actions You Can Handle: Dependent Types for AI Plans
• Authors: Alasdair Hill, Ekaterina Komendantskaya, Matthew L. Daggitt and Ronald P. A. Petrick
• Abstract summary: This paper proposes a methodology for embedding plans produced by AI planners into dependently-typed language Agda. It enables users to reason about and verify more general and abstract properties of plans.
• Score: 2.064612766965483
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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 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.

Related papers

• Joint Verification and Refinement of Language Models for Safety-Constrained Planning [21.95203475140736]
  We develop a method to generate executable plans and formally verify them against task-relevant safety specifications. Given a high-level task description in natural language, the proposed method queries a language model to generate plans in the form of executable robot programs. It then converts the generated plan into an automaton-based representation, allowing formal verification of the automaton against the specifications.
  arXiv  Detail & Related papers  (2024-10-18T21:16:30Z)
• Adaptation of XAI to Auto-tuning for Numerical Libraries [0.0]
  Explainable AI (XAI) technology is gaining prominence, aiming to streamline AI model development and alleviate the burden of explaining AI outputs to users. This research focuses on XAI for AI models when integrated into two different processes for practical numerical computations.
  arXiv  Detail & Related papers  (2024-05-12T09:00:56Z)
• TravelPlanner: A Benchmark for Real-World Planning with Language Agents [63.199454024966506]
  We propose TravelPlanner, a new planning benchmark that focuses on travel planning, a common real-world planning scenario. It provides a rich sandbox environment, various tools for accessing nearly four million data records, and 1,225 meticulously curated planning intents and reference plans. Comprehensive evaluations show that the current language agents are not yet capable of handling such complex planning tasks-even GPT-4 only achieves a success rate of 0.6%.
  arXiv  Detail & Related papers  (2024-02-02T18:39:51Z)
• Automated Process Planning Based on a Semantic Capability Model and SMT [50.76251195257306]
  In research of manufacturing systems and autonomous robots, the term capability is used for a machine-interpretable specification of a system function. We present an approach that combines these two topics: starting from a semantic capability model, an AI planning problem is automatically generated.
  arXiv  Detail & Related papers  (2023-12-14T10:37:34Z)
• Learning adaptive planning representations with natural language guidance [90.24449752926866]
  This paper describes Ada, a framework for automatically constructing task-specific planning representations. Ada interactively learns a library of planner-compatible high-level action abstractions and low-level controllers adapted to a particular domain of planning tasks.
  arXiv  Detail & Related papers  (2023-12-13T23:35:31Z)
• General Purpose Artificial Intelligence Systems (GPAIS): Properties, Definition, Taxonomy, Societal Implications and Responsible Governance [16.030931070783637]
  General-Purpose Artificial Intelligence Systems (GPAIS) has been defined to refer to these AI systems. To date, the possibility of an Artificial General Intelligence, powerful enough to perform any intellectual task as if it were human, or even improve it, has remained an aspiration, fiction, and considered a risk for our society. This work discusses existing definitions for GPAIS and proposes a new definition that allows for a gradual differentiation among types of GPAIS according to their properties and limitations.
  arXiv  Detail & Related papers  (2023-07-26T16:35:48Z)
• Robots That Ask For Help: Uncertainty Alignment for Large Language Model Planners [85.03486419424647]
  KnowNo is a framework for measuring and aligning the uncertainty of large language models. KnowNo builds on the theory of conformal prediction to provide statistical guarantees on task completion.
  arXiv  Detail & Related papers  (2023-07-04T21:25:12Z)
• Instruct2Act: Mapping Multi-modality Instructions to Robotic Actions with Large Language Model [63.66204449776262]
  Instruct2Act is a framework that maps multi-modal instructions to sequential actions for robotic manipulation tasks. Our approach is adjustable and flexible in accommodating various instruction modalities and input types. Our zero-shot method outperformed many state-of-the-art learning-based policies in several tasks.
  arXiv  Detail & Related papers  (2023-05-18T17:59:49Z)
• HuggingGPT: Solving AI Tasks with ChatGPT and its Friends in Hugging Face [85.25054021362232]
  Large language models (LLMs) have exhibited exceptional abilities in language understanding, generation, interaction, and reasoning. LLMs could act as a controller to manage existing AI models to solve complicated AI tasks. We present HuggingGPT, an LLM-powered agent that connects various AI models in machine learning communities.
  arXiv  Detail & Related papers  (2023-03-30T17:48:28Z)
• Improving Search by Utilizing State Information in OPTIC Planners Compilation to LP [1.9686770963118378]
  Many planners are domain-independent, allowing their deployment in a variety of domains. These planners perform Forward Search and call a Linear Programming (LP) solver multiple times at every state to check for consistency and to set bounds on the numeric variables. This paper suggests a method for identifying information about the specific state being evaluated, allowing the formulation of the equations to facilitate better solver selection and faster LP solving.
  arXiv  Detail & Related papers  (2021-06-15T07:23:31Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.