تم اكتشاف الثغرة في ورقة Tao Zhexuan بواسطة الذكاء الاصطناعي ، وسيتحقق التنبؤ لمدة 26 عاما! تخمين اتجاه البحث من خلال النظر إلى اسم النظرية ، دعا الإله العظيم قدرة الذكاء الاصطناعي مذهلة

مصدر المادة: نيو تشييوان

في الآونة الأخيرة ، اكتشف Tao Zhexuan ، إله الرياضيات الذي يحرص على استخدام GPT-4 و Copilot لإجراء البحوث ، خطأ مخفيا في ورقته بمساعدة الذكاء الاصطناعي!

قال Tao Zhexuan أنه في عملية إضفاء الطابع الرسمي على الحجة في الصفحة 6 مع Lean4 ، وجد أن التعبيرات

عند n = 3 و k = 2 ، يكون في الواقع متباعدا.

تم اكتشاف هذا الخطأ غير الواضح في الوقت المناسب بفضل Lean4.

والسبب هو أن لين طلب منه بناء 02. نتيجة لذلك ، لا يمكن أن يعتمد Lean على 0 سالب

لحسن الحظ ، هذا مجرد خطأ بسيط لا يوجد إلا عندما تكون قيمة n صغيرة. في هذه المرحلة ، تحتاج فقط إلى تعديل بعض الثوابت في الورقة.

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

قال تاو تشيشوان إن هذا ممكن تماما.

ربما في المستقبل القريب ، يمكننا بناء طبقة الذكاء الاصطناعي فوق Lean.
من خلال وصف الخطوات الواردة في الدليل على الذكاء الاصطناعي ، يمكن الذكاء الاصطناعي استخدام Lean لتنفيذ الإثبات ، وفي هذه العملية يمكنه أيضا استدعاء حزم جبر الكمبيوتر المختلفة.

في يونيو من هذا العام ، توقع Tao Zhexuan في مدونة حول تجربة GPT-4 التجريبية -

في عام 2026 ، سيتم دمج الذكاء الاصطناعي مع أدوات البحث والرياضيات الرمزية لتصبح مؤلفا مشاركا موثوقا به في البحث الرياضي.

خلال هذه الفترة ، هناك أشخاص يواصلون إثبات ذلك. على سبيل المثال ، قام علماء من Caltech و NVIDIA و MIT ومؤسسات أخرى ببناء بروفير نظرية يعتمد على LLM مفتوح المصدر.

وقد مارسها Tao Zhexuan أيضا ، وبدأت كتابة الورقة الجديدة في GPT-4 ، وهتف مرارا وتكرارا - القدرة المذهلة ل GitHub Copilot تجعلني أشعر بعدم الارتياح!

**الذكاء الاصطناعي بركة الله بحوث الرياضيات **

في الآونة الأخيرة ، "دخل Tao Zhexuan تماما" حفرة الذكاء الاصطناعي.

بمساعدة GPT-4 ، بدأ في تعلم كتابة الأوراق وإجراء البحوث الرياضية باستخدام Lean4.

كان متحمسا جدا للعملية لدرجة أنه كان ينشر على Mastodon كل بضع ساعات لتسجيل ما تعلمه وخبراته.

في كتابة ورقة عن عدم المساواة في ماكلولين ، استخدم تاو على نطاق واسع أدوات الذكاء الاصطناعي مثل GPT-4 و Copilot و Lean4.

عنوان:

بينما نمضي قدما ، أكمل تاو إصلاح الحجة في القسم 2 من الورقة في Lean4.

ومع ذلك ، كانت العملية مملة أكثر مما توقع ، واستغرق كل سطر من الإثبات حوالي ساعة لإضفاء الطابع الرسمي.

خلال الأسبوع الأول من المشروع ، كان عنق الزجاجة هو افتقاره إلى الإلمام ببناء الجملة والأدوات اللينة. لكن عنق الزجاجة الحالي يكمن في الأدوات نفسها - ليست متقدمة مثل تلك الموجودة في حزم الجبر الحاسوبية.

على سبيل المثال ، في سطر واحد من ورقته ، يذكر أن عدم المساواة:

يمكن إعادة ترتيبها على النحو التالي:

بافتراض أن جميع المقامات موجبة ، فهذه مهمة سريعة جدا للحسابات اليدوية ويمكن إجراؤها بسهولة إلى حد ما في أي حزمة جبر كمبيوتر قياسية.

يحتوي Lean على أدوات تلقائية مفيدة للغاية للتعامل مع العمليات الخطية ، ولكن لا توجد حاليا أداة لتبسيط التعبيرات المعقدة التي تتضمن الأسس تلقائيا.

لذلك ، يتعين علينا التعامل مع القانون الأسي والعمليات الأخرى المذكورة أعلاه خطوة بخطوة ، وهذه العملية تستغرق وقتا طويلا للغاية.

