Ob Softwareverifikation oder Künstliche Intelligenz: automatische Theorembeweiser sind dort essenziell, wo die Korrektheit komplexer Systeme mathematisch nachgewiesen werden muss. Sie können logische Aussagen selbstständig analysieren und mithilfe formaler Methoden beweisen oder widerlegen. Damit sind sie eine wichtige Grundlage für sichere Software, verlässliche KI und formale Verifikation.

Mit Vampireentwickelt die Research Unit FORSYTE, öffnet eine externe URL in einem neuen Fenster von Laura Kovács, öffnet eine externe URL in einem neuen Fenster an der TU Wien in enger Zusammenarbeit mit der Universität Manchester, der Universität Southampton und der Technischen Universität in Prag den weltweit leistungsstärksten automatischen Theorembeweiser Vampire. Nun konnte das System seinen internationalen Spitzenplatz erneut unter Beweis stellen und gewann – wie bereits im Vorjahr – haushoch.

Neben dem Wettbewerbserfolg stellte das Team auch ein neues KI-System vor: Gemeinsam mit UnAxiMa, öffnet eine externe URL in einem neuen Fenster PhD-Student Jonas Bodingbauer, öffnet eine externe URL in einem neuen Fenster entwickelten die Forschenden VaLeaDate, ein Werkzeug zur Bewertung und Überprüfung automatisch erzeugter Beweise. Das System wurde als Most Valuable Benchmark Contributor ausgezeichnet und setzt damit neue Maßstäbe für vertrauenswürdige KI-gestützte Beweissysteme.

Neben dem Erfolg von FORSYTE wurde die TU Wien auch für die Entwicklung des besten Beweisprüfers GAPT ausgezeichnet. Entwickelt von Fabian Achammer, öffnet eine externe URL in einem neuen Fenster, Martin Riener, öffnet eine externe URL in einem neuen Fenster und Stefan Herzl, unterstreicht der Erfolg der TU Wien im Bereich der Beweisprüfung die herausragende Zusammenarbeit zwischen den Fakultäten für Informatik und Mathematik und Geoinformation.

Informatik-Dekanin Gerti Kappel, öffnet eine externe URL in einem neuen Fenster gratuliert dem Team: „Die erneuten Erfolge zeigen eindrucksvoll, dass Spitzenforschung an der TU Wien international Maßstäbe setzt. Automated Reasoning ist eine Schlüsseltechnologie für sichere Software, verlässliche KI und zahlreiche wissenschaftliche Anwendungen. Ich gratuliere dem gesamten Team herzlich zu diesen herausragenden Auszeichnungen und freue mich, dass die TU Wien ihre internationale Führungsrolle in diesem zukunftsweisenden Forschungsgebiet weiter ausbaut.“

Ohne ausreichende Finanzierung ist eine solche Spitzenforschung nicht möglich. Dieser Erfolg zeigt, was die enge Verbindung von Forschung und moderner Forschungsinfrastruktur leisten kann. Eine Schlüsselrolle spielte Research Software Engineer Márton Hajdu, öffnet eine externe URL in einem neuen Fenster, der aktuelle Forschungsergebnisse in hochoptimierte Software überführt. Ebenso entscheidend ist der Automated Reasoning Computing Cluster der TU Wien, der leistungsstarke lokale Berechnungen ermöglicht.

Laura Kovács: „Diese Spitzenleistung zeigt, wie wichtig das Zusammenspiel von exzellenter Grundlagenforschung und moderner Forschungsinfrastruktur ist – besonders in der Verbindung von Mathematik und Informatik. Der Erfolg ist auch unserer Kolleg_innen an der Fakultät für Mathematik und Geoinformation zu verdanken. Gemeinsam haben wir erneut unter Beweis gestellt, dass die TU Wien zu den weltweit führenden Standorten für Logik, Automated Reasoning und Formal Methods zählt.“