Neurosymbolic · Safe Autonomy · Composition of Verified Cores

Detect, recover, or halt

An LLM proposes a route. A deterministic verifier checks it. On a fail, a provably-correct classical planner recovers a safe path, which is re-verified before anything moves. And when no safe path exists at all, the shield stops - because knowing the difference between "the model was wrong, here's the fix" and "there is no safe action" is what safe autonomy actually means.

View on GitHub Read the plain-language guide (PDF) Jump to results

38/38

flawed qwen2.5-7B proposals recovered with verified safe paths

unsafe fallbacks forwarded - the load-bearing zero, CI-enforced

10/10

sealed-goal cases halted instead of inventing a route

The keystone

This repository is the sentence that connects my other work: LLM planners fail in measurable ways (plan-failure-bench), so I detect those failures deterministically (the safety verifier) and recover with a path from a planner that is provably correct (the planning core) - or halt when no safe path exists. It is deliberately a composition of already-verified components, pinned as git submodules at exact commits: no new algorithms, just the full detect-and-recover loop, with every guarantee re-proven by CI on every push. The term shield follows the safe-RL usage of Alshiekh et al.

The forward gate is goal-aware: a proposal passes only if it is both verifier-safe and actually ends at the goal. That requirement exists because a dry run caught a real case - a qwen proposal that was perfectly safe and went nowhere near the goal. Safety and task-success stay separate judgments; the gate requires both, and the design change is documented in the pre-registration commit, made before any result was published.

The decision flow

Flowchart: LLM proposal enters the gate (verifier-safe and at the goal?); pass forwards to the controller; fail goes to the A* fallback on the inflated fine grid, whose result is re-verified by the verifier, the independent oracle, and a goal check before forwarding; no path means halt, and a failed re-verification is the load-bearing fallback_unsafe cell that CI keeps at zero — The whole system in one picture: two ways to a forwarded plan, one honest halt, and one red cell whose emptiness is the entire safety claim. The outcome names are the pre-registered buckets from the code; the counts live in the results below, not in the diagram.

The results

Bar charts: all 40 qwen proposals by outcome bucket, and the 10 sealed-goal variants all halting — All 40 committed qwen2.5:7b-instruct proposals, replayed deterministically - no model inference at evaluation time. Only 2 were both safe and goal-reaching; 38 were recovered; nothing unsafe was forwarded. The halt suite seals the goal so no safe path exists, and all 10 correctly halt.

Map showing a rejected unsafe qwen path in red beside the shield's verified recovery path in green — Detect and recover, from committed data: the model's proposal (red) wanders off the map through walls; the shield rejects it, plans on the fine-resolution truth, re-verifies with two independent judges plus a goal check, and forwards the green path instead. Median decision time: 0.48 ms.

Map with the goal sealed inside a ring of obstacles; the model's short stub path is shown and the shield halts — The branch almost no demo has: the goal is sealed, the model's plan is safe but useless, and the shield halts rather than forwarding it or inventing a route. Any other outcome here fails CI.

Discipline, same as every project on this site: the outcome taxonomy was committed before the first published results, every number above is quoted from the tool's output, the figures are rendered from the evaluation's own committed artifacts, and CI replays the entire evaluation - failing on any unsafe fallback or any sealed-goal case that doesn't halt.