LLMs und formale Solver für zuverlässige KI-Entscheidungen kombinieren

Eine hybride Architektur verbindet die Flexibilität von LLMs mit deterministischen Solvern und ermöglicht so zuverlässige, überprüfbare Unternehmensentscheidungen.

Large Language Models (LLMs) haben außergewöhnliche Fortschritte dabei gemacht, natürliche Sprache zu verstehen, flüssige Antworten zu erzeugen und völlig neue Erlebnisse für Kundschaft und Beschäftigte zu ermöglichen. Da LLMs jedoch grundsätzlich stochastisch arbeiten, bieten sie bei komplexem numerischem oder logischem Reasoning nur begrenzte Gewähr dafür, dass ihre Ergebnisse regelkonform oder optimal sind. Zum Beispiel:

  • Eine Führungskraft weist einen KI-Planungsassistenten an: “Ship as much as possible next week while keeping costs low,” und das System liefert einen ehrgeizigen Plan, der effizient wirkt, aber unbemerkt die Lagerkapazität überschreitet und Lieferzusagen verletzt.

  • Eine koordinierende Person weist einen KI-Assistenten an: “Reassign crews to reduce overnight stays and minimize disruption,” und das Modell erstellt einen kostengünstigeren Plan, der optimal wirkt, aber verbindliche Vorgaben zu Dienst- oder Ruhezeiten verletzt.

  • Ein KI-Assistent für Finanzprozesse muss Transaktionen unter strengen regionalen und risikobezogenen Vorgaben genehmigen. Dennoch gibt er eine verdächtige Transaktion frei, indem er eine Begründung erfindet, die regelkonform klingt, aber gegen interne Richtlinien verstößt.

In Umgebungen mit strengen betrieblichen Anforderungen hilft die Kombination von LLMs und formalen Solvern dabei, Entscheidungen auf Basis natürlicher Sprache innerhalb festgelegter Grenzen zu halten und nicht umsetzbare, suboptimale oder regelwidrige Ergebnisse zu vermeiden.

Unser Forschungs- und Entwicklungsteam untersucht einen hybriden Ansatz, der die Kreativität und Flexibilität von LLMs mit der Präzision, den Garantien und der Transparenz formaler mathematischer Solver wie Z3, Pyomo und OR-Tools verbindet. Außerdem entwickeln wir eine wiederverwendbare formale KI-Engine, um diese Funktion zu einem festen Bestandteil der Technologiearchitektur von Unternehmen zu machen. Die Plattform soll es Organisationen ermöglichen, Geschäftsregeln direkt aus ihren bestehenden Systemen zu übernehmen, Entscheidungen fortlaufend anhand dieser Regeln zu prüfen und KI-Agenten sicher innerhalb klar festgelegter Grenzen einzusetzen.

Unsere Vision ist es, betriebliche Risiken zu senken und zugleich Entscheidungen in großem Maßstab zu beschleunigen. Führungskräfte erhalten schneller regelkonforme Entscheidungen auf Basis natürlichsprachlicher Eingaben. Organisationen können zugleich kurzfristige Änderungen bei Einsatzplanung, Ressourcenzuweisung in der Lieferkette, Finanzprozessen, Richtlinienprüfung und sogar Video- oder 3D-Design automatisieren. Integrierte Schutzmechanismen verhindern, dass nicht umsetzbare, regelwidrige oder unsichere Ergebnisse in den Produktivbetrieb gelangen.

In kontrollierten Experimenten mit Optimierungsproblemen aus der Logistik und drei öffentlichen Benchmarks zeigte unser hybrider Ansatz durchgehend:

  • Höhere Genauigkeit

  • Bessere Interpretierbarkeit und Prüfbarkeit

Die hybride Architektur

Unser Ansatz kehrt das übliche Paradigma „Das LLM erledigt alles“ um und folgt stattdessen diesem Aufbau:

Diagramm zum Zusammenspiel von Large Language Models und deterministischen Solvern, das natürliches Sprachverständnis mit überprüfbarer Optimierung verbindet.

Dieser Ansatz trennt die Verantwortlichkeiten klar: LLMs extrahieren Regeln und Einschränkungen aus natürlicher Sprache, während deterministische Solver wie OR-Tools, Z3 und Pyomo die Optimierung und Prüfung übernehmen. Das Ergebnis verbindet die Stärken beider Ansätze:

