💻 computer science

GPU-Accelerated Search and Certification of Bounded Indistinguishability in Finite Kripke Semantics

Cet article présente un cadre accéléré par GPU qui encode la sémantique de Kripke finie sous forme de masques de bits pour effectuer l'évaluation exhaustive de formules modales et la certification de contre-modèles à une échelle massive, révélant des bornes serrées sur la réfutabilité, synthétisant des mirages sémantiques et permettant une exploration sémantique assistée par graphisme.

Auteurs originaux : Faruk Alpay, Baris Basaran

Publié 2026-06-16

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Faruk Alpay, Baris Basaran

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez de déterminer si deux ensembles d'instructions différents (appelés « formules ») sont en réalité la même chose. Dans le monde de la logique, il arrive que deux instructions semblent complètement différentes mais donnent exactement le même résultat dans chaque petite situation imaginable. La grande question est : Quelle doit être la taille de la situation avant que l'on finisse par voir une différence ?

Ce document est comme une expérience massive et à haute vitesse conçue pour répondre à cette question en utilisant une puce informatique super rapide (un GPU). Voici la décomposition de ce qu'ils ont fait et trouvé, en utilisant des analogies simples.

1. Le Problème : Le piège du « Monde Minuscule »

En logique, il existe une règle qui stipule que si une instruction est fausse, on peut prouver qu'elle est fausse avec un « contre-exemple » — un scénario spécifique où elle échoue. Habituellement, nous savons que ces scénarios existent, mais les mathématiques disent qu'ils pourraient être incroyablement vastes (comme une ville avec des milliards de maisons).

Les chercheurs se sont demandé : Avons-nous vraiment besoin d'une ville pour trouver une erreur, ou pouvons-nous la trouver dans un petit village ? Et plus important encore : Si deux instructions semblent identiques dans un village, quelle taille le bourg doit-il atteindre avant qu'elles ne commencent à agir différemment ?

2. L'Outil : Le Super-Scanner de « Masque de Bits »

Pour tester cela, ils ont construit un scanner spécial. Au lieu de vérifier un scénario à la fois (comme un humain lisant un livre), ils ont transformé tout le monde des possibilités en entiers (nombres).

L'analogie : Imaginez une rangée d'interrupteurs. Si un interrupteur est sur « on », une condition est vraie ; si c'est sur « off », elle est fausse.
L'astuce : Ils ont compressé des milliers de ces interrupteurs dans un seul nombre. Ensuite, ils ont utilisé la carte graphique de l'ordinateur (le GPU) pour basculer ces interrupteurs pour des millions de « mondes » différents simultanément.
Le résultat : Ils ont pu vérifier 163 billions (1,63 × 10¹⁴) de scénarios différents en seulement 45 minutes. C'est comme vérifier toutes les combinaisons possibles d'un jeu de cartes le temps de préparer une tasse de café.

3. Premier Résultat : Les petites erreurs sont courantes

Ils ont testé des milliers de formules logiques simples.

La découverte : La plupart des formules qui sont « fausses » (invalides) échouent très rapidement. En fait, pour la grande majorité d'entre elles, vous n'avez besoin que d'un monde avec une ou deux « pièces » (mondes) pour prouver qu'elles sont fausses.
La métaphore : Les vieux livres de mathématiques disaient : « Pour prouver que ceci est faux, vous pourriez avoir besoin d'un manoir avec 128 pièces. » Les chercheurs ont découvert que, dans la pratique, vous n'avez presque toujours besoin que d'un placard (1 ou 2 pièces) pour attraper l'erreur. L'estimation du « manoir » était bien trop pessimiste.

4. Deuxième Résultat : Le « Mirage Sémantique » (Les Jumeaux Trompeurs)

La partie la plus excitante a été de trouver deux formules qui sont indiscernables pendant longtemps.

L'analogie : Imaginez deux jumeaux, Alpha-2 et Alpha-3. Si vous les placez dans une pièce avec 1, 2, 3, 4 ou même 5 personnes, ils agissent exactement de la même manière. Vous ne pouvez pas les distinguer.
La percée : Les chercheurs ont découvert que ces jumeaux finissent bien par agir différemment, mais seulement lorsqu'on les place dans une pièce avec 6 personnes.
La preuve : Ils ne se sont pas contentés de deviner cela. Ils ont construit une pièce spécifique de 6 personnes (un « contre-modèle ») et ont prouvé mathématiquement que c'est la plus petite pièce possible où les jumeaux se séparent. Avant cela, personne ne savait exactement où la ligne était tracée.

5. Troisième Résultat : La « Carte » vs Le « Moteur de Recherche »

Ils ont également essayé de visualiser ces formules logiques sur une carte en 2D (comme un diagramme de dispersion) pour voir si les humains pouvaient repérer les différences simplement en regardant l'image.

