Joint Verification and Refinement of Language Models for Safety-Constrained Planning

• URL: http://arxiv.org/abs/2410.14865v1
• Date: Fri, 18 Oct 2024 21:16:30 GMT
• Title: Joint Verification and Refinement of Language Models for Safety-Constrained Planning
• Authors: Yunhao Yang, William Ward, Zichao Hu, Joydeep Biswas, Ufuk Topcu,
• Abstract summary: 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.
• Score: 21.95203475140736
• License:
• Abstract: Although pre-trained language models can generate executable plans (e.g., programmatic policies) for solving robot tasks, the generated plans may violate task-relevant logical specifications due to the models' black-box nature. A significant gap remains between the language models' outputs and verifiable executions of plans. 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. We prove that given a set of verified plans, the composition of these plans also satisfies the safety specifications. This proof ensures the safety of complex, multi-component plans, obviating the computation complexity of verifying the composed plan. We then propose an automated fine-tuning process that refines the language model to generate specification-compliant plans without the need for human labeling. The empirical results show a 30 percent improvement in the probability of generating plans that meet task specifications after fine-tuning.

Related papers

• Unlocking Reasoning Potential in Large Langauge Models by Scaling Code-form Planning [94.76546523689113]
  We introduce CodePlan, a framework that generates and follows textcode-form plans -- pseudocode that outlines high-level, structured reasoning processes. CodePlan effectively captures the rich semantics and control flows inherent to sophisticated reasoning tasks. It achieves a 25.1% relative improvement compared with directly generating responses.
  arXiv  Detail & Related papers  (2024-09-19T04:13:58Z)
• Ask-before-Plan: Proactive Language Agents for Real-World Planning [68.08024918064503]
  Proactive Agent Planning requires language agents to predict clarification needs based on user-agent conversation and agent-environment interaction. We propose a novel multi-agent framework, Clarification-Execution-Planning (textttCEP), which consists of three agents specialized in clarification, execution, and planning.
  arXiv  Detail & Related papers  (2024-06-18T14:07:28Z)
• Probabilistically Correct Language-based Multi-Robot Planning using Conformal Prediction [11.614036749291216]
  We introduce a new distributed multi-robot planner called S-ATLAS for Safe plAnning for Teams of Language-instructed AgentS. We show that the proposed planner can achieve user-specified task success rates, assuming successful plan execution. We provide comparative experiments against related works showing that our method is significantly more computational efficient and achieves lower help rates.
  arXiv  Detail & Related papers  (2024-02-23T15:02:44Z)
• Consolidating Trees of Robotic Plans Generated Using Large Language Models to Improve Reliability [6.4111574364474215]
  The inherent probabilistic nature of Large Language Models (LLMs) introduces an element of unpredictability. This paper introduces an innovative approach aims to generate correct and optimal robotic task plans for diverse real-world demands and scenarios.
  arXiv  Detail & Related papers  (2024-01-15T18:01:59Z)
• 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)
• Planning as In-Painting: A Diffusion-Based Embodied Task Planning Framework for Environments under Uncertainty [56.30846158280031]
  Task planning for embodied AI has been one of the most challenging problems. We propose a task-agnostic method named 'planning as in-painting' The proposed framework achieves promising performances in various embodied AI tasks.
  arXiv  Detail & Related papers  (2023-12-02T10:07:17Z)
• Embodied Task Planning with Large Language Models [86.63533340293361]
  We propose a TAsk Planing Agent (TaPA) in embodied tasks for grounded planning with physical scene constraint. During inference, we discover the objects in the scene by extending open-vocabulary object detectors to multi-view RGB images collected in different achievable locations. Experimental results show that the generated plan from our TaPA framework can achieve higher success rate than LLaVA and GPT-3.5 by a sizable margin.
  arXiv  Detail & Related papers  (2023-07-04T17:58:25Z)
• Multimodal Contextualized Plan Prediction for Embodied Task Completion [9.659463406886301]
  Task planning is an important component of traditional robotics systems enabling robots to compose fine grained skills to perform more complex tasks. Recent work building systems for translating natural language to executable actions for task completion in simulated embodied agents is focused on directly predicting low level action sequences. We focus on predicting a higher level plan representation for one such embodied task completion dataset - TEACh.
  arXiv  Detail & Related papers  (2023-05-10T22:29:12Z)
• ProgPrompt: Generating Situated Robot Task Plans using Large Language Models [68.57918965060787]
  Large language models (LLMs) can be used to score potential next actions during task planning. We present a programmatic LLM prompt structure that enables plan generation functional across situated environments.
  arXiv  Detail & Related papers  (2022-09-22T20:29:49Z)
• Actions You Can Handle: Dependent Types for AI Plans [2.064612766965483]
  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.
  arXiv  Detail & Related papers  (2021-05-24T13:33:56Z)
• From Abstractions to Grounded Languages for Robust Coordination of Task Planning Robots [4.496989927037321]
  We study the automatic construction of languages that are maximally flexible while being sufficiently explicative for coordination. Our language expresses a plan for any given task as a "plan sketch" to convey just-enough details while maximizing the flexibility to realize it.
  arXiv  Detail & Related papers  (2019-05-01T22:05:42Z)

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.