LLMs

Solver

Hybrid (LLM + Solver)

Menschliche Absichten in verschiedenen Bereichen verstehen

✅ Hervorragend

❌ Keine

✅ Hervorragend

Deterministisches Verhalten

❌ Nein

✅ Garantiert

✅ Ja

Nachweislich korrektes mathematisches Reasoning und Optimieren unter mehreren Einschränkungen

⚠️ Fehleranfällig

✅ Garantiert

✅ Ja

Prüfbarkeit und Interpretierbarkeit

⚠️ Fehleranfällig

✅ Klar

✅ Klar

Robustheit gegenüber Störungen und Injection-Angriffen in Prompts

❌ Anfällig

✅ Immun

✅ Hoch

Versuchsreihe 1: Logistik und Personaleinsatz

Der Problembereich

Wir begannen mit einer Herausforderung, vor der einige unserer Kundenunternehmen stehen:

Natürlichsprachliche Anfragen in optimale Ressourcenentscheidungen in Echtzeit überführen und dabei betriebliche, richtlinienbezogene und finanzielle Einschränkungen strikt durchsetzen.

Diese Herausforderung ist für moderne Logistik und Lieferketten von zentraler Bedeutung. Dazu gehören Personaleinsatzplanung, Zuweisung von Betriebsmitteln, Routenplanung, Lieferplanung und Kapazitätsmanagement. Gerade hier müssen LLMs und formale Solver zusammenarbeiten, um vertrauenswürdige Systeme zu schaffen. Für unsere Auswertung erstellten wir kontrollierte Testszenarien, Datenquellen und Einschränkungen sowie 240 synthetische Anfragen. Beispiele:

  • Please revise the existing schedule following a cancellation. The target facility must be fully supplied by 24 December 2025. When possible, source inventory from a nearby warehouse and route it through a specific consolidation point. The earliest allowable start date is 14 December 2025.

  • Last-minute request: a VIP will arrive at location A in three hours. We need the required staff on site within two hours. Please adjust staff allocations while minimizing changes to the existing schedule.

Die Anfragen zeigen, dass das System harte und weiche Einschränkungen zuverlässig direkt aus natürlichsprachlichen Anfragen extrahieren und durchsetzen muss:

  • Harte Einschränkungen sind nicht verhandelbar, etwa früheste Starttermine, Vertragsbedingungen und Kapazitätsobergrenzen. Die Verletzung auch nur einer dieser Einschränkungen macht die Lösung ungültig.

  • Weiche Einschränkungen bilden Präferenzen ab, etwa Verzögerungen zu minimieren, Kosten zu senken und Änderungen zu begrenzen. Das Ziel ist eine Optimierung, ohne harte Grenzen zu überschreiten.

Einige Aspekte dieser Optimierungsprobleme lassen sich nicht vollständig vorab definieren. Sie müssen dynamisch zusammengestellt werden. Dazu fließen neben vordefinierten Einschränkungen und Zielen aus strukturierter Geschäftslogik, internen Dokumenten und Betriebsdaten auch die jeweilige Anfrage ein.

Die untersuchten Ansätze

Um die Leistung verschiedener Verfahren in diesem Umfeld zu verstehen, implementierten und verglichen wir drei Ansätze.

  1. Reines LLM: Beim einfachsten Ansatz werden alle relevanten Daten und die natürlichsprachliche Anfrage an einen einzigen LLM-Prompt übergeben. Dieser soll einen optimalen Plan oder eine optimale Zuweisung erstellen. Das kann bei kleinen oder nur wenigen Einschränkungen unterliegenden Problemen funktionieren, scheitert aber mit zunehmender Komplexität. Das Modell kann Einschränkungen ignorieren, das falsche Ziel priorisieren oder Pläne erstellen, die plausibel klingen, aber nicht umsetzbar sind. Fehler lassen sich dabei nicht zuverlässig erkennen oder verhindern.

  2. LLM + Code Interpreter: Bei diesem Ansatz interpretiert das LLM die Anfrage und greift mithilfe von Tools auf Datenquellen zu, um ausführbaren Optimierungscode zu erzeugen. Das erhöht Flexibilität und Nachvollziehbarkeit, doch die Zuverlässigkeit bleibt problematisch. Das LLM muss Einschränkungen weiterhin in korrekten Code übersetzen. Kleine Fehler beim Reasoning oder Programmieren können insbesondere bei vielen Einschränkungen zu ungültigen oder suboptimalen Ergebnissen führen.

  3. Hybrid: LLM → strukturierte Einschränkungen → deterministischer Solver: Der dritte Ansatz trennt die Verantwortlichkeiten. Das LLM „entscheidet“ nie über das Ergebnis, sondern hilft dabei, Variablen, Einschränkungen und Ziele formal zu beschreiben. Ein bewährter Optimierungssolver setzt Einschränkungen durch, gewährleistet die Umsetzbarkeit und liefert Ergebnisse, die verifiziert und geprüft werden können. Die Rolle des LLM beschränkt sich darauf, natürlichsprachliche Anfragen anhand vordefinierter Schemas in explizite, strukturierte Einschränkungen zu übersetzen. Diese Einschränkungen werden automatisch in Solver-Code, etwa für OR-Tools, kompiliert. Dieser berechnet deterministisch eine umsetzbare, optimale Lösung.

