28 Arbeiten
Die Arbeit stellt FATE vor, eine neue Benchmark-Serie für formale Algebra, die LLMs vor extrem schwierige Forschungsprobleme stellt und dabei massive Leistungslücken sowie spezifische Fehlermuster bei der Formalisierung aufzeigt.
Die Arbeit untersucht die Zustandskomplexität von -automatischen Folgen und deren linearen Teilfolgen, stellt eine Verbindung zur Subwortkomplexität her, löst eine offene Frage von Zantema und Bosma bezüglich der Eingabe im Most-Significant-Digit-First-Format und analysiert die Komplexität der Konstruktion entsprechender Automaten mittels Büchi-Arithmetik.
Diese Arbeit erweitert das Mining von Spezifikationen aus Ausführungsstraces über reine Boolesche Abstraktionen hinaus, indem sie Syntax-gesteuerte Synthese mit der temporalen Logik TSL kombiniert, um datenbewusste Transformationen und Spezifikationen zu lernen und damit das passive Lernen von reaktiven Programmen in puncto Robustheit und Sample-Effizienz signifikant zu verbessern.
Diese Arbeit untersucht kooperative Graphspiele mit verteiltem Zufall, bei denen Spieler keine gemeinsame Zufallsquelle teilen, und zeigt, dass für das Schwellenwertproblem memoryless Strategien ausreichen, während das fast-sichere Erreichbarkeitsproblem NP-vollständig ist, was zur Entwicklung der Logik IRATL und eines entsprechenden Löser-Algorithmus führt.
Diese Arbeit entwickelt eine ereignisordnungsunabhängige Semantik für höherdimensionale Automaten auf Basis von Intervall-ipomsets, die die kategorische Isomorphie zwischen presheaf-theoretischen und kombinatorischen Darstellungen nachweist und durch die Charakterisierung von Bisimulationen eine vereinheitlichte Grundlage für die Modellierung echter Parallelität schafft.
Die Arbeit untersucht die Unentscheidbarkeit der Beschränkbarkeit von Umschaltvorgängen (Turns) bei Pushdown- und Ein-Zähler-Automaten und etabliert eine nicht-rekursive Trade-off-Beziehung sowie eine unendliche Hierarchie von Komplexitätsklassen, die durch sublineare Funktionen der Eingabelänge definiert sind.
Die Arbeit untersucht bona fide kontextfreie Bäume als eine Unterklasse kontextfreier Graphen, zeigt, dass sie durch endliche Automaten mit mehreren Kanten beschreibbar sind, und beweist, dass das Isomorphieproblem für deterministische kontextfreie Bäume sowohl im verankerten als auch im nicht-verankerten Fall NL-vollständig ist.
In diesem Artikel werden neue Eigenschaften der -Darstellung von ganzen Zahlen bewiesen, wobei insbesondere eine 2012 von Kimberling aufgestellte Vermutung bestätigt wird, wofür die Theorembeweiser Walnut und ChatGPT 5 eingesetzt wurden.
Die Arbeit identifiziert sechs Dimensionen, darunter neuartige Aspekte wie Richtung und Zeitlichkeit, die eine fundamentale operationale Asymmetrie zwischen der Erzeugung und der Erkennung formaler Sprachen aufzeigen, wobei sie die verbreitete Annahme widerlegt, dass Erzeugung immer einfacher sei als Parsing, und die anhaltende Trennung dieser Prozesse in modernen KI-Modellen kritisch beleuchtet.
Diese Arbeit beweist, dass die Faktoren glatter Wörter f-glatt sind, und liefert Fortschritte zur Vermutung von Sing über das Komplexitätswachstum f-glatter Wörter über binären Alphabeten, indem sie die Vermutung für gerade Alphabeten bestätigt, eine untere Schranke für beliebige binäre Alphabeten etabliert und die bekannte obere Schranke für ungerade Alphabeten verbessert.
Die Arbeit stellt ZipLex vor, ein in Stainless verifiziertes Framework für invertible lineare lexikalische Analyse, das durch den Einsatz von Zippern und verifizierter Memoisierung nicht nur die längste Übereinstimmung garantiert, sondern auch die Linearzeitkomplexität und die Umkehrbarkeit von Lexing und Printing nachweist.
Dieses Papier entwickelt einen datengesteuerten Ansatz für die nicht-blockierende Markierungsüberwachung diskreter Ereignissysteme, indem es das neuartige Konzept der Markierungsdaten-Informativität einführt, dessen Verifizierungsalgorithmus bereitstellt und bei unzureichenden Daten Strategien zur Einschränkung der Spezifikation oder zur Daten-Informativierung vorschlägt.
Diese Arbeit untersucht die strukturelle Äquivalenz und Effizienz von grammatikbeschränktem Decodieren, indem sie einen Invarianzsatz für Orakel beweist, strukturelle Mehrdeutigkeitskosten quantifiziert, untere Schranken für den Rechenaufwand herleitet und die Verzerrung durch Hard-Masking mittels Doob-h-Transform analysiert, um Optimierungsmöglichkeiten für Transformer-Architekturen aufzuzeigen.
Diese Arbeit beweist die exakte Realisierbarkeit von Moore-Maschinen als Zustandsraummodelle und zeigt, dass eine Warm-Start-Initialisierung dieser Modelle mit symbolisch gelernten Automaten zu einer deutlich schnelleren Konvergenz und höheren Genauigkeit führt als eine zufällige Initialisierung.
Diese Arbeit stellt ein effizientes und skalierbares Online-Monitoring-Framework vor, das durch die einheitliche Konstruktion sequenzieller Netze aus MTL-Spezifikationen mittels der neuen „future temporal marking"-Technik sowohl für diskrete als auch dichte Zeitabläufe optimierte Überwachung ermöglicht.
Die Arbeit untersucht das Modul-Checking von Pushdown-Multi-Agenten-Systemen gegen ATL- und ATL*-Spezifikationen und zeigt, dass die Komplexität für ATL bei 2EXPTIME-vollständig liegt, während sie für ATL* überraschenderweise 4EXPTIME-vollständig ist und damit exponentiell höher als bei verwandten Problemen ausfällt.
Der Artikel untersucht Ramsey-ähnliche Theoreme für unendliche Bäume und wendet diese als kombinatorisches Werkzeug zur Analyse des Erweiterungsproblems für Baumalgebren an.
Dieser Beitrag stellt einen Ansatz vor, der durch die Erweiterung von LTL-Spezifikationen um zeitliche und schwerewegsbezogene Risikomaße sowie die Formulierung als lineares Optimierungsproblem autonome Fahrzeuge befähigt, menschähnliche Risikoabwägungen zwischen Kollisionsgefahren und Verkehrsregelverstößen zu treffen.
In diesem Artikel werden die von Clark Kimberling aufgestellten Vermutungen über eine von ihm definierte binäre Folge bewiesen, deren Zusammenhang mit dem unendlichen Tribonacci-Wort aufgezeigt sowie ihre Subwortkomplexität und kritische Exponenten bestimmt werden.
Diese Arbeit präsentiert eine vollständige Klassifizierung der verteilten Komplexität lokaler Optimierungsprobleme in gerichteten Zyklen, die zeigt, dass die Komplexität für jede Approximation in deterministischen und randomisierten LOCAL-Modellen genau eine von vier möglichen Stufen annimmt, und bietet zudem einen effizienten Algorithmus zur automatischen Bestimmung dieser Komplexitätsklasse sowie zur Synthese optimaler verteilter Algorithmen.