Preuve de correction générée par des réseaux neuronaux

La vérification fondamentale permet aux programmeurs de concevoir des logiciels dont l’assurance de correction a été démontrée empiriquement dans divers domaines cruciaux. Toutefois, le coût de production de logiciels vérifiés fondamentalement reste prohibitif pour la majorité des projets, car il exige un effort manuel important de la part d’experts hautement formés. Dans cet article, nous présentons Proverbot9001, un système de recherche de preuves basé sur des techniques d’apprentissage automatique, conçu pour générer des preuves de correction logicielle dans des vérificateurs de théorèmes interactifs. Nous évaluons Proverbot9001 sur les obligations de preuve issues d’un vaste projet de vérification pratique, à savoir le compilateur C vérifié CompCert, et montrons qu’il peut automatiser efficacement des preuves auparavant réalisées manuellement, produisant automatiquement des preuves pour 27,5 % des énoncés de théorèmes dans notre ensemble de tests, lorsqu’il est combiné à des outils basés sur des solveurs. Sans l’ajout de solveurs supplémentaires, nous obtenons un taux de complétion des preuves quatre fois supérieur à celui des modèles d’apprentissage automatique les plus avancés précédemment publiés pour la génération de preuves dans Coq.