Seite 2: Websites automatisch mit GPT-3 programmieren

Inhaltsverzeichnis

Eine der beeindruckendsten Anwendungen dieser Technologie ist die automatische Programmierung von Websites. Auf Twitter kursieren Videos, etwa von Debuild-Gründer Sharif Shameem, die zeigen, wie GPT-3 aus einer beliebigen Layoutbeschreibung JSX-Code macht. Nutzer geben lediglich einen kurzen englischen Text ein, beispielsweise: "the google logo, a search box, 2 lightgrey buttons that say ‘Search Google’ and ‘I’m feeling Lucky’ with padding in-between them”. Doch es stellt sich die Frage, wie zuverlässig das ist und ob die automatische Codegenerierung mehr als nur automatisiertes Copy-and-Paste ist.

Das Potenzial von Sprachmodellen wie GPT-3 hat auch Microsoft erkannt und im Jahr 2019 eine Milliarde US-Dollar in OpenAI investiert. Jetzt stellte die Microsoft-Tochter GitHub gemeinsam mit OpenAI den GitHub Copilot vor. Copilot nutzt Codex, eine Weiterentwicklung von GPT-3: Die KI analysiert Kommentare und das bisher geschriebene Programm, um damit einzelne Codezeilen oder ganze Funktionen zu vervollständigen.

GitHub Copilot: KI schreibt Code

Mittlerweile haben GitHub und OpenAI den GitHub Copilot vorgestellt. Der "AI Pair Programmer" schlägt beim Programmieren nicht nur einzelne Codezeilen, sondern auch komplette Funktionen vor. Grundlage der Vorschläge ist der restliche Inhalt der Datei, insbesondere auch der natürlichsprachliche Kontext wie Funktions- und Variablennamen, Kommentare und Docstrings. In vielen Demonstrationen genügen Funktionskopf und Kommentar, um die komplette Funktion zu vervollständigen.

Laut GitHub trifft der Copilot in 43 % der Fälle auf Anhieb die richtige Lösung, bei zehn Versuchen soll sich die Quote auf 57 % erhöhen. Die Vorschläge liefert das von OpenAI entwickelte Codex-Modell, das auf Milliarden öffentlicher Programm- und Textzeilen trainiert wurde. Entsprechend funktioniert der Copilot besonders gut für populäre Sprachen wie Python und JavaScript. Derzeit steht der GitHub Copilot als Erweiterung für Visual Studio Code nur einer kleinen, ausgewählten Gruppe von Testern zur Verfügung. Nach erfolgreicher Testphase will GitHub eine kommerzielle Version anbieten.

Erste Reaktionen sind mehrheitlich positiv, doch nicht immer funktioniert der von Copilot produzierte Code. GitHub selbst rät dazu, den generierten Code sorgfältig zu prüfen. Die Verantwortung dafür, dass das Programm am Ende stimmt, bleibt beim menschlichen Programmierer.

Der Klassiker unter den Methoden für die Codegenerierung ist die Programmsynthese aus logischen Spezifikationen. Genau wie eine informelle Beschreibung der Programmfunktionalität in natürlicher Sprache ist eine logische Spezifikation deklarativ, das heißt, sie kann viele verschiedene Ausführungen zulassen. Zum Beispiel fordert die Formel x > 0 nur, dass der Wert von x positiv ist; ein Programm, das x auf 1 setzt, erfüllt die Anforderung genauso wie eines, das x auf 2 oder 500 setzt. Im Gegensatz zu natürlicher Sprache haben formale Logiken eine mathematisch präzise Semantik: Ist eine Anforderung einmal als logische Formel spezifiziert, gibt es keine Unsicherheit mehr darüber, wie die Anforderung zu verstehen ist.

Ein typisches Beispiel für Systeme, die sich gut für die automatische Synthese aus logischen Spezifikationen eignen, ist der AMBA-AHB-Buscontroller von ARM. Die Advanced Microcontroller Bus Architecture (AMBA) ist ein Kommunikationsstandard für den On-Chip-Nachrichtenaustausch zwischen Prozessorkernen, Cache Memory und DMA-Controllern. An den Bus sind sechzehn solcher Geräte als Master und weitere sechzehn als Slave angeschlossen; die Master melden dem Bus Kommunikationswünsche an bestimmte Slaves und bekommen vom Buscontroller entsprechende Zeitfenster zugewiesen. Der Standard wurde in eine logische Spezifikation übersetzt und wird seither oft als Benchmark für die Codegenerierung verwendet.

Die Spezifikation besteht aus fünfzehn Formeln, die beispielsweise ausdrücken, dass jeder Master, dem ein Zeitfenster zugeteilt wird, dieses auch tatsächlich verlangt hat und dass sich die Zeitfenster verschiedener Master niemals überlappen. Aus der logischen Spezifikation erzeugt ein Synthesewerkzeug wie das am CISPA Helmholtz-Zentrum für Informationssicherheit entwickelte BoSy automatisch korrekten Verilog-Code, der sich direkt in Hardware oder auf einem FPGA (Field Programmable Gate Array) realisieren lässt.

Die nächste Abbildung zeigt das Prinzip an einem einfacheren Beispiel, der Synthese eines Arbiters: Jeder Request ist mit einem Grant zu beantworten, aber niemals dürfen zwei Grants zugleich vergeben werden. Der von BoSy automatisch generierte Verilog-Code wählt die einfachste Lösung: Er wechselt einfach zwischen den Grants hin und her.

Im Detail finden sich drei logische Formeln:

(G ((r_0) -> (F (g_0))))

bedeutet, dass ein Wert 1 auf dem Eingang r_0 (ein Request) die Ausgabe g_0 (ein Grant) auf den Wert 1 setzt.

(G ((r_1) -> (F (g_1))))

meint das Gleiche für das Eingabesignal r_1 und das Ausgabesignal g_1. Die Formel

G (!(g_0 && g_1))

besagt, dass die Ausgabesignale g_0 und g_1 niemals gleichzeitig den Wert 1 haben dürfen. Der für diese Spezifikation generierte Verilog-Code ist rechts in der Abbildung 2 zu sehen. Die synthetisierte Lösung wechselt zwischen dem Ausgangssignal g_0 und dem Ausgangssignal g_1.

Mathematisch gesehen ist die Programmsynthese aus logischen Spezifikationen perfekt: Der generierte Code ist beweisbar korrekt, das heißt, er erfüllt mit Sicherheit die gestellten Anforderungen, egal auf welchen Eingaben er angewendet wird. Diesem Vorteil steht allerdings ein hoher Rechenaufwand gegenüber. Deshalb lassen sich derzeit nur relativ kleine Programme synthetisieren. In der Praxis ist darüber hinaus der Aufwand für das logische Formalisieren der gewünschten Programmeigenschaften oft eine nicht zu unterschätzende Hürde.