Grounding Generative Planners in Verifiable Logic: A Hybrid Architecture for Trustworthy Embodied AI

TL;DR

This paper tackles the safety challenges of planning with stochastic Large Language Models in embodied AI by grounding a generative planner in a formal symbolic framework. It introduces the Verifiable Iterative Refinement Framework (VIRF), composed of a Logic Tutor (OWL 2 DL-based verifier), a rich perception pipeline (VLM-Cascade), and a scalable knowledge-acquisition workflow (Traceable Axiom Synthesis), enabling plan repair via a pedagogical dialogue rather than mere rejection. The approach delivers a perfect $0\%$ Hazardous Action Rate (HAR) and a high Task Efficacy with a $77.3\%$ Goal-Condition Rate (GCR) on SafeAgentBench, while maintaining efficiency through parallel verification and a tutoring loop that teaches the planner. By bridging evaluation blind spots with real-world safety axioms and demonstrating robustness to perception noise and planner scaling, VIRF provides a principled pathway toward trustworthy, verifiable autonomy in embodied agents.

Abstract

Large Language Models (LLMs) show promise as planners for embodied AI, but their stochastic nature lacks formal reasoning, preventing strict safety guarantees for physical deployment. Current approaches often rely on unreliable LLMs for safety checks or simply reject unsafe plans without offering repairs. We introduce the Verifiable Iterative Refinement Framework (VIRF), a neuro-symbolic architecture that shifts the paradigm from passive safety gatekeeping to active collaboration. Our core contribution is a tutor-apprentice dialogue where a deterministic Logic Tutor, grounded in a formal safety ontology, provides causal and pedagogical feedback to an LLM planner. This enables intelligent plan repairs rather than mere avoidance. We also introduce a scalable knowledge acquisition pipeline that synthesizes safety knowledge bases from real-world documents, correcting blind spots in existing benchmarks. In challenging home safety tasks, VIRF achieves a perfect 0 percent Hazardous Action Rate (HAR) and a 77.3 percent Goal-Condition Rate (GCR), which is the highest among all baselines. It is highly efficient, requiring only 1.1 correction iterations on average. VIRF demonstrates a principled pathway toward building fundamentally trustworthy and verifiably safe embodied agents.

Figures (13)

• Figure 1: The architecture of the Verifiable Iterative Refinement Framework (VIRF). Instead of direct execution, an LLM planner's actions are verified in a symbolic sandbox against a formal knowledge base. The framework's core is the Logic Tutor feedback loop, which provides three distinct responses: approval for safe plans, clarification questions for UNKNOWN states, and a structured diagnostic report for unsafe plans. This report enables a pedagogical dialogue, teaching the LLM Linguistic Apprentice how to refine its plan and avoid hazards.
• Figure 2: The Traceable Axiom Synthesis workflow, a semi-automated, human-in-the-loop process for building the TBox from unstructured texts. The workflow consists of three main phases: (a) RAG Preparation, where authoritative documents are vectorized and indexed; (b) Offline Preparation, where the base ontology (BFO) is also vectorized to create a semantic vocabulary index; and (c) the Interactive Extraction Loop, where an expert queries the system. In this loop, an LLM drafts candidate OWL axioms based on retrieved evidence, which are then semantically normalized using the vectorized vocabulary before a final expert audit. This ensures every axiom is both formally sound and directly traceable to its source document.
• Figure 3: A side-by-side comparison revealing the evaluation blind spot. (a) The distribution of unsafe tasks in SafeAgentBench's kitchen scenarios is concentrated in a few simple categories. (b) Our RAG-synthesized knowledge base is significantly richer and more diverse, covering critical real-world domains like food safety and chemical hazards that are absent from the benchmark.
• Figure 4: Performance Quadrant Plots. VIRF (triangles) consistently achieves the ideal performance—low hazardous actions (HAR) with high task success (GCR) in (a), and a balanced safety mechanism (low FPR/FNR) in (b)—across all planner scales, unlike scattered baselines.
• Figure 5: The layered and compositional architecture of our RobotSafety-Ontology. It is structured into Core, Domain, and Scenario layers to enable logical rigor and reusability. The Core layer is grounded in BFO, while the Domain layer implements a compositional modeling strategy, linking abstract material types to attribute properties for robust zero-shot generalization of safety rules.