From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory

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

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

المشروع: تحويل كتاب مدرسي إلى خريطة كنز يتم فحصها حاسوبيًا

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

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

التحدي الكبير: التحدث بلغتين مختلفتين

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

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

دور الروبوت وشبكة الأمان البشرية

هنا تصبح القصة مثيرة للاهتمام. لم يقم المؤلفون بكل عمليات الكتابة بأنفسهم، بل استخدموا "سير عمل وكيل" (agentic workflow)، وهو ما يشبه امتلاك فريق من روبوتات الذكاء الاصطناعي للقيام بالأعمال الشاقة. هذه الروبوتات تقرأ صفحات الكتاب المدرسي وتحاول كتابة كود "Lean". لكن المؤلفين تعلموا درسًا حيويًا: لا يمكنك الوثوق بالروبوتات ببساطة.

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

المفاجآت والأخطاء المكتشفة

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

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

لماذا يهم هذا في المستقبل

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

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