Royal Society International Exchanges Grant, IES\R3\223051

Breiterer Forschungskontext

Reine Grundlagenforschung liefert die Grundlage für erfolgreiche Anwendungen. Ein bemerkenswertes Beispiel im Kontext unseres Vorschlags ist ein Tool, RaML: Während RaML auf impliziten Charakterisierungen möglicher Berechnungen von Martin Hofmann basiert, um elegante Beschreibungen zu liefern, ist es heutzutage das fortschrittlichste Tool zur Schätzung des Ressourcenverbrauchs von OCaml-Programmen. Auch die Richtung von der Anwendung zur Theorie ist bedeutsam. Tief verwurzelt in praktischen Fragen definierte Ashish Tiwari eine restriktive Klasse linearer Schleifenprogramme und initiierte eine laufende Studie zu deren Beendigung. Es stellte sich heraus, dass dies eng mit Skolems Problem zusammenhängt, einem tiefgreifenden Problem der Zahlentheorie, das Kommentare von Terence Tao hervorrief.

Ziele

Inspiriert durch diese Beispiele wollen wir Ergebnisse zwischen anwendungsorientierten Bereichen der Programmanalyse und grundlegenden Aspekten der Beweistheorie untersuchen. Genauer gesagt geht es bei der Analyse realisierbarer Algorithmen um die Entwicklung (häufig) automatisierter Methoden zur Ableitung der Laufzeitkosten von Programmen. Andererseits ist die Komplexitätstheorie, die Untersuchung der inhärenten Komplexität gegebener Rechenprobleme, natürlich in Theorien der begrenzten Arithmetik (BA) verankert. So werden Fragen der Machbarkeit von Algorithmen und Problemen in der BA zu Fragen der Beweisbarkeit.

Methoden

In einer ersten Phase des Projekts wollen wir unseren Ansatz validieren, indem wir den Methodentransfer bei der Untersuchung von Rewriting-Systemen und der Analyse von Beweisen in BA untersuchen. In einer zweiten Phase werden die Methoden des BA-Studiums und der Programmanalyse erforscht, mit dem Ziel, ein langfristiges Programm zu entwickeln, das durch eine Folgefinanzierung aufrechterhalten werden kann.

FWF Projektnummer: P 36623

Breiterer Forschungskontext

Die amortisierte Analyse ist eine Methode zur Worst-Case-Kostenanalyse von (probabilistischen) Datenstrukturen, bei der eine einzelne Datenstrukturoperation als Teil einer größeren Folge von Operationen betrachtet wird. Die Kostenanalyse anspruchsvoller Datenstrukturen, wie etwa selbstanpassender binärer Suchbäume, war bereits im ursprünglichen Vorschlag einer amortisierten Analyse ein Hauptziel. Die Analyse dieser Datenstrukturen erfordert ausgefeilte Potentialfunktionen, die typischerweise sublineare Ausdrücke (wie den Logarithmus) enthalten. Abgesehen von unserem Pilotprojekt entzog sich die Analyse dieser Datenstrukturen bislang einer Automatisierung.

Ziele

Unser Ziel ist eine automatisierte Analyse der gängigsten Datenstrukturen mit guten, d.h. sublinearer, Komplexität, wie ausgeglichene Bäume, Fibonacci-Heaps, randomisierte Suchbäume, Skip-Listen, Skew-Heaps, Union-Find usw. Unsere Ziele sind die Überprüfung von Lehrbuch-Datenstrukturen, die Bestätigung und Verbesserung (an Koeffizienten) der zuvor gemeldeten Komplexität Grenzen sowie die automatisierte Analyse realistischer Datenstrukturimplementierungen. Zunächst betrachten wir nur streng funktionale Programmiersprachen (erster Ordnung). Später werden wir unsere Forschung auf Lazy Evaluation ausweiten, um die Analyse persistenter Datenstrukturen zu ermöglichen. Darüber hinaus werden wir auch probabilistische Datenstrukturen berücksichtigen.

