ICLR 2024 Spotlight |. Sie müssen sich keine Gedanken über Zwischenschritte machen, MUSTARD kann hochwertige mathematische Inferenzdaten generieren

Die AIxiv-Kolumne ist eine Kolumne, in der akademische und technische Inhalte auf dieser Website veröffentlicht werden. In den letzten Jahren sind in der AIxiv-Kolumne dieser Website mehr als 2.000 Berichte eingegangen, die Spitzenlabore großer Universitäten und Unternehmen auf der ganzen Welt abdecken und so den akademischen Austausch und die Verbreitung wirksam fördern. Wenn Sie hervorragende Arbeiten haben, die Sie teilen möchten, können Sie gerne einen Beitrag leisten oder uns für die Berichterstattung kontaktieren. E-Mail-Adresse: liyazhou@jiqizhixin.com; zhaoyunfeng@jiqizhixin.com.

In den letzten Jahren haben große Sprachmodelle (LLM) große Fortschritte bei Aufgaben wie mathematischen Anwendungsproblemen und dem Beweis mathematischer Theoreme gemacht. Mathematische Argumentation erfordert einen strengen, formalisierten mehrstufigen Argumentationsprozess und ist daher ein wichtiger Meilenstein bei der Weiterentwicklung der Argumentationsfähigkeiten von LLMs, steht jedoch noch vor großen Herausforderungen.

Frühere Forschungsarbeiten wie Chain of Thoughts (CoT) haben die Wirksamkeit von ZwischenschrittenAnleitung gezeigt. Das manuelle Annotieren solcher Zwischenschritte erfordert jedoch viel Personal und Zeitaufwand, und automatisch synthetisierte Daten sind auch anfällig für Probleme in Bezug auf Richtigkeit und menschliche Lesbarkeit.

In diesem Artikel schlagen Forscher der City University of Hong Kong, der Sun Yat-sen University, des Huawei Noah's Ark Laboratory und anderer Institutionen ein einheitliches Datensynthese-Framework für mathematisches Denken MUSTARD vor, das eine große Anzahl korrekter Daten generieren kann und vom Menschen lesbare und verständliche, qualitativ hochwertige mathematische Argumentationsdaten.

• Papiertitel: MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
• Papierlink: https://openreview.net/forum?id=8xliOUg9EW
• Code-Link: https:/ // /github.com/Eleanor-H/MUSTARD
• Datensatz-Link: https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view
• Homepage des Autors: https://eleanor - h.github.io/

Ein hochwertiges Datensynthese-Framework unter Verwendung formaler Prüfer

MUSTARD-Framework besteht aus drei Phasen:

Phase 1, Konzepterwerb : Zunächst wird eine mathematische Konzeptbibliothek definiert und erstellt, die Konzepte in den vier Bildungsstufen Grundschule, Mittelschule, Oberstufe und Hochschulbildung abdeckt. Jede Bildungsstufe umfasst 5 bis 9 mathematische Bereiche, die verschiedene Arten mathematischer Probleme abdecken als Algebra und Geometrie. Jeder Bereich enthält aufgeschlüsselte mathematische Konzepte wie Polynomoperationen oder Faktorisierung. Anschließend werden ein oder mehrere mathematische Konzepte aus der Bibliothek mathematischer Konzepte als Seeds extrahiert, um die generierten Fragekategorien zu spezifizieren.

Die zweite Stufe, Datengenerierung: Veranlassen Sie große Sprachmodelle, mathematische Probleme und mehrstufige Lösungsprozesse basierend auf mathematischen Konzepten zu generieren. Insbesondere nutzt MUSTARD die Fähigkeit großer Sprachmodelle, natürliche Sprache und Code zu generieren, und veranlasst große Sprachmodelle, drei Aufgaben zu erfüllen: (T1) Generieren Sie mathematische Probleme im Zusammenhang mit einem bestimmten Konzept (T2) Geben Sie Lösungen für die Probleme in natürlicher Sprache; (T3) Automatische Formalisierung, Umwandlung einer Lösung in natürlicher Sprache in eine formale Lean-3-Lösung.

Die dritte Stufe, Formale Verifizierung: Verwenden Sie die Verifizierung des interaktiven formalen Theorembeweisers, um den genauen Lösungsprozess herauszufiltern. Nachdem MUSTARD die formale Lösung von Lean 3 an den Lean-Formalprüfer übermittelt hat und der Theoremprüfer keine Fehlerinformationen zurückgibt, werden die entsprechenden Daten im gültigen Satz gesammelt. Andernfalls sammelt MUSTARD Fehlermeldungen vom Theorembeweis und fordert das Sprachmodell auf, die formale Lösung zu ändern. MUSTARD führt mehrere Verifizierungs- und Selbstkorrekturrunden durch, bis eine gültige formale Lösung vorliegt. Das MUSTARD-Framework besteht aus drei Phasen: Konzepterhebung, Datengenerierung und formale Verifizierung.

