67 articles
Ce papier présente Strat2Rocq, une méthode qui extrait et formalise les stratégies de preuve des grands modèles de langage en lemmas Rocq pour améliorer significativement l'efficacité des prouveurs symboliques comme CoqHammer, tout en bénéficiant également aux agents de preuve basés sur les LLM.
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.
Cet article présente une méthode évolutive de vérification formelle de l'arithmétique à virgule flottante au niveau RTL, qui combine une stratégie de vérification directe RTL-à-RTL, un raffinement guidé par les contre-exemples et la génération automatisée de propriétés par intelligence artificielle pour améliorer l'efficacité et la couverture.
Cet article propose une contrainte d'assertibilité inspirée de Brouwer pour les systèmes d'IA responsables, exigeant que les affirmations dans les domaines à haut risque soient accompagnées d'un certificat contestable ou marquées comme « indéterminées », afin de préserver l'agence épistémique démocratique en séparant l'entitlement interne de la portée publique.
Cet article démontre, à l'aide de modèles contre-exemples, que les principes d'induction et de coinduction ne sont pas dérivables dans la théorie des types dépendants polymorphes (P2) pure, soulignant ainsi la nécessité cruciale de l'extensionnalité fonctionnelle pour prouver l'induction et l'impossibilité de définir des types quotients paramétriques ou d'obtenir une coinduction forte dans ce système de base.
Ce papier propose les Réseaux de Neurones Logiques Modaux Continus (CMLNNs), une nouvelle approche nommée « Fluid Logic » qui remplace les structures de Kripke discrètes par des équations différentielles stochastiques neuronales pour intégrer le raisonnement modal dans l'apprentissage profond, permettant ainsi de garantir la cohérence structurelle des solutions neuronales via des contraintes logiques sans nécessiter la connaissance des équations gouvernantes.
Le papier présente SpotIt+, un outil open-source qui évalue les systèmes Text-to-SQL en générant des bases de données de différenciation réalistes grâce à une vérification d'équivalence bornée et à un pipeline de minage de contraintes combinant règles et LLM.