MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics
تقدم هذه الورقة MathlibLemma، وهو مسار مؤتمت يعتمد على النماذج اللغوية الكبيرة لاكتشاف وصياغة لِمات "الفلكلور" المفقودة لتوسيع مكتبة Lean Mathlib، مع إنشاء معيار شامل يتضمن أكثر من 4,000 عبارة رياضية مُحققة للنهوض بالرياضيات المساعدة للذكاء الاصطناعي.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تحاول بناء مكتبة ضخمة ومثالية للمعرفة الرياضية باستخدام مساعد آلي. لديك مكتبة موجودة بالفعل وعملاقة تسمى Mathlib (بُنيت للغة الإثبات Lean)، وهي تشبه موسوعة منظمة للغاية للحقائق الرياضية.
ومع ذلك، هناك مشكلة: بينما تحتوي المكتبة على النظريات الكبيرة والمشهورة، إلا أنها تفتقر إلى الآلاف من الحقائق الصغيرة "البديهية" التي يستخدمها علماء الرياضيات البشر يومياً دون تفكير. تُسمى هذه الحقائق "الاستنتاجات الشعبية" (folklore lemmas).
فكر في الأمر على هذا النحو: إذا كنت تكتب رواية، فلن تحتاج إلى شرح أن "المربع له أربعة أضلاع" أو أن "إضافة صفر إلى رقم ما لا تغير قيمته". أنت تفترض فقط أن الجميع يعرف ذلك. لكن بالنسبة لآلة التحقق من البراهين الآلية، إذا لم تكن هذه الحقيقة الصغيرة مكتوبة صراحة في المكتبة، فستتعثر. الأمر يشبه محاولة بناء منزل، ثم تكتشف أنك نسيت شراء نوع معين من المسامير اللازمة لتثبيت السقف. الهيكل (البرهان) سليم من الناحية المفاهيمية، ولكن لا يمكنك إكمال عملية البناء لأن قطعة صغيرة "بديهية" مفقودة.
المشكلة: "الميل الأخير"
تجادل الورقة البحثية بأن هذا النسيج الرابط المفقود هو حاجز "الميل الأخير". إنه يمنع علماء الرياضيات من استخدام هذه الأدوات الحاسوبية القوية بنفس السهولة التي يستخدمون بها معالجات النصوص أو الآلات الحاسبة. فحتى لو كان الإنسان يعرف البرهان، فإن الكمبيوتر لا يستطيع القيام به لأن تلك الخطوات المتوسطة الصغيرة مفقودة.
علاوة على ذلك، عندما تحاول نماذج الذكاء الاصطناعي (النماذج اللغوية الكبيرة - LLMs) المساعدة في كتابة هذه البراهين، فإنها غالباً ما تفشل. لماذا؟ لأن الذكاء الاصطناعي إذا لم يجد الحقيقة "البديهية" في المكتبة، فإنه يحاول اختراع البرهان بأكمله من الصفر. هذا يشبه طلب بناء جسر من شخص دون تزويده بمخطط؛ قد يتوه، أو يرتكب أخطاءً، أو يهلوِس (يختلق أشياء من عنده) لأن المهمة ضخمة جداً.
الحل: MATHLIBLEMMA
ابتكر المؤلفون نظاماً يسمى MATHLIBLEMMA. فكر في هذا النظام كـ مصنع مكون من أربع مراحل مصمم للعثور على تلك الحقائق "البديهية" المفقودة، وكتابتها بشكل صحيح، وإثبات صحتها.
إليك كيف يعمل هذا المصنع، خطوة بخطوة:
المستكشف (وحدة الاكتشاف - Discovery Module):
تخيل أمين مكتبة فضولياً يقرأ المكتبة الموجودة ويقول: "مهلاً، لدينا الكثير من الحقائق حول المثلثات، ولكن ليس لدينا قاعدة لما يحدث عندما نقلب أحدها رأساً على عقب. من المحتمل أن هذا صحيح، لكنه مفقود!". تستخدم هذه الوحدة الذكاء الاصطناعي لابتكار هذه الحقائق المفقودة بناءً على ما هو موجود بالفعل.حارس البوابة (وحدة الحكم - Judge Module):
قد يرتكب "المستكشف" أخطاءً. قد يقترح شيئاً يبدو رائعاً ولكنه خاطئ رياضياً (مثل القول بأن "كل الأرقام زوجية"). "حارس البوابة" هو ذكاء اصطناعي ثانٍ ينظر إلى الاقتراحات ويقول: "لا، هذا هراء"، أو "نعم، هذا يبدو صحيحاً". إنه يقوم بتصفية النفايات قبل أن يهدر المصنع وقته عليها.المحرر (وحدة الصياغة الرسمية - Formalizer Module):
حتى لو كانت الفكرة صحيحة رياضياً، فقد يكتبها الذكاء الاصطناعي بطريقة غريبة لا يفهمها الكمبيوتر (مثل جملة ذات قواعد لغوية سيئة). يقوم "المحرر" بإصلاح الصياغة. إنه يتواصل مع خادم Lean ليرى ما الخطأ، ويطلب من الذكاء الاصطناعي إصلاح الخطأ حتى يقول الكمبيوتر: "حسناً، هذه الجملة صحيحة قواعدياً".البنّاء (وحدة الإثبات - Prover Module):
الآن بعد أن كُتبت الحقيقة بشكل صحيح، يحاول "البنّاء" إثباتها. يحاول بناء الحجة المنطقية. إذا فشل، يتلقى خطأً، ثم يحاول مجدداً ويصلح أخطاءه. وإذا نجح، فإنه ينتج برهاناً موثقاً يقبله الكمبيوتر كحقيقة بنسبة 100%.
ما وجدوه
قام الفريق بتشغيل هذا المصنع وأنتج شيئين رئيسيين:
- مكتبة جديدة من الحقائق: وجدوا وأثبتوا 1,506 من هذه "الاستنتاجات الشعبية" المفقودة. بل إنهم أخذوا عينة صغيرة منها وأضافوها بنجاح إلى مكتبة Mathlib الرسمية، مما يثبت أن الذكاء الاصطناعي يمكنه توليد حقائق تلبي المعايير العالية للخبراء البشريين.
- تحدٍ جديد (الاختبار المعياري - The Benchmark): أنشأوا مجموعة اختبار مكونة من 4,028 من هذه الحقائق المفقودة لمعرفة مدى جودة نماذج الذكاء الاصطناعي المختلفة في إيجادها وإثباتها.
النتائج:
- نماذج الذكاء الاصطناعي الحالية تتحسن، لكنها لا تزال بعيدة عن المثالية. أفضل النماذج استطاعت حل حوالي 19% فقط من هذه الحقائق "البديهية" بمفردها.
- ومع ذلك، عندما تجمع بين نقاط القوة لنماذج مختلفة (مثل استخدام فريق من المتخصصين)، يمكنها حل حوالي 37%.
- والأهم من ذلك، عندما نظر الخبراء البشريون في الحالات التي فشل فيها الذكاء الاصطناعي، وجدوا أن 78% منها كانت في الواقع قابلة للحل وصحيحة رياضياً. هذا يعني أن الذكاء الاصطناعي لم يفشل لأن الحقائق كانت زائفة، بل فشل لأن المهمة كانت صعبة حقاً.
الخلاصة
تظهر هذه الورقة أننا يمكننا استخدام الذكاء الاصطناعي ليس فقط لاستلاك مكتبات الرياضيات الموجودة، بل لتوسيعها بنشاط. من خلال أتمتة اكتشاف هذه القطع الصغيرة المفقودة، نحن نساعد في بناء أساس أكثر اكتمالاً، وقابلية للاستخدام، وموثوقية للرياضيات الرسمية. إنه يشبه ملء الفجوات في خريطة ما، بحيث تصبح الرحلة من الفكرة الرياضية إلى البرهان الموثق حاسوبياً سلسة وسهلة.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.