Ergebnisse

Wir testeten die Methoden mit mehreren LLMs, darunter GPT-5, GPT-5.1 und GPT-5.2. Wie erwartet übertraf der hybride Ansatz die Alternativen:

Methode

Zuweisungsgenauigkeit

Durchschnittliche Latenz

Verwendete Tokens je Anfrage

Reines LLM

70–78 %

62–190 s

ca. 175.000

LLM + Code Interpreter

82–84 %

62–140 s

ca. 9.000

LLM → Solver (hybrid)

95–97 %

6–25 s

ca. 2.000

Unsere hybride Methode erzielt eine deutlich höhere Genauigkeit, eine mehr als viermal so hohe Token-Effizienz und eine Verringerung der Latenz um eine Größenordnung.

Versuchsreihe 2: universelle Optimierung anhand natürlicher Sprache

Als Nächstes entwickeln wir eine verallgemeinerbare, wiederverwendbare Schnittstelle, die natürliche Sprache in strukturierte semantische Darstellungen umwandelt. Unser Backend kann diese anschließend in Solver-fähigen Code übersetzen. Für dieses Experiment konzentrierten wir uns auf lineare Optimierungsprobleme und werteten den Ansatz anhand von drei öffentlichen Datensätzen aus: NLP4LP, NL4OPT und IndustryOR.

Die untersuchten Ansätze

  1. Eigenständiges LLM

  2. Hybride Methode (LLM → strukturierte Regeln → Solver → verifiziertes Ergebnis)

Diagramm des hybriden Ablaufs von natürlichsprachlichen Anfragen über strukturierte Einschränkungen und deterministische Lösung bis zum verifizierten Ergebnis.

  • Mit einem LLM Variablen, Einschränkungen und Ziele aus der Eingabe extrahieren und daraus ein strukturiertes Optimierungsproblem formulieren.

  • Das strukturierte Problem und die ursprüngliche Anfrage zur Selbstprüfung an ein LLM übergeben.

  • Das strukturierte Problem in OR-Tools-Code übersetzen, um die optimale Zuweisung zu berechnen.

Ergebnisse

Wir werteten diesen Ansatz mit proprietären Frontier-Modellen aus, darunter GPT-5.1, GPT-5 mini, GPT-5.1-Codex-Max und GPT-5.2, sowie mit Open-Source-Modellen wie Kimi K2, GPT-OSS-Modellen und MiniMax M2. Die Boxplots fassen die Ergebnisse der einzelnen Methoden zusammen.

Diagramm zum Vergleich eigenständiger Large Language Models und hybrider solverbasierter Ansätze anhand von Optimierungsbenchmarks.

Bei nahezu allen untersuchten zugrunde liegenden Sprachmodellen liefert der hybride Ansatz durchgehend genauere, stabilere und besser überprüfbare Ergebnisse als eine Vergleichsbasis mit einem eigenständigen LLM. Die absolute Leistung unterscheidet sich zwar je nach Modell, doch die relativen Verbesserungen durch den hybriden Ansatz bleiben konstant. Das deutet darauf hin, dass die Verbesserungen aus der Trennung von natürlichem Sprachverständnis und formaler Optimierung entstehen und nicht von der Reasoning-Fähigkeit eines einzelnen Modells abhängen.

