pith. sign in

arxiv: 2602.08373 · v1 · submitted 2026-02-09 · 💻 cs.AI · cs.LG

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

Feiyu Wu , Xu Zheng , Yue Qu , Zhuocheng Wang , Zicheng Feng , Hui Li This is my paper

Pith reviewed 2026-05-16 06:00 UTC · model grok-4.3

classification 💻 cs.AI cs.LG
keywords neuro-symbolic planningLLM plannersembodied AI safetyformal safety ontologyiterative refinementverifiable AIhome roboticsplan repair
0
0 comments X

The pith

A hybrid architecture pairs an LLM planner with a deterministic logic tutor to repair plans and eliminate hazardous actions in embodied tasks.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces the Verifiable Iterative Refinement Framework to address the lack of formal safety guarantees in LLM-based planners for robots. It establishes a tutor-apprentice dialogue in which a deterministic Logic Tutor, grounded in a formal safety ontology, supplies causal and pedagogical feedback that lets the LLM repair unsafe plans instead of simply rejecting them. A sympathetic reader would care because stochastic LLM outputs currently prevent reliable physical deployment in settings like homes, and existing methods either rely on the same unreliable models for checks or offer no repairs. The work also supplies a pipeline to synthesize safety knowledge bases from real documents, filling gaps in standard benchmarks. Experiments on home safety tasks show the approach reaches zero hazardous actions while preserving high goal completion with minimal corrections.

Core claim

The central claim is that the Verifiable Iterative Refinement Framework (VIRF) shifts embodied AI planning from passive safety gatekeeping to active collaboration. A deterministic Logic Tutor grounded in a formal safety ontology engages in tutor-apprentice dialogue with an LLM planner, delivering causal and pedagogical feedback that enables targeted plan repairs. This architecture, combined with a scalable pipeline for building safety knowledge bases from documents, produces zero hazardous action rates and the highest goal-condition rates among tested baselines on challenging home safety tasks, using an average of only 1.1 correction iterations.

What carries the argument

The Verifiable Iterative Refinement Framework (VIRF) and its tutor-apprentice dialogue, in which a deterministic Logic Tutor grounded in a formal safety ontology supplies causal and pedagogical feedback to guide LLM plan repairs.

If this is right

  • Embodied agents can be deployed in homes with guaranteed absence of hazardous actions rather than probabilistic safety.
  • Safety enforcement moves from rejection-only gates to collaborative repair, preserving more usable plans.
  • Safety knowledge bases can be generated at scale from existing documents instead of relying on limited manual benchmarks.
  • Plan generation requires only about one correction round on average, keeping computational cost low while meeting safety criteria.
  • The neuro-symbolic pattern supplies a concrete route toward verifiably safe rather than merely statistically safe embodied AI.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same tutor-apprentice structure could be adapted to other safety-critical domains such as autonomous driving or medical robotics by swapping the underlying ontology.
  • The document-synthesis pipeline offers a general method for correcting blind spots in any benchmark that currently under-represents real-world constraints.
  • Combining VIRF-style feedback with existing robot simulators would allow direct measurement of whether simulated safety transfers to physical hardware.
  • If the logic tutor is extended with richer temporal or probabilistic reasoning, the framework might support safety properties beyond simple hazard avoidance.

Load-bearing premise

The deterministic Logic Tutor grounded in a formal safety ontology can always supply accurate feedback that repairs plans without introducing new errors or missing safety violations.

What would settle it

A test set of home safety scenarios in which the Logic Tutor either misses a hazardous action or recommends a repair that creates a new hazard would show the framework fails to deliver verifiable safety.

Figures

Figures reproduced from arXiv: 2602.08373 by Feiyu Wu, Hui Li, Xu Zheng, Yue Qu, Zhuocheng Wang, Zicheng Feng.

