💻 computer science

Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale

Dieses Paper stellt VerIbmc vor, eine neuro-symbolische Pipeline, die lokale Open-Weight-Sprachmodelle in Kombination mit symbolischer Invariantensynthese und iterativem Verifizierer-Feedback nutzt, um eine State-of-the-Art-Generierung von Schleifeninvarianten für die Softwareverifikation zu erreichen und somit eine datenschutzwahrende sowie kosteneffiziente Alternative zu proprietären, cloudbasierten Werkzeugen anzubieten.

Ursprüngliche Autoren: Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

Veröffentlicht 2026-06-16

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen zu beweisen, dass eine komplexe Maschine (ein Computerprogramm) niemals kaputtgeht, egal wie oft man sie ausführt. Der schwierigste Teil dieses Beweises ist das Verständnis der „Schleifen“ der Maschine – Teile, in denen sie eine Aufgabe immer und immer wieder wiederholt. Um zu beweisen, dass die Maschine sicher ist, müssen Sie eine Schleifeninvariante finden.

Denken Sie bei einer Schleifeninvariante an eine „Sicherheitsregel“, die jedes Mal wahr sein muss, wenn die Maschine einen neuen Zyklus ihrer Schleife beginnt. Wenn zum Beispiel eine Schleife von 10 bis 0 rückwärts zählt, könnte die Sicherheitsregel lauten: „Die Zahl liegt immer zwischen 0 und 10.“ Wenn Sie beweisen können, dass diese Regel zu Beginn wahr ist, nach jedem Schritt wahr bleibt und zu einem sicheren Ende führt, ist die gesamte Maschine als sicher bewiesen.

Das Problem ist, dass das automatische Finden dieser Regeln unglaublich schwer ist. Es ist, als würde man versuchen, die geheime Kombination eines Tresors zu erraten, ohne jegliche Hinweise zu haben.

Der alte Weg vs. der neue Weg

Der alte Weg (Symbolische Argumentation):
Traditionell versuchten Computer, diese Regeln mittels strenger Mathematik und Logik zu finden. Es ist wie ein superpräziser Buchhalter, der jede einzelne Zahl prüft. Das ist sehr zuverlässig, aber langsam und scheitert oft an komplexen, unordentlichen Problemen. Es ist, als würde man versuchen, ein Labyrinth zu lösen, indem man jede einzelne Wand einzeln überprüft.

Der „Cloud“-Weg (Große KI-Modelle):
In jüngster Zeit haben Menschen angefangen, massive Modelle der Künstlichen Intelligenz (KI) zu verwenden, um diese Regeln zu erraten. Diese KIs sind wie brillante, belesene Studenten, die Millionen von Code-Beispielen gelesen haben. Sie können die richtige Regel sehr schnell erraten. Um sie jedoch zu nutzen, muss man seinen Code normalerweise an einen riesigen, teuren Cloud-Server senden (wie das Versenden Ihrer geheimen Baupläne an einen Fremden). Das ist schlecht für Unternehmen, die ihre Code-Privatsphäre schützen müssen, und es kostet viel Geld.

Die Lösung: VerIbmc (Der lokale „Super-Helfer“)

Die Autoren dieses Papers haben ein neues System namens VerIbmc entwickelt. Denken Sie an eine lokale Werkstatt, in der Sie einen smarten KI-Assistenten nutzen können, ohne jemals Ihr Gebäude zu verlassen.

So funktioniert VerIbmc, unter Verwendung einer einfachen Analogie:

Stellen Sie sich vor, Sie versuchen, ein schwieriges Rätsel (die Schleifeninvariante) zu lösen.

Der deterministische Detektiv (Phase 0 & 1): Bevor VerIbmc die KI um Hilfe bittet, schickt es einen strengen, logischen Detektiv (ein Tool namens ESBMC) los, um das Rätsel zu betrachten. Der Detektiv prüft zuerst einfache Fakten. Wenn das Rätsel einfach ist, löst der Detektiv es sofort. Wenn der Detektiv ein paar solide Hinweise findet (wie „die Zahl ist immer positiv“), schreibt er diese auf ein Whiteboard.
Der lokale KI-Assistent (Phase 2): Wenn der Detektiv stecken bleibt, ruft er den lokalen KI-Assistenten zu Hilfe. Aber hier ist der Trick: Die KI beginnt nicht bei Null. Der Detektiv übergibt der KI das Whiteboard mit den Hinweisen, die er bereits gefunden hat.
Die Feedback-Schleife: Die KI rät eine vollständige Lösung. Der Detektiv prüft sie.
- Wenn sie falsch ist, sagt der Detektiv nicht einfach nur „Nein“. Er sagt: „Dieser Teil ist falsch, aber dieser andere Teil ist tatsächlich korrekt.“ Er nimmt den korrekten Teil, schreibt ihn auf das Whiteboard und bittet die KI, es erneut zu versuchen, unter Verwendung der neuen Hinweise.
- Dies geschieht immer und immer wieder, bis das Rätsel gelöst ist oder die Zeit abläuft.

