Résumé Technique : Théorie des Modèles Ultraconstructive via des Structures Finies Adversarielles Bornées

1. Énoncé du Problème

La théorie des modèles classique repose sur la relation idéale $A \models T$, où une structure achevée $A$ satisfait une théorie $T$. Ce cadre suppose des ressources illimitées et des structures achevées, ce qui entre en conflit avec les contraintes des échelles de calcul finies et les perspectives de l'ultrafinitisme.

Le document répond à la question suivante : Que peut-on certifier lorsque les structures sont partielles, les ressources sont bornées et les tests sont choisis de manière adversarielle ? L'auteur propose de remplacer la notion statique de « modelité » par un concept dynamique de survie adversarielle bornée. Au lieu de déclarer une structure comme modèle de manière définitive, le système certifie si une structure partielle peut survivre à une surface d'attaque, une profondeur et un budget de calcul spécifiés face à un adversaire actif.

2. Méthodologie : Le Jeu UCMT

La méthodologie centrale est le jeu de la Théorie des Modèles Ultraconstructive (UCMT), une interaction à trois parties impliquant :

1. Le Constructeur (Dieu) : Propose des éditions sémantiques légales sur une structure partielle pour satisfaire des obligations ou réparer des violations.
2. L'Opposant (Le Diable) : Sélectionne des défis légaux à partir d'une surface d'attaque bornée (profondeur $k$) pour exposer des violations ou forcer de nouvelles obligations.
3. Le Juge Symbolique : La seule source de verdicts logiques. Il vérifie si les engagements actuels satisfont le fragment borné de la théorie et l'objectif.

Composantes Formelles Clés

