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

Titel: Kunnen LLM's de optimaliteit van robotische padplanning bewijzen? Een benchmark voor verificatie van algoritmen op onderzoeksniveau.

1. Probleemstelling

Robotische padplanningsproblemen zijn vaak NP-hard. In de praktijk vertrouwen oplossingen daarom op benaderingsalgoritmen met bewezen prestatiegaranties (approximatie-ratio's). Hoewel het ontwerpen van dergelijke algoritmen uitdagend is, is het formeel bewijzen van hun optimaliteit nog veel veeleisender. Dit vereist:

• Domeinspecifieke geometrische inzichten.
• Meestaps wiskundig redeneren over complexe operationele beperkingen (zoals energielimieten, tijdslimieten of terreinrestricties).
• Het verbinden van concrete taakbeschrijvingen met abstracte wiskundige voorwaarden.

Hoewel Large Language Models (LLM's) sterke prestaties laten zien op algemene wiskundige redeneerbenchmarks (zoals MATH of GSM8K), is hun vermogen om onderzoeksniveau-bewijzen te genereren voor robotische padplanning nog onvoldoende onderzocht. De kernvraag is of LLM's de complexiteit van deze specifieke, context-gebonden bewijzen aankanen zonder menselijke expertise.

2. Methodologie en Benchmark

De auteurs introduceren de eerste benchmark specifiek gericht op het evalueren van LLM's in het bewijzen van approximatie-ratio's voor robotische padplanning.

• Dataset: De benchmark bestaat uit 34 onderzoekskwaliteit bewijstaken, ontleend aan 11 gepubliceerde, peer-reviewed robotica-papers. Deze dekken diverse probleemtypes:
  • Energie-besparende navigatie.
  • Routen met perceptie-beperkingen.
  • Tijd-kritieke missies.
  • Werklastbalancering voor multi-robot systemen.
• Taakdefinitie: Het model moet bewijzen dat de kosten van een gegeven algoritme $A$ voor een probleem $T$ hoogstens $\alpha$ keer de kosten van de optimale oplossing zijn.
• Evaluatie Settings: De modellen werden getest onder vier verschillende informatie-scenario's:
  1. Setting 1 (Geen context): Alleen probleem- en algoritmebeschrijving.
  2. Setting 2 (Context-augmentatie): Toevoeging van domeinspecifieke lemmata en theorema's uit de bron.
  3. Setting 3 (Posterior-augmentatie): Toevoeging van de grond-waarheid approximatie-ratio ($\alpha$), maar geen lemmata.
  4. Setting 4 (Combinatie): Zowel lemmata als de grond-waarheid ratio.
• Modellen: Er zijn state-of-the-art modellen getest, waaronder GPT-5.2, Gemini 3 Pro, Grok 4.1 en Qwen3.5 (open-source).
• Evaluatiemetrics: Een "LLM-as-Judge" (GPT-5.2) evalueerde de gegenereerde bewijzen op drie schalen (1-10):
  • Final Answer: Nauwkeurigheid van de ratio.
  • Reasoning Correctness: Logische geldigheid van de afleiding.
  • Proof Relevance: Hoe goed het bewijs gebaseerd is op de gegeven context (geen hallucinaties).

3. Belangrijkste Resultaten

• Moeite zonder externe kennis: Zelfs de sterkste modellen worstelen om geldige bewijzen te produceren zonder domeinkennis (Setting 1). De succesratio (score $\ge$ 7) lag slechts rond de 26% voor de beste modellen (GPT-5.2) en lager voor anderen.
• Impact van In-Context Lemmata: Het verstrekken van taak-specifieke lemmata (Setting 2) leidt tot de grootste verbetering in bewijskwaliteit. Dit effect is sterker dan het verstrekken van de grond-waarheid ratio (Setting 3) of het gebruik van generieke "Chain-of-Thought" (CoT) prompts.
  • Opmerkelijk: Het open-source model Qwen3.5 presteerde in Setting 2 zelfs beter dan de gesloten bron modellen, wat wijst op een groot latent vermogen dat wordt vrijgemaakt door domeinspecifieke begeleiding.
• Rol van Posterior Informatie: Het geven van de juiste ratio (Setting 3) helpt, maar alleen als het model al door lemmata is "geankerd" (Setting 4). De ratio fungeert dan als een consistentiecheck die het model helpt om niet af te dwalen, maar vervangt geen domeinkennis.
• Chain-of-Thought (CoT): Generieke CoT-prompting alleen vermindert de taakmoeilijkheid niet significant. Het biedt echter een complementair voordeel wanneer gecombineerd met posterior kennis.
• Foutanalyse:
  • De meest voorkomende fouten zijn logische fouten (zoals onondersteunde inferenties en oversimplificatie) en hallucinaties (het invoegen van onterechte aannames).
  • Zonder context ontstaan fouten vroeg in het bewijsproces (gemiddeld bij ~24% van de bewijslengte).
  • Met context verschuift de eerste fout naar later in het proces (~30%+), wat aangeeft dat domeinkennis helpt om coherentie langer vol te houden.
  • Er is een sterke negatieve correlatie tussen de positie van de eerste fout en de algehele bewijskwaliteit: vroege fouten leiden tot cascade-fouten.

4. Kernbijdragen

1. Eerste Benchmark: Introductie van de eerste gestructureerde benchmark voor het evalueren van LLM's op het gebied van bewijzen van approximatie-optimaliteit voor robotica.
2. Empirische Inzichten: Het aantonen dat LLM's domeinspecifieke kennis (lemmata) nodig hebben om complexe wiskundige bewijzen te genereren, en dat generieke redeneerstrategieën onvoldoende zijn voor dit niveau van complexiteit.
3. Fouttaxonomie: Een gedetailleerde analyse van logische fouten versus hallucinaties en de identificatie van structurele faalpatronen (bijv. het verkeerd interpreteren van probleemdefinities of het niet controleren van precondities van lemmata).
4. Openbare Tooling: De auteurs maken een geautomatiseerde pipeline vrij om padplanning-algoritmen uit onderzoekspapers te extraheren en te formaliseren, wat toekomstig onderzoek faciliteert.

5. Significantie en Toekomstperspectief

De studie concludeert dat LLM's momenteel nog niet in staat zijn om autonome, volledige bewijzen te leveren voor onderzoeksproblemen in robotische padplanning zonder menselijke input in de vorm van domeinkennis. De grootste barrière is niet het ontbreken van wiskundige vaardigheden, maar het gebrek aan contextuele binding aan specifieke operationele beperkingen en geometrische inzichten.

Toekomstige richtingen die door de auteurs worden voorgesteld:

• Multimodale Integratie: Het gebruik van Vision-Language Models (VLM's) om geometrische structuren (zoals zichtcones of tours) visueel te verifiëren en logische fouten in ruimtelijke redenering te verminderen.
• Herbruikbare Kennisbibliotheken: Het opbouwen van gestandaardiseerde bibliotheken met lemmata en bewijs-schema's die specifiek zijn voor robotica en meetkunde.
• Bewijs-bewust Training: Het trainen van modellen met straffen voor onondersteunde inferenties en het belonen van het correct citeren van lemmata, mogelijk ondersteund door een "LLM-as-Judge" die tussentijdse claims verifieert tijdens het generatieproces.

Samenvattend biedt dit paper een realistisch beeld van de huidige grenzen van AI in wetenschappelijk bewijsvoering en schetst een pad naar hoe domeinspecifieke kennisintegratie deze grenzen kan verleggen.