Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SafePlan: Leveraging Formal Logic and Chain-of-Thought Reasoning for Enhanced Safety in LLM-based Robotic Task Planning

Ike Obi, Vishnunandan L. N. Venkatesh, Weizheng Wang, Ruiqi Wang, Dayoon Suh, Temitope I. Amosa, Wonse Jo, Byung-Cheol Min

TL;DR

SafePlan addresses safety challenges in LLM-guided robotic task planning by integrating formal logic with chain-of-thought reasoning. It introduces a Prompt Sanity Checking COT Reasoner with Societal, Organizational, and Individual Alignment Layers and an Invariant COT Reasoner using Linear Temporal Logic to generate and verify invariants, preconditions, and postconditions. Through a 621-prompt benchmark and AI2-THOR simulations, SafePlan achieves a $90.5\%$ reduction in harmful prompt acceptance while maintaining safe task acceptance, demonstrating improved discrimination across task domains and complexities. The work highlights a practical pathway to safer real-world LLM-enabled robotics by pruning unsafe prompts early and ensuring plan integrity via formal verification.

Abstract

Robotics researchers increasingly leverage large language models (LLM) in robotics systems, using them as interfaces to receive task commands, generate task plans, form team coalitions, and allocate tasks among multi-robot and human agents. However, despite their benefits, the growing adoption of LLM in robotics has raised several safety concerns, particularly regarding executing malicious or unsafe natural language prompts. In addition, ensuring that task plans, team formation, and task allocation outputs from LLMs are adequately examined, refined, or rejected is crucial for maintaining system integrity. In this paper, we introduce SafePlan, a multi-component framework that combines formal logic and chain-of-thought reasoners for enhancing the safety of LLM-based robotics systems. Using the components of SafePlan, including Prompt Sanity COT Reasoner and Invariant, Precondition, and Postcondition COT reasoners, we examined the safety of natural language task prompts, task plans, and task allocation outputs generated by LLM-based robotic systems as means of investigating and enhancing system safety profile. Our results show that SafePlan outperforms baseline models by leading to 90.5% reduction in harmful task prompt acceptance while still maintaining reasonable acceptance of safe tasks.

SafePlan: Leveraging Formal Logic and Chain-of-Thought Reasoning for Enhanced Safety in LLM-based Robotic Task Planning

TL;DR

SafePlan addresses safety challenges in LLM-guided robotic task planning by integrating formal logic with chain-of-thought reasoning. It introduces a Prompt Sanity Checking COT Reasoner with Societal, Organizational, and Individual Alignment Layers and an Invariant COT Reasoner using Linear Temporal Logic to generate and verify invariants, preconditions, and postconditions. Through a 621-prompt benchmark and AI2-THOR simulations, SafePlan achieves a reduction in harmful prompt acceptance while maintaining safe task acceptance, demonstrating improved discrimination across task domains and complexities. The work highlights a practical pathway to safer real-world LLM-enabled robotics by pruning unsafe prompts early and ensuring plan integrity via formal verification.

Abstract

Robotics researchers increasingly leverage large language models (LLM) in robotics systems, using them as interfaces to receive task commands, generate task plans, form team coalitions, and allocate tasks among multi-robot and human agents. However, despite their benefits, the growing adoption of LLM in robotics has raised several safety concerns, particularly regarding executing malicious or unsafe natural language prompts. In addition, ensuring that task plans, team formation, and task allocation outputs from LLMs are adequately examined, refined, or rejected is crucial for maintaining system integrity. In this paper, we introduce SafePlan, a multi-component framework that combines formal logic and chain-of-thought reasoners for enhancing the safety of LLM-based robotics systems. Using the components of SafePlan, including Prompt Sanity COT Reasoner and Invariant, Precondition, and Postcondition COT reasoners, we examined the safety of natural language task prompts, task plans, and task allocation outputs generated by LLM-based robotic systems as means of investigating and enhancing system safety profile. Our results show that SafePlan outperforms baseline models by leading to 90.5% reduction in harmful task prompt acceptance while still maintaining reasonable acceptance of safe tasks.

Paper Structure

This paper contains 29 sections, 14 equations, 4 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Related Works
  3. LLM Models and Safety Reasoning
  4. LLM-Based Robot Systems
  5. Preliminaries
  6. Problem Formulation
  7. Methods
  8. Prompt Sanity Checking COT Reasoner
  9. Societal Alignment Layer
  10. Obligatory
  11. Permissible by Default
  12. Organizational Alignment Layer
  13. Obligatory
  14. Permissible by Default
  15. Individual Alignment Layer
  16. ...and 14 more sections

Figures (4)

  • Figure 1: A conceptual image of the SafePlan framework screening a prompt for safety profile.
  • Figure 2: A system diagram of the SafePlan framework.
  • Figure 3: Overview of the AI2-THOR simulation environment used to evaluate the SafePlan framework. Blue circles denote robots navigating diverse indoor settings (e.g., kitchen, living room, bedroom, and bathroom) as part of a curated benchmark of error-prone tasks.
  • Figure 4: Comparison of acceptance rates for safe and unsafe requests across three models (Gemini 1.5 Pro, GPT4o, and Gemini Flash 2.0), with or without SafePlan. Bars represent the percentage of requests accepted under each condition.