نظام Seed-Prover: ثورة في برهنة النظريات الرياضية من بايتدانس
أحدثت نماذج اللغات الكبيرة (LLMs) تحسناً ملحوظاً في مجال الاستدلال الرياضي من خلال توسيع قدراتها عبر اللغة الطبيعية، مما أدى إلى تحقيق مكاسب في الأداء على معايير قياسية مثل MATH و AIME. ومع ذلك، تواجه عملية التعلم المعزز (RL) المستخدمة في تدريب هذه النماذج تحدياً رئيسياً: صعوبة التحقق من صحة البرهان المكتوب باللغة الطبيعية، حيث يتطلب ذلك فحصاً يدوياً دقيقاً لكل خطوة من خطوات الاستدلال. يحد هذا من تطبيق التعلم المعزز في تدريب نماذج برهنة النظريات الرياضية. وبينما توفر اللغات الرسمية مثل Lean التحقق التلقائي من الصحة، إلا أن برامج البرهنة الرسمية الحالية القائمة على نماذج اللغات الكبيرة تواجه قيودها الخاصة.
Seed-Prover: نهج جديد قائم على البرهان باستخدام المعادلات
يقدم فريق Seed في بايتدانس نظام Seed-Prover، وهو نموذج استدلال قائم على أسلوب المعادلات (Lemmas) لإثبات النظريات الرياضية كاملة. يعمل النظام على صقل البرهان بشكل متكرر باستخدام ملاحظات من Lean، والمعادلات التي تم إثباتها سابقاً، والتلخيص الذاتي. يستخدم Seed-Prover ثلاث استراتيجيات استنتاجية متخصصة في وقت الاختبار، مما يسمح له بتطبيق طرق استدلال عميقة وواسعة النطاق لحل مسائل رياضية على مستوى أولمبياد الرياضيات الدولية (IMO). يكمن الابتكار الرئيسي في اعتماد أسلوب البرهان القائم على المعادلات كطريقة أساسية، حيث يتم وضع المعادلات في قلب عملية الاستدلال بدلاً من الاعتماد على الأساليب التقليدية خطوة بخطوة أو توليد البرهان كاملاً.
Seed-Geometry: محرك هندسي مكمل
بالإضافة إلى ذلك، يقدم هذا البحث Seed-Geometry، وهو محرك استدلال هندسي مكمل يتغلب على قيود Lean في التعامل مع الدعم الهندسي. يتم استخدام التعلم المعزز متعدد المراحل والمتعدد المهام القائم على VAPO للتفاعل بين Seed-Prover و Lean.
بيانات التدريب واستراتيجيات الاستنتاج
تجمع مجموعة بيانات التدريب بين مجموعات البيانات مفتوحة المصدر والمشاكل الرسمية الداخلية، باستخدام مُقترح لإنشاء متغيرات أبسط للمهام الصعبة. يستبعد النظام المسائل البسيطة للغاية التي تتجاوز نسبة إثباتها 25%. يدعم الواجهة الخلفية لـ Seed-Geometry إنشاء مشكلات على نطاق واسع، حيث قام بتحديد أكثر من 230 مليون مشكلة فريدة على مدى سبعة أيام مع تحسين كفاءة البحث بمقدار ثمانية أضعاف.
تم تدريب نموذج منفصل للسياسة والقيمة، على الرغم من أن الاختبارات المكثفة أظهرت أن نماذج القيمة قد تقلل من الأداء بسبب أخطاء التقدير. ونتيجة لذلك، تم اعتماد توليد خطوة بخطوة مع بحث شعاعي في الإعدادات الموزعة.
الأداء على معايير قياسية مختلفة
حقق Seed-Prover نتائج متقدمة على معايير قياسية رياضية متعددة:
- أولمبياد الرياضيات الدولية (IMO 2025): حل Seed-Prover 5 من أصل 6 مسائل بشكل كامل، حيث حل Seed-Geometry المسألة الثانية على الفور، واستنتج Seed-Prover برهانات للمسائل المتبقية باستخدام إعدادات استنتاجية مختلفة.
- مسائل IMO السابقة: برهن على 121 من أصل 155 مهمة، محققاً نسبة نجاح بلغت 78.1% عبر جميع مستويات الصعوبة.
- MiniF2F: حقق معدل إثبات 99.6% لمجموعتي التحقق والاختبار في الإعدادات المتوسطة، وحل مسائل صعبة مثل IMO 1990 P3.
- PutnamBench: تحسن من 201 إلى 331 مسألة محلولة من أصل 657 عند الترقية من إعدادات الاستنتاج الخفيفة إلى المتوسطة.
- CombiBench: حل 30 من أصل 100 مسألة في التوافقيات، متفوقاً على الأساليب الموجودة.
- MiniCTX-v2: حقق نسبة نجاح 81.8%.
الخلاصة
يقدم فريق Seed في بايتدانس نظامي Seed-Geometry و Seed-Prover، وهما طريقتان للاستدلال الرسمي تُدمجان قدرات نماذج اللغات الكبيرة. يُوفر Seed-Geometry التحقق المُسرّع وآليات بحث مُحسّنة، بينما يستخدم Seed-Prover الصقل المتكرر واستراتيجيات استنتاجية معقدة في وقت الاختبار. يُظهر نجاح حل 5 من أصل 6 مسائل في IMO 2025 الفعالية العملية لهذه الأساليب في معالجة مسابقات رياضية عالية المستوى. يُوفر اعتماد اللغات الرسمية مثل Lean التحقق السريع من البرهان، وهو أكثر فعالية من حيث التكلفة من الخبراء البشريين وأكثر موثوقية من القضاة القائمين على نماذج اللغات الكبيرة. سيركز البحث في المستقبل على دمج الأنظمة الرسمية مع نماذج اللغات الكبيرة لمعالجة التخمينات المفتوحة.
مواضيع مشابهة:
DeepSeek-Prover-V2: نموذج لغوي كبير مفتوح المصدر لإثبات النظريات الرياضية
الاستنتاج الموازي في نماذج اللغات الكبيرة: ثورة في كفاءة المعالجة
بروتوكول سياق النموذج (MCP): المعيار الجديد لتكامل أدوات الذكاء الاصطناعي
جوجل تُطلق جيميني 2.5 برو (إصدار I/O): تفوق على GPT-4 في البرمجة ودعم فهم الفيديو الأصلي وريادة منصة WebDev Arena
اترك تعليقاً