لا يصدق هذا الاسمغاوسيشعر وكيل الذكاء الاصطناعي الجديد (جاوس) بالجنون بعض الشيء. لأنه يستخدم فقطثلاثة أسابيعالوقت، لقد تم ذلكتيرينس تاووالتحدي الرياضي الذي يواجهه Alex Kontorovich المتمثل في إضفاء الطابع الرسمي على نظرية الأعداد الأولية (PNT) في Lean.
كما تعلمون، بعد أن اقترح تاو زيكسوان وكونتوروفيتش هذا التحدي في يناير 2024، أمضوا الكثير من الوقت18 شهرا(يوليو من هذا العام)، لم يتحقق سوى التقدم المرحلي.
فما هو أصل هذا غاوس؟
وخلفها شركة اسمهاالرياضياتشركة الذكاء الاصطناعي، وفقًا للتقارير، فإن غاوس هو أول من ساعد كبار علماء الرياضيات في التحقق الرسميإضفاء الطابع الرسمي التلقائي(إضفاء الطابع الرسمي) الوكيل:
يشير إضفاء الطابع الرسمي هنا إلى تحويل المحتوى الرياضي الذي يكتبه البشر إلى لغة رسمية قابلة للقراءة آليًا وقابلة للفحص وصارمة ولا لبس فيها، ثم استخدام أجهزة الكمبيوتر للمساعدة في التحقق من صحتها.
السبب وراء إحراز تاو زيكسوان وأليكس كونتوروفيتش تقدمًا تدريجيًا حتى الآن هو أن المشكلة عالقة في المشكلة الأساسية المتمثلة في التحليل المعقد.
كحياة قائمة على السيليكون، يتميز جهاز غاوس هذا بقدرته على العمل دون توقف، مما يقلل بشكل كبير من عبء العمل الذي لم يتمكن من إكماله إلا كبار الخبراء الرسميين في الماضي؛ وفي الوقت نفسه، قام غاوس أيضًا بإضفاء الطابع الرسمي على النتائج الرئيسية المفقودة في التحليل المعقد المذكور أعلاه.
ولهذا السبب يمكنه حل التحدي الرياضي الذي فشل تيرينس تاو في إكماله خلال 18 شهرًا في ثلاثة أسابيع.
كيف يتم تنفيذ غاوس؟
في الوقت الحاضر، لم تصدر شركة Math رسميًا تقريرًا فنيًا محددًا.
ولكن انطلاقًا من النتيجة النهائية، أنشأ غاوس ما يقرب من 25000 سطرًا من أكواد Lean، تحتوي على آلاف النظريات والتعريفات.
كما تعلمون، غالبًا ما تستغرق البراهين الرسمية لهذا المقياس سنوات عديدة لإكمالها.
إن أكبر المشاريع الرسمية الفردية في التاريخ (التي تمتد غالبًا حتى 10 سنوات) هي أكبر من ذلك بكثير (ما يصل إلى 500000 سطر من التعليمات البرمجية).
بالمقارنة، تحتوي مكتبة الرياضيات القياسية التابعة لشركة Lean Mathlib على حوالي 2 مليون سطر من التعليمات البرمجية وتحتوي على 350.000 نظرية، لكن بناءها استغرق أكثر من 600 مساهم لمدة 8 سنوات.
من أجل دعم تشغيل Gauss، تعاون الفريق أيضًا مع Morph Labs لتطوير البنية التحتية لبيئة Trinity.
لأن تشغيل Gauss على هذا النطاق الواسع سيتطلب آلاف الوكلاء المتزامنين، ولكل وكيل بيئة تشغيل Lean خاصة به، والتي ستستهلك عدة تيرابايت من الذاكرة العنقودية، مما يجعل الأمر تحديًا هندسيًا معقدًا للغاية.
وذكر فريق الرياضيات أيضًا:
سوف يقلل غاوس بشكل كبير من الوقت اللازم لإكمال مشاريع الرياضيات الكبيرة.
ومع استمرار التحسين في الخوارزميات، نخطط لزيادة إجمالي كمية التعليمات البرمجية الرسمية بمقدار 100 إلى 1000 مرة في الأشهر الـ 12 المقبلة.
وسيكون هذا بمثابة أرض التدريب لنماذج جديدة - نحو "الذكاء الفائق الذي يمكن التحقق منه" و"علماء الرياضيات الآليين العموميين".
والآن فقط،تيرينس تاولقد شرحت بعض القضايا المتعلقة بإضفاء الطابع الرسمي على Mastodon (ما يلي هو بيان Tao Zhexuan).
تميل المشاريع مهما كانت درجة تعقيدها إلى أن تكون لها أهداف صريحة وأهداف ضمنية غير معلنة. على سبيل المثال، قد يكون الهدف المعلن لمشروع إضفاء الطابع الرسمي على اللين هو الحصول على دليل رسمي لبعض الافتراضات الرياضية …؛ تعلم كيفية استخدام مجموعة متنوعة من الأدوات التعاونية وتعيين المهام؛ اكتشاف عضويا البنية الدقيقة للبراهين
في الماضي، لم يكن من الضروري في كثير من الأحيان توضيح هذه الأهداف الضمنية لأنه كان هناك ارتباط تجريبي قوي بين تحقيق هذه الأهداف وتحقيق الأهداف الصريحة. في حالة المشاريع الرسمية، فإن أي جهد يتمحور حول الإنسان لتحقيق أهداف واضحة سيحقق في النهاية وبشكل طبيعي معظم الأهداف الضمنية المذكورة أعلاه. وبالتالي، تصبح الأهداف الواضحة بديلاً قابلاً للتطبيق للأهداف العملية الأوسع.
ومع ذلك، فإن الأمور تتغير مع ظهور أدوات الذكاء الاصطناعي القوية التي تتبع أساليب مختلفة تمامًا عن البشر. ويمكن توجيه هذه الأدوات لحل هدف صريح دون الحاجة إلى تحقيق جميع الأهداف الضمنية التي يمكن تحقيقها في وقت واحد إذا تم تنفيذ المهمة من قبل فريق بشري. في الواقع، فإن طبيعة خوارزميات تحسين الذكاء الاصطناعي تملي أنها قد تحقق أداءً عاليًا في تحقيق أهداف واضحة على حساب جميع الأهداف الضمنية. (انظر قانون جودهارت: "عندما يصبح المقياس هدفًا، فإنه يتوقف عن أن يكون مقياسًا جيدًا.")
ونظرًا للنشر المتزايد لهذه الأدوات، فإن هذا يوحي لي أن منظمي المشروع بحاجة الآن إلى بذل جهد أكبر لتوضيح جميع أهداف المشروع بوضوح، وليس فقط الأهداف الاسمية. في بعض الحالات، قد لا تكون هذه الأهداف واضحة في البداية للمنظمين أنفسهم وقد تتطلب بعض المناقشة بين المشاركين. يجب على الأطراف الخارجية المهتمة باختبار مثل هذه المشاريع باستخدام أدوات الذكاء الاصطناعي الخاصة بها التنسيق مع المنظمين مسبقًا في حالة فشلهم في تحقيق هدف أو أكثر من الأهداف الضمنية الرئيسية التي لن تتمكن أدواتهم من تحسينها.
المؤسس هو مؤلف جائزة اختبار الزمن ICML’25
ومن الجدير بالذكر أن رئيس شركة الرياضيات يتمتع أيضًا ببعض القوة.
لأنه أحد مؤلفي الورقة التي فازت بجائزة ICML Time Test في مؤتمر الذكاء الاصطناعي لهذا العام.كريستيان سيجيدي.
هذه الورقة هي تطبيع الدفعة (تطبيع الدفعة، يشار إليها باسم BatchNorm) التي اقترحها هو ومؤلف آخر سيرجي لوف في عام 2015.
واليوم، تم الاستشهاد بهذه الورقة أكثر من 60.000 مرة. إنه إنجاز بارز في تاريخ تطوير التعلم العميق وقد عزز بشكل كبير تدريب وتطبيق الشبكات العصبية العميقة.
ويمكن القول إنها إحدى التقنيات الرئيسية التي تسمح للتعلم العميق بالانتقال من التجارب الصغيرة إلى التطبيق العملي والموثوقية على نطاق واسع.
بالطبع، على الرغم من هتاف مستخدمي الإنترنت بعد قراءة غاوس، فقد طالبوا المسؤول أيضًا بإصدار الصحيفة بسرعة.
أما بالنسبة للمحتوى الفني الأكثر تفصيلاً، فيمكننا إلقاء نظرة ~