في عالمٍ يتطور بسرعة، تقدم نماذج اللغات الضخمة (Large Language Models) خطوات جديدة نحو الثورة الرياضية. في دراسة جديدة منشورة على موقع arXiv، تم تسليط الضوء على قدرة هذه النماذج على اكتشاف نظريات جديدة وإنتاج براهين موثوقة.

تعتمد الدراسة على سلسلة من العمليات تسمى "حلقة التخمين والإثبات" (Conjecturing-Proving Loop) والتي تهدف إلى توليد افتراضات رياضية ومحاولة إثباتها باستخدام أداة Lean 4. يتميز هذا النظام الجديد بأن كل مرحلة تعتمد على النظريات التي تم توليدها سابقًا وبراهينها، مما يمكن النموذج من تحسين استراتيجيات الإثبات بطريقة فعالة ودون الحاجة لضبط المعلمات.

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

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