Le résultat : La carte était désordonnée. C'était comme essayer de trouver une aiguille spécifique dans une botte de foin où 99 % des aiguilles étaient empilées les unes sur les autres.
La conclusion : La carte est bonne pour générer des idées (trouver des candidats), mais elle n'est pas un moteur de découverte. Vous ne pouvez pas simplement regarder l'image et dire : « Ah, voilà la différence ! » Vous avez toujours besoin de l'ordinateur ultra-rapide pour vérifier les candidats spécifiques que la carte suggère. L'ordinateur est le juge ; la carte n'est qu'une boîte à suggestions.

6. Le Système de « Certificat »

Pour s'assurer que l'ordinateur ultra-rapide ne faisait pas d'erreur (puisqu'il est si rapide qu'il pourrait sauter une étape), ils ont construit un programme « arbitre » séparé, plus lent mais très prudent.

Comment ça marche : L'ordinateur rapide trouve une erreur potentielle et lui remet un « certificat » (une note disant : « Voici la formule, voici le monde, voici la preuve »).
La vérification : L'arbitre lent lit le certificat et dit : « Oui, ceci est correct. »
Pourquoi c'est important : Cela signifie que les résultats sont 100 % dignes de confiance. Ils n'ont pas seulement obtenu une réponse rapide ; ils ont obtenu une réponse vérifiée.

Résumé

Ce document traite de l'utilisation d'une carte graphique ultra-rapide pour tester de manière exhaustive des règles logiques dans des mondes minuscules. Ils ont découvert que :

La plupart des erreurs logiques sont capturées dans des mondes très petits (1 ou 2 pièces).
Ils ont trouvé une paire spécifique de règles logiques qui semblent identiques jusqu'à ce que l'on atteigne un monde de 6 pièces, et ils ont prouvé que c'est le point exact où elles divergent.
Les cartes visuelles aident à savoir où chercher, mais vous avez toujours besoin de l'ordinateur pour confirmer ce que vous voyez.

C'est l'histoire de l'utilisation de la force brute (vérifier tout) combinée à des mathématiques intelligentes pour trouver le moment précis où deux choses cessent d'être les mêmes.

Résumé Technique : Recherche accélérée par GPU et certification de l'indistinguabilité bornée dans les sémantiques de Kripke finies

Énoncé du Problème
L'article traite de deux questions fondamentales concernant la logique modale et la théorie des modèles finis qui sont décidables mais coûteuses en termes de calcul :

Taille du contre-modèle minimal : Pour les formules modales invalides, quelle est la taille réelle des contre-modèles minimaux par rapport aux limites exponentielles standards fournies par la propriété du modèle fini (FMP) et la filtration ?
Indistinguabilité bornée : Quelle doit être la taille d'un modèle fini pour qu'il puisse distinguer deux formules qui semblent équivalentes sur tous les modèles plus petits ? Les auteurs définissent une paire de formules comme étant k-indistinguables si elles concordent sur tous les cadres (frames) de taille $\le k$ mais divergent sur un cadre de taille $k+1$ .

Alors que les techniques standard de vérification de modèles symbolique basées sur les BDD compressent les grands espaces d'états pour une seule formule, ce travail cible le régime opposé : un recensement complet de nombreuses formules contre de nombreux petits cadres simultanément.

Méthodologie
Les auteurs exploitent la nature bit à bit de l'évaluation de Kripke finie pour permettre un parallélisme massif sur GPU.

Encodage par masque de bits (Bitmask Encoding) : Les mondes sont encodés sous forme d'entiers, et les évaluations sous forme de masques de bits. Les connecteurs booléens correspondent à des opérations bit à bit, tandis que les opérateurs modaux ( $\Box$ et $\Diamond$ ) sont réduits à des tests de contenance et d'intersection sur les masques de successeurs (Lemme 1). Cela élimine la nécessité de matérialiser le tenseur de vérité $(frame \times valuation)$ .
Noyau CUDA fusionné (Fused CUDA Kernel) : Un noyau unique évalue tout un corpus de formules contre tous les cadres d'une taille fixe en un seul passage. Les threads sont assignés aux cadres, itérant à travers les évaluations via des indices de boucle (évitant les tableaux d'évaluations) et réduisant les résultats via la mémoire partagée pour minimiser la contention atomique.
Architecture de vérification : Le système emploie un paradigme « recherche rapide, vérification lente ». Le GPU effectue l'énumération exhaustive, tandis qu'un évaluateur récursif distinct sur CPU (indépendant du moteur de masque de bits) vérifie chaque contre-modèle rapporté. Cela garantit que les résultats sont dignes de confiance, indépendamment des détails d'implémentation de l'accélérateur.
Synthèse active : Au-delà de l'énumération passive, les auteurs utilisent un protocole de synthèse active pour générer des paires de formules candidates (par exemple, $(\Box\Diamond)^m\top$ ) et rechercher des « mirages sémantiques » (paires indistinguables) en utilisant la génération de cadres adverses (Erdős–Rényi, goulots d'étranglement SCC, etc.) et des solveurs SAT pour les preuves de minimalité.
Récupération guidée par la représentation : L'article construit un « atlas sémantique » (une matrice de densité de profils d'échec) et évalue diverses techniques de réduction de dimensionnalité (PCA, UMAP, spectrale) pour la récupération de candidats. Crucialement, les visualisations sont traitées comme des interfaces de génération de candidats, et non comme des moteurs de découverte autonomes ; chaque candidat est revérifié par une recherche exhaustive.

