Auf der Suche nach optimalen Berechnungen mit Erklärungen

Eine Vielzahl von Aufgaben in der Informatik, insbesondere der formalen Verifikation, dem Entwurf von elektronischen Schaltungen und Computer-Chips sowie der künstlichen Intelligenz, lassen sich mit Hilfe logischer Ausdrücke und Bedingungen beschreiben. Solver werden üblicherweise zur Lösung von Planungs- und Optimierungsfragen eingesetzt, die auch bei vielen praktischen Problemen eine wichtige Rolle spielen. Im Gesundheitsbereich stellt sich beispielsweise bei Patienten, die an mehreren chronischen Krankheiten gleichzeitig leiden, die Frage, welche Kombination von Medikamenten und Behandlungen für einen einzelnen Patienten unter Berücksichtigung seiner persönlichen Präferenzen optimal ist, so dass die bestmögliche Wirkung erzielt und zugleich das Risiko von unerwünschten Wechsel- bzw. Nebenwirkungen minimiert wird. Die zugrundeliegenden logischen Ausdrücke und Bedingungen können sehr komplex sein und viele (hunderte) Variablen umfassen. Sie können mit den bestehenden computer- unterstützten Lösungsverfahren auf unterschiedliche Weise berechnet werden, je nachdem, ob es sich um Ausdrücke mit rein logischen Bedingungen oder auch um Bedingungen mit numerischen Parametern handelt. In diesem Projekt wird ein allgemein verwendbarer, formaler Ansatz basierend auf solchen bestehenden, automatisierten Lösungsverfahren entwickelt, mit dem die Suche nach optimalen Lösungen hinsichtlich unterschiedlicher Kriterien (Zeit, Vollständigkeit, Wirksamkeit, Kosten, Energieverbrauch usw.) gesteuert werden kann. Der Ansatz soll jedoch nicht nur optimale Lösungen berechnen, sondern auch den Lösungsweg nachvollziehbar und die Lösungen damit erklärbar machen. Erklärbarkeit ist eine wichtige Eigenschaft, denn sie erlaubt dem Benutzer verschiedene Lösungen zu vergleichen, die Unterschiede zu verstehen und die optimale Lösung bzw. den optimalen Berechnungsansatz für den jeweiligen Einsatzzweck auszuwählen. Logik dient auch dabei als vereinheitlichendes Werkzeug für die Modellierung, Argumentation, Suche und Erklärung optimaler Berechnungen. Das Projekt wird von Frau Dr. Juliana Küster Filipe Bowles am Software Competence Center Hagenberg (SCCH) durchgeführt. Sie arbeitet dort mit Forschern aus den Bereichen der Software Science und Data Science zusammen, in denen die Projektergebnisse einfließen und für verschiedene praktische und industrielle Anwendungen (z.B. Robotersteuerung, Medizintechnik, Energieversorgung) angewendet werden.