Zusammenfassung - In Richtung formale Verifikation von Code, der durch natürliche Sprachanweisungen von LLM generiert wird

In Richtung formale Verifikation von Code, der durch natürliche Sprachanweisungen von LLM generiert wird

2025-07-17 16:54:42

{"Aaron Councilman","David Fu","Aryan Gupta","Chengxiao Wang","David Grove","Yu-Xiong Wang","Vikram Adve"}

{cs.PL,cs.AI}

Das Papier schlägt ein System namens Astrogator vor, das die Richtigkeit von Code überprüft, der von Grossen Sprachmodellen (LLMs) auf Basis natürlicher Sprachbeschreibungen generiert wird. Ziel ist es, formale Garantien der Richtigkeit bereitzustellen, die die Benutzererfahrung bei der Nutzung von AI-Code-Assistenten verbessert und natürliche Sprachprogrammierung für Benutzer mit wenig oder gar keinem Programmierwissen ermöglicht. ### Schlüsselpunkte: * **Herausforderung**: LLMs generieren oft falschen Code, der für Benutzer schwer zu erkennen ist. Dies ist ein erhebliches Problem in der natürlichen Sprachprogrammierung und im Kontext von AI-Code-Assistenten. * **Lösung**: Astrogator integriert eine formale AnfrageSprache, um Benutzerintentionen darzustellen und generierten Code der LLMs gegen diese zu überprüfen. * **Formale AnfrageSprache**: Die Sprache ist so gestaltet, dass sie der natürlichen Sprachsyntax nahekommt, aber präzise definiert ist. Sie nutzt hochrangige Konzepte und eine Wissensbasis, um Ambiguitäten zu vermeiden. * **Überprüfung**: Astrogator verwendet symbolische Interpretation und einen Kalculus, um das Verhalten von Ansible-Programmen darzustellen und deren Richtigkeit zu überprüfen. * **Evaluation**: Bei einer Benchmark-Suite von 21 Code-Generierungsaufgaben konnte Astrogator in 83% der Fälle richtigen Code überprüfen und in 92% der Fälle falschen Code identifizieren. ### Schlüsselbeiträge: 1. **Formalisierung der natürlichen Sprachprogrammierung**: Definiert ein formales Rahmenwerk für die natürliche Sprachprogrammierung und die Richtigkeit. 2. **Formale AnfrageSprache**: Vorschlag einer formalen AnfrageSprache, um Benutzerintentionen zu erfassen und die Überprüfung zu erleichtern. 3. **Überprüfungsansatz**: Entwickelt einen Überprüfungsansatz mittels symbolischer Interpretation und eines Kalculus. 4. **Implementierung**: Implementiert das System in Astrogator für die Ansible-Programmiersprache. 5. **Evaluation**: Bewertet das System in einer Benchmark-Suite und zeigt seine Effektivität. ### Einschränkungen: * **Beschränkte Sprachunterstützung**: Unterstützt derzeit nur Ansible. * **Beschränkte AnfrageSprache**: Die formale AnfrageSprache und die Wissensbasis bedürfen weiterer Entwicklung. * **Behandlung von Annahmen**: Das System könnte unter bestimmten Annahmen falschen Code akzeptieren und erfordert möglicherweise Benutzerintervention. ### Schlussfolgerung: Astrogator ist ein vielversprechender Ansatz zur Überprüfung der Richtigkeit von durch LLMs generierten Code. Es bietet ein formales Rahmenwerk für die natürliche Sprachprogrammierung und zeigt seine Effektivität in einer Benchmark-Suite. Für die Beseitigung der Einschränkungen und die Erweiterung der Sprachunterstützung bedarf es weiterer Entwicklung.