KI-Agenten übersetzen CPython in Lean und finden 418 Bugs
Formalizing CPython
Ein Team ließ Opus 5.5 die Funktionen von CPython Zeile für Zeile in Lean nachbauen, jede Kopie gegen echtes Python auf mindestens 50.000 Eingaben testen und die Beweise von einem zweiten Agenten prüfen. 4.071 Funktionen haben diese Kontrolle bestanden, insgesamt 613.318 Zeilen Lean mit 18.898 Theoremen. Dabei kamen 418 Fehlerberichte zutage, etwa 55 davon können den Interpreter zum Absturz bringen oder Speicher beschädigen.
Der schwierigste Teil war nicht, KI-Agenten zum Schreiben von Beweisen zu bringen, sondern Beweise zu bekommen, die tatsächlich etwas bedeuten.
- debugnik
Wäre es nicht produktiver, die Tokens dafür zu verwenden, ACSL-Annotationen hinzuzufügen, um CPython mit Frama-C zu verifizieren? Man würde die tatsächliche Laufzeitumgebung verifizieren statt eine KI-Übersetzung davon, und Fixes könnten direkt upstream beigesteuert werden.
- anewhnaccount2
Gleicher Ansatz für Julias stdlib: https://discourse.julialang.org/t/formalizing-julia-in-lean-...
- jakobnissen
Ich denke, dieser Ansatz zur Fehlersuche ist super vielversprechend (offensichtlich – er findet eine Menge Fehler). Das langfristige Problem ist, wie diese Art der Fehlersuche routinemäßig durchgeführt werden kann, z. B. als Teil einer Testsuite. Der von diesen Leuten gewählte Ansatz, derselbe wie bei den Julia-Leuten, ist nicht wirklich automatisierbar, weil er viel Arbeit sowohl von Menschen als auch von KI-Agenten erfordert.
Ich schätze, längerfristig muss es in die Sprache eingebaut werden, um zu verhindern, dass Code und Lean-Beweise auseinanderdriften. Das heißt, es könnten Opt-in-Eigenschaften sein, die zusammen mit dem Code geschrieben und dann in der Testsuite überprüft werden. Also sehr ähnlich zu gewöhnlichen Compiler-Prüfungen, nur ausdrucksstärker und teurer, und nur zur Testzeit durchgeführt.
- tomtom1337
Ich bin bei ein paar Punkten verwirrt und würde mich freuen, wenn mir jemand helfen könnte, das zu klären!
- Wenn die Neuschreibung in Lean Zeile für Zeile erfolgt, wie können sich die beiden Implementierungen dann in ihrem Ergebnis unterscheiden (Schritt 2)?
- Woher weiß dieser Ansatz in Schritt 3, was "etwas, das immer wahr sein sollte" ist (ist es die Intelligenz des LLM, das "rät"?).
- erfgh
Liest überhaupt jemand Artikel, die von KI geschrieben wurden? Das ist eine ernst gemeinte Frage.