Η ταχεία επέκταση των επίσημων βιβλιοθηκών μαθηματικών απαιτεί αναδιάρθρωση επαληθευμένων αποδείξεων για συντηρησιμότητα και βελτίωση δεδομένων εκπαίδευσης νευρωνικών αποδεικτών. Ωστόσο, η κλιμακούμενη βελτιστοποίηση αποδείξεων παρεμποδίζεται από σπάνια δεδομένα και υψηλό κόστος εκπαίδευσης/συμπερασμάτων. Για την αντιμετώπιση αυτών των προκλήσεων, παρουσιάζεται το ImProver 2, ένα νευροσυμβολικό πλαίσιο για αυτοματοποιημένη βελτιστοποίηση αποδείξεων στο Lean 4.
Το ImProver 2 συνδυάζει αποδοτική ως προς τα δεδομένα διαδικασία επανάληψης ειδικών με σκελετό που εκθέτει επίσημη δομή και ελαφριές άτυπες αφαιρέσεις. Εισάγεται επίσης σειρά μετρικών για δομικές ιδιότητες αποδείξεων.
Με το ImProver 2, εκπαιδεύτηκε μοντέλο 7 δισεκατομμυρίων παραμέτρων, το οποίο υπερτερεί κατά πολύ μεγαλύτερων μοντέλων της ίδιας οικογένειας και ανταγωνίζεται πρωτοποριακά μοντέλα μεσαίου επιπέδου σε όλες τις μετρικές. Ο νευροσυμβολικός σκελετός του βελτιώνει επίσης σημαντικά την απόδοση σε μικρά και πρωτοποριακά μοντέλα.
Με κατάλληλο σκελετό και εκπαίδευση, μικρά μοντέλα αναδιαρθρώνουν αποτελεσματικά αποδείξεις ερευνητικού επιπέδου βάσει πολύπλοκων μετρικών, ανταγωνιζόμενα μεγαλύτερα συστήματα και καθιστώντας τη βελτιστοποίηση αποδείξεων κλιμακούμενη, εκπαιδεύσιμη εργασία.