Zwei Denkweisen (CoT vs. ToT)

Das Paper testete auch, wie die KI während des Lösens des Rätsels „denken“ sollte:

Chain-of-Thought (CoT): Die KI denkt in einer geraden Linie, Schritt für Schritt, wie das Schreiben einer einzelnen Geschichte.
Tree-of-Thoughts (ToT): Die KI verzweigt sich wie ein Baum. Sie probiert mehrere Pfade gleichzeitig aus, sieht, welcher vielversprechend aussieht, und konzentriert ihre Energie dann auf die besten Pfade. Das Paper fand heraus, dass diese Verzweigungsmethode für die stärksten KI-Modelle großartig war, für kleinere, schwächere Modelle jedoch manchmal Zeit verschwendete.

Die Ergebnisse: Warum das wichtig ist

Die Forscher haben dieses System an Hunderten von verschiedenen Programmierrätseln mit fünf verschiedenen „Open-Weight“-KI-Modellen (Modelle, die jeder herunterladen und auf dem eigenen Computer ausführen kann) getestet.

Privatsphäre an erster Stelle: Da alles auf einer lokalen Maschine läuft, verlässt kein Code jemals die Organisation. Es ist, als würde man seine Hausaufgaben in seinem eigenen Zimmer machen, anstatt sie einem Fremden zu übergeben.
Kosteneffizient: Sie müssen keine teuren Gebühren an große Cloud-Unternehmen zahlen.
Leistung: Das beste Setup (unter Verwendung eines großen lokalen Modells namens GPT-OSS-120B) löste 86,4 % der Probleme. Dies ist besser als viele traditionelle Tools und konkurrenzfähig mit den teuren Cloud-basierten KI-Tools.
Der „Gratis“-Boost: Das System fand heraus, dass die „Detektiv“-Phase (der symbolische Teil) 75 Probleme ganz allein gelöst hat, ohne die KI überhaupt zu benötigen. Für schwächere KI-Modelle halfen die Hinweise des Detektivs ihnen, 35 weitere Probleme zu lösen, als sie es alleine geschafft hätten.

Das Fazit

VerIbmc beweist, dass man keine teuren, die Privatsphäre verletzenden Cloud-Supercomputer benötigt, um die Sicherheit von Software zu verifizieren. Indem man einen strengen logischen Detektiv mit einem smarten, lokalen KI-Assistenten kombiniert, der aus seinen Fehlern lernt, kann man erstklassige Ergebnisse direkt auf dem eigenen Computer erzielen. Es ist ein Weg, die Softwareverifizierung privat, erschwinglich und leistungsstark zu machen.

Technisches Resümee: Neuro-symbolische Softwareverifikation mit VerIbmc

Problemstellung

Die Synthese von Schleifeninvarianten bleibt ein zentraler Engpass in der formalen Softwareverifikation. Während symbolische Techniken (z. B. abstrakte Interpretation, Constraint-Lösung) und datengesteuerte „Guess-and-Check“-Methoden existieren, haben diese oft Schwierigkeiten mit Skalierbarkeit, Ausdrucksstärke oder der Diversität von realem Code. In jüngster Zeit haben Large Language Models (LLMs) vielversprechende Ansätze zur Generierung von Kandidaten-Invarianten gezeigt, indem sie gelernte Muster aus Code-Korpora nutzen. Bestehende neuro-symbolische Ansätze verlassen sich jedoch typischerweise auf proprietäre, geschlossene Modelle, die über externe Cloud-APIs aufgerufen werden. Diese Abhängigkeit führt zu erheblichen Hürden für den industriellen Einsatz:

Datenschutz und Compliance: Der Quellcode muss an Drittanbieter übermittelt werden, was Bedenken hinsichtlich der Vertraulichkeit aufwirft.
Reproduzierbarkeit: Die Abhängigkeit von externen Anbietern erschwert die Integration in kontrollierte Verifikations-Pipelines.
Kosten und Nachhaltigkeit: Große Modelle sind rechenintensiv und energieaufwendig, was ihre Praktikabilität für kontinuierliche Verifikations-Workflows einschränkt.