في النهاية ، قرر تاو عدم استخدام التدوين المقارب في هذا الجزء من الحجة ، ولكن لتأسيس عدم مساواة مع ثابت محدد C:

وفيه

في البداية ، اعتقد تاو أنه سيكون من "الأبسط" إثبات عدم المساواة بقيم مثل C = 7. ومع ذلك ، كان من المرهق استخدام الأدوات الحالية لإثبات C≤7 بدقة ، لذلك تم التخلي عن الفكرة لصالح قيمة C التشغيلية بشكل رسمي. تم تحديده الآن ، القيمة حوالي 6.16.

في هذا الصدد ، سأل بعض مستخدمي الإنترنت الفضوليين ، "كيف يفعل الذكاء الاصطناعي في إثبات السرعة مقارنة بحساب اليد؟"

قال تاو تشيشوان إنه بناء على ملاحظاته الخاصة ، فإن أنواع المهام الميكانيكية لحزم الجبر الحاسوبي والآلات الحاسبة ليست بالضرورة ميكانيكية لمساعدي الإثبات الرسميين.

ولكن مع ظهور LLMs ، يجب أن نكون قادرين على توحيد جميع الأدوات بمساعدة الكمبيوتر في أداة واحدة عالمية سهلة الاستخدام. وسيكون لهذه الأداة جميع مزايا كل مكون.

حتى في المستقبل القريب ، يمكننا أيضا تصور بناء طبقة الذكاء الاصطناعي فوق Lean -

يتم وصف الخطوات الواردة في الدليل إلى الذكاء الاصطناعي في "اللغة الإنجليزية الرياضية" ، ويمكن الذكاء الاصطناعي بعد ذلك محاولة تنفيذها باستخدام Lean ، وربما استدعاء حزمة جبر الكمبيوتر في هذه العملية.

** يمكن لمساعد الطيار تخمين الخطوات التالية **

في السابق ، في هذه الورقة حول أبحاث عدم المساواة في McLaughlin ، فوجئ Tao Zhexuan عندما وجد أن Copilot كان قادرا على التنبؤ بما يريد القيام به بعد ذلك!

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

هذا جعل تاو تشيشوان يهتف مرارا وتكرارا: إنه أمر لا يصدق!

في عملية إثبات النظرية 1.3 في الورقة ، استخدم Tao Zhexuan Lean4 لإكمال إضفاء الطابع الرسمي على إثبات النظرية.

في الورقة ، هناك صفحة واحدة فقط في عملية الإثبات ، لكن الدليل الرسمي يستخدم 200 سطر من Lean4.

على سبيل المثال ، في الورقة ، يفترض Tao Zhexuan فقط

محدب على أي عدد حقيقي من a>0 وتسمى متباينة جنسن بعد ذلك. لكن الكود يستغرق حوالي 50 سطرا.

في هذه العملية ، أظهر GitHub Copilot جميع أنواع التنبؤات الإلهية ، وتنبأ بطريقة سحرية بالاتجاه التالي لبحث Tao Zhexuan.

تسمح له استراتيجية إعادة كتابة لين بمراجعة الافتراضات أو الأهداف المطولة من خلال البدائل المستهدفة.

هذه الميزة مهمة للغاية لأنها تسمح للأشخاص بمعالجة هذه التعبيرات بحرية دون الحاجة إلى إدخالها بالكامل طوال الوقت.

نسبيا ، في LaTex ، هذه العملية أكثر تعقيدا.

قال Tao Zhexuan إنه بحاجة إلى محاكاة استراتيجية إعادة كتابة Lean4 تقريبا ، وإجراء تعديلات مستهدفة على التعبيرات الطويلة من سطر إلى آخر من خلال عمليات مثل القص واللصق. يمكن أن يتسبب ذلك في انتشار الأخطاء الإملائية عبر أسطر متعددة في المستند.

يمكن ل Lean4 القيام بإعادة الكتابة هذه بطريقة آلية ويمكن التحقق منها.

بالطبع ، Lean 4 ليس حلا سحريا في الوقت الحالي ، وهناك بعض القيود. على سبيل المثال ، إعادة كتابة التعبيرات التي تتضمن متغيرات القيد ليست سهلة دائما.

قال Tao Zhexuan إنه يتطلع إلى الوقت الذي يكون فيه من السهل استخدام اللغة الطبيعية لمطالبة LLM بإجراء مثل هذا التحويل.

** في الحفرة GPT-4 + مساعد الطيار GitHub ، مجنون امواى **

في وقت مبكر من بداية شهر سبتمبر ، نشر Tao Zhexuan منشورا يشيد بتأثير ChatGPT في إنشاء كود Python - مما يوفر عبء العمل لمدة نصف ساعة مباشرة!

كتجربة ، طلب من ChatGPT كتابة جزء من كود بايثون يحسب الطول M (n) لأطول متتالية فرعية تبلغ 1,...,n لكل عدد طبيعي n ، حيث لا ينخفض φ دالة أويلر كلي القدرة.

