28 papers
Dit paper introduceert FATE, een nieuwe reeks formele algebra-benchmarks met problemen die variëren van undergraduate-oefeningen tot PhD-niveau, om de aanzienlijke kloof tussen de huidige prestaties van grote taalmodellen in wiskundig redeneren en het niveau van modern wetenschappelijk onderzoek in kaart te brengen.
Dit artikel onderzoekt de toestandcomplexiteit van lineaire deelrijen en basisoperaties op -automatische rijen, legt een verband met de subwoordcomplexiteit en beantwoordt een recente vraag van Zantema en Bosma over het meest-significant-digit-first-formaat.
Dit artikel introduceert een methode die Syntax Guided Synthesis en Temporal Stream Logic combineert om databewuste tijdspecificaties en transformaties te leren uit uitvoeringstraces, wat leidt tot een robuustere en veel efficiëntere synthese van reactieve programma's dan bestaande passieve leerbasislijnen.
Dit artikel onderzoekt concurrente graafspellen met gedistribueerde randomisatie, waarbij het aantoont dat geheugenloze strategieën volstaan voor drempelproblemen, de complexiteit van deze problemen analyseert, een nieuwe logica (IRATL) introduceert en een solver implementeert.
Dit paper lost de fundamentele mismatch in hogere-dimensionale automaten op door een orde-onafhankelijke semantiek te ontwikkelen die gebaseerd is op interval-ipomsets, waardoor een verenigde en zuivere grondslag voor concurrentiemodellen wordt geboden die vrij is van kunstmatige totale ordening.
Dit artikel bewijst dat het onbeslisbaar is of het aantal 'bochten' (switches tussen het vergroten en verkleinen van de stapel) in acceptatieberekeningen van context-vrije talen en pushdown-automata begrensd is, en beschrijft een niet-recursieve trade-off en een oneindige hiërarchie van complexiteitsklassen gebaseerd op sublineaire bochtgroei.
Dit artikel onderzoekt de klasse van echte context-vrije bomen, toont aan dat ze een eindige staatbeschrijving hebben via multi-arc NFAs en bewijst dat het isomorfismeprobleem voor deterministische context-vrije bomen NL-volledig is.
In dit artikel bewijzen de auteurs nieuwe eigenschappen van de -representatie van gehele getallen, waaronder een conjectuur van Kimberling uit 2012, met behulp van de theorema-prover Walnut en ChatGPT 5.
Dit artikel identificeert zes onafhankelijke dimensies waarin generatie en herkenning binnen de formele taaltheorie fundamenteel verschillen, weerlegt het simplistische idee dat generatie altijd makkelijk is, en verbindt deze asymmetrie met concepten als verrassing (surprisal) en de operationele beperkingen van grote taalmodellen.
Dit artikel bewijst dat de factoren van gladde woorden f-gladde woorden zijn en maakt vooruitgang in het bewijzen van Sing's conjectuur over de complexiteit van f-gladde woorden over binaire alfabetten, door het resultaat te bevestigen voor even alfabetten, een ondergrens voor elk binair alfabet te tonen en de bovengrens voor oneven alfabetten te verbeteren.
Dit paper introduceert ZipLex, een formeel geverifieerd framework voor lineaire, omkeerbare lexing dat gegarandeerde wederzijdse inversie tussen lexing en printen biedt, lineaire tijdscomplexiteit garandeert via geverifieerde memoïzatie, en aanzienlijk sneller is dan bestaande geverifieerde lexers zoals Verbatim++ en Coqlex.
Dit paper introduceert een data-gedreven aanpak voor het ontwerpen van niet-blokkerende supervisors voor discrete-event systemen met onbekende modellen door het concept van 'marking data-informativity' te definiëren, te verifiëren en uit te breiden tot beperkte varianten en informatiseerbaarheid om een geldige supervisor te garanderen.
Dit paper introduceert een theoretisch raamwerk voor grammatica-gedwongen decoding dat bewijst dat taalkundig equivalente grammatica's weliswaar identieke toekenningsmasks opleveren, maar aanzienlijk verschillende computatiekosten kunnen veroorzaken door structurele ambiguïteit, en biedt bovendien onderbouwing voor het optimaliseren van grammatica's en het beperken van de distortie bij het maskeren van logits.
Dit artikel bewijst dat Moore-machines exact kunnen worden gerealiseerd als state-space modellen en toont aan dat het combineren van symbolisch automata-leren met deze continue modellen leidt tot snellere convergentie en betere prestaties dan willekeurige initialisatie.
Dit artikel presenteert een schaalbaar online bewakingsframework voor Metrische Temporele Logica dat gebruikmaakt van sequentiële netwerken en een nieuwe 'future temporal marking'-techniek om tijdsgebonden specificaties efficiënt te verwerken voor cyber-fysische systemen.
Dit artikel onderzoekt het module-checking-probleem voor pushdown multi-agent systemen en stelt vast dat dit probleem 2EXPTIME-volledig is voor ATL, maar 4EXPTIME-volledig voor ATL*, wat een zeldzaam voorbeeld is van een natuurlijk beslissingsprobleem met een complexiteit die hoger is dan drievoudig exponentieel.
Dit artikel onderzoekt Ramsey-achtige stellingen voor oneindige bomen en combinatorische hulpmiddelen, met als toepassing het uitbreidingsprobleem voor boomalgebra's.
Deze paper introduceert een risicobewuste aanpak voor autonoom rijden die lineaire temporale logica (LTL) specificeert met timing en ernst, waardoor een lineair programmeringsprobleem wordt geformuleerd dat het synthetiseren van besturingsbeleid mogelijk maakt dat verschillende risico's, zoals botsingen en verkeersovertredingen, op een menselijke manier in evenwicht brengt.
In dit artikel worden de conjectures van Clark Kimberling over zijn door inflatieregels gedefinieerde binaire rij bewezen met behulp van de Walnut-theorema-prover, waarbij de relatie met het oneindige Tribonacci-woord wordt aangetoond en zowel de subwoordcomplexiteit als de kritische exponent van de rij worden bepaald.
Dit artikel presenteert een volledige classificatie van de gedistribueerde complexiteit voor lokale optimalisatieproblemen in gerichte cycli, waarbij het aantoont dat de complexiteit voor zowel deterministische als probabilistische modellen valt binnen één van vier specifieke klassen en dat deze klasse automatisch kan worden bepaald en een optimale algoritme kan worden gegenereerd.