Figure 1
Figure 1. Figure 1: The architecture of the Verifiable Iterative Refinement Framework (VIRF). Instead of direct exe￾cution, 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 p… view at source ↗
Figure 2
Figure 2. Figure 2: The Traceable Axiom Synthesis workflow, a semi-automated, human-in-the-loop process for build￾ing 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, … view at source ↗
Figure 3
Figure 3. Figure 3: A side-by-side comparison revealing the evaluation blind spot. (a) The distribution of [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Performance Quadrant Plots. VIRF (triangles) consistently achieves the ideal perfor [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗
Figure 5
Figure 5. 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. B.2 COMPOSITIONAL AND LAYER… view at source ↗
Figure 6
Figure 6. Figure 6: The protocol for hierarchical concept classification uses an LLM to propose the placement [PITH_FULL_IMAGE:figures/full_fig_p029_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The multi-threaded verification architecture designed to accelerate the validation of a [PITH_FULL_IMAGE:figures/full_fig_p031_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: A concrete example of the Verifiable Iterative Refinement loop. The Logic Tutor provides [PITH_FULL_IMAGE:figures/full_fig_p036_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Distribution of processing times for the two perception pipelines across 30 scenes. The vi [PITH_FULL_IMAGE:figures/full_fig_p041_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Visual input for the Chemical Mixture Hazard scenario. [PITH_FULL_IMAGE:figures/full_fig_p042_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Visual input for the Child Safety Hazard scenario, where the most critical risk is nuanced [PITH_FULL_IMAGE:figures/full_fig_p044_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Visual input for the Hot Oil Splatter Hazard scenario. [PITH_FULL_IMAGE:figures/full_fig_p045_12.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript introduces the Verifiable Iterative Refinement Framework (VIRF), a neuro-symbolic architecture for embodied AI planning. An LLM planner collaborates iteratively with a deterministic Logic Tutor grounded in a formal safety ontology that is synthesized from real-world documents via a scalable knowledge-acquisition pipeline. The central claim is that this tutor-apprentice dialogue enables causal and pedagogical feedback for plan repair, yielding a perfect 0% Hazardous Action Rate (HAR) and 77.3% Goal-Condition Rate (GCR) on challenging home-safety tasks—outperforming all baselines—while requiring only 1.1 correction iterations on average.

Significance. If the empirical claims hold under broader scrutiny, the work provides a concrete, verifiable pathway from stochastic LLM planning to safety-guaranteed embodied agents. The document-synthesis pipeline for constructing the safety ontology is a practical contribution that could mitigate benchmark blind spots, and the low iteration count demonstrates efficiency. These elements together address a core reliability gap in current generative planners for physical deployment.

major comments (2)
  1. [Evaluation] Evaluation section: The headline 0% HAR result is load-bearing for the claim of 'verifiably safe' agents, yet the reported experiments use only benchmarks aligned with the synthesized ontology. No stress-test cases (e.g., implicit, context-dependent, or low-frequency hazards absent from the document pipeline) are described, leaving open whether the perfect score reflects ontology completeness or benchmark distribution.
  2. [Results] Methodology and results: The definitions and measurement protocols for HAR and GCR are not explicitly linked to the formal ontology in the reported tables or figures. Without an ablation that isolates the tutor's feedback accuracy (e.g., false-negative rate on held-out hazards), it is impossible to confirm that the Logic Tutor supplies complete causal feedback rather than merely avoiding the hazards present in the test distribution.
minor comments (2)
  1. [Abstract] Abstract: The phrase 'challenging home safety tasks' should be accompanied by a brief reference to the specific benchmark or task distribution to allow readers to assess scope immediately.
  2. [Architecture] Notation: The distinction between the synthesized safety knowledge base and the runtime Logic Tutor could be clarified with a single diagram or pseudocode block early in the architecture section.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on our manuscript. We address each major comment below, providing clarifications where possible and indicating planned revisions to strengthen the presentation of our results.

read point-by-point responses

  1. Referee: [Evaluation] Evaluation section: The headline 0% HAR result is load-bearing for the claim of 'verifiably safe' agents, yet the reported experiments use only benchmarks aligned with the synthesized ontology. No stress-test cases (e.g., implicit, context-dependent, or low-frequency hazards absent from the document pipeline) are described, leaving open whether the perfect score reflects ontology completeness or benchmark distribution.

    Authors: The evaluation deliberately uses benchmarks for which the safety ontology—synthesized via our document pipeline—provides complete coverage of the relevant hazards. This design isolates the contribution of the iterative tutor-apprentice dialogue in achieving zero hazardous actions under full ontology alignment. We agree that the absence of explicit stress tests on implicit or low-frequency hazards outside the pipeline leaves open questions about generalization. In the revised manuscript we will add a dedicated limitations subsection in the evaluation that discusses ontology scope, acknowledges this boundary condition, and outlines a protocol for future stress testing using supplementary documents or synthetic scenarios. revision: partial

  2. Referee: [Results] Methodology and results: The definitions and measurement protocols for HAR and GCR are not explicitly linked to the formal ontology in the reported tables or figures. Without an ablation that isolates the tutor's feedback accuracy (e.g., false-negative rate on held-out hazards), it is impossible to confirm that the Logic Tutor supplies complete causal feedback rather than merely avoiding the hazards present in the test distribution.

    Authors: We will revise the methods section and figure/table captions to explicitly connect HAR and GCR to the formal ontology by describing how hazardous actions are identified through predicate violations and how goal conditions are verified against the ontology state. The reported 0% HAR already implies that the tutor produced no false negatives on the evaluated distribution. We will add clarifying text on the measurement protocol and note that a dedicated ablation on held-out hazards would require additional data collection. This point will be listed as an important avenue for future work rather than claimed as already demonstrated. revision: partial

Circularity Check

0 steps flagged

No significant circularity; empirical results independent of framework inputs

full rationale

The VIRF architecture defines a deterministic Logic Tutor grounded in a synthesized safety ontology that supplies causal feedback to an LLM planner for iterative repairs. The reported 0% HAR and 77.3% GCR are presented as measured outcomes on home safety tasks, not as quantities derived by construction from the ontology or pipeline. The document-synthesis pipeline is an external knowledge-acquisition step whose completeness is an empirical assumption, not a definitional identity. No self-citations, fitted parameters relabeled as predictions, uniqueness theorems, or ansatz smuggling appear in the derivation chain. The central claims therefore remain self-contained against the external task benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claim rests on the effectiveness of the tutor-apprentice interaction and the completeness of the synthesized safety knowledge base.

axioms (1)
  • domain assumption The safety ontology provides complete and accurate coverage of hazardous actions in home environments.
    The framework relies on this for the logic tutor to function correctly.
invented entities (2)
  • Verifiable Iterative Refinement Framework (VIRF) no independent evidence
    purpose: Hybrid architecture for safe planning
    Newly introduced system.
  • Logic Tutor no independent evidence
    purpose: Provides deterministic feedback based on formal ontology
    Core component of the new architecture.

pith-pipeline@v0.9.0 · 5519 in / 1295 out tokens · 30480 ms · 2026-05-16T06:00:56.615237+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages · 1 internal anchor

  1. [1]

    B Cuenca Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler

    URLhttps://arxiv.org/abs/2011.15091. B Cuenca Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler. Modular reuse of ontologies: Theory and practice.Journal of Artificial Intelligence Research, 31:273–318, 2008. 14 Published as a conference paper at ICLR 2026 Na Hong, Guoqian Jiang, Jyotishiman Pathak, and Christopher G Chute. A pilot study on modeling...

    work page arXiv 2011

  2. [2]

    Visual Genome: Connecting Language and Vision Using Crowdsourced Dense Image Annotations

    URLhttps://arxiv.org/abs/1602.07332. Christine P Lee, David Porfirio, Xinyu Jessica Wang, Kevin Chenkai Zhao, and Bilge Mutlu. Veri- plan: Integrating formal verification and llms into end-user planning. InProceedings of the 2025 CHI Conference on Human Factors in Computing Systems, pp. 1–19, 2025. Douglas B Lenat. Cyc: A large-scale investment in knowled...

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.1109/cvpr52733.2024.02652 2025

  3. [3]

    UnsafeMicrowaveUsage

    The Setup: Axioms, World State, and Plan.The verification process begins with three key inputs: •The Safety Axiom (in TBoxT):A key safety rule defines what constitutes unsafe mi- crowave usage. The following OWL 2 axiom states that an “UnsafeMicrowaveUsage” is a Microwavethat is in anOnStateand contains an object made ofMetal. ABox Representation <owl:equ...

    work page 2026

  4. [5]

    pick(TestPot_Action)

    work page

  5. [6]

    find(TestMicrowave_Action)

    work page

  6. [7]

    open(TestMicrowave_Action)

    work page

  7. [8]

    put_in(TestPot_Action, TestMicrowave_Action)

    work page

  8. [9]

    close(TestMicrowave_Action)

    work page

  9. [10]

    turn_on(TestMicrowave_Action)

    work page

  10. [11]

    For each stepi, it first performsAction Executionby applying the effects of actiona i to a persistent temporary world stateA ′

    The Verification Loop in Action.The verifier iterates through the plan. For each stepi, it first performsAction Executionby applying the effects of actiona i to a persistent temporary world stateA ′. It then performsAction Instantiationby simulating the effects of thenextaction,a i+1, on a non-persistent copy ofA ′ to predict future hazards. For simplicit...

    work page 2026

  11. [12]

    From ABox:TestMicrowave Actionis aMicrowave

    work page

  12. [13]

    From Action Effect:TestMicrowave ActionnowhasState OnState

    work page

  13. [14]

    From ABox (Step 5):TestMicrowave Action contains TestPot Action

    work page

  14. [15]

    5.From TBox (the general axiom): The reasoner infers that because TestPot Actionis aPot, it musthasMaterial Metal

    From ABox:TestPot Actionis aPot. 5.From TBox (the general axiom): The reasoner infers that because TestPot Actionis aPot, it musthasMaterial Metal. With all three conditions from the safety axiom now met, the reasoner automati- cally classifies the instanceTestMicrowave Actionas a member of the class UnsafeMicrowaveUsage. – Result:The functioncheck for un...

    work page

  15. [16]

    status":

    The Outcome.The verifier constructs a detailed feedback dictionary, as described in the next section. The report will pinpoint step 7 as the failure point, citeUnsafeMicrowaveUsageas the violated concept, and list the crucial facts (the microwave being on, the pot being inside it, and the pot being metal) as the root cause. E.3 STRUCTUREDFEEDBACK FOR THEL...

    work page 2026

  16. [17]

    Initial Plan (Apprentice)

    work page

  17. [18]

    pick up Pot 1 (Material: Metal)

    work page

  18. [19]

    put Pot 1 in Microwave 1

    work page

  19. [20]

    toggle Microwave 1 on←Hazardous Action (Fire Risk)

    work page

  20. [21]

    Metal objects in active microwaves cause fire hazards

    Logic Tutor Feedback (Diagnostic Report) Verdict:UNSAFE Violation:UnsafeMicrowaveUsage Causal Explanation:The plan causes a hazard becauseMicrowave 1is active (State: On) while containingPot 1which has propertyMaterial: Metal. Metal objects in active microwaves cause fire hazards

    work page

  21. [22]

    I see. The metal pot cannot go in the microwave. I need a non-metal container

    Refined Plan (Apprentice) “I see. The metal pot cannot go in the microwave. I need a non-metal container. ”

    work page

  22. [23]

    pour soup from Pot 1 to GlassBowl 1←Adaptive Correction

    work page

  23. [24]

    put GlassBowl 1 in Microwave 1

    work page

  24. [25]

    Use the cleaners available

    toggle Microwave 1 on←Verified Safe Figure 8: A concrete example of the Verifiable Iterative Refinement loop. The Logic Tutor provides causal feedback linking object attributes (Metal) to consequences (Fire), enabling the Apprentice to generate a logically sound correction (switching containers) rather than abandoning the task. contextual hint to the inst...

    work page 2022