Neuro‑Symbolische KI CodeLogician verbessert Softwareanalyse um bis zu 47 %
Large Language Models (LLMs) haben in der Code‑Verständnis‑Forschung große Fortschritte erzielt, doch sie fehlen die Fähigkeit, präzise und umfassende mathematische Schlüsse über das Verhalten von Programmen zu ziehen. Mit dem neu entwickelten Agenten CodeLogician wird dieses Problem angegangen: LLMs werden genutzt, um explizite formale Modelle von Softwaresystemen zu erstellen, die anschließend von ImandraX – einem industriellen automatisierten Beweis‑Engine, der bereits in Finanzmärkten und sicherheitskritischen Anwendungen eingesetzt wird – analysiert werden.
CodeLogician geht über die bisher üblichen Formal‑Methoden hinaus, die LLM‑Ausgaben lediglich validieren. Stattdessen ermöglicht die neuartige Integration, dass automatisierte Beweise komplexe semantische Fragen beantworten, die weit über einfache Ja‑/Nein‑Verifikation hinausgehen. Um die Wirksamkeit dieser neuartigen Herangehensweise zu messen, wurde das Benchmark‑Set code‑logic‑bench entwickelt. Es prüft die Richtigkeit von Schlussfolgerungen zu Zustandsräumen, Kontrollflüssen, Abdeckungsbedingungen und Randfällen, wobei die korrekten Antworten durch formale Modellierung und Region‑Decomposition festgelegt werden.
Der Vergleich von reinen LLM‑Modellen mit LLMs, die durch CodeLogician unterstützt werden, zeigt einen deutlichen Leistungszuwachs: Die Genauigkeit der mathematischen Analyse steigt um 41 bis 47 Prozentpunkte. Diese Ergebnisse unterstreichen, dass die Kombination von neuronalen und symbolischen Techniken entscheidend ist, um Softwareanalyse auf ein neues Niveau der Präzision und Autonomie zu heben.