Genauigkeit

Bei NLP4LP und NL4OPT, die hauptsächlich aus linearen Optimierungsproblemen bestehen, erreicht die hybride Methode nahezu die maximal mögliche Genauigkeit und übertrifft Prompts für eigenständige LLMs. Statt „annähernd korrektes“ Reasoning zu erzeugen, erstellt das hybride System zuverlässiger gültige, korrekt aufgebaute mathematische Formulierungen. Beim anspruchsvolleren IndustryOR-Datensatz sinkt die Genauigkeit beider Methoden, allerdings aus unterschiedlichen Gründen. Viele IndustryOR-Probleme umfassen kombinatorische Strukturen wie Fahrzeugrouten, Aufgabenreihenfolgen und Personaleinsatz. Diese übersteigen die derzeit von unserem Solver-Backend unterstützten Möglichkeiten der linearen Optimierung.

Die Analyse der Fehlerarten zeigt, dass eigenständige LLMs erforderliche Einschränkungen häufig verletzen, wie die folgenden Beispiele verdeutlichen:

Beispiel 1:

Plain Text

"A bodybuilder buys prepared meals: a turkey dinner and a tuna salad sandwich. The turkey dinner contains 20 grams of protein, 30 grams of carbohydrates, and 12 grams of fat. The tuna salad sandwich contains 18 grams of protein, 25 grams of carbohydrates, and 8 grams of fat. The bodybuilder needs at least 150 grams of protein and 200 grams of carbohydrates. Because turkey dinners are expensive, no more than 40% of the meals should be turkey dinners. How many of each meal should the bodybuilder eat to minimize total fat intake?"

Das eigenständige LLM erstellt eine Lösung mit einem geringeren Gesamtfettgehalt, verletzt jedoch die Vorgabe, dass Gerichte mit Putenfleisch höchstens 40 % der Mahlzeiten ausmachen dürfen. Der hybride Ansatz setzt diese harte Einschränkung korrekt durch und liefert eine gültige Antwort.

Beispiel 2:

Plain Text

"A hospitalized patient can take two pills: Pill 1 and Pill 2. Each Pill 1 provides 0.2 units of pain medication and 0.3 units of anxiety medication. Each Pill 2 provides 0.6 units of pain medication and 0.2 units of anxiety medication. Pill 1 causes 0.3 units of discharge, while Pill 2 causes 0.1 units. At most 6 units of pain medication may be provided, and at least 3 units of anxiety medication must be provided. How many of each pill should the patient receive to minimize total discharge?"

Das eigenständige LLM erstellt erneut eine Lösung mit geringerer Entlassungsrate, überschreitet dabei jedoch den zulässigen Höchstwert für Schmerzmittel. Der hybride Ansatz setzt auch diese harte Einschränkung korrekt durch und liefert eine gültige Antwort.

Latenz und Token-Nutzung

Die Daten zu Latenz und Token-Nutzung zeigen einen wichtigen Unterschied. Der hybride Ansatz weist eine höhere durchschnittliche Latenz und Token-Nutzung auf als ein einzelner LLM-Prompt. Das ist jedoch auf Architekturentscheidungen und nicht auf Ineffizienz zurückzuführen.

Die hybride Verarbeitungskette umfasst:

  1. Einen oder mehrere LLM-Aufrufe, um strukturierte Variablen, Einschränkungen und Ziele zu extrahieren.

  2. Einen Schritt zur Selbstprüfung, um interne Widersprüche zu erkennen.

Diese Schritte verursachen zwar mehr Aufwand als ein einzelner Prompt, doch die Latenz bleibt begrenzt und vorhersehbar. Sobald das Problem korrekt formuliert ist, wird der Solver in der Regel schnell ausgeführt. Der zusätzliche Aufwand erzeugt explizite, wiederverwendbare und prüfbare Zwischendarstellungen. Eigenständige LLM-Ansätze hingegen bündeln das Reasoning in einer einzigen undurchsichtigen Generierung. Dadurch verlagern sich die Kosten auf erneute Versuche, manuelle Prüfungen und nachgelagerte Fehler. Künftige Versionen können diesen Aufwand verringern durch:

  • Zwischenspeichern extrahierter Schemas.

  • Schrittweises Aktualisieren von Einschränkungen.

  • Verbessertes Zusammenspiel von Prompts und Aufrufen.

