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
Nr. 223/2017 vom 21.08.2017
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. Dennoch schaffte es der vergleichsweise junge Leo-III 382 der 500 gestellten Aufgaben als korrekt zu beweisen; einzig der an der Universität Innsbruck und Tschechischen Technischen Universität Prag entwickelte Beweiser Satallax konnte mehr Beweise liefern. Die Entwicklung von Leo-III wurde von der Deutschen Forschungsgemeinschaft (DFG) gefördert und ist als Open-Source-Software frei verfügbar.
Kontakt
Alexander Steen, Dahlem Center for Machine Learning and Robotics, Institut für Informatik, Freie Universität Berlin, Telefon: 030 / 838-75101, E-Mail: a.steen@fu-berlin.de