مجموعة بيانات مشكلة نظرية صلصة الخردل الرياضية

اقترح باحثون من جامعة مدينة هونج كونج وجامعة صن يات صن ومختبر هواوي نوح آرك ومؤسسات أخرى إطار عمل موحد لتجميع بيانات التفكير الرياضي يسمى MUSTARD، والذي يمكنه توليد كميات كبيرة من بيانات التفكير الرياضي عالية الجودة الصحيحة والقابلة للقراءة والفهم من قبل الإنسان.تعتبر مجموعة البيانات هذه مجموعة بيانات مفتوحة المصدر لـ MUSTARDSAUCE لأغراض البحث.تحتوي كل من هذه البيانات على وصف للمشكلة وحل متعدد الخطوات باللغة الطبيعية، بالإضافة إلى وصف للمشكلة وحل متعدد الخطوات باللغة الرسمية المزدوجة Lean 3. تتضمن بيانات MUSTARDSAUCE مسائل كلمات الرياضيات ومسائل إثبات النظرية، والتي تغطي مستويات الصعوبة من المدرسة الابتدائية إلى التعليم العالي. يزداد عدد خطوات التفكير في السؤال مع زيادة صعوبة السؤال. تتطلب المشكلة الأصعب حوالي 30 خطوة لحلها، أي حوالي 20 تكتيكًا من تكتيكات Lean 3.