Logik und Lernen
Unsere Arbeit zu Logik und Lernen integriert deduktives und induktives Denken und bildet (teilweise) die Grundlage für die Lehre der Gruppe im Spezialisierungsthema „Logik und Lernen“ des Informatik-Masters.
Reinforcement Learning
Wir untersuchen eine neue Sicht auf das verstärkende Lernen (Reinforcement Learning), wobei wir an Anwendungen von RL in Anwendungsfällen interessiert sind, bei denen die durchschnittlichen Belohnungen ungleich Null sein können. Während RL-Methoden umfassend erforscht wurden, hat dieser spezielle Anwendungsbereich in der Literatur nur wenig Beachtung gefunden. Unsere Motivation rührt zum Teil von Anwendungen im Operation Research her, wo es typischerweise so ist, dass Belohnungen gewinnorientiert sind. Ähnliche Anwendungsfälle finden sich in allgemeineren Anwendungen der Wirtschaftswissenschaften. Basierend auf einer prinzipiellen Untersuchung des mathematischen Hintergrunds des Discounted Reinforcement Learning entwickeln wir eine neuartige Adaption des standardmäßigen Reinforcement Learning, die als Average Reward Adjusted Discounted Reinforcement Learning bezeichnet wird. Unser Ansatz basiert auf einer erneuten Betrachtung der Laurent-Serien-Erweiterung des diskontierten Zustandswerts und einer anschließenden Neuformulierung der Zielfunktion, die den Lernprozess leitet.
Rule Learning
In vielen Anwendungsbereichen des maschinellen Lernens, beispielsweise in der Automobil-, Medizin-, Gesundheits- und Versicherungsbranche usw., wird das Bedürfnis nach Sicherheit und Transparenz der angewandten Methoden nicht nur bevorzugt, sondern immer häufiger auch von größter Bedeutung. Moderne Ergebnisse bei typischen Klassifizierungsaufgaben werden meist durch unerklärliche Methoden des maschinellen Lernens erzielt, beispielsweise durch Deep Neural Networks. Allerdings mangelt es diesen Ansätzen an Erklärbarkeit und Interpretierbarkeit und die Anwendung solcher Black-Box-Methoden führt häufig zu für den Menschen unverständlichen Klassifizierungen. Daher wird versucht, reine Black-Box-Modelle durch interpretierbare Methoden zu ersetzen. Unser Ziel ist es, Einblicke in die Anwendung von Rule Learning-Methoden und die damit verbundenen Vor- und Nachteile zu gewinnen. Insbesondere arbeiten wir an einer modularen Methodik, die modernste Methoden des (stochastischen) maschinellen Lernens mit traditionellen Methoden des Rule Learning kombiniert, um effiziente und skalierbare Algorithmen für die Klassifizierung großer Datenmengen bereitzustellen und dabei erklärbar zu bleiben.
Maschinelle Übersetzungen
In Zusammenarbeit mit dem Ladinischen Kulturinstitut "Micurá de Rü" entwickeln wir maschinelle Übersetzungen für ressourcenarme Sprachen, insbesondere für Ladinisch. Unser Hauptinteresse gilt dabei vertrauenswürdigen Anwendungen von mehrsprachigen Modellen. Die größte Herausforderung bei diesem Unterfangen ist die begrenzte Verfügbarkeit von Trainingsdaten, ein entscheidender Faktor für die Implementierung von qualitativ hochwertigen Übersetzungssystemen mit modernsten Techniken. Um dieser Einschränkung zu begegnen, wurde die Effektivität der Feinabstimmung von vortrainierten mehrsprachigen Modellen (wie NLLB oder T5) ausgenutzt.
Programmanalyse
Unter Programmanalyse versteht man die algorithmische Entdeckung von Eigenschaften eines Programms durch Untersuchung des Quelltextes. Bei unserer Arbeit konzentrieren wir uns auf (voll)automatisierte Methoden und Kostenanalysen.
Funktionale Programme und Rewriting
Ursprünglich befasste sich unsere Forschung mit der Ableitungs- und Laufzeitkomplexität von Term-Rewrite-Systemen und entsprechenden Arbeiten zur impliziten Komplexitätstheorie. Ein Meilenstein dieser Arbeit stellt die Entwicklung unseres preisgekrönten Tyrolean Complexity Tool (TcT) dar; TcT ist Open Source und frei verfügbar. In jüngerer Zeit konzentrieren wir uns auf die Analyse der amortisierten Kosten funktionaler Datenstrukturen. Hier legen wir Wert auf die vollautomatische Inferenz präziser Grenzen. Die Analyse dieser Datenstrukturen erfordert ausgefeilte Potentialfunktionen, die typischerweise logarithmische Ausdrücke enthalten. Möglicherweise aus diesen Gründen und trotz der jüngsten Fortschritte bei der automatisierten Ressourcenanalyse haben sie sich der Automatisierung lange entzogen. Ein Meilenstein unserer Arbeit in diese Richtung ist die Entwicklung von ATLAS. ATLAS etablierte die erste vollautomatische amortisierte Komplexitätsanalyse selbstanpassender Datenstrukturen. In Anlehnung an frühere Arbeiten basiert unsere Analyse auf potenziellen Funktionsvorlagen mit unbekannten Koeffizienten.
Probabilistische und Quantenprogramme
Wahrscheinlichkeitsvarianten bekannter Rechenmodelle wie Automaten, Turingmaschinen oder die Lambda-Kalküle werden seit den Anfängen der Informatik untersucht. Einer der Hauptgründe für die Berücksichtigung probabilistischer Modelle besteht darin, dass sie häufig den Entwurf effizienterer Algorithmen ermöglichen als ihre deterministischen Gegenstücke. Ein Meilenstein unserer Gruppe bei der Programmanalyse probabilistischer Programme waren hochmoderne Methoden zur (vollständigen) Automatisierung funktionaler und imperativer Programme. Kurz gesagt, wir befassen uns mit der automatisierten Verifizierung (und manchmal Verbesserung) der Analyse anspruchsvoller Wahrscheinlichkeitsprogramme. Unser Interesse an der Verifizierung probabilistischer Programme und stochastischer Prozesse passt gut zu unserem anhaltenden Interesse an Interpretierbarkeit und auch an der Verifizierung maschineller Lernmethoden. Aufbauend auf früheren Verbesserungen der Modularität und Skalierbarkeit der Analyse probabilistischer Programme haben wir auch einen soliden Rahmen für die erwartete Kostenanalyse gemischter Klassik-Quanten-Programme geschaffen.
Verifikation
Um Datenstrukturen zu formalisieren, müssen Datentypen, ihre Eigenschaften, Verhaltensweisen und Beziehungen genau definiert und dargestellt werden. Die Formalisierung bietet eine mathematische Grundlage für Überlegungen zum Verhalten, zur Korrektheit und zur Leistung von Datenstrukturen in Softwaresystemen. Liquid Haskell (kurz LH) ist eine Erweiterung der Programmiersprache Haskell, die statische Analysen verwendet, um die Korrektheit von Programmen zu überprüfen. Es ermöglicht die Spezifikation von Prädikaten und Invarianten über Datentypen und Funktionen. Diese Spezifikationen beschreiben die erwarteten Eigenschaften von Datenstrukturen und deren Operationen auf präzise, mathematische Weise. LH verwendet dann SMT-Solver, um automatisch zu überprüfen, ob die Spezifikationen im gesamten Programm eingehalten werden. Wir nutzen die Formalisierung in LH, um eine fundierte und präzise Wiedergabe von Lehrbuchargumenten zur Kostenanalyse von Datenstrukturen zu liefern.
Weitere Forschungsbereiche
Beweistheorie
Am abstraktsten stellt die Beweistheorie die Frage (und beantwortet sie oft): Was wissen wir mehr aus einem Beweis eines Theorems als aus seiner Wahrheit? Eine traditionelle, aber etwas vergessene Technik in der Logik (und Beweistheorie) ist Hilberts Epsilon-Kalkül. Bemerkenswerterweise liefert die verwandte Epislon-Eliminationsmethode immer noch den aktuellsten und direktesten Algorithmus zur Berechnung der Herbrand-Disjunktion einer Extensionalformel. Ein zentraler Vorteil besteht darin, dass die Obergrenze der erhaltenen Herbrand-Komplexität unabhängig von der Aussagenstruktur des Beweises ist. Ein Meilenstein unserer Gruppe ist die Beobachtung, dass diese Unabhängigkeit auch für Logik erster Ordnung mit Gleichheit gilt.
Subrekursive Hierarchien
Es ist bekannt, dass bei gegebener arithmetischer Theorie T mit beweistheoretischem Ordinalalpha die beweisbaren rekursiven Funktionen von T genau diejenigen Funktionen sind, die innerhalb der Komplexitätsgrenzen durch die Hardy-Funktionen (streng) kleiner als Alpha berechenbar sind. Die Hardy-Funktionen stellen somit eine Hierarchie schnell wachsender subrekursiver Funktionen dar, die es uns ermöglichen, zwei verschiedene Vorstellungen von Komplexität zu verknüpfen: (i) die logische Komplexität des Nachweises der Wohldefiniertheit einer Spezifikation und (ii) die rechnerische Komplexität eines Programms, das diese Spezifikation erfüllt. Dieses tiefgreifende (und weitreichende) Ergebnis der Beweistheorie legt einen starken Zusammenhang zwischen Terminierungstechniken und Kostenanalyse nahe, der in konkreten Anwendungen leider sehr subtil ist. Die Erforschung dieser Feinheiten ist ein wiederkehrendes Thema der Forschung unserer Gruppe.