Methoden

Basierend auf dem Erfolg unserer Pilotstudie stellen wir uns die folgenden Schritte zur Automatisierung der amortisierten Analyse vor: (i) Fixieren einer parametrisierten potenziellen Funktion; (ii) ein (lineares) Einschränkungssystem über die Funktionsparameter aus dem AST des Programms ableiten; (iii) Erfassen der erforderlichen nichtlinearen Argumentation durch explizites Hintergrundwissen, das in den Mechanismus zur Lösung von Zwangsbedingungen integrierbar ist; und schließlich (iv) Werte für die Parameter durch einen (optimierenden) Constraint-Löser finden.

Breiterer Forschungskontext

Traditionell benötigen moderne Ansätze für die Entwicklung leistungsfähiger maschineller Übersetzungssysteme eine große Menge an Trainingsdaten. Die begrenzte Verfügbarkeit von Ressourcen und Texten in kleineren Sprachen verhindert jedoch eine effektive Anwendung dieser Algorithmen. In den letzten Jahren hat sich dieser Forschungsbereich verstärkt auf low-resource Szenarien und damit auch auf die maschinelle Übersetzung von weniger verbreiteten Sprachen konzentriert. Das hat zur Entwicklung verschiedener Methoden geführt, die das Problem der begrenzten Datenverfügbarkeit umgehen oder die verfügbaren Daten effizienter nutzen. Mit der Veröffentlichung von ChatGPT und anderen Large Language Models (LLMs) ist zudem ein völlig neuer Forschungszweig der maschinellen Übersetzung entstanden. LLMs verfügen als Sprachmodelle über ein beeindruckendes Verständnis für natürliche Sprache und können komplexe Kontexte verarbeiten. Darüber hinaus können sie mit wenigen Trainingsbeispielen auf neue Problemstellungen angepasst werden. Diese Fähigkeiten könnten in Kombination mit den entwickelten Methoden nun auch für die Weiterentwicklung der maschinellen Übersetzung für ressourcenarme Sprachen genutzt werden und den Weg zu gut funktionierenden Systemen auch in solchen Sprachen ebnen. Es bleibt die Frage, wie dies am besten gelingen kann.

Ziele

Ziel dieses Projekts ist es, in Zusammenarbeit mit dem ladinischen Kulturinstitut 'Micurá de Rü' ein maschinelles Übersetzungssystem für die ladinische Sprache zu entwickeln. Das Ladinische oder Dolomitenladinische ist eine offiziell anerkannte Minderheitensprache in Italien, die von etwa 30.000 Menschen in den fünf Tälern rund um den Sellastock gesprochen wird. Die Sprache variiert von Tal zu Tal, und es wird zwischen den folgenden Idiomen unterschieden: Val Badia (Gadertal), Val Gardena (Grödnertal), Fassa (Fassa), Ampezzo (Anpezo) und Buchenstein (Fodom). Diese Varianten müssen bei diesem Problem getrennt behandelt werden, wodurch eine zusätzliche Herausforderung entsteht. Vorerst beschränken wir uns auf die Gadertal-Variante und versuchen, Methoden zu entwickeln, die in dieser Variante gut funktionieren und die wir dann auf die anderen Varianten ausweiten können.

Wirkung

Die erfolgreiche Entwicklung eines funktionsfähigen maschinellen Übersetzungssystems für Ladinisch würde neue Möglichkeiten für die Verwendung und Erforschung dieser Sprache schaffen. Auf der einen Seite könnte damit der Zugang zu dieser Sprache und Kultur erleichtert werden, auf der anderen Seite stünde ein wertvolles Werkzeug für das Erfassen ladinischer Texte zur Verfügung, das auch für die ladinische Gemeinschaft von Nutzen wäre. Somit wäre es auch ein wichtiger Beitrag zur Erhaltung dieser Sprache, zumindest in der digitalen Welt.