64 papers
Dit paper introduceert een nieuwe aanpak voor het automatiseren van first-order logica-bewijzen door connectie-calculi te combineren met SAT-oplossers en symmetriebreking, wat is geïmplementeerd in de nieuwe solver upCoP.
Dit artikel introduceert commutatiegroepen en contextuele woorden als een algebraïsche structuur om toestandsonafhankelijke contextualiteit te analyseren, waarbij het de voorwaarden voor het ontstaan van dergelijke fenomenen karakteriseert en unitaire representaties van deze groepen construeert.
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.
Deze paper identificeert en formaliseert in Lean 4 een onmogelijkheidsbarrière voor directe compositiebewijzen bij stap-duplicerende recursoren, demonstreert hoe projectiemethoden deze barrière omzeilen, en levert een volledig geverifieerde certificeringsketen voor een specifiek voorbeeldsysteem dat door geautomatiseerde tools als TTT2 wordt bevestigd.
Dit paper introduceert MPBMC, een hybride benadering die Graph Neural Networks en runtime-statistieken combineert om eigenschappen te clusteren en zo de prestaties van Bounded Model Checking bij multi-eigenschapverificatie aanzienlijk te verbeteren.
Dit artikel onderzoekt behoudsresultaten voor de onafhankelijke fusie van één-variabele eerste-orde modale logieken en toont aan dat Kripke-compleetheid en beslisbaarheid behouden blijven zonder gelijkheid, maar verloren gaan bij fusies met gelijkheid en niet-rigide constanten door middel van het coderen van Diophantische vergelijkingen.
Dit artikel biedt volledige axiomatische beschrijvingen van Kullback-Leibler- en Rényi-divergenties binnen een categorisch raamwerk, waarbij deze divergenties worden geanalyseerd als kwantitatieve verrijkingen van categorieën van stochastische matrices onder zowel de Kronecker-product- als de direct-sum-monoidale structuren.
Dit artikel geeft een overzicht van systematische benaderingen voor basis-begrensde fragmenten van de propositielogica en modale logica, waarbij de afhankelijkheid van expressiviteit en computationele complexiteit van de toegestane operatoren wordt onderzocht door Post's tralie te combineren met een kader voor modale fragmenten, terwijl ook resultaten over leerbaarheid worden geïntegreerd en open problemen worden geïdentificeerd.
Dit artikel introduceert de semantisch gedefinieerde constructieve master-modale logieken en , bewijst dat deze EXPTIME-volledig zijn en een exponentiële eindige model-eigenschap bezitten, en lost hiermee het conjectuur van Afshari et al. op door de EXPTIME-compleetheid van hun diamant-vrije fragment vast te stellen.
Dit paper introduceert een methode voor het leren van constraints in de klassieke eerste-orde connectie-calculus om de excessieve terugkoppeling bij niet-confluente bewijszoekprocessen te verminderen zonder de volledigheid te verliezen.
Dit artikel introduceert een nieuwe aanpak voor het oplossen van stringvergelijkingen door Nielsen-transformaties uit te breiden met een machtsoperator, generalisaties van Parikh-afbeeldingen en gelijkheidsontbinding.
NL2GDS is een innovatief framework dat grote taalmodellen gebruikt om natuurlijke taalbeschrijvingen om te zetten in synthesiseerbare RTL-code en volledige GDSII-layouts via de OpenLane-flow, waardoor de ASIC-ontwerpproces wordt gedemocratiseerd en aanzienlijke verbeteringen in oppervlakte, vertraging en energieverbruik worden bereikt.
Dit paper introduceert SCORE, een programmeertaal voor het manipuleren van variabelen en stacks, en bewijst met behulp van een bewijshulpmiddel dat alle operaties in deze taal totale bijecties zijn, waardoor het een reversibel computationeel model biedt dat geschikt is voor het bestuderen van computationele complexiteit.
Dit paper introduceert een nieuwe theorie voor de I-calculus, gebaseerd op "Ohana-trees" die vergeten variabelen vasthouden, en bewijst de consistentie daarvan via Taylor-ontwikkeling en een aangepast relationeel denotationeel model.
Dit paper introduceert LeanTutor, een proof-of-concept systeem dat de kracht van Large Language Models en theorem-provers combineert om een AI-gestuurde wiskundige bewijstutor te creëren die fouten minimaliseert en natuurlijke taalfeedback biedt, getest op de nieuwe PeanoBench-dataset.
Dit artikel introduceert een nieuw geometrisch raamwerk dat redeneren in grote taalmodellen beschrijft als vloeiende trajecten in representatieruimte, waarbij empirische bevindingen aantonen dat deze modellen logische invarianten als hogere-orde geometrie internaliseren, wat de "stochastische papegaai"-hypothese uitdaagt en wijst op een universeel representatief principe.
Dit paper introduceert Strat2Rocq, een methode die bewijsstrategieën uit grote taalmodellen extraheert en formaliseert als lemmata om het succespercentage van het symbolische bewijsinstrument CoqHammer te verhogen, terwijl deze lemmata ook de prestaties van taalmodel-agenten ten goede komen.
Dit paper introduceert SpotIt, een nieuwe evaluatiepipeline die formele verificatie gebruikt om onbetrouwbare testgebaseerde Text-to-SQL-evaluaties te verbeteren door actief databases te zoeken die gegenereerde en grondwaarheid SQL-query's onderscheiden.
Dit artikel presenteert een schaalbare methodologie voor het formeel verifiëren van drijvende-kommaberekeningen via directe RTL-tot-RTL modelchecking, waarbij een verdeel-en-heerst-strategie wordt gecombineerd met door AI gegenereerde eigenschappen en menselijke feedback om de dekking en efficiëntie te maximaliseren.