Die Autoren argumentieren, dass diese Herausforderungen einen Wechsel hin zu lokal bereitstellbaren, Open-Weight-Sprachmodellen erfordern, die vollständig innerhalb der Infrastruktur einer Organisation operieren können, ohne proprietären Code preiszugeben.

Methodik: Die VerIbmc-Pipeline

Das Paper präsentiert VerIbmc, eine neuro-symbolische Pipeline zur Synthese von Schleifeninvarianten für C-Programme, die symbolisches Schließen mit lokal gehosteten Open-Weight-LLMs kombiniert. Das System nutzt ESBMC (Efficient SMT-Based Context-Bounded Model Checker) als Verifikations-Oracle. Die Pipeline folgt dem Prinzip „Eskalation nur bei Notwendigkeit“ und priorisiert kostengünstige, deterministische symbolische Logik vor dem Aufruf des LLMs.

Kernarchitektur

Die Pipeline arbeitet in drei distinkten Phasen:

Phase 0 (Baseline-Verifikation): ESBMC verifiziert das unannotierte Programm. Wenn das Programm trivial sicher oder nachweislich unsicher ist, bricht der Prozess sofort ab, um unnötigen Syntheseaufwand zu vermeiden.
Phase 1 (Symbolische Kandidatengenerierung): Falls Phase 0 „Unknown“ zurückgibt, enumeriert das System symbolisch atomare Kandidaten-Invarianten durch paarweisen Vergleich von Schleifen-Eintrittsvariablen und Konstanten. Diese Atome werden auf Induktivität mittels ESBMC überprüft. Das System führt drei Speicher: Provable ( $P$ ), Disprovable ( $D$ ) und Unknown ( $U$ ). Wenn die Konjunktion aller beweisbaren Atome ausreicht, um die Post-Condition zu beweisen, terminiert die Pipeline erfolgreich, ohne einen LLM-Aufruf zu tätigen.
Phase 2 (LLM-Refinement-Loop): Falls die symbolische Phase unzureichend ist, tritt die Pipeline in eine iterative Schleife ein, in der ein LLM aufgefordert wird, neue Invarianten zu generieren.
- Feedback-Mechanismus: Das LLM erhält das aktuelle Programm, den Inhalt der $P$ -, $D$ - und $U$ -Speicher als strukturiertes Feedback sowie Few-Shot-Beispiele.
- Dekomposition und Rekombination: Wenn ein LLM-generierter Kandidat die Verifikation fehlschlägt, dekomponiert das System ihn in Sub-Formeln (Atome). Die Atome werden einzeln verifiziert und den entsprechenden Speichern zugeordnet. Die Konjunktion aller aktuell beweisbaren Atome wird daraufhin erneut verifiziert. Dies ermöglicht es dem System, nützliche Komponenten fehlgeschlagener LLM-Vorschläge zu retten.
- Terminierung: Die Schleife läuft weiter, bis eine gültige Invariante gefunden wird, das Iterationsbudget erschöpft ist oder ein Timeout eintritt.

Inferenzstrategien

Die Autoren evaluieren vier Inferenzstrategien basierend auf zwei Design-Achsen:

Verifier-Feedback (Symbolischer Prior):
- Basic: Führt die vollständige Drei-Phasen-Pipeline unter Nutzung des symbolischen Priors aus Phase 1 und der Atom-Level-Filterung aus.
- LLM-Only: Überspringt Phase 1 und die Atom-Dekomposition und verlässt sich allein darauf, dass das LLM induktive Invarianten als Ganzes generiert. Dies dient als Ablations-Baseline.
Reasoning-Struktur:
- Chain-of-Thought (CoT): Nutzt Standard-Prompting mit schrittweisen Reasoning-Beispielen (Induktiv, Hoare-Logik, Horn-Klauseln oder direkte Ableitung).
- Tree-of-Thoughts (Toft): Exploriert mehrere Ableitungsstile parallel während einer „Scouting“-Phase, bewertet diese basierend auf der Anzahl der generierten beweisbaren Atome und konzentriert das verbleibende Iterationsbudget auf die zwei leistungsstärksten Stile.

Zentrale Beiträge

