News104: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Alex Ivliev (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=ICCL Forschende tragen zur Lean-Standardbibliothek bei |Titel EN=ICCL Researchers Contribute to Lean Standard Library |Beschreibung DE=<p>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 Standard…“) |
Alex Ivliev (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 2: | Zeile 2: | ||
|Titel DE=ICCL Forschende tragen zur Lean-Standardbibliothek bei | |Titel DE=ICCL Forschende tragen zur Lean-Standardbibliothek bei | ||
|Titel EN=ICCL Researchers Contribute to Lean Standard Library | |Titel EN=ICCL Researchers Contribute to Lean Standard Library | ||
|Beschreibung DE=<p>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 [https://lean-lang.org/ 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.</p><p>In seiner Diplomarbeit hat Johannes unter Aufsicht von Lukas, [[Stephan Mennicke]] und [[Markus Krötzsch]] ein [https://github.com/knowsys/CertifyingDatalog 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. | |Beschreibung DE=<p>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 [https://lean-lang.org/ 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.</p><p>In seiner Diplomarbeit hat Johannes unter Aufsicht von Lukas, [[Stephan Mennicke]] und [[Markus Krötzsch]] ein [https://github.com/knowsys/CertifyingDatalog 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.</p><p>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 [https://github.com/leanprover/lean4/pull/6211 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.</p><p>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.</p> | Obwohl solche Ergebnisse offensichtlich erscheinen, ist es keine triviale Aufgabe, dies anhand der internen Implementierung der Hash-Map zu beweisen.</p><p>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 [https://github.com/leanprover/lean4/pull/6211 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.</p><p>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.</p> | ||
|Beschreibung EN=<p>Johannes Tantow (former student at the Knowledge-Based Systems group; now Research Associate at TU Chemnitz) and [[Lukas Gerlach]] (Research Associate at the Knowledge-Based Systems group) have recently contributed a sizable number of results around hash maps to the standard library of the interactive theorem prover [https://lean-lang.org/ Lean]. Interactive theorem provers allow to write proofs in a machine-verifiable format. In the case of Lean, proofs are written as part of a functional programming language.</p><p>In his Diploma Thesis, Johannes, under supervision of Lukas, [[Stephan Mennicke]], and [[Markus Krötzsch]], built a [https://github.com/knowsys/CertifyingDatalog tool] that is able to check correctness of Datalog proof trees. This tool is written and formally verified in Lean. That is, if the tool accepts a given Datalog proof tree, we can be certain that the proof tree is indeed correct. For performance reasons, this tool is using hash map data structures, which already existed in the Lean standard library but only a handful of correctness results had been formalized at the time. | |Beschreibung EN=<p>Johannes Tantow (former student at the [[Knowledge-Based Systems]] group; now Research Associate at TU Chemnitz) and [[Lukas Gerlach]] (Research Associate at the [[Knowledge-Based Systems]] group) have recently contributed a sizable number of results around hash maps to the standard library of the interactive theorem prover [https://lean-lang.org/ Lean]. Interactive theorem provers allow to write proofs in a machine-verifiable format. In the case of Lean, proofs are written as part of a functional programming language.</p><p>In his Diploma Thesis, Johannes, under supervision of Lukas, [[Stephan Mennicke]], and [[Markus Krötzsch]], built a [https://github.com/knowsys/CertifyingDatalog tool] that is able to check correctness of Datalog proof trees. This tool is written and formally verified in Lean. That is, if the tool accepts a given Datalog proof tree, we can be certain that the proof tree is indeed correct. For performance reasons, this tool is using hash map data structures, which already existed in the Lean standard library but only a handful of correctness results had been formalized at the time. | ||
For example, one would like to verify that if a hash map is built from a list of key-value pairs, then each of the keys occurs in the hash map afterwards. While such results seem obvious, it is a non-trivial task to prove this over the internal implementation of the hash map.</p><p>In close collaboration with members of the Lean development team, Johannes and Lukas spent some time throughout the last weeks and months to fill in some of these gaps. A [https://github.com/leanprover/lean4/pull/6211 PR] verifying properties around building hash maps from lists just landed on the main branch with around 5000 lines of code added. These changes will be part of the upcoming Lean version 4.17 and be used by Johannes and Lukas themselves to round up the already existing Datalog proof tree verification tool.</p><p>Both Johannes and Lukas are very happy with how the collaboration went. "It was a great opportunity to not only make some tangible contributions for the Lean community but also to obtain valuable insights about developing Lean at scale", Lukas said.</p> | For example, one would like to verify that if a hash map is built from a list of key-value pairs, then each of the keys occurs in the hash map afterwards. While such results seem obvious, it is a non-trivial task to prove this over the internal implementation of the hash map.</p><p>In close collaboration with members of the Lean development team, Johannes and Lukas spent some time throughout the last weeks and months to fill in some of these gaps. A [https://github.com/leanprover/lean4/pull/6211 PR] verifying properties around building hash maps from lists just landed on the main branch with around 5000 lines of code added. These changes will be part of the upcoming Lean version 4.17 and be used by Johannes and Lukas themselves to round up the already existing Datalog proof tree verification tool.</p><p>Both Johannes and Lukas are very happy with how the collaboration went. "It was a great opportunity to not only make some tangible contributions for the Lean community but also to obtain valuable insights about developing Lean at scale", Lukas said.</p> | ||
|Datum=2025/01/20 | |Datum=2025/01/20 | ||
Aktuelle Version vom 20. Januar 2025, 15:50 Uhr
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.
