Guoxin Chen Jing Wu Xinjie Chen Wayne Xin Zhao Ruihua Song Chengxi Li Kai Fan Dayiheng Liu Minpeng Liao

الملخص

الإعادة التمثيلية التلقائية (Autoformalization)، التي تُحول الرياضيات المكتوبة بلغة طبيعية إلى عبارات رياضية رسمية قابلة للتحقق آليًا، تُعدّ حاسمة في استخدام التفكير الرياضي الرمزي لحل المسائل الرياضية المطروحة بلغة طبيعية. وعلى الرغم من أن النماذج الكبيرة للغة (LLMs) قادرة على إنتاج عبارات رسمية صيغية صحيحة، إلا أنها غالبًا ما تفشل في الحفاظ على النية الدلالية الأصلية للمشكلة. وينتج هذا التقييد عن نهج النماذج الكبيرة للغة التي تُعامل إعادة التمثيل التلقائي كمهمة ترجمة بسيطة، تفتقر إلى آليات التفكير الذاتي والتحسين التكراري التي يوظفها الخبراء البشريون بشكل طبيعي. ولحل هذه المشكلات، نقترح "ReForm"، وهي طريقة مُعَدَّلة للإعادة التمثيلية التلقائية، تُدمج بشكل وثيق تقييم الاتساق الدلالي في عملية إعادة التمثيل التلقائي. وبهذا، يمكن للنموذج إنتاج عبارات رسمية بشكل تكراري، وتقييم دقة تعبيره الدلالي، ثم إجراء تصحيح ذاتي للأخطاء المُحددة من خلال عملية تحسين تدريجيّة. ولتدريب هذا النموذج المُعَدَّل بشكل فعّال، نقدّم "تحسين التسلسل المحدود الواعي" (Prospective Bounded Sequence Optimization - PBSO)، الذي يستخدم مكافآت مختلفة في مواقف متعددة داخل التسلسل، لضمان تطوير النموذج لكلاً من إعادة التمثيل التلقائي الدقيق وعمليات التحقق الدلالي الصحيحة، ومنع التقييمات السطحية التي قد تُضعف غاية التفكير الذاتي. أظهرت تجارب واسعة على أربع معايير لإعادة التمثيل التلقائي تفوق ReForm بمتوسط 17.2 نقطة مئوية مقارنة بأقوى النماذج السابقة. ولضمان موثوقية التقييم، نقدّم "ConsistencyCheck"، وهو معيار مكوّن من 859 عنصرًا تم تقييمها من قبل خبراء، لا يُستخدم فقط لاختبار قدرة النماذج الكبيرة للغة على التقييم، بل يُظهر أيضًا أن إعادة التمثيل التلقائي صعبة بشكل جوهري: فحتى الخبراء البشريون يرتكبون أخطاء دلالية في ما يصل إلى 38.5% من الحالات.