Neuigkeit aus der Forschungsgruppe Knowledge-Based Systems vom 20. Januar 2025

ICCL Forschende tragen zur Lean-Standardbibliothek bei

Johannes Tantow (ehemaliger Student der Gruppe Wissensbasierte Systeme; jetzt wissenschaftlicher Mitarbeiter an der TU Chemnitz) und Lukas Gerlach (Wissenschaftlicher Mitarbeiter der Gruppe Wissensbasierte Systeme) haben kürzlich eine große Anzahl von Resultaten rund um Hash-Maps zur Standardbibliothek des interaktiven Theorembeweisers Lean beigetragen. Interaktive Theorembeweiser ermöglichen das Schreiben von Beweisen in einem maschinenüberprüfbaren Format. Im Fall von Lean werden Beweise als Teil einer funktionalen Programmiersprache geschrieben.

In seiner Diplomarbeit hat Johannes unter Aufsicht von Lukas, Stephan Mennicke und Markus Krötzsch ein Tool entwickelt, mit dem die Korrektheit von Datalog-Beweisbäumen überprüft werden kann. Dieses Tool ist in Lean geschrieben und formal verifiziert. Das heißt, wenn das Tool einen gegebenen Datalog-Beweisbaum akzeptiert, kann man sicher sein, dass der Beweisbaum tatsächlich korrekt ist. Aus Performanzgründen verwendet das Tool Hash-Maps, die bereits in der Lean-Standardbibliothek vorhanden waren, für die jedoch zu diesem Zeitpunkt nur eine Handvoll Korrektheitsergebnisse formalisiert wurden. Man möchte beispielsweise verifizieren, dass, wenn eine Hash-Map aus einer Liste von Schlüssel-Wert-Paaren erstellt wird, jeder der Schlüssel anschließend in der Hash-Map vorkommt. Obwohl solche Ergebnisse offensichtlich erscheinen, ist es keine triviale Aufgabe, dies anhand der internen Implementierung der Hash-Map zu beweisen.

In enger Zusammenarbeit mit Mitgliedern des Lean-Entwicklungsteams haben Johannes und Lukas in den letzten Wochen und Monaten viel Zeit damit verbracht, einige dieser Lücken zu schließen. Ein PR zur Überprüfung von Eigenschaften rund um das Erstellen von Hash-Maps aus Listen ist gerade mit rund 5000 hinzugefügten Codezeilen in den Main-Branch übernommen worden. Diese Änderungen werden Teil der kommenden Lean-Version 4.17 sein und von Johannes und Lukas selbst verwendet werden, um das bereits vorhandene Datalog-Beweisbaum Verifizierungstool abzurunden.

Sowohl Johannes als auch Lukas sind sehr zufrieden mit dem Verlauf der Zusammenarbeit. „Es war eine großartige Gelegenheit, nicht nur einige konkrete Beiträge für die Lean-Community zu leisten, sondern auch wertvolle Einblicke in die Entwicklung von Lean im großen Maßstab zu erhalten“, sagte Lukas.