Fil de Alexander Doria (@Dorialexander)

Donc DeepSeek-Math-V2. On pourrait sous-titrer cela : « Comment former de meilleurs vérificateurs ? », et l'essentiel du sujet consiste simplement à améliorer le traitement des données et les pipelines de synthèse (même si tous les modèles sont entraînés avec l'apprentissage par renforcement). DeepSeek s'éloigne encore davantage des promesses initiales d'auto-vérification spontanée de R0, tout simplement parce que l'approche n'est pas évolutive : un raisonnement tortueux aboutissant finalement à des réponses correctes reste très fragile et sujet à l'échec. Le projet débute par une annotation humaine, certes de haut niveau, mais elle représente en elle-même une évolution plus large du secteur, où nous cherchons à généraliser et automatiser le processus de contrôle qualité des données le plus performant possible. Ce processus tire également parti d'une observation faite lors de la conception du pipeline mathématique de SYNTH : les humains (et les modèles correctement guidés) peuvent identifier les raisonnements fallacieux sans avoir besoin de consulter les résultats finaux. L'article mentionne également une technique qui devrait se généraliser dans les pipelines de synthèse : les « méta-vérificateurs », qui consistent essentiellement à évaluer le processus d'évaluation lui-même. En effet, même le vérificateur peut être victime de piratage du système de récompenses : « lors de l'évaluation de preuves erronées (où 𝑠𝑖 < 1) pendant l'entraînement, le vérificateur peut recevoir la récompense complète en prédisant les scores corrects tout en imaginant des problèmes inexistants ». Les annotations humaines sont d'abord réalisées sur des ébauches synthétiques, puis servent à construire des évaluateurs qui produisent de manière itérative de meilleures preuves et des chemins de résolution toujours plus performants. Globalement, le processus crée une boucle de rétroaction positive : « Le vérificateur et le générateur de preuves créent un cycle synergique : le vérificateur améliore le générateur, et à mesure que le générateur s'améliore, il produit de nouvelles preuves qui mettent à l'épreuve les capacités actuelles du vérificateur. » L'entraînement de tous les vérificateurs, méta-vérificateurs et du modèle final est réalisé par apprentissage par renforcement (ce qui est judicieux pour les très grands modèles, car les méthodes SFT et midtrain peuvent s'avérer très destructives). Cependant, même dans ce cas, la complexité croissante de l'apprentissage par renforcement et de la vérification (RLVR), qui ne peut se limiter à une simple « vérification » formelle, exige le développement de pipelines synthétiques intégrés et de plus en plus autonomes. Une fois de plus, les démonstrateurs mathématiques amènent la recherche LLM à la frontière même du domaine et aboutissent à une solution créative et élégante qui est susceptible d'irriguer l'ensemble du domaine dans les mois à venir.