63 articles
Cet article étudie comment les propriétés de commutativité et de lois de Kleisli de plusieurs monades de probabilités, notamment le monade de Giry et celui de Radon, découlent de leurs présentations comme monades de codensité, en établissant de nouvelles propriétés universelles et des conditions pour qu'elles soient monoidales et affines dans le cadre des catégories de Markov.
Cet article introduit un opérade de diagrammes de câblage dirigés dépendants pour composer des systèmes instantanés comme les machines de Mealy, en définissant une algèbre de diagrammes de stocks et flux et en établissant une sémantique via un morphisme vers les machines de Mealy.
Ce papier présente Preguss, un cadre modulaire qui combine l'analyse statique et les grands modèles de langage pour générer automatiquement des spécifications formules et vérifier l'absence d'erreurs d'exécution dans de grands programmes, réduisant ainsi l'effort de vérification humaine de 80,6 % à 88,9 %.
Cet article présente une méthode de vérification formelle évolutive pour les circuits d'estimation de phase quantique, capable de vérifier des circuits comportant jusqu'à 1 024 qubits de phase en utilisant une abstraction symbolique basée sur la logique des vecteurs de bits.
Cet article établit explicitement que la taille d'un circuit optimal varie au plus de lors d'une perturbation ponctuelle de la table de vérité, une borne confirmée comme optimale pour via une vérification exhaustive sur la base AIG.
Le papier présente RoadLogic, une solution open-source qui comble le fossé entre les spécifications déclaratives OpenSCENARIO et les simulations exécutables pour les véhicules autonomes en utilisant la programmation par ensembles de réponses et la planification de mouvement pour générer automatiquement des scénarios réalistes et conformes.
Cet article présente un cadre général permettant d'étendre la compilation en d-DNNF aux requêtes SMT modulo théories, réduisant ainsi les problèmes au niveau SMT à des problèmes propositionnels résolubles en temps polynomial grâce à l'ajout de lemmes théoriques pré-calculés.
Ce papier présente BemaGANv2, un vocodeur basé sur les GAN optimisé pour la génération audio longue durée, qui améliore la fidélité et la cohérence temporelle grâce à l'intégration de modules AMP et d'une combinaison systématique de discriminateurs innovants comme le MED et le MRD.
Le papier présente FATE, une nouvelle série de benchmarks en algèbre formelle couvrant des niveaux de difficulté allant des exercices universitaires à des problèmes dépassant les examens de doctorat, révélant que les modèles de langage actuels éprouvent des difficultés majeures à formaliser un raisonnement mathématique avancé, avec des taux de réussite extrêmement faibles sur les problèmes les plus complexes.
Cet article formalise en théorie des types homotopique la correspondance de Galois entre les espaces de revêtement et les sous-groupes du groupe fondamental, en développant une généralisation n-dimensionnelle et en classifiant les revêtements des espaces lenticulaires ainsi que la construction de la sphère d'homologie de Poincaré.
Cet article présente une nouvelle méthode qui étend l'extraction de spécifications à partir de traces d'exécution au-delà des abstractions booléennes en combinant la synthèse guidée par la syntaxe et la logique temporelle TSL pour apprendre des transformations de données et des spécifications temporelles, permettant ainsi de générer des programmes réactifs plus robustes et nettement plus efficaces en échantillons que les approches d'apprentissage passif.
Cet article compare trois notions de satisfaisabilité pour la logique quantique en dimension fixe, démontrant que la sémantique standard admet des formules satisfaisables (comme SEP-1) qui sont rejetées par les sémantiques à projecteurs commutants globaux et à algèbres booléennes partielles locales, établissant ainsi une hiérarchie stricte entre ces classes de satisfaisabilité.
L'article présente une expérience d'autoformalisation à grande échelle de la topologie algébrique dans un environnement de preuve interactive, où des agents LLM collaborent de manière décentralisée via un marché de récompenses simulé pour proposer, prouver et vérifier dynamiquement des énoncés mathématiques.
Ce papier présente Twitch, un outil qui découvre automatiquement des abstractions (modèles de termes récurrents) à partir d'échecs de preuve ou de théorèmes réussis pour guider le prouveur de théorèmes équationnels Twee, permettant ainsi de résoudre de nouveaux problèmes et d'accélérer significativement les preuves.
Cet article présente LLM2SMT, une étude de cas démontrant qu'un agent codant basé sur un LLM peut construire entièrement, sans aucune ligne de code humain, un solveur SMT compétitif pour la logique QF_UF capable d'émettre des preuves formelles en Lean.
Le papier présente Elenchus, un système de dialogue entre un expert humain et un modèle de langage qui, en résolvant des tensions dialectiques, construit une base de connaissances formalisée dans la logique NMMS pour expliciter les relations inférentielles, comme démontré sur l'ontologie de provenance PROV-O.
Cette étude propose d'utiliser des réseaux de neurones à graphes pour prédire un ordre de branchement initial efficace afin d'accélérer les solveurs SAT de type CDCL sur des instances aléatoires et pseudo-industrielles, tout en constatant que cette approche perd de son efficacité sur des instances industrielles complexes où les heuristiques dynamiques du solveur annulent rapidement l'initialisation.
Cet article propose le cadre formel des bases de données orientées esquisses, qui encode les paradigmes de bases de données graphiques et leurs fonctionnalités via des modèles catégoriels, tout en introduisant des localisateurs pour le calcul paresseux de chemins et des esquisses de « bégaiement » pour faciliter la composition modulaire et l'évolutivité.
Cet article présente une méthode automatisée pour générer des exercices de preuve mathématique de complexité comparable, en utilisant des preuves par tableaux analytiques sans symboles logiques pour évaluer et contrôler la difficulté des exercices destinés aux cours de mathématiques discrètes du premier cycle.
Ce document présente les actes de la huitième conférence internationale sur la théorie des catégories appliquées, qui s'est tenue à l'Université de Floride du 2 au 6 juin 2025, et rassemble des contributions interdisciplinaires allant de l'informatique à la chimie en passant par la mécanique quantique.