L’autoformalisation, qui consiste à traduire les énoncés mathématiques exprimés en langage naturel en énoncés formels vérifiables par machine, est essentielle pour exploiter le raisonnement mathématique formel afin de résoudre des problèmes mathématiques énoncés en langage naturel. Bien que les grands modèles linguistiques (LLM) soient capables de générer des énoncés formels syntaxiquement corrects, ils échouent fréquemment à préserver l’intention sémantique initiale du problème. Cette limitation provient du fait que les approches basées sur les LLM traitent l’autoformalisation comme une tâche de traduction simpliste, dépourvue de mécanismes d’autoréflexion et de raffinement itératif, des outils que les experts humains utilisent naturellement. Pour remédier à ces lacunes, nous proposons ReForm, une méthode d’autoformalisation réfléchie qui intègre étroitement l’évaluation de la cohérence sémantique dans le processus d’autoformalisation. Cela permet au modèle de générer itérativement des énoncés formels, d’évaluer sa fidélité sémantique, puis de corriger automatiquement les erreurs identifiées grâce à un raffinement progressif. Pour entraîner efficacement ce modèle réfléchi, nous introduisons Prospective Bounded Sequence Optimization (PBSO), une méthode qui applique des récompenses différentes selon les positions dans la séquence, garantissant ainsi que le modèle développe à la fois une autoformalisation précise et des validations sémantiques correctes, tout en évitant des critiques superficielles qui compromettraient l’objectif même de la réflexion. Des expérimentations étendues sur quatre benchmarks d’autoformalisation montrent que ReForm obtient une amélioration moyenne de 17,2 points de pourcentage par rapport aux meilleures méthodes de référence. Pour assurer davantage la fiabilité de l’évaluation, nous introduisons ConsistencyCheck, un benchmark composé de 859 éléments annotés par des experts, qui non seulement valide l’utilisation des LLM comme juges, mais révèle également la difficulté intrinsèque de l’autoformalisation : même les experts humains commettent des erreurs sémantiques dans jusqu’à 38,5 % des cas.