MUSTARDSAUCE Mathematisches Theoremproblem Datensatz

Forscher der City University of Hong Kong, der Sun Yat-sen University, des Huawei Noah's Ark Lab und anderer Institutionen haben ein einheitliches Framework zur Datensynthese für mathematisches Denken namens MUSTARD vorgeschlagen, das große Mengen qualitativ hochwertiger Daten zum mathematischen Denken generieren kann, die korrekt, für Menschen lesbar und verständlich sind.Dieser Datensatz ist der Open-Source-MUSTARDSAUCE-Datensatz für die Forschung.Jeder dieser Datensätze enthält die Problembeschreibung und die mehrstufige Lösung in natürlicher Sprache sowie die Problembeschreibung und die mehrstufige Lösung in der dualen formalen Sprache Lean 3. Die MUSTARDSAUCE-Daten umfassen mathematische Textaufgaben und Theorembeweisprobleme und decken Schwierigkeitsgrade von der Grundschule bis zur Hochschulbildung ab. Die Anzahl der Denkschritte in einer Frage steigt mit zunehmender Schwierigkeit der Frage. Zur Lösung des schwierigsten Problems sind etwa 30 Schritte und etwa 20 Lean 3-Taktiken erforderlich.