Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning

في عالم الرياضيات، هناك انقسام مستمر بين اللغة التي يستخدمها البشر لوصف الأفكار واللغة الصارمة والدقيقة التي تحتاجها الحواسيب للتحقق منها. يكتب الرياضيون البراهين بلغة طبيعية، مليئة بالفروق الدقيقة والسياق، بينما تتطلب الحواسيب عبارات رسمية لا تترك مجالاً للغموض. إن سد هذه الفجوة هو مهمة تسمى "الأتمتة الصورية" (autoformalization)، حيث يحاول الذكاء الاصطناعي ترجمة فكرة رياضية بشرية إلى تنسيق يشبه الكود البرمجي يمكن للحاسوب التحقق منه. لسنوات، كان الأمل يكمن في أن الآلات لن تكتفي فقط بإجراء هذه الترجمات، بل ستتمكن أيضاً من الحكم على عملها، لتعمل كحكم آلي لضمان صحة الرياضيات. ومع ذلك، ظل التحقق من هذا العمل يمثل عقبة مستعصية. فبينما يمكن للحواسيب بسهولة اكتشاف ما إذا كان سطر برمجي مكسوراً من الناحية النحوية، إلا أنها تجد صعوبة في فهم ما إذا كانت الفكرة المترجمة تعني حقاً نفس الشيء الذي تعنيه الفكرة البشرية الأصلية. يمكن للخبراء البشريين القيام بذلك، لكن العملية بطيئة ومكلفة وصعبة التوسع مع زيادة تعقيد المسائل الرياضية.

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

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

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

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

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

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

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