ICLR 2024 Spotlight | Pas besoin de vous soucier des étapes intermédiaires, MUSTARD peut générer des données d'inférence mathématique de haute qualité

La rubrique AIxiv est une rubrique où des contenus académiques et techniques sont publiés sur ce site. Au cours des dernières années, la rubrique AIxiv de ce site a reçu plus de 2 000 rapports, couvrant les meilleurs laboratoires des principales universités et entreprises du monde entier, favorisant efficacement les échanges et la diffusion académiques. Si vous souhaitez partager un excellent travail, n'hésitez pas à contribuer ou à nous contacter pour un rapport. Courriel de soumission : liyazhou@jiqizhixin.com ; zhaoyunfeng@jiqizhixin.com.

Ces dernières années, les grands modèles de langage (LLM) ont fait de grands progrès dans des tâches telles que les problèmes d'application mathématique et la démonstration de théorèmes mathématiques. Le raisonnement mathématique nécessite un processus de raisonnement rigoureux et formalisé en plusieurs étapes et constitue donc une étape clé dans l'avancement des capacités de raisonnement des LLM, mais il reste confronté à des défis importants.

Des travaux de recherche antérieurs, tels que Chain of Thoughts (CoT), ont révélé l'efficacité des étapes intermédiaires de l'orientation. Cependant, l'annotation manuelle de telles étapes intermédiaires nécessite beaucoup de main d'œuvre et de temps, et les données synthétisées automatiquement sont également sujettes à des problèmes d'exactitude et de lisibilité humaine.

Dans cet article, des chercheurs de la City University of Hong Kong, de l'Université Sun Yat-sen, du Huawei Noah's Ark Laboratory et d'autres institutions proposent un cadre unifié de synthèse de données de raisonnement mathématique MUSTARD, qui peut générer un grand nombre de bonnes et des données de raisonnement mathématique de haute qualité, lisibles et compréhensibles par l'homme.

• Titre de l'article : MOUTARDE : Maîtriser la synthèse uniforme du théorème et des données de preuve
• Lien de l'article : https://openreview.net/forum?id=8xliOUg9EW
• Lien du code : https:/ // /github.com/Eleanor-H/MUSTARD
• Lien de l'ensemble de données : https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view
• Page d'accueil de l'auteur : https://eleanor - h.github.io/

Un cadre de synthèse de données de haute qualité utilisant des prouveurs formels

Le cadre MUSTARD se compose de trois phases :

Phase 1, Acquisition de concepts : Premièrement, une bibliothèque de concepts mathématiques est définie et établie, couvrant les concepts des quatre niveaux éducatifs de l'école primaire, du collège, du lycée et de l'enseignement supérieur. Chaque niveau éducatif comprend 5 à 9 domaines mathématiques, couvrant différents types de problèmes mathématiques tels que. comme l'algèbre et la géométrie. Chaque zone contient des concepts mathématiques décomposés, tels que les opérations polynomiales ou la factorisation. Ensuite, un ou plusieurs concepts mathématiques sont extraits de la bibliothèque de concepts mathématiques en tant que valeurs initiales pour spécifier les catégories de questions générées.

La deuxième étape, génération de données : inviter de grands modèles de langage à générer des problèmes mathématiques et des processus de solution en plusieurs étapes basés sur des concepts mathématiques. Plus précisément, MUSTARD exploite la capacité des grands modèles de langage à générer du langage naturel et du code, incitant les grands modèles de langage à accomplir trois tâches : (T1) Générer des problèmes mathématiques liés à un concept donné (T2) Donner des solutions aux problèmes en langage naturel ; (T3) Formalisation automatique, conversion d'une solution en langage naturel en solution formelle Lean 3.

La troisième étape, Vérification formelle : utilisez la vérification du prouveur formel interactif du théorème pour filtrer le processus de solution précis. Une fois que MUSTARD a livré la solution formelle de Lean 3 au vérificateur formel Lean, si le prouveur de théorème ne renvoie pas d'informations d'erreur, les données correspondantes seront collectées dans l'ensemble valide. Sinon, MUSTARD collecte les messages d'erreur du prouveur de théorème et invite le modèle de langage à modifier la solution formelle. MUSTARD effectue plusieurs cycles de vérification et d'autocorrection jusqu'à ce qu'une solution formelle valide soit obtenue. Le cadre MUSTARD comprend trois étapes : la collecte de concepts, la génération de données et la vérification formelle.

Évaluation humaine de la qualité des données

