64 articles
Cet article présente une nouvelle approche combinant saturation basée sur l'ordre et réduction de buts pour l'automatisation de la logique du premier ordre, en proposant trois encodages SAT pour les calculs de connexions et en implémentant cette méthode dans le solveur upCoP.
Cet article introduit les groupes de commutation et les mots contextuels comme structures algébriques pour analyser et caractériser la contextualité indépendante de l'état, en reliant ces concepts aux représentations unitaires des groupes de Pauli généralisés.
Cet article propose un cadre de surveillance en ligne efficace et évolutif pour la Logique Temporelle Métrique (MTL) en construisant unifié des réseaux séquentiels à partir de spécifications temporelles, grâce à une technique de marquage temporel futur utilisant des représentations symboliques par intervalles.
Cet article établit que la vérification de module des systèmes multi-agents à pile (PMS) est 2EXPTIME-complète pour ATL, mais 4EXPTIME-complète pour ATL*, ce qui constitue un cas rare d'un problème de décision élémentaire dont la complexité dépasse le temps tri-exponentiel.
Cet article établit, grâce à une vérification formelle dans Lean 4 et à des preuves externes, l'impossibilité de prouver la terminaison de recursors dupliquant les étapes par des mesures compositionnelles globales, tout en démontrant que les méthodes basées sur la projection échappent à cette barrière et en délivrant une chaîne de certification complète pour un fragment sécurisé.
Cet article présente MPBMC, une approche hybride combinant des représentations fonctionnelles de circuits matériels via des réseaux de neurones à graphes et des statistiques d'exécution pour regrouper intelligemment les propriétés et accélérer la vérification par model checking borné multi-propriétés.
Cet article établit que la fusion indépendante de logiques modales du premier ordre à une variable préserve la complétude de Kripke et la décidabilité sans égalité, mais pas avec égalité ou constantes non rigides, tout en fournissant une condition suffisante générale pour le transfert de ces propriétés via une interprétation comme fusion de logiques modales propositionnelles partageant une modalité S5.
Cet article propose des axiomatisations complètes de la divergence de Kullback-Leibler et des divergences de Rényi d'ordre arbitraire en les étudiant sous un angle catégorique via une algèbre monoidale quantitative et un langage de diagrammes en cordes enrichi d'équations quantitatives, pour deux structures monoidales naturelles sur les matrices stochastiques.
Cet article propose une enquête sur les fragments restreints de la logique propositionnelle et modale, en montrant comment leur puissance expressive et leur complexité computationnelle dépendent des opérateurs autorisés, tout en unifiant des approches historiques et en étendant des résultats sur l'apprenabilité.
Cet article introduit les logiques modales constructives et , démontre qu'elles sont EXPTIME-complètes et possèdent la propriété de modèles finis de taille exponentielle, et résout ainsi la conjecture d'Afshari et al. concernant leur fragment sans opérateur diamant tout en permettant l'encodage de et .
Cet article présente une méthode d'apprentissage de contraintes appliquée au calcul des connexions en logique du premier ordre, permettant de réduire considérablement le retour en arrière dans la recherche de preuves tout en préservant la complétude.
Cet article présente une nouvelle approche pour résoudre des équations de chaînes en étendant les transformations de Nielsen grâce à la combinaison d'un opérateur de puissance, de généralisations des images de Parikh et d'une décomposition d'égalité.
Le papier présente NL2GDS, un cadre innovant utilisant des modèles de langage pour convertir des descriptions matérielles en langage naturel en conceptions RTL et en layouts GDSII optimisés via le flux OpenLane, démontrant des réductions significatives de la surface, du délai et de la consommation d'énergie par rapport aux conceptions de base.
Cet article présente SCORE, un langage conçu pour manipuler des variables et des piles, et démontre comment interpréter ses opérations comme des bijections totales certifiées par un assistant de preuve, permettant ainsi d'étudier la complexité computationnelle dans des modèles réversibles complets.
Cet article introduit une nouvelle théorie équationnelle pour le I-calcul basée sur les « arbres Ohana », qui préservent les variables libres masquées dans les sous-arbres sans signification, et démontre la compatibilité de cette égalité avec les opérations du calcul grâce à des théorèmes de commutation avec l'expansion de Taylor et à un modèle dénotationnel non idempotent étendu.
Ce papier présente LeanTutor, un système de tutorat mathématique basé sur l'IA qui combine les forces des grands modèles de langage et des prouveurs de théorèmes pour fournir des preuves vérifiables, évalué grâce à un nouveau jeu de données nommé PeanoBench.
Cet article propose un cadre géométrique novateur qui modélise le raisonnement des grands modèles de langage comme des flux lisses dans l'espace des représentations, démontrant que l'apprentissage par prédiction de token suffit à internaliser des invariants logiques sous forme de géométrie d'ordre supérieur, indépendamment de l'architecture ou des données d'entraînement.
Ce papier présente Strat2Rocq, une méthode qui extrait et formalise les stratégies de preuve des grands modèles de langage en lemmas Rocq pour améliorer significativement l'efficacité des prouveurs symboliques comme CoqHammer, tout en bénéficiant également aux agents de preuve basés sur les LLM.
Ce papier présente SpotIt, une nouvelle méthode d'évaluation Text-to-SQL qui remplace les tests basés sur des données statiques par une vérification formelle d'équivalence capable de détecter des différences entre les requêtes générées et les références, révélant ainsi les limites des approches actuelles sur le jeu de données BIRD.
Cet article présente une méthode évolutive de vérification formelle de l'arithmétique à virgule flottante au niveau RTL, qui combine une stratégie de vérification directe RTL-à-RTL, un raffinement guidé par les contre-exemples et la génération automatisée de propriétés par intelligence artificielle pour améliorer l'efficacité et la couverture.