L'article présente Lean4Agent, un cadre utilisant Lean4 pour la modélisation et la vérification formelle du comportement des agents, notamment pour les workflows multi-étapes pilotés par les LLM. Il vise à pallier le manque de méthodes formales dans les systèmes d'agents actuels, permettant des vérifications de cohérence sémantique et la localisation des échecs d'exécution.
Cette recherche introduit un nouveau cadre d'apprentissage pour raffiner, visant à réduire le coût de calcul prohibitif des Grands Modèles de Langage (LLM) dans la preuve formelle de théorèmes. En exploitant les sorties des compilateurs qui compressent diverses tentatives de preuve en modes d'échec structurés, la méthode permet une exploration efficace des preuves et une correction locale des erreurs, amplifiant significativement les capacités de raisonnement des prouveurs de base.
Cet article propose un cadre formellement vérifié pour l'analyse de brevets, utilisant un pipeline hybride IA et Lean 4. C'est la première application connue de la preuve de théorèmes interactive à l'analyse de la propriété intellectuelle, résolvant les lacunes des méthodes actuelles.
Ceci est un plan v0.0 de l'article 'Rei as a Formal-Verification Compilation Pass for AI-Generated Mathematics', détaillant la proposition de Rei en tant que passe de compilation pour la vérification formelle des hypothèses générées par l'IA. La validation actuelle est au stade de l'exécution de tests préliminaires, avec une démonstration complète en attente pour la promotion de la v0.1.
Cet article présente une sémantique algébrique pour l'exécution gouvernée, construite sur des arbres d'interaction et la coinduction paramétrée, avec une implémentation mécanisée en Rocq. Le cadre introduit une GovernanceAlgebra qui induit une catégorie monoïdale symétrique et un système d'effets algébriques assurant des gestionnaires préservant la gouvernance.
Cet article propose BODHI, une méthode d'invite de connaissance de domaine pour l'inférence de spécifications de noyau de système d'exploitation, visant à surmonter les limitations actuelles des LLM. Elle augmente l'invite standard en quelques coups avec un guide de traduction structuré C vers Python, améliorant l'automatisation et la précision des spécifications.
Cette recherche introduit les Transformers Vérifiables, un cadre pour convertir les circuits de Transformer localisés par tâche en assertions bornées et vérifiables par solveur. Il permet la vérification de propriétés telles que l'équivalence fonctionnelle et la robustesse via un encodage SMT direct ou médiatisé par substitut.
NeuroNL2LTL est une architecture neurosymbolique unifiant la traduction apprise et la vérification formelle pour traduire le langage naturel en Logique Temporelle Linéaire. Elle utilise un entraînement avec vérificateur dans la boucle, où les résultats de vérification servent de signaux de récompense pour l'apprentissage par renforcement, optimisant la correction formelle.