تعلم إثبات النظريات من خلال تعلم إنشاء النظريات

نعتبر مهمة إثبات النظريات التلقائي، وهي مهمة رئيسية في الذكاء الاصطناعي. أظهر التعلم العميق إمكانات كبيرة في تدريب أدوات إثبات النظريات، لكن هناك قلة محدودة من النظريات والبراهين المكتوبة يدويًا التي يمكن استخدامها في التعلم المراقب. وللتغلب على هذه القيود، نقترح تعلُّم مُولِّد عصبي يُولِّد تلقائيًا نظريات وبراهين بهدف تدريب أدوات إثبات النظريات. أظهرت التجارب على مهام واقعية أن البيانات الاصطناعية الناتجة عن منهجيتنا تُحسّن أداء أدوات إثبات النظريات، وتساهم في تقدُّم حالة الفن في إثبات النظريات التلقائي في منصة Metamath. يمكن الوصول إلى الكود عبر الرابط: https://github.com/princeton-vl/MetaGen.