Die KI-Forscherin, die Formeln für morgen erfindet

SYMBOLISCHE KI arbeitet mit mathematischer Logik statt statistischer Daten - so lässt sich der Unterschied zwischen symbolischer KI und anderen KI-Forschungszweigen beschreiben. "Wir hängen nicht von der Statistik ab. Wir arbeiten mit präzisen Formeln, um Systeme zu beschreiben", sagt Martina Seidl.

In der Praxis sind bestimmte dieser Formeln extrem relevant. "Amazon braucht diese Formeln, um die Zugangsrechte für seine Cloudservices zu organisieren." Derzeit optimiert Seidl mit diesen Formeln Maschinen eines oberösterreichischen Industrieunternehmens.

Seidl hat sich für diese Formeln (Quantified Boolean Formulas) bereits interessiert, als KI noch ein Nischenthema war und die vielen praktischen Anwendungen nicht absehbar waren. Neben der forscherischen Neugier ist Geduld wichtige Voraussetzung: "Für die Formeln, die mich am meisten interessieren, fehlt noch die Killer-App. Ein Riesendurchbruch wäre die industrielle Anwendung, die es für ähnliche Formeln schon gibt."

Eine solche Killer-App hat Professor Armin Biere mit dem Bounded Model Checking vor 20 Jahren gefunden - das ist heute ein Standardverfahren in der Chipproduktion. 2010 hatte Biere, der "Hochreiter" für Symbolic AI, Seidl für sein Institut an der JKU Linz angeworben, 2016 habilitierte sie dort und gründete 2020 das Institut für Symbolic AI.