اختيار المقدمات لبرهان النظريات بواسطة التضمين الرسومي العميق

نقترح نهجًا يستند إلى التعلم العميق لمشكلة اختيار المقدمات: وهو اختيار العبارات الرياضية ذات الصلة لإثبات حدس معين. نمثل صيغة المنطق من الرتب العليا كرسم بياني ثابت تجاه إعادة تسمية المتغيرات ولكنه يحافظ تمامًا على المعلومات النحوية والدلالية. ثم نقوم بتمثيل هذا الرسم البياني في متجه عبر طريقة تمثيل جديدة تحافظ على معلومات ترتيب الحواف (edges). لقد حقق نهجنا أفضل النتائج الحالية في مجموعة بيانات HolStep، حيث تم تحسين دقة التصنيف من 83% إلى 90.3%.