Lyra : Orchestration de la correction double dans la démonstration automatique de théorèmes

Les grands modèles linguistiques (LLM) offrent une voie prometteuse pour l’exploration en preuve formelle de théorèmes. Toutefois, leur potentiel intégral — en particulier en ce qui concerne la réduction des hallucinations et l’amélioration par le biais des messages d’erreur du vérificateur — reste une zone qui n’a pas encore été suffisamment explorée. Pour renforcer l’efficacité des LLM dans ce domaine, nous introduisons Lyra, un nouveau cadre qui met en œuvre deux mécanismes de correction distincts : la Correction par Outil (Tool Correction, TC) et la Correction par Conjecture (Conjecture Correction, CC). Pour implémenter la Correction par Outil dans le post-traitement des preuves formelles, nous exploitons des connaissances préalables afin d’utiliser des outils de vérification prédéfinis (par exemple, Sledgehammer) afin de guider le remplacement des outils incorrects. La Correction par Outil contribue de manière significative à atténuer les hallucinations, améliorant ainsi la précision globale de la preuve. En outre, nous proposons la Correction par Conjecture, un mécanisme de retour d’erreur conçu pour interagir avec le vérificateur afin de raffiner les conjectures de preuve formelle à l’aide des messages d’erreur fournis par le vérificateur. Contrairement au cadre précédent de raffinement, la Correction par Conjecture améliore la génération à l’aide d’instructions, sans nécessiter la collecte de paires (génération, erreur & raffinement). Notre méthode atteint des performances de pointe (SOTA) sur les ensembles de validation miniF2F (48,0 % → 55,3 %) et de test (45,5 % → 51,2 %). Nous présentons également trois problèmes de l’IMO résolus par Lyra. Nous estimons que la Correction par Outil (post-traitement pour atténuer les hallucinations) et la Correction par Conjecture (ajustement des sous-objectifs par interaction avec l’environnement) pourraient ouvrir une voie prometteuse pour les recherches futures dans ce domaine.