CriticLean : Apprentissage par renforcement guidé par un critique pour la formalisation mathématique

La traduction de déclarations mathématiques en langage naturel en code formel et exécutable est un défi fondamental dans la preuve automatique de théorèmes. Bien que les travaux antérieurs se soient concentrés sur la génération et le succès de la compilation, peu d'attention a été portée à la phase critique – l'évaluation de si les formalisations générées capturent réellement l'intention sémantique du problème original. Dans cet article, nous présentons CriticLean, un cadre novateur d'apprentissage par renforcement guidé par un critique qui élève le rôle du critique d'un validateur passif à une composante active d'apprentissage. Plus précisément, nous proposons tout d'abord CriticLeanGPT, formé par un ajustement supervisé et un apprentissage par renforcement, pour évaluer rigoureusement la fidélité sémantique des formalisations Lean 4. Ensuite, nous introduisons CriticLeanBench, un benchmark conçu pour mesurer la capacité des modèles à distinguer les formalisations sémantiquement correctes des incorrectes, et nous montrons que nos modèles CriticLeanGPT formés peuvent largement surpasser des baselines ouvertes et fermées solides. En nous appuyant sur le cadre CriticLean, nous construisons FineLeanCorpus, un ensemble de données comprenant plus de 285 000 problèmes qui présente une diversité de domaines riche, une couverture large en termes de difficulté et une grande exactitude selon l'évaluation humaine. Dans l'ensemble, nos résultats soulignent que l'optimisation de la phase critique est essentielle pour produire des formalisations fiables, et nous espérons que notre CriticLean fournira des pistes précieuses pour les avancées futures dans le raisonnement mathématique formel.