Afin d'explorer la qualité des données générées par MUSTARD, l'équipe de recherche a demandé à des professionnels maîtrisant les mathématiques et le langage Lean 3 d'effectuer un contrôle qualité sur les données. Ils ont sélectionné au hasard 200 éléments à partir des données générées, parmi lesquels 100 éléments ont réussi la vérification du prouveur du théorème Lean (groupe valide) et 100 éléments n'ont pas réussi la vérification (groupe invalide). Le contrôle de qualité couvre quatre parties de chaque élément de données (c'est-à-dire la description du problème en langage naturel, la solution en langage naturel, la description formelle du problème et la solution formelle), y compris les contrôles d'exactitude et de cohérence. Plus précisément, les données de haute qualité doivent avoir une description correcte du problème en langage naturel (D1) et une résolution correcte du problème (D4). La description formelle du problème et sa solution doivent être cohérentes avec la description et la solution du problème en langage naturel (D5, D6). De plus, les données doivent être conformes aux concepts mathématiques spécifiés (D2) et aux types de problèmes (D3). Le tableau 3 présente ces six dimensions et exigences d’inspection. Si les données répondent aux exigences, elles obtiennent un score de 1 dans la dimension, sinon elles obtiennent un score de 0.

Le tableau 3 montre la précision et la valeur p correspondante du groupe effectif et du groupe invalide dans chaque dimension. La différence significative entre (D1) et (D4) illustre l'exactitude des questions et réponses générées par MUSTARD. La différence significative en (D6) indique la grande cohérence entre la description en langage naturel et la description formelle des données générées.

Efficacité des données sur la capacité de raisonnement mathématique du modèle

Pour évaluer l'impact de MUSTARDSAUCE sur l'amélioration de la capacité de raisonnement mathématique, l'équipe de recherche a utilisé ces données pour affiner un langage à plus petite échelle modèle et réalisé Il est évalué sur les problèmes de mots mathématiques (MWP) et la preuve automatique du théorème (ATP). Cet article compare l'efficacité des données combinées suivantes de l'ensemble de données MUSTARDSAUCE :

• MUSTARDSAUCE-valid : 5866 éléments de données vérifiés par le prouveur formel Lean
• MUSTARDSAUCE-invalid : échec de la réussite du Lean ; 5866 éléments de données vérifiés par le prouveur formel ;
• MUSTARDSAUCE-random : 5866 éléments de données aléatoires 
• MUSTARDSAUCE-tt : les 28 316 éléments de données générés par MUSTARD.

L'équipe de recherche utilise LoRA [1] pour affiner les logiciels open source GPT2-large [2], Llama 2-7B et Llama 2-70B [3] sur chaque donnée combinée. Pour les tâches de problèmes de mots mathématiques, ils ont utilisé les ensembles de données GSM8K [4] et MATH [5][6] pour l'évaluation. Lors de l’évaluation de la preuve automatisée des théorèmes, l’équipe de recherche a utilisé les benchmarks Mathlib [8] et miniF2F [7]. En outre, ils ont également été évalués selon le test MUSTARDSAUCE.

En général, affiner le modèle sur MUSTARDSAUCE améliore les capacités de raisonnement mathématique du modèle. Dans la démonstration automatique de théorèmes (tableau 5 ci-dessous) et la résolution de problèmes d'application mathématique (tableau 4 ci-dessous), en utilisant MUSTARDSAUCE-valid pour le réglage fin par rapport à l'utilisation de MUSTARDSAUCE-random pour le réglage fin, la performance relative moyenne a augmenté de 18,15 % (tableau 5). ci-dessous) et 11,01% % (tableau 4 ci-dessous).

Pour la preuve automatique du théorème, l'amélioration moyenne des performances du Llama 2-7B affiné est de 15,41 %, et l'amélioration moyenne des performances du GPT 2-large affiné est de 20,89 %.

Pour résoudre des problèmes d'application mathématiques, les performances moyennes du Llama 2-7B affiné sont améliorées de 8,18 %, et les performances moyennes du GPT 2-large affiné sont améliorées de 15,41 %. De plus, bien que le modèle affiné avec MUSTARDSAUCE-tt ait un avantage absolu en termes de quantité de données affinées, ses performances ne sont pas aussi bonnes que le modèle affiné avec MUSTARDSAUCE-valid. Plus de résultats pour

Llama 2-70B. Les données MUSTARDSAUCE restent valides lors du réglage fin de modèles de langage plus grands.

Ensemble de données MUSTARDSAUCE

Cet article a open source l'ensemble de données MUSTARDSAUCE. Chacune des données contient une description du problème et une solution en plusieurs étapes en langage naturel, ainsi qu'une description du problème et une solution en plusieurs étapes dans le double langage formel Lean 3. Les données de MUSTARDSAUCE comprennent des questions d'application mathématique et des questions de démonstration de théorèmes, couvrant les niveaux de difficulté de l'école primaire à l'enseignement supérieur. Le nombre d’étapes de raisonnement pour une question augmente avec la difficulté de la question. Les questions les plus difficiles nécessitent environ 30 étapes à résoudre et environ 20 tactiques Lean 3.

