Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
تقدم الورقة البحثية "Formal Conjectures"، وهو معيار مرجعي ديناميكي مفتوح المصدر يتكون من 2,615 مسألة رياضية تمت صياغتها بلغة Lean 4 ومستمدة من أبحاث نشطة، صُمم لتقييم ودفع قدرات أنظمة الاستدلال الآلي في اكتشاف براهين جديدة مع ضمان سلامة البيانات من خلال التعاون المجتمعي والتحقق المدقق بواسطة الذكاء الاصطناعي.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تحاول تعليم روبوت كيفية القيام بالرياضيات المتقدمة. في الماضي، ربما كنت ستعطي الروبوت كومة من واجبات الرياضيات القديمة. ولكن هناك مشكلة كبيرة: قد يكون الروبوت قد حفظ الإجابات فقط من الإنترنت بدلاً من تعلم كيفية التفكير حقاً. الأمر يشبه طالباً حفظ نموذج إجابات الاختبار لكنه لا يفهم الرياضيات.
تقدم هذه الورقة طريقة أذكى لاختبار هذه الروبوتات. هم يسمونها التخمينات الصورية (Formal Conjectures).
إليك كيف يعمل الأمر، مقسماً إلى أفكات بسيطة:
١. اختبار "اللحم الطازج" (عدم التلوث - Zero Contamination)
معظم اختبارات الرياضيات للذكاء الاصطناعي هي اختبارات "قديمة". الإجابات موجودة بالفعل عبر الإنترنت، لذا قد يقوم الذكاء الاصطناعي بمجرد النسخ واللصق.
- التشبيه: تخيل مسابقة طبخ حيث يعطي الحكام الطهاة وصفة لم يروها من قبل، مكتوبة بشفرة سرية. إذا استطاع الطاهي طهي الطبق، فهو يعرف حقاً كيف يطبخ. إذا لم يستطع، فهو مجرد شخص يخمن.
- حل الورقة البحثية: أنشأ المؤلفون مكتبة مكونة من ١,٠٢٩ مسألة رياضية غير محلولة (تخمينات). هذه مسائل يحاول رياضيون بشريون حقيقيون حلها حالياً. ولأن أحداً لم يحلها بعد، فلا يمكن للذكاء الاصطناعي أن يكون قد حفظ إجاباتها. إذا حل الذكاء الاصطناعي إحداها، فهذا اكتشاف حقيقي وليس مجرد عملية نسخ ولصق.
٢. "الحكم الصارم" (Lean 4)
في الرياضيات العادية، يمكنك كتابة برهان يبدو جيداً ولكنه يحتوي على خطأ منطقي صغير. البشر قد لا يلاحظونه.
- التشبيه: فكر في لعبة فيديو حيث يتعين عليك بناء جسر. إذا استخدمت طوبة ضعيفة، سينهار الجسر. في هذه الورقة، "الجسر" هو البرهان الرياضي. يستخدم المؤلفون لغة حاسوبية خاصة تسمى Lean 4 لتكون هي الحكم.
- حل الورقة البحثية: Lean 4 هي مثل حكم صارم للغاية. هي لا تهتم إذا كان برهانك يبدو "جميلاً"؛ بل تتحقق من كل خطوة منطقية. إذا وجد خطأ واحد صغير، سيقول الحكم: "لا، هذا خطأ". هذا يضمن أنه عندما يقول الذكاء الاصطناعي إنه حل مسألة ما، فإنه قد فعل ذلك حقاً.
٣. "المكتبة الحية" (معيار متطور - An Evolving Benchmark)
عادةً، بمجرد وضع اختبار ما، فإنه يبقى كما هو للأبد. ولكن الذكاء الاصطناعي يصبح أذكى كل يوم، لذا تصبح الاختبارات القديمة سهلة للغاية.
- التشبيه: تخيل لعبة فيديو يتم تحديثها كل أسبوع. مع تحسن اللاعبين، تضيف اللعبة مستويات أصعب وتصلح الأخطاء في الخريطة.
- حل الورقة البحثية: هذا المعيار هو مشروع "حي":
- إنه ينمو: يستمرون في إضافة مسائل جديدة من أوراق بحثية حقيقية.
- إنه يصلح نفسه: أحياناً، تُكتب المسائل الرياضية نفسها بشكل غامض. عندما يحاول الذكاء الاصطناعي حلها، قد يفشل لأن المسألة لم تكن واضحة. هذا الفشل يساعد الرياضيين البشر على إدراك: "أوه، لقد كتبنا تلك المسألة بشكل خاطئ!" ثم يقومون بتصحيح نص المسألة.
- يحتوي على مسارين:
- مسار الاكتشاف: محاولة حل المسائل غير المحلولة (الـ "لحم الطازج").
- مسار الترجمة: أخذ المسائل التي حلها البشر بالفعل وتعليم الذكاء الاصطناعي كيفية كتابتها بلغة الحاسوب الصارمة (Lean 4).
٤. "شبكة الأمان" (تجنب الغش)
يخشى المؤلفون من "تسرب البيانات" (غش الذكاء الاصطناعي من خلال رؤية الإجابات في بيانات التدريب الخاصة به).
- التشبيه: لمنع الطلاب من الغش، يقوم المعلمون أحياناً بقفل نموذج الإجابات في خزنة ولا يفتحونها إلا بعد الاختبار.
- حل الورقة البحثية: أنشأوا نسخة "مجمدة" من الاختبار. هذه نسخة ثابتة من ١٠٠ مسألة محددة في زمن معين. حتى لو تغيرت المكتبة الرئيسية لاحقاً، تظل هذه النسخة المحددة ثابتة بحيث يمكن للعلماء مقارنة نماذج الذكاء الاصطناعي المختلفة بشكل عادل دون القلق من تغير الاختبار من تحتهم.
٥. لماذا هذا مهم؟
تظهر الورقة أن هذا النظام يعمل بالفعل.
- نتائج حقيقية: يذكرون أنه باستخدام هذا النظام، ساعد ذكاء اصطناعي (يسمى أرسطو - Aristotle) عالم رياضيات بشري في حل مسألة شهيرة كانت مفتوحة لفترة طويلة (مسألة إيردوس ١٢٤).
- الإشارة: يوفر المعيار "إشارة قابلة للتسلق" (climbable signal). إنه يوضح بالضبط مدى التقدم الذي حققه الذكاء الاصطناعي وكم يحتاج من المسافة ليقطعها. إذا حل الذكاء الاصطناعي ١٠٪ من المسائل غير المحلولة، فهذا أمر ضخم. وإذا حل ٠٪، فهو ليس جاهزاً بعد.
الملخص
التخمينات الصورية (Formal Conjectures) هي ملعب جديد ومتطور باستمرار لعلماء الرياضيات من الذكاء الاصطناعي. يستخدم حكماً حاسوبياً صارماً (Lean 4) للتحقق من العمل، ويركز على المسائل التي لم تُحل بعد لمنع الغش، ويعمل كأداة تعاونية حيث يساعد البشر والذكاء الاصطناعي بعضهم البعض في توضيد الأسئلة الرياضية الصعبة. إنه ليس مجرد اختبار؛ إنه أداة لتحقيق اكتشافات رياضية حقيقية.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.