LeanPRM: Lean يوسم 152 ألف خطوة برهان دون بشر ويرفع الدقة إلى 74,7%

أصبح التحقق من البراهين الرياضية الطويلة التي تكتبها النماذج اللغوية عنق زجاجة. يقترح مؤلفو LeanPRM الحصول على وسم لكل خطوة من مساعد البراهين Lean، دون مُعلِّقين. والنتيجة مجموعة بيانات من 10 634 براهين و152 ألف خطوة موسومة. رفع مُتحقِّق مبني على Qwen3-4B ومدرَّب عليها نسبة المطابقة لتسمية الخطوة على المجموعة المستقلة LeanPRM-Bench (200 برهان) من 48,2 إلى 74,7. أما النموذج الأساسي نفسه المدرَّب على PRM800K فسجّل 60,3.

من أين تأتي التسميات

لا يمكن تدريب مُتحقِّق إجرائي (PRM) إلا على بيانات تحمل كل خطوة فيها تقييماً بـ«صحيح» أو «خاطئ». ويصعب الحصول على هذه التسميات للبراهين المفتوحة. فالمُوسِّمون البشر مكلفون. ولا تفيد التسميات المستمدة من الإجابة النهائية، لأن البرهان لا يحتوي على رقم يمكن مطابقة النتيجة معه. كما أن إضفاء الصيغة الشكلية على كل برهان في Lean يتطلب جهد خبراء.

يتجاوز LeanPRM هذه القيود على النحو التالي. يكتب النموذج برهاناً بلغة طبيعية وبرهاناً شكلياً موازياً له، من دون تغذية راجعة من Lean. ثم يتحقق Lean من النسخة الشكلية ويضع تسمية لكل خطوة. ويستبعد نموذج ثانٍ الحالات التي يكون الإخفاق فيها ناجماً عن صياغة النص الشكلي وحدها. وبعد ذلك تعكس التسميات السلبية أخطاء رياضية فعلية، لا هفوات في الكتابة.

ماذا أظهرت الأرقام

أبرز النتائج الواردة في الدراسة:

• مجموعة البيانات: 10 634 براهين، و152 ألف خطوة موسومة، دون وسم يدوي؛
• LeanPRM-Bench (200 برهان مستقل): ارتفعت مطابقة Qwen3-4B لتسميات الخطوات من 48,2 إلى 74,7؛
• خط الأساس PRM800K على النموذج نفسه: 60,3؛
• في ثلاثة من أربعة مقاييس خارجية، يتفوق المُتحقِّق المدرَّب على LeanPRM على النسخة المدرَّبة على PRM800K؛
• في اختيار best-of-N على مسائل بمستوى IMO، يختار براهين أعلى جودة؛
• تأكد التحسن على نماذج من 0,6B إلى 8B معامل على LeanPRM-Bench وHard2Verify وIMO-GradingBench.

وثبات الأثر عبر الأحجام لا يقل أهمية عن الرقم القياسي. فالتحسن ظاهر في النموذج الصغير جداً وفي النموذج ذي 8 مليارات معامل. وهذا يعني أن السبب جودة الإشارة، لا حسن اختيار إعداد واحد.

أين يجدر التدقيق

الفجوة الرئيسة، 48,2 مقابل 74,7، قيست على مقياس بناه المؤلفون أنفسهم، وبإجراءات التوليد والوسم نفسها. وفي عيّنة كهذه يتمتع التدريب على LeanPRM بأفضلية طبيعية. لذلك تبدو الاختبارات الخارجية أكثر قيمة، لكن التفوق فيها حاصل في ثلاثة مقاييس من أربعة، أي ليس في كلها. ولا يوضح الوصف المتاح للدراسة النتيجة على المقياس الرابع، ويُستحسن التحقق منها في النص الكامل.

ثمة أيضاً قيد بنيوي. فصحة التسميات تساوي مدى مطابقة البرهان الشكلي للبرهان بلغة طبيعية. وإذا كتب النموذج نسخة شكلية تختلف عن النص، فسيقيّم Lean شيئاً غير ما يقرؤه الإنسان. ويقلل مرشِّح النموذج الثاني خطر الضوضاء الناجمة عن الصياغة، لكنه لا يضمن تطابقاً كاملاً بين النسختين. والتغطية محدودة كذلك: لا يمكن وسم إلا ما أمكن تحويله إلى صيغة شكلية.

وتكمن القيمة العملية في قابلية التوسع. فحجم البيانات ينمو مع عدد العبارات الشكلية المتاحة، لا مع ميزانية الخبراء. وبالنسبة إلى الفرق التي تدرّب نماذج رياضية باستخدام best-of-N أو RL مع مكافآت إجرائية، فهذه فرصة للحصول على إشارة كثيفة على مستوى خطوات الاستدلال دون شراء خدمات وسم. ولتقييم المنهج، يُستحسن اختبار المُتحقِّق الخاص بكم على Hard2Verify وIMO-GradingBench. ومن المفيد أيضاً التحقق من مدى بقاء المكسب على براهين بعيدة عن المجالات المُصاغة شكلياً في Lean.