Not Letting Proofs Die: xLaDe, a Lean 4 Ecosystem Framework

In der Welt der modernen Mathematik und des Software-Engineerings gibt es eine wachsende Bewegung, Beweise und Programme so zu schreiben, dass Computer sie auf absolute Korrektheit prüfen können. Anstatt sich auf menschliche Augen zu verlassen, die Fehler in einem komplexen Argument entdecken sollen, nutzen Forscher spezialisierte Softwarewerkzeuge, die sogenannten Proof Assistants (Beweisassistenten). Diese Programme fungieren als rigorose Editoren, die jeden einzelnen logischen Schritt verifizieren, um sicherzustellen, dass ein Ergebnis zweifelsfrei wahr ist. Systeme wie Lean 4 sind für diese Arbeit populär geworden und ermöglichen es großen Teams, massive Bibliotheken verifizierter Mathematik und sicherer Software aufzubauen. Diese Werkzeuge werden jedoch ständig aktualisiert und verbessert. Genau wie ein Haus, das mit einem Satz von Bauplänen errichtet wurde, der morgen vielleicht nicht mehr standhalten würde, wenn sich die Regeln für die Konstruktion ändern, könnte ein mathematischer Beweis, der heute perfekt funktioniert, morgen nicht mehr lauffähig sein, wenn sich die Softwareversion ändert. Dies schafft ein Problem für die langfristige Geschichte der Wissenschaft: Wenn sich die Werkzeuge zu schnell entwickeln, könnte die heute geleistete Arbeit in der Zukunft unmöglich zu reproduzieren oder zu verstehen sein.

Ein Forscherteam der Central University of Andhra Pradesh hat einen neuen Weg vorgeschlagen, um dieser Herausforderung zu begegnen – nicht, indem es die Veränderung der Software verhindert, sondern indem es eine Schutzschicht um sie herum baut. Sie nennen ihre Schöpfung xLaDe, was für das „Experimental Lean 4 Advanced Development Ecosystem“ steht. Anstatt zu versuchen, die Lean-Software in der Zeit einzufrieren oder sie dazu zu zwingen, gleich zu bleiben, fungiert xLaDe als ein hochentwickeltes Aufzeichnungs- und Managementsystem, das über den bestehenden Werkzeugen sitzt. Sein Ziel ist es, die Kernsoftware als ein solides, unveränderliches Fundament zu behandeln, während Forscher darüber frei experimentieren können. Das Framework ist darauf ausgelegt, jedes Detail darüber zu erfassen, wie ein Beweis ausgeführt wurde – die spezifische Version der Software, die Abhängigkeiten und die exakten Bedingungen der Umgebung –, damit die Arbeit auch Jahre später rekonstruiert werden kann, selbst wenn sich die zugrunde liegenden Werkzeuge weiterentwickelt haben.

Die Kernidee hinter xLaDe ist eine strikte Trennung zwischen dem vertrauenswürdigen Herzstück des Systems und der experimentellen Arbeit, die darum herum stattfindet. Die Forscher behandeln die Lean-Software selbst als unveränderliche Infrastruktur (immutable infrastructure), was bedeutet, dass sie durch die Experimente niemals verändert werden darf. Stattdessen agiert xLaft als Orchestrierungsschicht, ein Satz von Werkzeugen, die sich um externe Projekte legen, ohne deren Quellcode zu berühren. Dieser Ansatz ermöglicht es Wissenschaftlern, neue Ideen zu testen, Arbeitsabläufe zu ändern und verschiedene Wege auszuprobieren, wie sie ihre Arbeit organisieren, ohne die Integrität der mathematischen Beweise selbst zu gefährden. Wenn ein Experiment schiefgeht oder verworfen werden muss, kann es sauber entfernt werden, ohne Spuren zu hinterlassen oder die stabilen Teile des Projekts zu beeinflussen. Diese Umkehrbarkeit ist entscheidend, da sie Forscher dazu ermutigt, Neues auszuprobieren, ohne die Befürchtung haben zu müssen, ihre Arbeit dauerhaft zu beschädigen.

