Can LLMs Prove Robotic Path Planning Optimality? A Benchmark for Research-Level Algorithm Verification

Abstract

Robotic path planning problems are often NP-hard, and practical solutions typically rely on approximation algorithms with provable performance guarantees for general cases. While designing such algorithms is challenging, formally proving their approximation optimality is even more demanding, which requires domain-specific geometric insights and multi-step mathematical reasoning over complex operational constraints. Recent Large Language Models (LLMs) have demonstrated strong performance on mathematical reasoning benchmarks, yet their ability to assist with research-level optimality proofs in robotic path planning remains under-explored. In this work, we introduce the first benchmark for evaluating LLMs on approximation-ratio proofs of robotic path planning algorithms. The benchmark consists of 34 research-grade proof tasks spanning diverse planning problem types and complexity levels, each requiring structured reasoning over algorithm descriptions, problem constraints, and theoretical guarantees. Our evaluation of state-of-the-art proprietary and open-source LLMs reveals that even the strongest models struggle to produce fully valid proofs without external domain knowledge. However, providing LLMs with task-specific in-context lemmas substantially improves reasoning quality, a factor that is more effective than generic chain-of-thought prompting or supplying the ground-truth approximation ratio as posterior knowledge. We further provide fine-grained error analysis to characterize common logical failures and hallucinations, and demonstrate how each error type can be mitigated through targeted context augmentation.

Figures (3)

• Figure 1: LLM proof generation pipeline. The LLM receives a path-planning problem $\mathcal{T}$ and algorithm $\mathcal{A}$, along with optional in-context lemmas and theorems $\mathcal{C}$. It is then prompted (optionally) with a Chain-of-Thought style instruction) to generate the approximation ratio $\hat{\alpha}$ and a corresponding proof $\hat{y}$, both evaluated against ground-truth references. When ground-truth $\alpha^*$ is also provided as part of the input, the task reduces to generating reasoning $\hat{y}$ proving how the given $\alpha^*$ is derived.
• Figure 2: An Example Comparison of a Path Planning Optimality Proof vs. a Generic Math Inequality Proof.
• Figure 3: Distribution of the reasoning errors occurring in Setting 1.