Contributions Clés et Résultats

Correction et Complexité : Les auteurs fournissent une preuve de correction pour l'évaluateur de masque de bits (Théorème 1) et une analyse de complexité montrant que l'approche évite de stocker le tenseur de vérité (Proposition 1). Les 20 990 certificats générés ont été indépendamment vérifiés.
Petits Contre-modèles Minimaux : Dans un corpus de 5 624 formules sans constantes (jusqu'à 7 nœuds, 2 variables), l'étude a constaté que les contre-modèles minimaux sont étonnamment petits.
- Chaque formule réfutable dans la logique K est réfutée sur au plus 2 mondes (Proposition 3).
- La limite de filtration standard ( $2^{|Sub(\phi)|}$ ) est empiriquement lâche ; pour des formules à 7 nœuds, la limite suggère jusqu'à 128 mondes, mais le maximum observé était de 2 (Corollaire 1).
Synthèse de l'Indistinguabilité Bornée : Les auteurs ont synthétisé avec succès une paire 5-indistinguable ( $\alpha_2 = (\Box\Diamond)^2\top$ $α_{2} = (□◊)^{2} ⊤$ et $\alpha_3 = (\Box\Diamond)^3\top$ $α_{3} = (□◊)^{3} ⊤$ ). Ces formules concordent sur tous les cadres de taille $\le 5$ $\leq 5$ mais sont séparées par un chemin spécifique de 6 mondes (Proposition 5).
- Cette séparation a été confirmée à la fois par l'énumération exhaustive sur GPU et par des preuves SAT symboliques (Tableau 3).
- La synthèse de cadres adverses a produit 90 séparations vérifiées, dont 78 étaient non-templates (c'est-à-dire pas de simples chemins ou cycles).
Performance du Système :
- L'implémentation fusionnée sur H100 a atteint un taux soutenu de 60,2 milliards d'évaluations par seconde (1,63 $\times$ 10 $^{14}$ évaluations totales en 45 minutes).
- Elle était 47,1 $\times$ plus rapide qu'un CPU OpenMP bit-parallèle et 7,06 $\times$ plus rapide qu'une base CPU AVX-512 explicite sur des charges de travail identiques.
- Le calibrage matériel a atteint 18,87 source-level uint32 TOPS avec 98,3 % de temps moyen NVML busy.
Représentation et Récupération :
- Dans une tâche de récupération sur 5,4 millions de paires de candidats, les caractéristiques brutes de haute dimension ont été les plus performantes à des budgets de voisinage serrés ( $k=16$ ), tandis qu'un atlas PCA en 2D a été le plus performant à des budgets plus larges ( $k=1024$ ).
- Cependant, les auteurs soulignent que les visualisations en 2D souffrent d'un encombrement extrême (98,6 % des points partagent un bin à l'échelle de 100k) et ne sont pas des outils de découverte autonomes. Le pipeline repose sur la proposition guidée par la représentation suivie d'une vérification exhaustive.
Récupération de Correspondance : Le moteur a récupéré avec succès les conditions de cadre du premier ordre pour tous les axiomes de Sahlqvist (T, D, 4, 5, B, etc.) et a correctement identifié que l'axiome de McKinsey n'a pas de correspondant du premier ordre dans la bibliothèque testée, validant ainsi le système par rapport à la théorie établie.

Signification et Portée
L'article revendique sa importance non pas comme un nouveau procédure de décision pour la logique modale générale (qui reste PSPACE-complète), mais comme un protocole reproductible pour explorer le « régime des petits modèles » et les frontières de l'indistinguabilité.

Modestie des Revendications : Les auteurs précisent explicitement que leurs résultats sont limités. Le recensement décide de la validité uniquement pour les formules où la limite FMP est dans la taille recherchée (jusqu'à 5 mondes). Les affirmations concernant les formules survivant au-delà de cette plage sont des estimations ou des survivants bornés, et non des théorèmes.
Découverte vs Vérification : Le papier distingue la génération de candidats (via la synthèse ou les atlas visuels) de la certification de ceux-ci. La « découverte » de la paire 5-indistinguable est le résultat d'une synthèse active et d'une vérification exhaustive, et non d'une simple inspection visuelle.
Complémentarité : Ce travail est présenté comme complémentaire à la vérification de modèles symbolique (BDD/SAT). Alors que les méthodes symboliques compressent un grand espace d'états, cette approche balaie explicitement de nombreux petits modèles contre de nombreuses formules, un régime où les méthodes symboliques peuvent ne pas être optimales.

En résumé, l'article démontre que l'évaluation bit à bit accélérée par GPU permet le recensement exhaustif de petits modèles de Kripke, révélant que les contre-modèles minimaux sont souvent beaucoup plus petits que les limites théoriques ne le suggèrent, et fournit un cadre rigoureux pour la synthèse et la certification de l'indistinguabilité bornée dans la logique modale.