T3 Planner
An LLM proposes robot waypoints and controller code, a temporal-logic checker scores them, and failures go back until a plan passes.
The loop
- Proposes
Subgoal waypoints, timed waypoints and a Python controller script, written by an LLM in three stages
- Judged by
Signal Temporal Logic robustness checks, a Python syntax check, and simulation of the controller on annotated cases
- Steers
A failed output goes back to the LLM as the previous failed result, until all checks pass
Headline result
In simulated household, chip-design and navigation scenarios, success rates with GPT-4o were 91.65%, 91.60% and 83.69%, against 56.67%, 61.29% and 50.00% for AutoTAMP with GPT-4o. The authors claim a 30 to 40% improvement.
What this does not prove
All scenarios are in a simulated 2D environment with no real-robot tests, and the paper gives no retry limit. The checker is a temporal-logic verifier, not model predictive control, and this is a single preprint with no venue listed.
How it generalizes the harness
A formal temporal-logic verifier, not an LLM judge, decides whether each proposed plan is valid.
Classification
| What it proposes | Program |
|---|---|
| Generative model | Pretrained LLMs (GPT-4o, DeepSeek-reasoner, Gemini-2.5-Pro), plus a distilled Qwen3-4B |
| Algorithmic authority | Signal Temporal Logic robustness computation and simulation of the generated controller |
| Feedback | Verifier errors |
| What gets updated | Prompt context |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |