28 Arbeiten
Diese Arbeit erklärt die überlegene Parallelisierbarkeit linearer RNNs im Vergleich zu nichtlinearen RNNs durch eine Verbindung zu Komplexitätsklassen, wonach lineare RNNs logarithmische Tiefenschaltungen darstellen, während nichtlineare Varianten P-vollständige Probleme lösen können, was eine fundamentale Barriere für ihre effiziente Parallelisierung darstellt.
Diese Arbeit präsentiert einen einrundenigen randomisierten verteilten Algorithmus zum 2-Färben von Zyklen, der einen erwarteten Anteil monochromer Kanten unter 0,24118 erreicht, und verbessert damit die bisherigen Schranken, wobei die Beweise maßgeblich von großen Sprachmodellen entwickelt und in Lean 4 formalisiert wurden.
Die Arbeit untersucht die Komplexität des Erreichbarkeitsproblems für VASS+Z (VASS mit zusätzlichen ganzzahligen Zählern), indem sie NP-Vollständigkeit für eine Dimension, eine -Obergrenze für sowie signifikant verschärfte PSPACE- und TOWER-Härte-Untergrenzen im Vergleich zu klassischen VASS nachweist.
Diese Arbeit charakterisiert algebraisch eine Teilmenge reversibler zellulärer Automaten ersten Grades über unter Nullrandbedingungen, indem sie zeigt, dass die Reversibilität für beliebige Gittergrößen durch die Überprüfung von nur drei algebraischen Bedingungen in konstanter Zeit bestimmt werden kann.
Diese Arbeit untersucht die algorithmische Komplexität von Alignments in der Prozessmining und zeigt, dass das Problem im Allgemeinen PSPACE-vollständig ist, während es für bestimmte Klassen wie lebende, sichere S-Systeme in P liegt, für andere wie Prozessbäume und T-Systeme jedoch NP-vollständig bleibt.
Diese Arbeit löst ein seit über einem Jahrzehnt offenes Problem, indem sie zeigt, dass ein historisch-deterministischer Büchi-Automat mit 65 Zuständen strikt weniger Zustände benötigt als jeder äquivalente deterministische Büchi-Automat, was durch eine Kombination aus theoretischen Erkenntnissen und computergestützter Analyse bewiesen wird.
Dieser Beitrag stellt eine formale Modellierung, Verifikation und Testung der verteilten Middleware „Contract Automata Runtime Environment" (CARE) mittels des Tools Uppaal vor, um durch die Generierung konkreter Tests aus abstrakten Modellen die Zuverlässigkeit der Anwendung zu erhöhen.
Die Arbeit stellt SpotIt vor, einen neuen Evaluierungsansatz für Text-to-SQL, der mithilfe formaler Verifikation nach Datenbanken sucht, die generierte Abfragen von den Ground-Truth-Abfragen unterscheiden, und zeigt damit auf, dass herkömmliche testbasierte Methoden oft Unterschiede übersehen.