PaperFormalizer يبقي المؤلفين في دائرة القرار عند فحص الأوراق البحثية بـ Lean والذكاء الاصطناعي
تصف ورقة أولية جديدة مساراً بالذكاء الاصطناعي يراجع ادعاءات البحث مع مؤلفه ثم يربط العبارات المنقحة بتصريحات مفحوصة في Lean.
صياغة ورقة بحثية رسمياً من دون تغيير معناها بصمت
تقدم ورقة أولية نُشرت في 22 أكتوبر نظام PaperFormalizer، وهو سير عمل قائم على وكلاء يهدف إلى مساعدة الباحثين على تحويل أوراقهم الرياضية إلى مخرجات يمكن لـ Lean فحصها. وليست فكرته المحورية نموذجاً جديداً لبرهنة المبرهنات بقدر ما هي قاعدة إجرائية: ينبغي للنظام أن يتوقف عندما يكون النص ملتبساً أو عندما قد يغير الإصلاح المقترح نتيجة ما، وأن يترك القرار لمؤلف الورقة.
وهذا التمييز مهم. يستطيع برهان Lean أن يثبت أن عبارة صورية تترتب على التعريفات والنتائج السابقة المقدمة إليه، لكنه لا يستطيع وحده أن يقرر ما إذا كانت العبارة لا تزال تمثل المبرهنة التي قصدها المؤلف بعد ترجمة جملة غير صورية أو إصلاحها. ويقدم المؤلفون PaperFormalizer بوصفه طريقة لإظهار هذه الفجوة بدلاً من إخفائها خلف نجاح عملية التجميع.
من مصدر TeX إلى سجل صوري مرتبط بالنص
بحسب الورقة، يبدأ المسار من مصدر LaTeX للبحث. يستخرج التعريفات والافتراضات والنتائج والادعاءات المستشهد بها في رسم بياني للتبعيات، ثم يراجعها من حيث الأمانة للنص والالتباس والصحة. وعندما يجد النظام مثالاً ناقضاً أو قراءة لا يحسمها النص، يمكنه اقتراح إصلاح محدود أو سؤال المؤلف عن القراءة المقصودة. وبعد هذه المراجعة فقط يخطط تصريحات Lean، ويعيد استخدام نتائج المكتبات المتاحة عند الاقتضاء، ويملأ البراهين، ويربط كل تصريح بالعبارة المقابلة له في الورقة.
ولا يقتصر المخرج المعلن على مجلد لملفات البرهان؛ إذ يشمل نسخة منقحة من الورقة ونسخة مشروحة تبرز التغييرات وتقريراً يصنف العبارات، مثل مثبتة أو مشروطة أو مصلحة أو مدحوضة أو غير محلولة. ويصف المؤلفون أيضاً «عدة Lean» شخصية يمكن أن تجمع نتائج قابلة لإعادة الاستخدام عبر أوراق الباحث. وقد يخفض ذلك كلفة الصياغة اللاحقة، لكنه يجعل من الضروري كذلك فحص الافتراضات والمواد المصاغة سابقاً التي يعاد استخدامها.
ما الذي تعرضه دراسة الحالة وما الذي لا تثبته
يفيد المؤلفون بأنهم طبقوا سير العمل على ثلاث من أوراقهم. وفي دراسة حالة عن آثار العلاج في الأحداث المتطرفة، يقولون إن خمس نتائج من أصل سبع احتاجت إلى مراجعة قبل أن يمكن إثبات النسخة النهائية في Lean من دون sorry أو مسلمات غير معيارية. وهذا تقرير توضيحي من فريق المشروع، وليس تدقيقاً مستقلاً للأوراق أو للتنفيذ أو لكل إصلاح مقترح. كما أن العمل ورقة أولية غير محكمة.
أما الفكرة المفيدة لرياضيات الذكاء الاصطناعي فليست أن الوكيل يستطيع حسم قصد المؤلف، بل أن سير عمل للصياغة الرسمية يستطيع كشف مواضع اختلاف القصد والافتراضات وشيفرة البرهان، ثم يمنح خبير المجال فرصة صريحة لاتخاذ قرار الحل.