على سبيل المثال ، M (6) = 5 لأن φ لا يتناقص في 1،2،3،4،5 (أو 1،2،3،4،6) ولكن ليس على 1،2،3،4،5،6.

ومن المثير للاهتمام ، أنه أنشأ جزءا بارعا للغاية من التعليمات البرمجية لحساب الوظائف الكلية القدرة ، والتي كانت بارعة للغاية لدرجة أن تاو اضطر إلى التحديق فيها لعدة دقائق قبل أن يفهم ما هو المبدأ الكامن وراء الكود.

بالطبع ، هذا الرمز متحيز أيضا - فهو يأخذ في الاعتبار فقط التسلسلات الفرعية للأعداد الصحيحة المستمرة ، وليس التسلسلات الفرعية التعسفية.

ومع ذلك ، هذا قريب بما فيه الكفاية ، باستخدام هذا الرمز الأولي الذي تم إنشاؤه بواسطة ChatGPT كنقطة انطلاق ، قام Tao Zhexuan أخيرا بإنشاء الرمز الذي يريده يدويا ، مما وفر له حوالي نصف ساعة من العمل.

نظرا لأن النتائج التي قدمها ChatGPT جيدة جدا ، قال Tao Zhexuan إنه سيستخدمها كثيرا في المستقبل لتوفير رمز أولي لحسابات مماثلة.

سرعان ما نشر Tao Zhexuan مرة أخرى أنه دخل GitHub Copilot بموجب توصية من مستخدمي الإنترنت!

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

يحتاج Tao Zhexuan فقط إلى إجراء تعديلات طفيفة على هذه الاقتراحات ، ويمكنه إكمالها في أقل من نصف الوقت المخطط له في الأصل.

في أكتوبر ، وجد Tao Zhexuan أنه على الرغم من أن GPT-4 لم يتمكن من تقديم مساعدة مباشرة للعبة ، عندما بدأ في استخدام Lean ، أصبح GPT-4 مفيدا للغاية.

عندما تصبح المستويات أكثر صعوبة ، يبدأ دور GPT في إظهار نفسه.

في الحالات التي يكون فيها من الواضح أن Z هي نتيجة X و Y ، فإن سؤال GPT "كيف يمكنني إثبات Z إذا كنت أعرف بالفعل X و Y؟" يمكن أن يحل جميع أنواع المشكلات النحوية الدقيقة في هذه العملية.

بالإضافة إلى المحتوى المرتبط بالمهنية ، وجد Tao Zhexuan أنه يمكنه استخدام DALL · E 3 وبدأت اللعب على الفور.

** Netizen: ماجستير في القانون يمكن أن يجعل الناس ممتازة 10000 مرة أفضل **

كما أثارت حقيقة أن الإله العظيم مهووس بأدوات الذكاء الاصطناعي في البحث الرياضي مناقشات ساخنة بين مستخدمي الإنترنت.

قال بعض الناس أن أوكامي بدأ تعلم Lean4 بمساعدة GPT-4 في وقت سابق من هذا الشهر ، ومن وقت لآخر سيسجل تقدمه في التعلم على المستودون.

كما يظهر أنه بالنسبة للأشخاص الأكثر نجاحا ، يمكن ل LLMs تسريع عملهم.

يقول بعض الناس أنه حتى الأشخاص الذين لا يستطيعون كتابة التعليمات البرمجية ، طالما أنهم متواصلون جيدون في LLM ، يمكنهم أتمتة الوظائف بسرعة.

ومع ذلك ، إذا كان بإمكان الأفراد ذوي المهارات العالية فقط استخدام LLMs بشكل فعال ، فإن النتيجة هي أن عدم المساواة بين الناس قد يزداد.

تقدم شخص ما على الفور ليقول إن هذا صحيح ، ولم يستطع صديقه كتابة أي شيء باستثناء صيغ Excel ، ولكن الآن ، يمكنه كتابة تطبيقات Python باستخدام GPT-4!

بصفته مبرمجا يتمتع بخبرة 30 عاما في التطوير ، يحتاج أيضا إلى التوسل إليه لتعليمه هذه التكنولوجيا.

ربما يرجع نجاحه إلى قدرته على التواصل مع LLMs.

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

بالنسبة للنخبة ، قد يحصلون على دفعة 100 ضعف من LLMs ، وبالنسبة لكبار المهندسين ، فهي حوالي 10,000 ضعف التعزيز.

موارد:

شاهد النسخة الأصلية
قد تحتوي هذه الصفحة على محتوى من جهات خارجية، يتم تقديمه لأغراض إعلامية فقط (وليس كإقرارات/ضمانات)، ولا ينبغي اعتباره موافقة على آرائه من قبل Gate، ولا بمثابة نصيحة مالية أو مهنية. انظر إلى إخلاء المسؤولية للحصول على التفاصيل.
  • أعجبني
  • تعليق
  • مشاركة
تعليق
0/400
لا توجد تعليقات
  • تثبيت