63 Arbeiten
Diese Arbeit untersucht, wie sich zentrale Eigenschaften von Wahrscheinlichkeitsmonaden – wie die Existenz von Kleisli-Gesetzen, die lax-monoidale Struktur und die Affinität – aus ihren Codensity-Darstellungen ableiten lassen, wobei insbesondere eine universelle Eigenschaft als terminale Liftings des Giry-Monads bewiesen und die Bedingung für punktweise Monoidalität mittels Day-Konvolution charakterisiert wird.
Die Arbeit führt einen Operaden abhängiger gerichteter Verdrahtungsdiagramme ein, um die Komposition von Mealy-Maschinen und von Eingängen parametrisierten Lager-Fluss-Diagrammen zu ermöglichen, und stellt eine Semantik für letztere durch einen Morphismus in Mealy-Maschinen bereit.
Das Paper stellt Preguss vor, ein modulares Framework, das durch die Kombination von statischer Analyse und LLM-gestützter Spezifikationssynthese die automatisierte Verifikation von Programmen mit über 1000 Zeilen Code ermöglicht und dabei den menschlichen Aufwand um 80,6 % bis 88,9 % reduziert.
Die Arbeit stellt eine skalierbare Methode zur formalen Verifikation von Quantenphasenschätzungsschaltungen vor, die mithilfe einer symbolischen Qubit-Abstraktion auf quantifiziererfreier Bitvektorlogik Schaltungen mit über 1.000 Qubits effizient auf funktionale Korrektheit überprüft.
Diese Arbeit stellt explizit eine obere Schranke von für die Änderung der optimalen Schaltkreisgröße bei einer Störung der Wahrheitstabelle dar, erweitert sie auf den allgemeinen Hamming-Abstand und bestätigt sie durch exhaustive SAT-basierte Berechnungen für im AIG-Basis-System, wobei die Tightness der Schranke nachgewiesen wird.
Die Arbeit stellt RoadLogic vor, ein Open-Source-System, das deklarative OpenSCENARIO-Spezifikationen mithilfe von Answer Set Programming, Bewegungsplanung und Überwachung in ausführbare, realistische Simulationen für das systematische Testen autonomer Fahrzeuge übersetzt.
Diese Arbeit stellt ein allgemeines Framework vor, das durch die Kombination von SMT-Formeln mit vorab berechneten Theorie-Lemmas die kompilierte d-DNNF-Darstellung für polytime-Abfragen auf SMT-Ebene nutzbar macht, indem sie diese auf propositionale Ebene reduziert.
Die Arbeit stellt BemaGANv2 vor, einen fortschrittlichen GAN-basierten Vocoder für die hochauflösende Langzeit-Audiogenerierung, der durch den Einsatz von AMP-Modulen im Generator und einer systematischen Evaluierung verschiedener Diskriminator-Kombinationen (insbesondere MED und MRD) zeitliche Kohärenz und harmonische Struktur über längere Zeiträume verbessert.
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.
Dieser Artikel formalisiert in der Homotopietypentheorie die Korrespondenz zwischen Überlagerungsräumen und Untergruppen der Fundamentalgruppe, entwickelt eine n-dimensionale Verallgemeinerung von Überlagerungen und klassifiziert konkret Überlagerungen von Linsenräumen sowie die Konstruktion der Poincaré-Homologiesphäre.
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.
Die Arbeit vergleicht drei Satisfiability-Semantiken für Quantenlogik in festen Dimensionen und zeigt, dass die Standard-Hilbert-Gitter-Semantik strikt mächtiger ist als die global-kommutierende und die lokal-partielle-Boolesche Semantik, indem sie eine explizite Formel als Separator konstruiert.
Die Arbeit beschreibt ein Experiment zur dezentralen, kollaborativen Autoformalisierung algebraischer Topologie, bei dem mehrere LLM-basierte Agenten in einem bountysbasierten Marktmechanismus dynamisch Lemmas vorschlagen, Beweise führen und diese durch ein interaktives Theorembeweissystem verifizieren lassen.
Die Arbeit stellt Twitch vor, ein Werkzeug, das mithilfe von Stitch automatisch abstrakte Termmuster aus erfolgreichen oder gescheiterten Beweisen ableitet und diese zur signifikanten Beschleunigung sowie zum Lösen zusätzlicher Gleichungsbeweise im Twee-Theorembeweiser nutzt.
Die Arbeit stellt eine Fallstudie vor, in der ein LLM-Agent einen vollständigen SMT-Löser für QF_UF ohne menschlich geschriebenen Code entwickelt, der den Nieuwenhuis-Oliveras-Kongruenzabschluss-Algorithmus implementiert, auf SMT-LIB-Benchmarks konkurrenzfähig ist und Beweise für Lean erzeugt.
Das Paper stellt Elenchus vor, ein dialogbasiertes System, das mithilfe von Inferentialismus und der NMMS-Logik Wissensbasen durch die strukturierte Auflösung von Spannungen zwischen einem Experten und einem LLM-gestützten Skeptiker konstruiert und dabei die Inferenzbeziehungen formal verifiziert.
Diese Arbeit untersucht den Einsatz von Graph Neural Networks zur Vorhersage eines initialen Verzweigungsordnungs für SAT-Löser, wobei zwar signifikante Beschleunigungen bei zufälligen und pseudo-industriellen Instanzen erzielt werden, die Vorhersagen jedoch bei komplexen industriellen Problemen aufgrund der dynamischen Heuristiken der Solver und der Schwierigkeit der Instanzen versagen.
Diese Arbeit stellt einen kategorischen Rahmen für skizzenorientierte Datenbanken vor, der Datenbankparadigmen als endliche Limit-Skizzen und Datenbanken als mengentheoretische Modelle formalisiert, um Graphenfeatures einheitlich zu erfassen, Pfade über lokale Inferenzregeln zu berechnen und durch „Stuttering-Skizzen" eine modulare Komposition sowie skalierbares Modellwachstum zu ermöglichen.
Diese Arbeit stellt eine Methode zur automatisierten Generierung von Beweisübungen mit vergleichbarem Schwierigkeitsgrad vor, die auf der Analyse von Tableau-Beweisen in der ersten Stufe basiert, um den manuellen Aufwand für die Erstellung von Übungsaufgaben im Bereich der diskreten Mathematik zu reduzieren.
Dieser Band enthält die Proceedings der achten internationalen Konferenz für angewandte Kategorientheorie (ACT2025), die im Juni 2025 an der University of Florida stattfand und Beiträge aus einem breiten Spektrum von Disziplinen wie Informatik, Quantencomputing und Chemie vereint.