64 Arbeiten
Die Arbeit stellt einen neuen SAT-basierten Ansatz mit Symmetriebrechung für Verbindungskalküle in der Prädikatenlogik erster Stufe vor, der in dem neu implementierten Solver upCoP realisiert wurde, um die Automatisierung von Beweisen durch die Kombination von Ordnungs-basierter Sättigung und Zielreduktion zu verbessern.
Die Arbeit führt den Begriff der Kommutationsgruppen ein, um zustandsunabhängige Kontextualität durch algebraische Strukturen, String-Umschreibesysteme und unitäre Darstellungen als Untergruppen verallgemeinerter Pauli-Gruppen zu analysieren und zu charakterisieren.
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.
Diese Arbeit identifiziert und mechanisch verifiziert eine fundamentale Barriere, die direkte kompositionelle Terminierungsbeweise für schrittverdoppelnde Rekursoren unmöglich macht, und schlägt einen modularen Ausweg vor, der durch eine vollständige Zertifizierungskette und externe Validierung bestätigt wird.
Die vorgestellte Arbeit führt MPBMC ein, einen hybriden Ansatz zur effizienten Verifikation mehrerer Eigenschaften mittels GNN-gestützter Clustering, der funktionale Repräsentationen von Hardware-Schaltungen und Laufzeitstatistiken nutzt, um die Leistung von Bounded Model Checking signifikant zu steigern.
Die Arbeit untersucht Erhaltungsresultate für die unabhängige Fusion einvariabler Prädikatenmodalllogiken und zeigt, dass Kripke-Vollständigkeit und Entscheidbarkeit ohne Gleichheit erhalten bleiben, während sie bei Gleichheit und nicht-rigiden Konstanten durch Kodierung diophantischer Gleichungen verloren gehen, wobei die endliche Modellität nur im lokalen Fall erhalten bleibt.
Dieser Artikel liefert vollständige diagrammatische Axiomatisierungen der Kullback-Leibler-Divergenz und allgemeiner Rényi-Divergenzen beliebiger Ordnung im Rahmen der quantitativen monoidalen Algebra, indem er relative Entropie aus kategorientheoretischer Sicht als quantitative Erweiterung von Kategorien stochastischer Matrizen unter den monoidalen Strukturen des Kronecker-Produkts und der direkten Summe untersucht.
Dieser Übersichtsartikel untersucht systematische Ansätze für basisbeschränkte Fragmente der Aussagen- und Modallogik, indem er die etablierte Post'sche Gitterstruktur auf den Aussagenfall anwendet und zwei historische Forschungsstränge zur Modallogik – einen allgemeinen Rahmen basierend auf beliebigen Modalformeln sowie einen handhabbareren Ansatz mit Booleschen Funktionen und ausgewählten Modaloperatoren – zusammenführt, um Zusammenhänge zwischen Ausdrucksstärke, Komplexität und Lernbarkeit aufzuzeigen und offene Probleme zu identifizieren.
Die Autoren führen die konstruktiven Meistermodi-Logiken und ein, zeigen deren EXPTIME-Vollständigkeit und endliche Modell-Eigenschaft, bestätigen damit eine Vermutung von Afshari et al. für den diamantfreien Fragment und ermöglichen durch Einbettung von und den Nachweis, dass deren Gültigkeitsprobleme in EXPTIME liegen.
Die Autoren wenden Constraint Learning auf den klassischen First-Order-Connection-Kalkül an, um das übermäßige Backtracking bei der Beweisführung in nicht-konfluenten Tableau-Kalkülen zu reduzieren, ohne dabei die Vollständigkeit zu verlieren.
Die Autoren stellen einen neuen Ansatz zur Lösung von String-Gleichungen vor, der durch die Kombination eines Potenzoperators, verallgemeinerter Parikh-Bilder und einer Gleichheitszerlegung als Erweiterung von Nielsen-Transformationen komplexe SMT-Eingaben über Strings bewältigt.
Das Paper stellt NL2GDS vor, ein Framework, das große Sprachmodelle nutzt, um natürliche Sprachbeschreibungen über den OpenLane-Flow in synthetisierbaren RTL-Code und GDSII-Layouts zu übersetzen, wodurch sich bei Benchmark-Designs signifikante Verbesserungen in Fläche, Verzögerung und Leistung ergeben.
Diese Arbeit stellt SCORE, eine Programmiersprache zur Manipulation von Variablen und Stacks, vor, deren Operationen mithilfe eines Beweisassistenten als totale Bijektionen zertifiziert werden, um reversible Berechnungsmodelle zu ermöglichen, die für die Untersuchung der Komplexitätstheorie essenziell sind.
Diese Arbeit stellt eine neue Gleichheitstheorie für den I-Kalkül vor, die auf sogenannten Ohana-Bäumen basiert, welche versteckte Variablen erfassen, und verbindet diese durch einen Kommutativitätssatz mit der Taylor-Entwicklung sowie einem neuartigen relationalen Typsystem.
Die Arbeit stellt LeanTutor vor, ein Beweis-tutor-System, das die Stärken von Large Language Models und dem Theorembeweiser Lean kombiniert, um mathematische Beweise in natürlicher Sprache zu erklären und gleichzeitig formale Korrektheit zu gewährleisten, wobei die Leistung anhand des neu eingeführten PeanoBench-Datensatzes evaluiert wird.
Diese Arbeit stellt ein neuartiges geometrisches Rahmenwerk vor, das das logische Denken von Large Language Models als glatte Flüsse im Repräsentationsraum modelliert und zeigt, dass diese Modelle logische Invarianten unabhängig von ihrer Architektur verinnerlichen, was die These der „stochastischen Papageien" widerlegt.
Die Arbeit stellt Strat2Rocq vor, ein Framework, das Beweissstrategien aus großen Sprachmodellen extrahiert und als formale Lemmas in Rocq integriert, um die Erfolgsrate symbolischer Beweiser wie CoqHammer sowie von LLM-Beweisagenten signifikant zu steigern.
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.
Dieser Beitrag stellt eine skalierbare Methode zur formalen Verifikation von Gleitkommaarithmetik vor, die durch direkte RTL-zu-RTL-Modellprüfung, eine modulare Zerlegungsstrategie und den Einsatz von KI-gestützter Eigenschaftsgenerierung mit menschlicher Rückkopplung Abstraktionslücken überwindet und eine höhere Abdeckungseffizienz als herkömmliche Ansätze erreicht.