Stepwise: Neuro-symbolische Beweissuche für automatisierte Systemverifikation

Die formale Verifikation mittels interaktiver Theorembeweise gewinnt zunehmend an Bedeutung, um die Korrektheit kritischer Systeme zu garantieren. Dabei bleibt die Erstellung umfangreicher Beweisskripte jedoch stark manuell und limitiert die Skalierbarkeit.

Mit den jüngsten Fortschritten in großen Sprachmodellen (LLMs), insbesondere im mathematischen Denken, eröffnet sich ein vielversprechender Ansatz, diese Modelle in die Softwareverifikation zu integrieren.

In dem vorliegenden Beitrag wird ein neuro-symbolisches Framework vorgestellt, das die Beweissuche für systemweite Verifikationsprojekte automatisiert. Das System führt einen best-first Baum‑Suchalgorithmus über Beweiszustände aus und ruft dabei wiederholt ein LLM auf, um den nächsten möglichen Beweisschritt zu generieren.

Auf der neuronalen Seite werden die LLMs mit Datensätzen aus Beweiszustand‑Schritt‑Paaren feinabgestimmt. Auf der symbolischen Seite kommen diverse ITP‑Werkzeuge zum Einsatz, die abgelehnte Schritte reparieren, Beweiszustände filtern und bewerten sowie Unterziele automatisch lösen, wenn die Suche ins Stocken gerät. Diese Kombination ermöglicht eine daten‑effiziente Anpassung der LLMs und eine semantisch informierte Pruning des Suchraums.

Das Framework wurde in einer neuen Isabelle‑REPL implementiert, die fein granularen Beweiszustände und Automatisierungstools bereitstellt. In der Evaluation auf dem FVEL‑seL4‑Benchmark sowie weiteren Isabelle‑Entwicklungen konnte das System bis zu 77,6 % der Theoreme beweisen – ein deutlicher Fortschritt gegenüber bisherigen LLM‑basierten Ansätzen und dem alleinigen Sledgehammer. Darüber hinaus löste es deutlich mehr mehrstufige Beweise. Ergebnisse auf weiteren Benchmarks zeigen eine starke Generalisierung, was einen vielversprechenden Weg zu skalierbarer automatisierter Softwareverifikation aufzeigt.