نمذجة اللغة التوليدية لإثبات النظرية التلقائي

نستكشف تطبيق نماذج اللغة المستندة إلى المحولات (transformer-based language models) في إثبات النظريات التلقائي. تُحفَّز هذه الدراسة على احتمال أن يكون أحد القيود الرئيسية التي تُعاني منها أدوات إثبات النظريات التلقائي مقارنة بالبشر — وهي توليد مصطلحات رياضية أصلية — قابلاً للحل من خلال التوليد باستخدام نماذج اللغة. نقدّم أدوات إثبات تلقائيّة ومساعد إثبات، تُسمى GPT-f، مصمّمة للغة الترميز الرمزي Metamath، ونحلّل أداؤها. وقد وجدت GPT-f أدلة قصيرة جديدة تم قبولها في المكتبة الرئيسية لـ Metamath، وهو ما نعتقد أنه لأول مرة يساهم نظام مبني على التعلم العميق بإثباتات تم اعتمادها من قبل مجتمع رياضيات رمزية رسمية.