Téléchargement de l'ensemble de données : https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view

Défi de formalisation/informalisation automatique

Recherche L'équipe a également ouvert un une formalisation automatique (autoformalisation) et un défi d'informalisation automatique (auto-informalisation) basés sur les données doubles du langage naturel et du langage formel Lean dans l'ensemble de données MUSTARDSAUCE. De plus, l'équipe de recherche a simultanément ouvert deux pistes de défis : la génération et la preuve automatisées de théorèmes et la résolution de problèmes d'optimisation automatisée assistée par code avec du code. Le concours se déroule du 3 avril au 27 mai 2024. L'équipe gagnante aura l'opportunité de participer à l'atelier ICML 2024 AI for Math le 26 juillet à Vienne, en Autriche.

• Track 1-1 (formalisation automatique) : https://www.codabench.org/competitions/2436/
• Track 1-2 (informalisation automatique) : https://www.codabench .org/competitions/2484/
• Track 2 (génération et preuve automatiques de théorèmes) : https://www.codabench.org/competitions/2437/
• Track 3 (code Solution automatique assistée d'optimisation de la recherche opérationnelle problèmes) : https://www.codabench.org/competitions/2438/

^{Références :}

^{[1] Edward J Hu, Yelong Shen , Phillip Wallis, Zeyuan Allen- Zhu, Yuanzhi Li, Shean Wang, Lu Wang et Weizhu Chen : adaptation de bas rang de grands modèles de langage arXiv arXiv :2106.09685, 2021.}

^{[2] Alec Radford, Jeffrey Wu, Rewon. Child, David Luan, Dario Amodei, Ilya Sutskever et al. Les modèles de langage sont des apprenants multitâches non supervisés, 1 (8): 9, 2019.}

^{[3] Hugo Touvron, Louis Martin, Kevin Stone. , Peter Albert, Amjad Almahairi, Yasmine Babaei, Niko-lay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, Dan Bikel, Lukas Blecher, Cristian Canton-Ferrer, Moya Chen, Guillem Cucurull, David Esiobu, Jude Fernandes, Jeremy Fu, Wenyin Fu, Brian Fuller, Cynthia Gao, Vedanuj Goswami, Naman Goyal, Anthony Hartshorn, Saghar Hosseini, Rui Hou, Hakan Inan, Marcin Kardas, Viktor Kerkez, Madian Khabsa, Isabel Kloumann, Artem Korenev, Punit Singh Koura, Marie-Anne Lachaux , Thibaut Lavril, Jenya Lee, Diana Liskovich, Yinghai Lu, Yuning Mao, Xavier Martinet, Todor Mihaylov, Pushkar Mishra, Igor Molybog, Yixin Nie, Andrew Poulton, Jeremy Reizenstein, Rashi Rungta, Kalyan Saladi, Alan Schelten, Ruan Silva, Eric Michael Smith, Ranjan Subramanian, Xiaoqing Ellen Tan, Binh Tang, Ross Taylor, Adina Williams, Jian Xiang Kuan, Puxin Xu, Zheng Yan, Iliyan Zarov, Yuchen Zhang, Angela Fan, Melanie Kambadur, Sharan Narang, Aurelien Rodriguez, Robert Stojnic , Sergey Edunov et Thomas Scialom 2 : Fondation ouverte et modèles de discussion affinés, abs/2307.09288, 2023. doi : 10.48550/arXiv.2307.09288. .}

^{[4] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse et John Schulman Formation des vérificateurs. résoudre des problèmes de mots mathématiques, abs/2110.14168, 2021.}

^{[5] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song et Jacob Steinhardt Mesurer un problème mathématique. résolution avec l'ensemble de données MATH. Dans Joaquin Vanschoren et Sai-Kit Yeung (éd.), Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets and Benchmarks 2021, décembre 2021, virtuel, 2021.}

^{[6] Hunter Lightman, Vineet Kosaraju, Yura Burda, Harri Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever et Karl Cobbe. Vérifions étape par étape. .}

^{[7] Kunhao Zheng, Jesse Michael Han et Stanislas Polu : une référence intersystème pour les mathématiques formelles au niveau des Olympiades, ICLR 2022, virtuelle. Événement, 25-29 avril 2022. OpenReview.net, 2022.}

^{[8] https://github.com/leanprover-community/mathlib}

Ce qui précède est le contenu détaillé de. pour plus d'informations, suivez d'autres articles connexes sur le site Web de PHP en chinois!