HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs
تقدم الورقة البحثية "هيرميس" (Hermes)، وهو أداة مساعدة للوكلاء تدمج بين الاستدلال غير الرسمي والبراهين المثبتة رسميًا في لغة "لين" (Lean) لتحقيق استدلال رياضي أكثر دقة وكفاءة وقابلية للتحقق في النماذج اللغوية الكبيرة مقارنة بالنهج الحالية.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تحاول حل لغز رياضي صعب للغاية. لديك مساعد عبقري ولكنه مشتت الذهن قليلاً (وهو النموذج اللغوي الكبير، أو LLM)؛ هو بارع في طرح الأفكلة وكتابة شروحات طويلة ومبدعة، ومع ذلك، قد يرتكب أخطاء منطقية صغيرة، أو يرتبك، أو "يهلوس" بحقائق تبدو صحيحة ولكنها ليست كذلك.
من ناحية أخرى، لديك حَكَم رياضي صارم ولا يتهاون (وهو نظام إثبات رسمي يُدعى Lean). هذا الحَكَم لا يرتكب أخطاءً أبداً، لكنه جامد جداً؛ فهو لا يفهم عصفك الذهني الإبداعي، بل يقبل فقط الكود الرسمي المنظم بدقة. إذا أعطيته شرحاً فوضوياً، فسيقول لك ببساطة: "خطأ".
Hermes هو أداة جديدة تعمل كـ مترجم ومدير لمراقبة الجودة بين المساعد والمساعد والـحَكَم. فهو يسمح لمساعدك الإبداعي بالعمل بحرية، ولكنه يوقفه كل بضع خطوات ليسأل الحَكَم الصارم: "هل هذه الخطوة المحددة صحيحة حقاً؟"
إليك كيف يعمل Hermes، مقسماً إلى أجزاء بسيطة:
١. المشكلة: "المشي الطويل" مقابل "الامتحان الصارم"
- الطريقة القديمة (الاستدلال غير الرسمي): يحاول مساعدك حل المشكلة بأكملها في تدفق واحد طويل من الأفكار. إنه مرن وسريع، ولكن إذا اتخذ مساراً خاطئاً في وقت مبكر، فقد يستمر في السير في الاتجاه الخاطيء لفترة طويلة قبل أن يدرك خطأه. الأمر يشبه قيادة سيارة وأنت مغمض العينين، على أمل ألا تصطدم بجدار.
- الطريقة الأخرى (الإثبات الرسمي): يحاول مساعدك كتابة الحل بكود صارم منذ البداية. إنه دقيق تماماً، لكنه صعب وبطيء جداً لدرجة أن المساعد غالباً ما يتعثر أو يستسلم. الأمر يشبه محاولة بناء منزل طوبة بطوبة مع فحص كل طوبة بمخطط هندسي قبل وضع التالية.
٢. حل Hermes: نظام "نقاط التفتيش"
يجمع Hermes بين أفضل ما في العالمين. فهو يسمح للمساعد بكتابة بضع خطوات من شرحه الإبداعي، ثم يتوقف لإجراء "نقطة تفتيش".
- المترجم (وحدة الصياغة الرسمية): عندما يقول المساعد: "لذلك، الزاوية هي ٤٥ درجة"، يقوم Hermes بترجمة هذه الجملة إلى الكود الصارم الذي يفهمه الحَكَم.
- الحَكَم (وحدة الإثبات): يقوم الحَكَم الصارم بفحص هذا الكود.
- إذا نجح: رائع! يقوم Hermes بحفظ هذه الخطوة في بنك الذاكرة ويخبر المساعد: "عملك جيد، استمر".
- إذا فشل: يقول الحَكَم: "لا، هذا خطأ". يخبر Hermes المساعد: "توقف! لقد ارتكبت خطأً هنا. عد وصحح خطأك".
- بنك الذاكرة: لأن المسائل الرياضية غالباً ما تتضمن سلاسل طويلة من المنطق، يتذكر Hermes جميع الخطوات التي اجتازت الفحص بنجاح. هذا يضمن أن المساعد لا ينسى القواعد التي أثبتها بالفعل، مما يحافظ على اتساق الحجة بأكملها.
٣. لماذا هو أفضل (النتائج)
اختبرت الورقة البحثية Hermes على مسائل رياضية صعبة (مثل AIME و HARDMath2) باستخدام نماذج ذكاء اصطناعي مختلفة.
- الدقة: جعل Hermes الذكاء الاصطناعي أكثر ذكاءً بشكل ملحوظ. في المسائل الأكثر صعوبة، حسن Hermes معدل نجاح الذكاء الاصطناعي بنسبة تصل إلى ٤٠٪. لقد منع الذكاء الاصطناعي من تقديم إجابات خاطئة بثقة.
- الكفاءة: قد تعتقد أن فحص كل خطوة سيكون بطيئاً ومكلفاً. ومن المثير للدهشة أن Hermes كان في الواقع أسرع وأرخص (من حيث قدرة الحاسوب) من الطرق الأخرى التي تحاول توليد ٥ أو ١٠ إجابات مختلفة واختيار الأفضل بينها. الأمر يشبه اتخاذ مسار مباشر ومتحقق منه بدلاً من التجول في متاهة وتجربة ١٠ طرق مختلفة.
- الوضوح: على عكس الطرق الأخرى التي تقول فقط "هذه الإجابة مرجح صحتها بنسبة ٨٠٪"، يعطي Hermes "نعم" أو "لا" واضحة على خطوات محددة، مما يجعل من السهل معرفة سبب كون الإجابة صحيحة أو خاطئة.
الخلاصة
Hermes يشبه إعطاء مساعدك الرياضي الإبداعي محرراً ذكياً وآلياً يراجع عمله في الوقت الفعلي. هو لا يمنع المساعد من التفكير بإبداع؛ بل يضمن فقط عدم انحرافه نحو الهاوية. النتيجة هي ذكاء اصطناعي لحل المسائل الرياضية ليس فقط أكثر دقة، بل أيضاً أكثر كفاءة وأسهل في الثقة به.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.