28 articles
Ce papier établit un lien fondamental entre la parallélisabilité des réseaux de neurones récurrents linéaires (LRNN) et les classes de complexité computationnelle, démontrant que leur structure permet une exécution efficace similaire aux transformateurs, contrairement aux RNN non linéaires qui, en raison de leur capacité à résoudre des problèmes P-complets, posent une barrière théorique à une telle parallélisation.
Cet article présente un algorithme distribué randomisé en une seule étape pour 2-colorer des cycles avec une fraction d'arêtes monochromes inférieure à 0,24118, établit une borne inférieure de 0,23879, et révèle que ces résultats ont été découverts par des modèles de langage et formalisés en Lean 4.
Cet article établit la complexité du problème de l'accessibilité pour les VASS étendus à des compteurs entiers (VASS+Z) en démontrant qu'il est NP-complet pour une seule composante non négative, en PSPACE-difficile et TOWER-difficile pour deux et trois composantes respectivement, et en prouvant qu'il se situe dans la classe pour , ce qui représente une amélioration significative par rapport aux bornes précédentes.
Cet article établit des conditions algébriques nécessaires et suffisantes sur les paramètres d'une règle de cellule automate de premier degré à états, permettant de vérifier sa réversibilité pour toute taille de réseau en temps constant et de synthétiser toutes les règles réversibles correspondantes.
Cet article établit que le problème de calcul des alignements en fouille de processus est PSPACE-complet sur les réseaux de Petri sûrs, NP-complet sur plusieurs sous-classes comme les arbres de processus et les systèmes T, mais résoluble en temps polynomial pour les systèmes S vivants et sûrs.
Cet article résout un problème ouvert depuis plus d'une décennie en démontrant, à l'aide d'un exemple de 65 états validé par ordinateur, qu'un automate de Büchi historiquement déterministe peut être strictement plus concis que tout automate de Büchi déterministe équivalent.
Cet article présente la modélisation formelle, la vérification et le test de l'environnement d'exécution des automates de contrat (CARE) à l'aide de l'outil Uppaal, démontrant ainsi comment ces processus formels améliorent la fiabilité d'une application distribuée open source.
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.