Informatiker der Freien Universität werden Vizeweltmeister im Automatischen Theorembeweisen

Der an der Freien Universität Berlin entwickelte automatische Theorembeweiser Leo-III hat in der Weltmeisterschaft im Theorembeweisen in der Kategorie ,,höherstufige Logik" den zweiten Platz belegt. Das Computerprogramm Leo-III wird seit 2014 von den wissenschaftlichen Mitarbeitern Alexander Steen und Max Wisniewski unter der Leitung von Dr. Christoph Benzmüller am Dahlem Center for Machine Learning and Robotics des Instituts für Informatik der Freien Universität Berlin entwickelt. Anfang August konnte das Programm bei der ,,CADE ATP System Competition 2017" im schwedischen Gothenburg 382 der 500 gestellten Aufgaben als korrekt beweisen und belegte damit den zweiten Platz. Automatische Theorembeweiser sind Computerprogramme, die eine Menge von Annahmen - genannt Axiome - und eine Vermutung als Eingabe erhalten und innerhalb einer vorher bestimmten Zeit versuchen, vollautomatisch einen formalen mathematischen Beweis für die Gültigkeit der Vermutung zu finden. Dazu werden sowohl die Annahmen als auch die Vermutung in einem mathematischen Logikformalismus formuliert. In der jährlich stattfindenden Weltmeisterschaft solcher Theorembeweiser, der ,,CADE ATP System Competition", treten die besten Theorembeweiser in verschiedenen Kategorien gegeneinander an und versuchen, aus den 500 zufällig gewählten Problemen so viele wie möglich zu lösen. Leo-III tritt dabei in einer besonders herausfordernden Kategorie des Theorembeweisens an, bei der viele Aspekte Gegenstand aktueller Grundlagenforschung sind.