将生成式规划器锚定于可验证逻辑：面向可信具身 AI 的混合架构

大语言模型（LLM）作为具身 AI 的规划器展现出前景，但其随机性缺乏形式化推理，无法为物理部署提供严格的安全保证。当前方法通常依赖不可靠的 LLM 进行安全检查，或只是拒绝不安全计划而不提供修复。我们提出可验证迭代细化框架（VIRF），一种神经符号架构，将范式从被动安全把关转变为主动协作。我们的核心贡献是一种导师-学徒对话：基于形式化安全本体的确定性 Logic Tutor 向 LLM 规划器提供因果性与教学性反馈。这使智能化的计划修复成为可能，而不仅仅是回避。我们还提出一个可扩展的知识获取流水线，从真实世界文档合成安全知识库，纠正现有基准中的盲点。在具有挑战性的家庭安全任务中，VIRF 达到完美的 0% 危险行为率（HAR）和 77.3% 的目标条件达成率（GCR），在所有基线中为最高。它非常高效，平均只需 1.1 次纠正迭代。VIRF 展示了一条构建根本可信且可验证安全的具身智能体的有原则的路径。