«بيبر فورمالايزر»: وكيل برمجي يسد ثغرات الأوراق البحثية بالبراهين الصورية

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

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

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

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

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

حصر الصلاحيات الجوهرية بيد الباحث البشري يمنع الانحرافات التوليدية الشائعة، ويثبت أن البرهنة الرياضية الحاسوبية باتت في متناول الفرق البحثية دون استنزاف أشهر من العمل اليدوي المضني.