Neuro-symbolische Pipeline: Ein vollständiges System, das lokal bereitgestellte Open-Weight-LLMs mit ESBMC zur automatisierten Schleifeninvarianten-Synthese integriert und vollständig auf interner Infrastruktur operiert.
Systematische Evaluierung der Strategien: Ein umfassender Vergleich von reinen LLM-, symbolisch-gestützten und Tree-of-Thoughts (ToT)-Varianten, die den Einfluss von symbolischem Feedback und Reasoning-Strukturen demonstriert.
Gewinne durch symbolisches Feedback: Nachweis, dass die Bereitstellung beweisbarer Invarianten-Atome als Kontext für das LLM konsistente Gewinne erzielt, insbesondere für schwächere Modelle (z. B. Llama-3.1-8B gewinnt +35 gelöste Benchmarks gegenüber einer reinen LLM-Baseline).
Analyse des Prompt Engineerings: Evaluierung verschiedener Prompting-Stile (CoT vs. ToT) und Reasoning-Templates (Induktiv, Hoare-Logik, Horn-Klausel) auf die Invarianten-Synthese.
Groß angelegtes Benchmarking: Eine umfangreiche Evaluierung über fünf Open-Weight-Modelle (7B bis 120 Parameter), vier Inferenzstrategien und fünf Benchmark-Familien (520 Probleme, 499 effektive), insgesamt 10.400 Ergebnisse pro Problem.

Experimentelle Ergebnisse

Die Evaluierung wurde auf einem Server mit vier NVIDIA RTX A6000 GPUs unter Verwendung von fünf Open-Weight-Modellen durchgeführt: GPT-OSS-120B, GPT-OSS-20B, Qwen2.5-32B, Qwen2.5-7B und Llama-3.1-8B.

Gesamtleistung: Die beste Einzelkonfiguration (GPT-OSS-120B mit der Basic-Strategie) löste 431 von 499 Problemen (86,4 %).
Vergleich mit dem Stand der Technik (SOTA):
- VerIbmc übertrifft traditionelle symbolische Tools (CPA-Checker, 2ls, ESBMC-Kind) und rein neuronale Tools (Code2Inv) bei Ausführung auf derselben lokalen Hardware deutlich.
- Auf gemeinsamen Benchmark-Suites ist VerIbmc wettbewerbsfähig mit oder liegt leicht unter den stärksten LLM-augmentierten Tools (Clause2Inv, LaM4Inv, LORIS), die teure externe APIs (z. B. GPT-4) nutzen. Bemerkenswert ist, dass VerIbmc diese Ergebnisse erzielt, ohne Code an die Cloud zu übertragen.
- VerIbmc skaliert einzigartig auf den vollen SV-COMP-Benchmark-Satz (154 Probleme), einschließlich Programmen mit Arrays, verschachtelten Schleifen und Pointern, die viele konkurrierende Tools aufgrund von Frontend-Limitierungen nicht ausdrücken können.
Einfluss der symbolischen Phase: Die symbolische Phase 1 löste 75 Probleme ohne jeglichen LLM-Aufruf. Für schwächere Modelle bot die symbolische Augmentierung signifikante Steigerungen (bis zu +35 zusätzliche gelöste Probleme für Llama-3.1-8B).
ToT vs. CoT: Das ToT-Prompting zeigte einen Trade-off zwischen Diversität und Genauigkeit. Während es zwar einzigartige Problem-Modell-Paare erreichte, die für CoT unzugänglich waren, verursachte es oft einen Overhead bei der Wanduhrzeit und führte bei schwächeren Modellen aufgrund der Erschöpfung des Iterationsbudgets zu einer Nettoabnahme der gelösten Probleme. Bei den stärksten Modellen (GPT-OSS-120B) war der Leistungsunterschied zwischen CoT und ToT vernachlässigbar.
Modellkapazität: Die Ergebnisse zeigen, dass die Modellkapazität der primäre Treiber der Genauigkeit ist. Die Lücke zwischen den stärksten und schwächsten Modellen war signifikant größer als die durch die Änderung der Strategien innerhalb desselben Modells verursachte Varianz.

Bedeutung und Ansprüche

Das Paper behauptet, dass VerIbmc zeigt, dass ein neuro-symbolischer Ansatz basierend auf LLMs effektiv für die Invariantensynthese in einer datenschutzfreundlichen und energieeffizienten Weise angewendet werden kann. Durch den Betrieb auf lokaler Infrastruktur mit Open-Weight-Modellen eliminiert der Ansatz die Notwendigkeit für teure proprietäre Frontier-Modelle, die hinter APIs gesperrt sind.

Die Autoren betonen, dass ihre Methode „sound by construction“ ist: Jede Kandidaten-Invariante wird durch einen formalen Verifizierer (ESBMC) vor der Annahme validiert. Obwohl das System aufgrund der Unentscheidbarkeit des Problems unvollständig ist, bietet es einen praktischen, skalierbaren und reproduzierbaren Weg für die KI-gestützte formale Verifikation von Produktionssoftware. Die Arbeit stellt einen Schritt in Richtung industriefertiger Verifikations-Pipelines dar, in denen Datenschutz und Ressourceneffizienz kritische Anforderungen sind.