Menschliche Bewertung der Datenqualität

Um die Qualität der von MUSTARD generierten Daten zu untersuchen, bat das Forschungsteam Fachleute mit Kenntnissen in Mathematik und Lean 3-Sprache, eine Qualitätsprüfung durchzuführen auf die Daten. Sie wählten zufällig 200 Elemente aus den generierten Daten aus, von denen 100 Elemente die Überprüfung durch den Lean-Theorem-Beweis bestanden (gültige Gruppe) und 100 Elemente die Überprüfung nicht bestanden (ungültige Gruppe). Die Qualitätsprüfung umfasst vier Teile jedes Datenelements (d. h. Problembeschreibung in natürlicher Sprache, Lösung in natürlicher Sprache, formale Problembeschreibung und formale Lösung), einschließlich Prüfungen auf Richtigkeit und Konsistenz. Insbesondere sollten qualitativ hochwertige Daten eine korrekte Problembeschreibung in natürlicher Sprache (D1) und eine korrekte Problemlösung (D4) aufweisen. Die formale Problembeschreibung und -lösung sollte mit der Problembeschreibung und -lösung in natürlicher Sprache übereinstimmen (D5, D6). Darüber hinaus sollten die Daten den vorgegebenen mathematischen Konzepten (D2) und Problemtypen (D3) entsprechen. Tabelle 3 zeigt diese sechs Inspektionsmaße und -anforderungen. Wenn die Daten die Anforderungen erfüllen, erhalten sie in der Dimension eine Bewertung von 1, andernfalls erhalten sie eine Bewertung von 0.

Tabelle 3 zeigt die Genauigkeit und den entsprechenden p-Wert der effektiven Gruppe und der ungültigen Gruppe in jeder Dimension. Der signifikante Unterschied zwischen (D1) und (D4) verdeutlicht die Richtigkeit der von MUSTARD generierten Fragen und Antworten. Der signifikante Unterschied in (D6) weist auf die hohe Konsistenz zwischen der Beschreibung in natürlicher Sprache und der formalen Beschreibung der generierten Daten hin.

Wirksamkeit von Daten auf die mathematische Denkfähigkeit des Modells

Um den Einfluss von MUSTARDSAUCE auf die Verbesserung der mathematischen Denkfähigkeit zu bewerten, nutzte das Forschungsteam diese Daten zur Feinabstimmung einer kleineren Sprache modelliert und durchgeführt. Es wird anhand mathematischer Wortprobleme (MWP) und automatischer Theoremprüfung (ATP) bewertet. In diesem Artikel wird die Wirksamkeit der folgenden kombinierten Daten des MUSTARDSAUCE-Datensatzes verglichen:

• MUSTARDSAUCE-gültig: 5866 vom Lean-Formalprüfer verifizierte Daten;
• MUSTARDSAUCE-ungültig: Lean konnte nicht bestanden werden 5866 vom formalen Prüfer verifizierte Daten;
• MUSTARDSAUCE-random: 5866 zufällige Daten;
• MUSTARDSAUCE-tt: alle 28316 von MUSTARD generierten Daten.

Das Forschungsteam hat LoRA [1] übernommen, um die Open-Source-Daten GPT2-large [2], Llama 2-7B und Llama 2-70B [3] für die einzelnen kombinierten Daten zu optimieren. Für mathematische Textaufgaben nutzten sie zur Auswertung die Datensätze GSM8K [4] und MATH [5][6]. Bei der Evaluierung automatisierter Theorembeweise verwendete das Forschungsteam die Benchmarks Mathlib [8] und miniF2F [7]. Darüber hinaus wurden sie auch im MUSTARDSAUCE-Test bewertet.

Im Allgemeinen verbessert die Feinabstimmung des Modells auf MUSTARDSAUCE die mathematischen Denkfähigkeiten des Modells. Bei der automatischen Theoremprüfung (Tabelle 5 unten) und der Lösung mathematischer Anwendungsprobleme (Tabelle 4 unten) stieg die durchschnittliche relative Leistung bei Verwendung von MUSTARDSAUCE-valid zur Feinabstimmung im Vergleich zur Verwendung von MUSTARDSAUCE-random zur Feinabstimmung um 18,15 % (Tabelle 5). unten) und 11,01 % % (Tabelle 4 unten).

