Große Sprachmodelle können Ihre Reisen rigoros mit formalen Verifikationstools planen

Die jüngsten Fortschritte großer Sprachmodelle (LLMs) mit ihrem umfangreichen Weltwissen und ihren Fähigkeiten im Umgang mit Werkzeugen und beim logischen Denken haben zahlreiche LLM-Planungsalgorithmen gefördert. Allerdings haben LLMs bisher nicht gezeigt, dass sie komplexe kombinatorische Optimierungsprobleme genau lösen können. In Xie et al. (2024) schlugen die Autoren TravelPlanner vor, einen Benchmark für die Reiseplanung im Inland der USA, und zeigten, dass LLMs selbst keine Reisepläne erstellen können, die die Benutzeranforderungen mit einer besten Erfolgsrate von 0,6 % erfüllen. In dieser Arbeit schlagen wir einen Rahmen vor, der es LLMs ermöglicht, das Reiseplanungsproblem formal als ein Satisfiability Modulo Theory (SMT)-Problem zu formulieren und SMT-Solver interaktiv zu nutzen, um das kombinatorische Suchproblem automatisch zu lösen. Die SMT-Solver garantieren die Erfüllbarkeit der Eingabebedingungen, und die LLMs ermöglichen eine sprachbasierte Interaktion mit unserem Framework. Wenn die Eingabebedingungen nicht erfüllbar sind, bietet unser auf LLM basierendes Framework interaktiv Vorschläge zur Modifikation der Reiseanforderungen durch automatische Schlussfolgerungen mithilfe der SMT-Solver. Wir evaluieren unser Framework mit TravelPlanner und erreichen eine Erfolgsrate von 97 %. Zudem erstellen wir einen separaten Datensatz mit internationalen Reisebenchmarks und verwenden beide Datensätze, um die Effektivität unseres interaktiven Planungsframeworks zu bewerten, wenn die ursprünglichen Benutzeranfragen nicht erfüllbar sind. Unser Framework konnte gültige Pläne mit einer durchschnittlichen Erfolgsrate von 78,6 % für unseren Datensatz und 85,0 % für TravelPlanner gemäß unterschiedlichen menschlichen Präferenzen generieren.