Faithful Autoformalization via Roundtrip Verification and Repair

ملخص تقني: الصياغة الشكلية الأمينة عبر التحقق من الرحلة العكسية والإصلاح

بيان المشكلة
يتناول هذا البحث فجوة حرجة في عملية "الصياغة الشكلية التلقائية" (Autoformalization): وهي غياب طريقة موثوقة للتحقق مما إذا كان النموذج اللغوي الكبير (LLM) قد نقل المعنى الدلالي لبيان باللغة الطبيعية بأمانة عند ترجمته إلى تمثيل رسمي قابل للفحص آلياً. تعتمد طرق التقييم الحالية على الصلاحية النحوية أو نجاح المهام اللاحقة، وهي طرق لا تختبر مباشرة الأمانة الدلالية. علاوة على ذلك، عندما تقع أخطاء، تقتصر استراتيجيات الإصلاح الحالية على إعادة التوليد الكامل (End-to-end regeneration)، مما يفتقر إلى القدرة على تشخيص أين فُقد المعنى في مسار الترجمة. ويعد هذا تحدياً خاصاً في مجالات مثل القانون التشريعي، حيث لا تتوفر صياغات شكلية نموذجية (Ground-truth).

المنهجية
يقترح المؤلفون إطار عمل للتحقق من الرحلة العكسية والإصلاح المحدود النطاق يعمل دون الحاجة إلى تسميات توضيحية نموذجية. وتتضمن الآلية الجوهرية مسار ترجمة يتكون من ثلاث مراحل:

1. T1 (الصياغة الشكلية التلقائية): ترجمة المدخلات باللغة الطبيعية $x$ إلى تعبير رسمي $y_{orig}$ في نظام شكلي مستهدف $\Sigma$.
2. T2 (الترجمة العكسية): ترجمة $y_{orig}$ مرة أخرى إلى لغة طبيعية $x'$.
3. T3 (إعادة الصياغة الشكلية): ترجمة $x'$ مرة أخرى إلى تعبير رسمي $y_{rt}$.

التحقق: يقوم النظام بالتحقق من التكافؤ المنطقي بين الصياغة الشكلية الأولية ($y_{orig}$) والصياغة الشكلية الناتجة عن الرحلة العكسية ($y_{rt}$) باستخدام أداة رسمية (تحديداً مُحلل SMT في التجارب). إذا كان $y_{orig} \equiv_\Sigma y_{rt}$، يُعتبر المسار متسقاً ذاتياً.

التشخيص والإصلاح: عندما يفشل التكافؤ، يستخدم إطار العمل إجراءً لـ التشخيص القائم على المراحل. يقوم "قاضٍ" من النماذج اللغوية الكبيرة بفحص المخرجات ($x, y_{orig}, x', y_{rt}$) لتحديد أول مرحلة حدث فيها الانحراف الدلالي (المرحلة 1، أو 2، أو 3). ومن الأهمية بمكان أن يكون التشخيص "محدود النطاق"، مما يعني أن التفسير مقيد بالمخرجات ذات الصلة بتلك المرحلة المحددة فقط.

• الإصلاح المحدود النطاق: بدلاً من إعادة توليد المسار بأكمله، يقوم عامل إصلاح مستهدف ($R_i$) بتصحيح المرحلة المعيبة المحددة فقط. بعد ذلك، يتم إعادة توليد المراحل اللاحقة للحفاظ على تماسك المسار.
• الحلقة التكرارية: تتكرر هذه العملية حتى ميزانية محددة ($K=3$) حتى يتم تحقيق التكافؤ أو استنفاد الميزانية.

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

المساهمات الرئيسية

1. إطار عمل التحقق من الرحلة العكسية: طريقة للإشارة إلى أمانة الصياغة الشكلية التلقائية دون الحاجة إلى صياغات نموذجية، وهي قابلة للتطبيق على أي نظام شكلي يسمح بالتحقق من التكافؤ (مثل SMT أو مدققات الأنواع).
2. الإصلاح المحدود النطاق الموجه بالتشخيص: إجراء يحدد موقع الأخطاء في خطوات الترجمة، مما يسمح بتصحيحات مستهدفة بدلاً من إعادة توليد المسار الكامل المكلفة.
3. التحليل التجريبي للاختناقات: دراسة عبر مجالين تشريعيين (قانون النقل في تكساس وقانون المنتزهات والحياة البرية في تكساس) وعائلتين من النماذج (Claude Opus 4.6 و GPT-5.2)، والتي حددت خطوة التشخيص باعتبارها الاختناق الرئيسي للإصلاح المحدود النطاق، وليس المسار أو عوامل الإصلاح نفسها.

النتائج
تم تقييم إطار العمل على 150 قاعدة مرورية و77 قاعدة للحياة البرية.

• فعالية الإصلاح: حقق الإصلاح المحدود النطاق الموجه بالتشخيص أعلى معدلات تكافؤ مُتحقق منها بأقل تكلفة عندما كانت وظيفة التشخيص موثوقة.
• الاعتماد على النموذج: مع قيام Claude بعملية المسار والتشخيص، تفوق الإصلاح المحدود النطاق على النماذج المرجعية (عدم الإصلاح، اختيار المرحلة عشوائياً، إعادة التوليد الكامل). ومع ذلك، مع GPT، كانت خطوة التشخيص غير موثوقة (منحازة بشدة لإلقاء اللوم على المرحلة الأولى)، مما تسبب في ضعف أداء الإصلاح المحدود النطاق وزيادة تكلفته مقارنة بإعادة التوليد الكامل.
• التدخل عبر النماذج: استبدال خطوة تشخيص GPT بـ Claude فقط (مع الإبقاء على GPT للمسار والإصلاح) استعاد كفاءة وفعالية الإصلاح المحدود النطاق، مما يثبت أن وظيفة التشخيص هي المتغير الحاسم.
• التنبؤ بالأمانة: يعد التكافؤ الشكلي مؤشراً قوياً على الأمانة الدلالية. القواعد التي اجتازت فحص التكافؤ (UNATS) أظهرت انحرافاً في NLI أقل بمقدار 1.4 إلى 2.5 مرة عن تلك التي فشلت (SAT). ومع ذلك، فإن التكافؤ الشكلي ضروري ولكنه ليس كافياً؛ حيث أظهرت حوالي 16% من القواعد المتكافئة شكلياً انحرافاً دلالياً.

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

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