28 articles
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.
Ce papier étudie la complexité des automates reconnaissant les relations et les opérations sur les suites -automatiques, établissant un lien entre la complexité des facteurs d'une suite intérieure et celle de ses sous-suites linéaires, tout en résolvant une question récente de Zantema et Bosma et en analysant la complexité de construction de ces automates via l'arithmétique de Büchi.
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 étudie les jeux graphiques concurrents où une équipe de joueurs coopère avec des sources de randomisation privées et indépendantes pour atteindre un état cible, démontrant que le problème de seuil se situe dans la théorie existentielle des réels et est NP-difficile, tandis que la quasi-certitude est NP-complète, et introduisant la logique IRATL pour formaliser ces scénarios.
Cet article résout les ambiguïtés des automates de dimensions supérieures en établissant une sémantique indépendante de l'ordre des événements basée sur les ipomsets d'intervalles, démontrant ainsi l'isomorphisme entre leurs présentations catégoriques et unifiant les notions de bisimulation pour offrir une fondation cohérente avec d'autres modèles de concurrence.
Cet article démontre l'indécidabilité de la borne du nombre de virages dans les automates à pile et à un compteur, établit des compromis non récursifs entre ces modèles, et prouve l'existence d'une hiérarchie infinie de classes de complexité basée sur des fonctions sous-linéaires croissantes.
Cet article étudie les arbres contextuels libres, démontrant qu'ils admettent une description par automates non déterministes à arêtes multiples et que le problème de l'isomorphisme pour les arbres contextuels libres déterministes est NL-complet, que les arbres soient enracinés ou non.
Cet article établit de nouvelles propriétés de la représentation des entiers, prouvant notamment une conjecture de Kimberling de 2012 à l'aide du prouveur de théorèmes Walnut et de l'assistant ChatGPT 5.
Cet article propose une synthèse unifiée de l'asymétrie fondamentale entre génération et reconnaissance en théorie des langages formels en identifiant six dimensions distinctes, dont deux nouvelles (directionnalité et temporalité), pour démontrer que cette divergence opérationnelle persiste malgré l'unification architecturale des modèles de langage modernes.
Cet article démontre que les facteurs des mots lisses sont des mots f-lisses et apporte des progrès significatifs vers la conjecture de Sing sur la complexité des mots f-lisses binaires, en prouvant la formule asymptotique pour les alphabets pairs, la borne inférieure pour tout alphabet binaire et en améliorant la borne supérieure pour les alphabets impairs.
Ce papier présente ZipLex, un cadre formellement vérifié en Scala pour l'analyse lexicale inversible et linéaire qui garantit que l'analyse et l'impression sont des inverses mutuels tout en surpassant les solutions existantes en termes de performance et de complexité temporelle.
Cet article propose une approche basée sur les données pour la commande supervisée non bloquante des systèmes à événements discrets en introduisant et en formalisant le concept d'« informativité des données de marquage », tout en développant des algorithmes pour vérifier cette propriété et déterminer les sous-ensembles de spécifications réalisables lorsque les données initiales sont insuffisantes.
Cet article établit un cadre théorique unifié pour le décodage contraint par grammaire, démontrant que l'équivalence linguistique n'implique pas l'efficacité computationnelle et prouvant que la complexité structurelle inhérente à certaines grammaires impose des bornes inférieures incompressibles sur le coût de décodage, tout en fournissant des métriques d'optimisation et des garanties de distorsion pour les architectures de modèles de langage modernes.
Ce papier établit une correspondance formelle entre les machines de Moore et les modèles d'espace d'état (SSM), démontrant que l'initialisation des SSMs par des automates appris symboliquement permet d'accélérer la convergence et d'améliorer la précision par rapport à une initialisation aléatoire.
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 étudie des théorèmes de type Ramsey pour les arbres infinis et leurs applications à la résolution du problème d'expansion pour les algèbres d'arbres.
Cet article propose une méthode de conduite autonome intégrant une conscience du risque inspirée du comportement humain, qui utilise des spécifications de logique temporelle linéaire (LTL) et une programmation linéaire pour équilibrer les risques de collision et les violations du code de la route dans des scénarios complexes.
Cet article démontre les conjectures de Clark Kimberling concernant la séquence binaire définie par inflation, établit son lien avec le mot de Tribonacci infini, et détermine sa complexité factorielle ainsi que son exposant critique, en s'appuyant notamment sur le prouveur de théorèmes Walnut.
Cet article établit une classification complète de la complexité computationnelle distribuée des problèmes d'optimisation locale dans les cycles orientés, démontrant que leur résolution se situe dans l'une des quatre classes de complexité distinctes (O(1), Θ(log* n) ou Θ(n)) et fournissant un algorithme centralisé capable d'identifier automatiquement cette classe ainsi que de synthétiser un algorithme distribué asymptotiquement optimal.