TLS4AI: Temporal Logic Sketching für Künstliche Intelligenz

• Antragsteller: Professor Dr. Daniel Neider
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 434592664

Formale Methoden umfassen eine Reihe von rigorosen, mathematischen Verfahren, die für die Spezifikation, den Entwurf und die Verifikation von Software, Hardware und cyber-physischen Systemen eingesetzt werden. Diese Techniken haben sich über Jahrzehnte hinweg bewährt und gewährleisten die Sicherheit und Zuverlässigkeit komplexer Computersysteme in einer Vielzahl von Bereichen wie der Software-, Automobil- und Luftfahrtindustrie sowie in kritischen Infrastrukturprojekten. Trotz dieses Erfolgs gibt es ein entscheidendes und oft vernachlässigtes Hindernis bei formalen Methoden: Praktisch alle Techniken beruhen auf der Annahme, dass die für den Entwurf oder die Verifikation eines Systems erforderlichen Spezifikationen in einem geeigneten Format vorliegen, funktional korrekt sind und die angestrebten Eigenschaften exakt beschreiben. Diese Annahmen sind jedoch oft unrealistisch, da die Formalisierung von Systemanforderungen äußerst komplex und fehleranfällig ist. Als mögliche Lösung für dieses herausfordernde Problem wurde in dem Vorgängerprojekt ein neues Konzept namens Temporal Logic Sketching (TLS) entwickelt. Dieser computergestützte Ansatz ermöglicht es Entwicklern, formale Spezifikationen zu erstellen, indem sie ihr Wissen über ein System zunächst durch einen sogenannten Sketch -- einer unvollständigen Spezifikation -- ausdrücken. Dabei können schwer zu formalisierende Teile der Spezifikation weggelassen und durch Beispiele für das gewünschte und unerwünschte Verhalten des Systems ersetzt werden. Basierend darauf vervollständigt dann ein Sketching-Algorithmus diesen Sketch, indem er die nicht spezifizierten Komponenten unter Berücksichtigung der Beispiele ergänzt. Das Ergebnis ist eine vollständige Spezifikation, die mit den bereitgestellten Beispielen konsistent ist und die Designziele des Entwicklers reflektiert. Aufgrund der stark wachsenden Bedeutung von sicherer und zuverlässiger KI und dem damit verbundenen Einsatz formaler Methoden besitzt TLS enormes Potential im KI-Bereich. Allerdings wurde TLS mit Blick auf formale Verifikation und Synthese entwickelt, was es oft schwierig und unpraktikabel macht, diese Methodik im KI-Bereich einzusetzen. Ziel dieses Folgeprojekts ist es daher, TLS zu erweitern und verbessern, um den Anforderungen von KI-Anwendungen besser gerecht zu werden. Insbesondere werden wir (i) TLS auf Multi-Agenten-Systeme und interpretierbares maschinelles Lernen erweitern, (ii) die Integration von Domänenwissen verbessern, (iii) die theoretischen Grundlagen von TLS untersuchen, (iv) seine Skalierbarkeit verbessern und (v) ein Software-Tool und einen webbasierten Demonstrator implementieren, um unsere Algorithmen empirisch zu evaluieren und die breite Sichtbarkeit unserer Forschung sicherzustellen. Durch dieses Projekt wird die Anwendung formaler Methoden in der KI erheblich vereinfacht, was es Forschern bzw. Praktikern ermöglichen wird, robustere, sicherere und transparentere KI-Systeme zu entwickeln.

• DFG-Verfahren: Sachbeihilfen