FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean
تقدم الورقة البحثية **FormalScience**، وهو مسار وكيل (agentic pipeline) يعتمد على تدخل العنصر البشري ومصمم لمساعدة الخبراء في المجال على أتمتة صياغة الاستدلال العلمي في كود Lean4 بكفاءة، وهو ما تم إثباته من خلال إنشاء **FormalPhysics**، وهي مجموعة بيانات عالية الجودة من مسائل الفيزياء بمستوى جامعي توفر تحليلاً منهجياً للانزياح الدلالي (semantic drift) في عملية الصياغة الرسمية القائمة على النماذج اللغوية الكبيرة (LLMs).
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك طاهٍ عالمي المستوى تكتب وصفاتك في دفتر يوميات جميل ومنساب بخط اليد. وصفاتك مليئة بالحدس: "أضف رشة ملح حتى تشعر أنها مناسبة،" أو "قلّب البصل حتى يبدو ذهبياً وحالماً." هكذا يكتب العلماء—باستخدام الاستدلال غير الرسمي (LaTeX) الذي يكون غنياً بالمعنى ولكنه "غامض" بالنسبة للكمبيوتر.
الآن، تخيل أنك تريد إعطاء هذه الوصفات لمطبخ عالي التقنية، يعمل بواسطة روبوت. الروبوت لا يفهم معنى "حالم" أو "رشة". هو فقط يفهم الكود الرسمي (مثل Lean4)، وهو لغة رياضية صارمة حيث يجب حساب كل ذرة بدقة. إذا نسيت فاصلة واحدة، سيتعطل الروبوت.
المشكلة؟ ترجمة "البصل الحالم" إلى "4.2 جرام بالضبط من البصل عند درجة حرارة 175 مئوية" أمر صعب للغاية. ورقة البحث هذه، FormalScience، تدور حول بناء جسر بين "الطاهي الحالم" (العالِم) و"المطبخ الروبوتي" (النظام الحاسوبي الرسمي).
الشخصيات الثلاث الرئيسية
- العالِم (الإنسان في الحلقة - Human-in-the-Loop): هو يعرف الفيزياء، لكنه ليس مبرمج كمبيوتر. هو يعمل كـ "رئيس تحرير"، يتحقق مما إذا كانت الترجمة منطقية أم لا.
- الوكيل (المترجم الذكي - The Agent): ذكاء اصطناعي يحاول ترجمة الوصفة. هو ليس مجرد مترجم؛ بل هو "وكيل" يمكنه تجربة ترجمة، ورؤية ما إذا كان الروبوت قد رفضها، ثم يحاول إصلاح أخطائه بنفسه.
- المُثبِت (الروبوت - The Prover): هو النظام الرسمي (Lean4) الذي يقول إما: "مثالي، هذا مؤكد رياضياً" أو "خطأ! أنا لا أعرف ما هو البصل الحالم."
مشكلة "انزياح الترجمة" (جوهر الورقة البحثية)
اكتشف الباحثون مشكلة رائعة ومخيفة قليلاً يسمونها "الانزياح الدلالي" (Semantic Drift).
تخيل أنك تترجم قصيدة عن "أسد مهيب وهادر" إلى دليل تقني لحديقة حيوان. لكي تجعل الدليل "صحيحاً" و"وظيفياً"، قد تكتفي بكتابة: "قط كبير، الوزن: 190 كجم."
من الناحية التقنية، الدليل صحيح (الأسد هو بالفعل قط كبير)، لكنك فقدت روح القصيدة. لقد "انزحْتَ" من المعنى إلى مجرد الحقائق المجردة.
في الفيزياء، وجد الباحثون ثلاثة أنواع من هذا "الانزياح":
- الانهيار الرمزي (تأثير "التقلص"): أنت تصف كوناً كمياً معقداً حيث ترقص الجسيمات بطرق محددة، لكن الكمبيوتر يبسط الأمر لدرجة أنه يعاملها كمجرد أرقام بسيطة. الأمر يشبه تحويل فيلم ثلاثي الأبعاد إلى رسم تخطيطي باللونين الأبيض والأسود. إنه "صحيح"، لكن الفيزياء قد ضاعت.
- رفع التجريد (تأثير "التخطي"): بدلاً من القيام بالعمل الشاق لحساب كيفية تأثير الجاذبية على كوكب ما، يخبر الذكاء الاصطناون الكمبيوتر ببساطة: "افترض أن الجاذبية تعمل." الكمبيوتر يقول: "حسناً، أنا أوافق!" ويعطي الضوء الأخضر. الرياضيات صالحة، لكن "الفيزياء" الفعلية تم تخطيها تماماً.
- اختيار المقدمات الضمنية (البطل الخفي): هذا هو النوع الجيد من الانزياح! أحياناً، يدرك الذكاء الاصطناعي أن العالِم نسي ذكر تفصيل صغير (مثل "تأكد من عدم القسمة على صفر"). يضيف الذكاء الاصطناعي هذا التفصيل، مما يجعل البرهان أقوى من النسخة البشرية الأصلية.
لماذا يهم هذا؟
في الوقت الحالي، يتفوق الذكاء الاصطناعي في كتابة المقالات، لكنه يعاني في مواجهة "الحقيقة الصعبة" للرياضيات والعلوم. إذا أخبر ذكاء اصطناعي عالماً ما: "لقد تم إثبات هذه الصيغة الجديدة لمفاعل الاندماج رياضياً،" يحتاج العالِم أن يعرف: هل أثبت الذكاء الاصطناعي الفيزياء فعلياً، أم أنه "غش" فقط عبر تبسيط المشكلة حتى أصبحت سهلة؟
من خلال إنشاء مجموعة بيانات FormalPhysics ومسار عمل FormalScience، قدم هؤلاء الباحثون طريقة لتدريب أجهزة ذكاء اصطناعي مستقبلية لتكون مترجمين أفضل—لضمان أنه عندما ننتقل من العالم "الحالم" للفكر البشري إلى العالم "الروبوتي" للبرهان الرسمي، فإننا لا نفقد السحر (أو الحقيقة) في الطريق.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.