63 papers
Dit artikel onderzoekt hoe drie fundamentele eigenschappen van kansmonaden, zoals de Giry- en Radon-monaden, voortvloeien uit hun codensity-presentaties, waarbij nieuwe universele eigenschappen worden afgeleid en voorwaarden worden geformuleerd voor hun monoidale en affiene structuur in de context van Markov-kategorieën.
Dit paper introduceert een operad van afhankelijke gerichte bedradingsdiagrammen om onmiddellijke systemen, zoals Mealy-machines en voorraad-stroomdiagrammen, te componeren door cycli in bedrading en directe input-afhankelijkheid van outputs te vermijden.
Dit paper introduceert Preguss, een modulair raamwerk dat statische analyse en deductieve verificatie combineert met LLM-ondersteunde synthesese om formele specificaties te genereren en zo de verificatie van grote, real-world programma's met meer dan 1000 regels code aanzienlijk te automatiseren en de menselijke inspanning met 80,6% tot 88,9% te verminderen.
Dit artikel presenteert een schaalbare formele verificatiemethode voor Quantum Phase Estimation-circuits die, door gebruik te maken van symbolische qubit-abstractie, correctheid garandeert voor circuits met meer dan 1.000 qubits binnen een beperkt geheugengebruik.
Dit artikel presenteert een expliciete constructieve bovengrens voor de verandering in circuitsgrootte bij verstoringen van de waarheidstabel, bevestigt deze theoretische schatting via een telescopisch argument en valideert de strakheid van de bound voor in de AIG-basis door middel van exhaustieve SAT-gebaseerde verificatie.
Dit paper introduceert RoadLogic, een open-source tool die declaratieve OpenSCENARIO-specificaties omzet in uitvoerbare simulaties voor het testen van autonome voertuigen door middel van Answer Set Programming, bewegingsplanning en specificatiegebaseerde monitoring.
Dit paper introduceert een algemeen raamwerk dat d-DNNF-compilatie toepast op SMT-problemen door theorielemmata te integreren, waardoor polytime SMT-query's mogelijk worden met behulp van standaard propositional reasoners.
Dit paper introduceert BemaGANv2, een geavanceerde GAN-gebaseerde vocoder voor hoogwaardige en langdurige audio-generatie die gebruikmaakt van innovatieve architecturale wijzigingen en een systematische evaluatie van discriminatorscombinaties om temporale coherentie en harmonische structuur te verbeteren.
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 formaliseert in homotopietypetheorie de Galoiscorrespondentie tussen overdekkingen en ondergroepen van de fundamentele groep, ontwikkelt een n-dimensionale generalisatie en past deze toe om overdekkingen van lensruimten te classificeren en de Poincaré-homologiesfeer te construeren.
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 vergelijkt drie waarheidsdefinities voor kwantumsatisfiabiliteit in een vaste eindige dimensie en bewijst dat de standaard Hilbert-lattice-semantiek strikt ruimer is dan zowel de globale commutatieve als de lokale partiële-Boolese semantiek, wat wordt aangetoond door een expliciet scheidingsformule die in de eerste wel maar in de andere twee niet satisfieerbaar is.
Dit paper beschrijft een experiment waarbij meerdere LLM-agenten in een interactief bewijssysteem samenwerken via een dynamisch bounty-marktmechanisme om algebraïsche topologie te formaliseren en te bewijzen.
Dit paper introduceert Twitch, een tool die automatisch abstraheringen ontdekt uit mislukte of succesvolle bewijzen om de prestaties en snelheid van de equationale bewijzer Twee aanzienlijk te verbeteren.
Dit paper presenteert LLM2SMT, een studie waarin een LLM-coderingsagent zonder enige menselijke code een complete SMT-oplosser voor QF_UF bouwt die concurrerend presteert op SMT-LIB-benchmarks.
Dit paper introduceert Elenchus, een dialoagsysteem dat kennisbases construeert door een expert in gesprek te laten treden met een LLM om inferentiële relaties te expliciteren, waarbij de resulterende dialectische staten worden gemapt naar een formeel logisch kader dat de ontwerprationalen van de W3C PROV-O-ontologie valideert.
Dit onderzoek toont aan dat het gebruik van grafische neurale netwerken om de initiële vertakkingsvolgorde van SAT-oplossers te voorspellen aanzienlijke snelheidswinst oplevert voor willekeurige en pseudo-industriële problemen, maar minder effectief is voor complexe industriële instanties doordat de dynamische heuristieken van de solver de initiële voorspelling snel overschrijven.
Dit paper introduceert schets-georiënteerde databases, een categorisch raamwerk dat databaseparadigma's en -schema's formaliseert als eindige limiet-schetsen en set-waardige modellen, en daarbij functies zoals paden en modulaire samenstelling behandelt via lokale inferentieregels en stuttering-schetsen.
Dit artikel presenteert een methode voor het automatisch genereren van bewoefsoefeningen met vergelijkbare complexiteit, waarbij de moeilijkheidsgraad wordt bepaald op basis van informele bewijsinspanning die formeel wordt vastgelegd via cut-gebaseerde tableau-bewijzen zonder logische symbolen.
Dit document presenteert de proceedings van de achtste internationale conferentie over toegepaste categorietheorie, die van 2 tot 6 juni 2025 aan de Universiteit van Florida plaatsvond en bijdragen omvatte die uiteenlopenden van pure wiskunde tot toepassingen in disciplines zoals informatica, kwantumrekenen en scheikunde.