Um dieses System nutzbar zu machen, hat das Team ein Kommandozeilen-Tool gebaut, das als Hauptschnittstelle für Benutzer dient. Dieses Tool verwaltet verschiedene „Modi“ des Betriebs, sodass dasselbe Framework unterschiedliche Bedürfnisse bedienen kann. Es gibt einen Onboarding-Modus für Anfänger, der sanfte Anleitung bietet, einen experimentellen Modus, in dem Forscher neue Arbeitsabläufe und Richtlinien testen können, und einen stabilen Modus, der die Dinge festlegt, um eine zuverlässige, langfristige Nutzung zu gewährleisten. Im stabilen Modus erzwingt das System strikte Regeln, um sicherzustellen, dass sich nichts unerwartet ändert, was es ideal für die Bewahrung von Forschungsergebnissen macht. Das Tool zeichnet auch automatisch Metadaten auf, wie etwa den Zeitpunkt, zu dem ein Experiment lief, und die beteiligten Softwareversionen, wodurch ein detaillierter Audit-Trail entsteht. Dies stellt sicher, dass jeder, der die Arbeit in der Zukunft betrachtet, genau sehen kann, wie sie durchgeführt wurde, und über die Informationen verfügt, die zur Wiederholung notwendig sind.

Die Forscher testeten ihr Framework mit zwei spezifischen Experimenten, um zu sehen, ob es in der Praxis tatsächlich funktionieren kann. In dem ersten Test nahmen sie ein kleines, in sich geschlossenes Projekt, das speziell für die Studie erstellt wurde, und betetteten es in das xLaDe-System ein. Sie ließen den Build-Prozess des Projekts durch das Framework laufen, ohne eine einzige Zeile des ursprünglichen Codes zu ändern. Das System kompilierte die Beweise erfolgreich und zeichnete die Ergebnisse auf, was bewies, dass es externe Projekte verwalten kann, während es sie vollständig vom Framework selbst trennt. In einem zweiten, strengeren Test wandten sie dieselbe Methode auf einen völlig unabhängigen Bildungskurs zu Lean 4 an, der von jemandem außerhalb ihres Teams erstellt wurde. Dieses Projekt hatte keine vorherige Beziehung zu xLaDe. Das Framework integrierte den Kurs erfolgreich, führte dessen Build-Prozess aus und verifizierte, dass er funktionierte, ohne die Kursdateien oder die Lean-Software zu modifizieren. Diese Ergebnisse legen nahe, dass das System als universeller Wrapper fungieren kann, der es ermöglicht, vielfältige Projekte unter einem gemeinsamen Satz von Regeln zu verwalten und zu reproduzieren.

Sicherheit und Vertrauen stehen im Zentrum des Designs von xLaDe. Die Forscher räumen ein, dass sie nicht gegen jede mögliche Bedrohung schützen können, wie etwa einen kompromittierten Computer oder einen böswilligen Insider mit Zugriff auf den Code. Stattdessen konzentrieren sie sich auf Transparenz und Verifizierung. Das System nutzt mehrere Spiegelserver (Mirrors), um den Code zu hosten, wodurch sichergestellt wird, dass das Projekt auch dann zugänglich bleibt, wenn eine Website offline geht. Es veröffentlicht zudem kryptografische Schlüssel und Prüfsummen – digitale Fingerabdrücke, die es Benutzern ermöglichen, zu verifizieren, dass die Dateien, die sie herunterladen, genau die sind, die die Autoren beabsichtigt haben, ohne versteckte Änderungen. Ein wesentlicher Teil dieses Sicherheitsmodells ist die automatische Erkennung jeglicher Versuche, die Kern-Lean-Software zu modifizieren. Wenn ein Skript oder ein Benutzer versucht, das unveränderliche Fundament zu ändern, erkennt das System die Verletzung und stoppt den Prozess, um sicherzustellen, dass die Integrität der mathematischen Beweise niemals durch experimentelle Werkzeuge gefährdet wird.

Das Paper kommt zu dem Schluss, dass xLaDe zwar noch ein experimentelles Projekt und keine fertige Lösung ist, aber einen vielversprechenden Weg für die Zukunft der formalen Verifikation bietet. Es beansprucht nicht, das Problem der Abwärtskompatibilität zu lösen, bei der alter Code gezwungen wird, mit neuen Werkzeugen zu funktionieren. Stattdessen bietet es eine andere Lösung an: die Bewahrung des Kontextes, in dem der Code geschrieben wurde. Indem es die Umgebung aufzeichnet und Experimente als erstklassige Forschungsartefakte behandelt, ermöglicht das Framework der Gemeinschaft, historische Ergebnisse mit Zuversicht wieder aufzugreifen. Die Autoren betonen, dass ihre Arbeit eine Methodik zur Durchführung von Ökosystem-Forschung ist, die einen strukturierten Weg bietet, um Ideen zu testen, Fehler zu dokumentieren und erfolgreiche Werkzeuge zu teilen. Durch diesen Ansatz hoffen sie, eine nachhaltige Umgebung zu schaffen, in der die schnelle Evolution von Beweisassistenten nicht auf Kosten der wertvollen Arbeit geschieht, die auf ihnen aufgebaut wurde.