Automatischer Theorembeweiser

Prof. Dr. Stephan Schulz und Martin Möhrmann (M.Sc.) entwickeln an der DHBW Stuttgart auch im Rahmen von Studienarbeiten (PDF) den automatischen Theorembeweiser E. Automatische Theorembeweiser sind Computerprogramme, die nachweisen, dass bestimmte Aussagen zwingend aus einer gegebenen formalen Beschreibung folgen. Ein wichtiges Anwendungsbeispiel ist die Verifikation von Software, z. B. der Nachweis, dass ein Fahrerassistenzsystem einen PKW niemals beschleunigt, wenn der Fahrer die Bremse tritt, oder dass eine Banktransaktion immer entweder vollständig oder gar nicht abgewickelt wird. Ein anderes Anwendungsbeispiel ist die Beantwortung von komplexen Fragen über großen formalen Wissensbasen, etwa die Frage "Welche europäischen Großstädte sind von Überflutungen bedroht?"

Theorembeweiser sind heute hoch entwickelt, und können sehr schnell Fragmente der Wissensbasis kombinieren, um so neue, gesicherte Aussagen herzuleiten. Ein Problem ist aber die Steuerung dieser Ableitungen – die Menge der ableitbaren Fakten ist in der Regel unendlich, und die allermeisten dieser Fakten sind für eine gegebene Fragestellung irrelevant. Um dieses Problem anzugehen, verfolgen die Forscher an der DHBW den Ansatz, aus einfachen automatischen Beweisen das Vorgehen auch für komplexere Probleme zu erlernen.

Zur Entwicklung dieser Suchheuristiken sollen mit Hilfe von künstlichen neuronalen Netzwerken große Datenmengen analysiert werden. NVIDIA fördert diesen Ansatz, indem sie dem Projekt im Rahmen eines Academic Hardware Grants einen Rechenbeschleuniger des Typs GeForce GTX TITAN X zur Verfügung stellt. Die GeForce GTX TITAN X besitzt 3072 Rechenkerne und 12 Gigabyte RAM mit einer Speicherbandbreite von 336,5 Gigabyte pro Sekunde. Die maximale theoretisch erreichbare Rechenleistung der Karte beträgt 6,144
TeraFLOPS.

Im Theorembeweisen stehen auf der einen Seite die syntaktische Manipulation von symbolischen Formeln nach strikten Regeln, auf der anderen Seite die unscharfe Intuition über die Struktur des Beweises und vielversprechende Zwischenergebnisse. Die Forscher hoffen hier mit Techniken des Deep Learning auf einen ähnlichen Durchbruch wie ihn kürzlich z. B. das Programm AlphaGo der Firma Google DeepMind erzielte, das den weltbesten Profispieler 4 zu 1 besiegen konnte. Auch bei Go stehen die strengen Spielregeln auf der einen Seite einer unscharfen Bewertung der erlaubten Züge auf der anderen Seite gegenüber.

Das Forschungsprojekt zur Weiterentwicklung des Theorembeweisers E findet im Rahmen des DHBW Innovationsprogramms Forschung im Fachbereich Informatik an der DHBW Stuttgart statt. Der Theorembeweiser E ist eines führenden Systeme für das automatische Schließen in Prädikatenlogik erster Stufe. Auch Studierende können im Rahmen von Studienarbeiten zu dem Erfolg des Projekts beitragen.