حوالي Theorem.chat
Theorem.chat يأخذ ادعاء رياضي ويحاول تسويته. أنت تذكر الادعاء، والمعيار الذي يجب أن يفي به. فريق من نماذج الذكاء الاصطناعي - كما تريد، من أي بائع تريده - يهاجمها، ونموذج آخر يحكمها. ثم يتم إضفاء الطابع الرسمي على الحجة في Lean 4 ضد Mathlib، وتقرر نواة اللين ما إذا كانت قد أثبتت. تلك الخطوة الأخيرة هي المنتج.
لماذا نواة، وليس نموذجا آخر
إذا سألت نموذجاً سؤالاً صعباً فستحصل على إجابة بسيطة سواء كان صحيحاً أم لا. وإذا سألت عدة أشخاص فسوف يتفقون في كثير من الأحيان، وهو ما يبدو وكأنه تأكيد، ولكنه ليس كذلك: فالنماذج تتقاسم بيانات التدريب وتشارك في النقاط العمياء. ونموذج ثانٍ يدقق في الأول لا يزال يمثل نفس النوع من الحكم، ويمكن الحديث عنه. ولا يمكن لنواة اللين أن تفعل ذلك. فهي إما تستمد البيان من البديهيات وMathlib، أو لا تستمد البيان، ولا تؤثر الثقة على النتيجة.
إن الطرق المعتادة لتزوير البرهان الرسمي يتم التحقق منها ورفضها. إن البرهان الذي يترك ثغرة في sorry، أو الذي يلجأ إلى native_decide لجعل النواة تقوم بحسابات على الثقة، أو الذي يقدم بديهية جديدة بهدوء، يتم اكتشافه ورفضه بدلاً من حسابه كنجاح.
ما يمكن للفريق أن يفعله فعلاً
إن الجدل هو الجزء الأرخص. فالفريق يعمل مع المؤلفات ـ arXiv، أوبن ألكس، كرورس ريفر ـ لذا فإن النتيجة المعروفة يتم اقتباسها بدلاً من إعادة استخلاصها بشكل سيئ. فهو يحتوي على SageMath وPARI/GP للحساب، وZ3 وCVC5 لحل مشكلة SMT، وOEIS للبحث عن التسلسل الذي بنته، وبيئة بايثون الرملية التي لا تتيح الوصول إلى الشبكة. ويمكن اختبار تخمين ما ضد عشرة آلاف حالة قبل أن يقوم أي شخص بإنفاق جولة من الوقت في محاولة إثباته، ومثال مضاد ينهي المناقشة على الفور.
الأدلة، وليس البلاغة
إن التوافق لا يحدد على أساس جودة الحجج. فالادعاء يتم تفكيكه إلى معايير قبول، ولا يتم تسوية المعيار إلا عندما يتمكن طرف ثالث من إعادة التحقق من شيء ما وراءه: مصدر مع اقتباس المقطع ذي الصلة، أو شفرة تم تنفيذها فعليا مع مخرجاتها الحقيقية. ويعيد المحكم التحقق من ذلك الدليل نفسه قبل الحكم، ولا يستطيع أن يعلن عن انتهاء التوافق بينما لا يزال المعيار مفتوحا.
أنت وضعت المعيار
إن المعيار الذي تختاره هو معيارك، ويحمله المحكم حرفياً. فإذا سألت عما قد يقبله خبير متأنٍ فسوف تحصل على ذلك. وإذا سألت عن حجة استقرائيه كاملة مع كل افتراضات محددة فسوف يحكم عليك على أساس ذلك بدلاً من ذلك. وإذا سألت عن الشروط التي قد تواجهها الجائزة، فإن النتيجة الصادقة عادة ما تكون وصفاً دقيقاً لمكان قصور اللجنة ـ وهو ما يعادل أكثر من ادعاء ثقة سوف تضطر إلى التحقق منه بنفسك على أية حال.
ولنتكلم بوضوح: هذه الآلة ليست آلة تسوي المشاكل المفتوحة. إنها آلة ترفض السماح للنقاش بأن يمر باعتباره قد تم تسويته عندما لا يكون كذلك، وهي تخبرك بالضبط أي خطوة فشلت.
فشل إضفاء الطابع الرسمي هو الناتج المفيد
عندما لا يقوم لين بإغلاق البرهان، فإنك تحصل على الهدف الدقيق الذي تبقى. وفي الممارسة العملية، فإن هذا يكاد يكون دائماً المكان الذي كانت فيه الحجة غير الرسمية تلوح بالأيدي ــ الخطوة التي كان كل من قرأ نسخة النثر ليهز رأسه قبلها. ثم يُسلَّم ذلك الهدف إلى أي مقعد يكون في أفضل وضع لمهاجمة ذلك الهدف، إلى جانب ما تم اختباره بالفعل، وليس أي شيء آخر. وتقوم النماذج بالهجوم عندما تجد نفسها عالقة، وتعيد صياغة نفسها بتكلفة كاملة؛ وعادة ما يفتح إتمام سؤال محدد واحد العائق مقابل جزء من الرموز.
العمل الطويل يبقى
إن كل مشكلة تحددها اللجنة تدخل في دفتر أستاذ مشترك مع دليلها، لذا فإن النتائج تُكتب مرة واحدة ولا يعاد استخلاصها أبدا، وتسجل المآزق بحيث لا يعود أحد إلى اللعب بها. وتجري المباريات على جانب الخادم وتوقف بشكل نظيف ــ بسبب الميزانية، أو بسبب انقطاع مقدم الخدمة، أو لأنك أغلقت العلامة ــ ثم تستأنف من حيث توقفت بالضبط.
ماذا لا يفعل هذا؟
النظرية هي كلمة استنتاجية. هذا الموقع بني للرياضيات، والمنطق، وعلوم الحاسوب النظرية، والفيزياء النظرية، والنظرية الاقتصادية - مجالات حيث يتم تسوية الادعاء من خلال البرهان. الأسئلة التجريبية في علم الأحياء، أو الطب، أو الكيمياء، أو العلوم الاجتماعية لا تنتج نظريات، بل تنتج نتائج، ولن يقررها أي قدر من الشكلية. موقعنا الشقيق referee.chat يدير نفس عملية الفريق والمحكم دون خطوة اللين، لتلك الأسئلة بالضبط.