Verbesserung des Skeleton-gesteuerten SMT Solver Fuzzing durch die Nutzung von LLM zur Erstellung von Formelgeneratoren

Satisfiability Modulo Theory (SMT) Solver sind grundlegend für moderne Systeme und die Forschung zu Programmiersprachen, da sie die Basis für Aufgaben wie symbolische Ausführung und automatisierte Verifizierung bieten. Da diese Solver auf dem kritischen Pfad liegen, ist ihre Korrektheit von entscheidender Bedeutung, und qualitativ hochwertige Testformeln sind der Schlüssel zur Aufdeckung von Fehlern. Während frühere Testtechniken bei älteren Solver-Versionen gut abschnitten, haben sie Schwierigkeiten, mit den sich schnell entwickelnden Funktionen Schritt zu halten. Neuere Ansätze, die auf großen Sprachmodellen (LLMs) basieren, zeigen das Potenzial, fortgeschrittene Solver-Funktionen zu erkunden, aber zwei Hindernisse bleiben: Fast die Hälfte der generierten Formeln ist syntaktisch ungültig, und iterative Interaktionen mit den LLMs führen zu erheblichen rechnerischen Überhängen. In dieser Studie stellen wir Chimera vor, ein neuartiges LLM-unterstütztes Fuzzing-Framework, das beide Probleme angeht, indem es von der direkten Formelgenerierung zur Synthese von wiederverwendbaren Termgeneratoren (d. h. logische Ausdrücke) wechselt. Insbesondere verwendet Chimera LLMs, um (1) kontextfreie Grammatiken (CFGs) für SMT-Theorien, einschließlich solver-spezifischer Erweiterungen, aus Dokumentationen automatisch zu extrahieren, und (2) zusammensetzbare boolesche Termgeneratoren zu synthetisieren, die diesen Grammatiken entsprechen. Während des Fuzzings füllt Chimera strukturelle Skelette, die aus bestehenden Formeln abgeleitet sind, mit den iterativ von den LLM-synthetisierten Generatoren produzierten Termen. Dieses Design gewährleistet syntaktische Gültigkeit und fördert die semantische Vielfalt. Bemerkenswert ist, dass Chimera nur eine einmalige Investition in die LLM-Interaktion erfordert, was die Laufzeitkosten drastisch senkt. Wir haben Chimera an zwei führenden SMT-Solvern: Z3 und cvc5 evaluiert. Unsere Experimente zeigen, dass Chimera 43 bestätigte Fehler identifiziert hat, von denen 40 bereits von Entwicklern behoben wurden.