Für den automatischen Theorembeweis beträgt die durchschnittliche Leistungsverbesserung des fein abgestimmten Llama 2-7B 15,41 % und die durchschnittliche Leistungsverbesserung des fein abgestimmten GPT 2-large beträgt 20,89 %.

Bei der Lösung mathematischer Anwendungsprobleme wird die durchschnittliche Leistung des fein abgestimmten Llama 2-7B um 8,18 % und die durchschnittliche Leistung des fein abgestimmten GPT 2-large um 15,41 % verbessert. Obwohl das mit MUSTARDSAUCE-tt fein abgestimmte Modell einen absoluten Vorteil hinsichtlich der Menge an fein abgestimmten Daten hat, ist seine Leistung nicht so gut wie die des mit MUSTARDSAUCE-valid fein abgestimmten Modells. Weitere Ergebnisse für

Lama 2-70B. Die MUSTARDSAUCE-Daten bleiben bei der Feinabstimmung größerer Sprachmodelle gültig.

MUSTARDSAUCE-Datensatz

Dieser Artikel ist eine Open-Source-Quelle für den MUSTARDSAUCE-Datensatz. Jede der Daten enthält eine Problembeschreibung und eine mehrstufige Lösung in natürlicher Sprache sowie eine Problembeschreibung und eine mehrstufige Lösung in der dualen formalen Sprache Lean 3. Die Daten von MUSTARDSAUCE umfassen mathematische Anwendungsfragen und Theorembeweisfragen, die Schwierigkeitsgrade von der Grundschule bis zur Hochschulbildung abdecken. Die Anzahl der Argumentationsschritte für eine Frage steigt mit der Schwierigkeit der Frage. Die Lösung der schwierigsten Fragen erfordert etwa 30 Schritte und etwa 20 Lean-3-Taktiken.

Datensatz-Download: https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view

Automatische Formalisierungs-/Informalisierungsherausforderung

Recherche Das Team hat auch eine eröffnet automatische Formalisierung (Autoformalisierung) und eine automatische Informalisierung (Autoinformalisierung)-Herausforderung basierend auf den dualen Daten der natürlichen Sprache und der Lean-Formalsprache im MUSTARDSAUCE-Datensatz. Darüber hinaus hat das Forschungsteam gleichzeitig zwei Herausforderungspfade eröffnet: automatisierte Theoremgenerierung und -beweis sowie codegestützte automatisierte Optimierungsproblemlösung mit Code. Der Wettbewerb findet vom 3. April bis 27. Mai 2024 statt. Das Gewinnerteam hat die Möglichkeit, am ICML 2024 AI for Math Workshop am 26. Juli in Wien, Österreich, teilzunehmen.

• Track 1-1 (automatische Formalisierung): https://www.codabench.org/competitions/2436/
• Track 1-2 (automatische Informalisierung): https://www.codabench .org/competitions/2484/
• Track 2 (automatische Theoremgenerierung und -beweis): https://www.codabench.org/competitions/2437/
• Track 3 (codegestützte automatische Lösung der Operations-Research-Optimierung Probleme): https://www.codabench.org/competitions/2438/

^Referenzen:

^{[1] Edward J Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen- Zhu, Yuanzhi Li, Shean Wang, Lu Wang und Weizhu Chen: Low-Rank-Adaption großer Sprachmodelle arXiv:2106.09685, 2021.}

^{[2] Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al. Sprachmodelle sind unbeaufsichtigte Multitasking-Lernende, 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, Aure ́lien Rodriguez, Robert Stojnic , Sergey Edunov und Thomas Scialom. Offene Grundlage und fein abgestimmte Chat-Modelle .}

^{[4] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse und John Schulman Lösen Sie mathematische Textaufgaben. CoRR, abs/2110.14168, 2021 Lösen mit dem MATH-Datensatz. In Joaquin Vanschoren und Sai-Kit Yeung (Hrsg.), Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets and Benchmarks 2021, Dezember 2021, virtuell, 2021.}

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

^{[7] Kunhao Zheng, Jesse Michael Han und Stanislas Polu: ein systemübergreifender Benchmark für formale Mathematik auf Olympianiveau, ICLR 2022, virtuell Veranstaltung, 25.–29. April 2022. OpenReview.net, 2022.}

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

Das obige ist der detaillierte Inhalt vonICLR 2024 Spotlight |. Sie müssen sich keine Gedanken über Zwischenschritte machen, MUSTARD kann hochwertige mathematische Inferenzdaten generieren. Für weitere Informationen folgen Sie bitte anderen verwandten Artikeln auf der PHP chinesischen Website!