• Relation de Forçage Bornée ($A \Vdash_{k,b} T$) : Cette notation signifie que la structure $A$ survit à un épisode de profondeur $k$ et de budget $b$. Elle n'implique pas une satisfaction classique illimitée.
• Structures Partielles avec Inconnues : Les structures sont définies sur des domaines finis avec des interprétations partielles (valeurs $\{0, 1, ?\}$ pour les relations ; applications partielles pour les fonctions).
• Obligations et Certificats :
  • Obligations : Existentials opérationnels (ex: $\exists y \psi(\bar{a}, y)$) qui doivent être déchargés par la production d'un témoin.
  • Certificats : Éléments validés (instances d'axiomes, invariants) qui doivent rester stables lors des réparations pour éviter le « battement » (corriger un problème en en brisant un autre précédemment stable).
• Résultats :
  • God_Wins (Dieu_Gagne) : Le Constructeur survit au budget et produit un candidat de modèle $(k,b)$.
  • Devil_Wins (Diable_Gagne) : L'Opposant produit un certificat d'obstruction bornée, prouvant qu'aucune continuation légale dans le domaine fini et les bornes ne peut réussir. Cela se distingue d'un simple dépassement de délai (timeout).
  • Draw (Match nul) : Le budget est épuisé sans victoire certifiée ni obstruction.

Intégration Neuro-Symbolique

Le document introduit la UCMT-CEGIS (Synthèse Inductive Guidée par Contre-exemple), où des politiques neuronales (NeuralDevil et NeuralGod) sélectionnent les coups. Crucialement, ces politiques sont admissibles : elles ne choisissent que parmi l'ensemble des coups légalement énumérés définis par la couche symbolique. Le Juge symbolique et les énumérateurs d'obstruction restent les seuls arbitres de la vérité et de l'échec.

3. Contributions Clés

Le document établit une métathéorie finie auto-contenue et un prototype d'implémentation :

1. Sémantique Finie Bornée : Une définition formelle du jeu Dieu–Diable–Juge sur des structures finies partielles, introduisant la relation de forçage bornée $\Vdash_{k,b}$ et le concept de certificats d'obstruction bornée.
2. Métathéorie Finie (Section 7) :
   • Terminaison : Prouvé que chaque épisode borné s'arrête et retourne exactement un résultat (God_Wins, Draw, ou Devil_Wins).
   • Correction (Soundness) :
     • God_Wins est correct par rapport au fragment vérifié par le Juge (instances de base de profondeur $\le k$).
     • Devil_Wins est correct en tant que certificat d'obstruction bornée, vérifié par énumération exhaustive de l'espace de complétion finie.
   • Complétude Bornée Exhaustive : Sur un domaine fini fixe et une profondeur donnée, la procédure est décidable et exhaustive ; elle trouve soit une complétion gagnante, soit certifie qu'aucune n'existe.
   • Admissibilité Neurale (Non-Hallucination) : Remplacer la sélection de mouvements symboliques par des politiques neurales ne compromet pas la correction logique, à condition que les agents neuraux ne choisissent que parmi les mouvements légaux pré-vérifiés.
3. Prototype (ADAMANTIUM) : Une implémentation réalisant la boucle avec des politiques apprises.
4. Pont Conditionnel vers MTU-II : Une connexion proposée entre UCMT et la sémantique MTU-II / Esenin–Volpin, présentant l'UCMT comme un raffinement de la sémantique de Kripke à ressources bornées avec un « adversaire explicite ».

4. Résultats Expérimentaux

L'auteur a mené des expériences contrôlées à très petite échelle pour valider la sémantique et la discipline des certificats, en affirmant explicitement ne pas prétendre à une performance de recherche de modèles finis généraux ou de mise à l'échelle.

• Démo A (Cyclic God_Wins) : Sur un domaine à 3 éléments avec une signature cyclique, le système a construit avec succès un 3-cycle sans point fixe, aboutissant à un résultat God_Wins où le Juge a accepté la complétion.
• Démo B (Cyclic Devil_Wins) : Sur un domaine à 2 éléments avec la même signature, le système a prouvé l'impossibilité. L'Opposant a généré un résultat Devil_Wins avec un certificat d'obstruction bornée certifié.
  • Métriques : 128 complétions vérifiées, 0 complétion gagnante, budget non épuisé.
  • Signification : Cela démontre une preuve certifiée d'impossibilité dans le régime borné, distincte d'un simple timeout de recherche.
• Co-entraînement Minimal Jugé : Une boucle où les politiques NeuralDevil et NeuralGod sont toutes deux mises à jour via des gradients de politique basés sur les récompenses du Juge. L'expérience a vérifié que les deux ensembles de paramètres se mettaient à jour tandis que les garanties de correction du Juge restaient intactes.

5. Signification et Revendications

Le document maintient une portée modeste, délimitant clairement ce qu'il accomplit et ce qu'il ne fait pas :

• Ce qu'il est : Un substitut opérationnel fini et mathématique à la théorie des modèles classique, remplaçant la satisfaction idéale par la survie adversarielle bornée. Il fournit un cadre pour générer des témoins observables et des certificats d'obstruction bornés.
• Ce qu'il n'est pas :
  • Ce n'est pas un prouveur de théorèmes général ou un chercheur de modèles finis complet pour des tailles de domaines arbitraires.
  • Il ne prétend pas être équivalent à MTU-II ; la connexion est énoncée comme un pont conditionnel (Section 11) dépendant d'importations de constructions.
  • Les expériences sont des démonstrations jouets (2 et 3 éléments) destinées à valider les sémantiques et la discipline des certificats, et non à établir la mise à l'échelle ou la performance par rapport aux solveurs SAT/SMT.

Conclusion : La contribution primaire est la formulation mathématique d'un jeu adversariel fini qui produit des résultats sonores et vérifiables (God_Wins/Devil_Wins), même lorsque des agents neuraux sont impliqués dans la sélection de mouvements. Le système garantit que la « vérité » et l'« échec » sont arbitrés uniquement par un Juge symbolique, tandis que l'apprentissage est confiné à la sélection de mouvements légaux, préservant ainsi la correction logique dans un contexte neuro-symbolique.