Transparenz und Prüfbarkeit

Selbst wenn beide Methoden scheitern, unterscheiden sich ihre Fehlerarten grundlegend.

  • Bei einem eigenständigen LLM bleiben Fehler häufig unbemerkt: Das Modell kann ein Ergebnis zurückgeben, das nur geringfügig, aber entscheidend falsch ist.

  • Beim hybriden Ansatz macht die explizite Problemformulierung Fehler sichtbar und hilft Teams zu erkennen, welcher Teil der Formulierung den Fehler verursacht hat.

Künftige Versionen könnten diese Formulierungen in einer Benutzeroberfläche anzeigen, damit sie vor der Ausführung des Solvers geprüft oder verifiziert werden können. Diese Transparenz verbessert die gemessene Genauigkeit und erleichtert es, Fehler im System zu beheben und das System weiterzuentwickeln. Das ist für den praktischen Einsatz entscheidend.

Wichtigste Erkenntnis

Über alle Benchmarks und die meisten getesteten zugrunde liegenden Modelle hinweg bekräftigen die Ergebnisse eine zentrale Schlussfolgerung unserer Arbeit:

LLMs sind leistungsfähig beim Verstehen und Übertragen von Absichten. Für die Durchsetzung korrekter Ergebnisse sind deterministische Solver jedoch unverzichtbar.

Der hybride Ansatz macht natürliche Sprache von einer Quelle der Mehrdeutigkeit zu einer zuverlässigen Schnittstelle für mathematisch fundierte Entscheidungen. Damit bringt er KI für Unternehmen einen Schritt näher an Systeme, die nicht nur intelligent, sondern auch vertrauenswürdig sind.

Nächster Schritt: eine wiederverwendbare formale KI-Engine für Unternehmen

Betriebliche Einschränkungen liegen nur selten in übersichtlichen Schemas oder perfekt formulierten Prompts vor. Sie sind über Datenbanken, Tabellen, interne Richtlinien und Verträge verteilt. Anfragen können unvollständig, mehrdeutig oder mit Geschäftsregeln unvereinbar sein. Damit dieser Ansatz in großem Maßstab funktioniert, entwickeln wir eine wiederverwendbare Backend-Engine, die diese Komplexität in eine zuverlässige Unternehmensfunktion überführt.

Diagramm der formalen KI-Engine für Unternehmen mit Geschäftsregeln, Solver-Übersetzung und prüfbarer Entscheidungsfindung.

Die Plattform

Im Kern bildet diese Engine das formale Rückgrat KI-gestützter Entscheidungssysteme und bietet:

  • Eine symbolische Wissensbasis mit Adaptern, die Geschäftsregeln, Einschränkungen, Variablen und Ziele übernehmen.

  • Eine Übersetzungsschicht, die Schemas in Solver-Code kompiliert.

  • Schnittstellen, über die Teams Einschränkungen einsehen, prüfen und ändern können.

Wo dadurch Potenziale entstehen

Die Experimente konzentrieren sich derzeit auf Optimierung, doch dieselbe Methode lässt sich auch auf logische Prüfungen übertragen. Mögliche betriebliche Anwendungen sind:

  • Kurzfristige dynamische Einsatzplanung, Routenplanung und Ressourcenzuweisung unter Einhaltung sämtlicher betrieblicher Einschränkungen.

  • Antworten und Empfehlungen erstellen, die Geschäftsregeln konsequent einhalten.

  • Komplexe 3D-Objekte, Videos und Architekturen entwerfen und validieren sowie nicht umsetzbare Entwürfe vor der Produktion erkennen.

Abschließende Gedanken

KI ist heute leistungsfähig. Unternehmen benötigen jedoch mehr als Leistung: Sie brauchen Korrektheit, Konsistenz und Kontrolle. Unser hybrides System aus LLM und Solver ist ein Schritt hin zu einer Welt, in der:

  • Agenten keine Regeln oder Einschränkungen halluzinieren.

  • Logische Schlussfolgerungen und Optimierungen mathematisch fundiert sind.

  • Natürliche Sprache als universelle Schnittstelle zu deterministischen Systemen dient.

Autor

Peng Seng Ang