Formale Beweistechnologien, die zur Validierung von komplexen mathematischen Beweisen oder auch zur Verifikation von Hard- und Software eingesetzt werden, sind Forschungsgegenstand von Cezary Kaliszyk. „Es ist wichtig, dass Programme auf alle möglichen Eventualitäten geprüft werden. Man kann sie testen und bestätigen, dass sie im ersten, zweiten oder dritten Fall einwandfrei funktionieren. Auch wenn man eine Million Tests durchführt, kann man noch nicht sicher sein, dass es nicht doch einen Fall gibt, in dem das Programm versagt“, erklärt Kaliszyk, der daran arbeitet, dass der Grad der Gewissheit, ob Software funktioniert und fehlerfrei ist, erhöht wird. Bisher brauchten die dazu verwendeten Computerprogramme und Beweisassistenten manuelle Unterstützung von Expertinnen und Experten.
Automatisches Lernen
Der Informatiker arbeitet derzeit daran, Beweistechnologien zu automatisieren und mit automatischem Lernen zu kombinieren, womit die bisher hohen Kosten solcher Prüfungen verringert werden sollen. „Meine Hoffnung ist es, dass Programme die aufwändigen Prüfungen übernehmen und mit der Zeit einen Teil der Rolle von Mathematikerinnen und Mathematikern einnehmen können. Ziel ist es, Beweisassistenten intelligenter zu machen sowie ihre Arbeit zu automatisieren“, so der Wissenschaftler. Die Forschungen von Cezary Kaliszyk sollen schlussendlich dazu führen, dass Programme mehr Probleme lösen und dadurch mehr Beweise durchgeführt werden können. „Wir konnten bereits zeigen, dass der Grad der Automatisierung in diesem Bereich deutlich erhöht werden kann. In einem weiteren Schritt soll die bisherige Arbeit mit Techniken des maschinellen Lernens kombiniert werden. Dadurch sollen Computer automatisch von früheren Beweisen lernen“, erläutert Kaliszyk. Für Menschen ist es leicht, das erlernte Wissen, wie das Addieren von niedrigen Zahlen, auf komplexere Rechenoperationen anzuwenden: „Wir lernen schon in der Volksschule: 2 + 2 = 4 oder 5 + 6 = 11. Daraus abgeleitet können wir auch lernen, größere Zahlen zu addieren. Dies ist aber immer noch eine große Herausforderung für Computer“, erklärt der Informatik-Experte. Als Beispiel führt Kaliszyk die Bestrebungen an, selbstfahrende Autos zu programmieren. „Man muss unzählige Situationen simulieren, in die Autos im Straßenverkehr kommen können. Ein spezieller Algorithmus kann lernen, wie man ein Auto fährt, ein Unterfangen, das bisher nicht modellierbar war.“ In den nächsten zehn bis fünfzehn Jahren sollte es laut Kaliszyk mehr Software geben, die zu 100 Prozent fehlerfrei sein wird. Ausblickend sollten die Programme irgendwann auch in der Lage sein, komplexere Lösungen anzubieten. Die Resultate seiner Forschungen sollen die Arbeit von Expertinnen und Experten der Mathematik und Informatik im Umgang mit Beweisassistenten erleichtern.
Zur Person
Priv.-Doz. Dr. Cezary Kaliszyk ist Mitarbeiter der Forschungsgruppe Computational Logic am Institut für Informatik. Der in Polen geborene Wissenschaftler studierte in Polen, Frankreich und den Niederlanden, war Postdoc an der Technischen Universität München und arbeitete an der Universität Tsukuba in Japan. Im Jahr 2012 wechselte er an die Uni Innsbruck, wo er im September 2016 den ERC Starting Grant für seine Arbeit gewann.