Automatisierte Programmverfeinerung: Anleitung und Überprüfung von Code durch ein großes Sprachmodell mit Verfeinerungs-Kalkül

In letzter Zeit hat der Aufstieg von codezentrierten großen Sprachmodellen (LLMs) die Softwaretechnik mit barrierefreien Werkzeugen wie Copilot, die Code einfach generieren können, neu gestaltet. Es gibt jedoch keine Garantien für die Korrektheit des von LLMs generierten Codes, der unter dem Halluzinationsproblem leidet, und die Ausgaben sind mit Risiken behaftet. Darüber hinaus ist der End-to-End-Prozess von der Spezifikation bis zum Code durch LLMs eine nicht transparente und unkontrollierte Black Box. Diese Undurchsichtigkeit erschwert es den Benutzern, den generierten Code zu verstehen und ihm zu vertrauen. Diese Herausforderungen anzugehen ist sowohl notwendig als auch kritisch. Im Gegensatz dazu transformiert die Programmverfeinerung hochrangige Spezifikationsaussagen in ausführbaren Code und bewahrt dabei die Korrektheit. Traditionelle Werkzeuge für die Programmverfeinerung sind hauptsächlich für Experten für formale Methoden konzipiert und bieten keine Automatisierung und Erweiterbarkeit. Wir wenden die Programmverfeinerung an, um LLMs zu leiten und den von LLMs generierten Code zu validieren, während wir die Verfeinerung in ein zugänglicheres und flexibleres Rahmenwerk umwandeln. Um diese Vision zu initiieren, schlagen wir Refine4LLM vor, einen Ansatz, der darauf abzielt: (1) Die Spezifikationen formal zu verfeinern, (2) Das LLM automatisch zu informieren und zu leiten, indem wir den Verfeinerungskalkül nutzen, (3) Mit dem LLM zu interagieren, um den Code zu generieren, (4) Zu überprüfen, dass der generierte Code die Einschränkungen erfüllt und somit seine Korrektheit garantiert, (5) Zu lernen und fortschrittlichere Verfeinerungsgesetze zu entwickeln, um den Verfeinerungskalkül zu erweitern. Wir haben Refine4LLM mit den aktuellsten Baselines zu Programmverfeinerung und LLM-Benchmarks bewertet. Die Experimentergebnisse zeigen, dass Refine4LLM effizient robusteren Code generieren und die Zeit für Verfeinerung und Überprüfung reduzieren kann.