Réf. : Form -- Réduction des prioris humains dans la vérification formelle logicielle évitable avec le renforcement par apprentissage dans les modèles de langage à grande échelle : Une étude préliminaire sur Dafny

Les modèles de langage à grande échelle (LLMs) basés sur des langages informels (par exemple, le langage humain) entraînés par apprentissage par renforcement (RL) font face à un défi important : leurs processus de vérification, qui fournissent des signaux d'entraînement cruciaux, ne sont ni fiables ni évolutifs. En effet, les modèles propriétaires de grande taille ont du mal à générer des programmes vérifiables. Une alternative prometteuse, mais largement inexplorée, est le raisonnement basé sur des langages formels. En ancrant les LLMs dans des systèmes formels rigoureux, où les modèles génératifs opèrent dans des espaces de langage formel (par exemple, Dafny), il devient possible de vérifier automatiquement et de manière mathématiquement prouvable leurs processus de raisonnement et leurs résultats. Cette capacité est essentielle pour atteindre une vérification logicielle formelle à grande échelle et fiable. Il est courant d'utiliser des chaînes de raisonnement annotées par des humains et d'autres connaissances a priori humaines afin d'induire les capacités de raisonnement et de codage des LLMs. Malheureusement, fournir ces connaissances a priori devient inacceptablement coûteux en termes de ressources humaines pour superviser des tâches de programmation complexes. Dans ce travail, nous explorons de manière systématique des moyens de réduire l'utilisation des connaissances a priori humaines, en utilisant le langage formel Dafny comme environnement principal pour notre étude pilote. Notre pipeline repose principalement sur l'introduction d'un pipeline de curation de données automatique et évolutif, ainsi que sur une conception soignée du RL intégrant des retours du vérificateur de langage formel. Nous introduisons DafnyComp, un benchmark de programmes formels composés avec des spécifications auto-formalisées pour le raisonnement sur les spécifications. La phase de finetuning supervisé (SFT) permet même aux petits modèles (par exemple, 0,5 milliard de paramètres) de générer du code Dafny syntaxiquement correct et vérifiable, surpassant ainsi les modèles propriétaires. L'apprentissage par renforcement avec régularisation améliore davantage les performances, permettant une meilleure généralisation aux tâches hors domaine et dépassant tous les modèles de base performants sur le benchmark exigeant DafnyComp.