Formal Proofs of Numerical Stability in Lean 4

Abstract

Κύριος στόχος της εργασίας είναι η κατασκευή της NumStability, μιας εξειδικευμένης βιβλιο- θήκης στη Lean 4 για την τυπική απόδειξη θεωρημάτων αριθμητικής σταθερότητας αλγορίθμων κινητής υποδιαστολής. Μαθηματικό σημείο αναφοράς είναι το βιβλίο του N. J. Higham Accuracy and Stability of Numerical Algorithms· η NumStability τυποποιεί επιλεγμένο υλικό από καθένα από τα 28 κεφάλαιά του και το οργανώνει σε επαναχρησιμοποιήσιμη υποδομή. Η βιβλιοθήκη κατασκευάστηκε κυρίως με το Codex της OpenAI και σποραδικά με το Claude της Anthropic. Η εργασία καταγράφει τις αδυναμίες μιας αρχικής αρχάριας τυποποίησης του βιβλίου, τις ανθρώπινες αποφάσεις που τις διόρθωσαν, την κατάτμηση ανά κεφάλαιο, τα skills και την αναδιοργάνωση που οδήγησε στην έκδοση higham_v01. Το HighamBench εξετάζει αν η πρόσβαση στη βιβλιοθήκη μειώνει το κόστος νέων αποδεί- ξεων για έναν πράκτορα ΤΝ, συγκρίνοντας τη συνθήκη N (Lean και Mathlib) με τη συνθήκη L (επιπλέον η NumStability). Στο HighamBench-Proof οι στόχοι δίνονται ήδη τυποποιημένοι ως σταθερές δηλώσεις Lean: ο πράκτορας αποδεικνύει 30 τέτοιους στόχους από 25 άρθρα. Στο HighamBench-E2E οι στόχοι προέρχονται από φυσική μαθηματική γλώσσα: ο πράκτορας διατυ- πώνει σε Lean δέκα αποτελέσματα από πέντε πηγές, με έλεγχο πιστότητας από ανεξάρτητους κριτές βασισμένους σε γλωσσικά μοντέλα, και έπειτα τα αποδεικνύει. Το κέρδος αυξάνεται μαζί με την πραγματική χρήση δηλώσεων της βιβλιοθήκης στις αποδείξεις: ο συντελεστής Spearman μεταξύ χρήσης και κέρδους χρόνου απόδειξης είναι +0,69 και +0,56 αντίστοιχα, και μεταξύ χρή- σης και μείωσης των γραμμών κώδικα +0,61 για το πλήρες υποβληθέν αρχείο και +0,64 για την απόδειξη, αντίστοιχα. Η επικάλυψη της βιβλιοθήκης με τα άρθρα αριθμητικής σταθερότητας ήταν όμως περιορισμένη: μόνο 9 από τα 25 άρθρα πρόσφεραν αποτέλεσμα για το οποίο αναμενόταν βοήθεια, και σε 17 από τους 30 σταθερούς στόχους η βιβλιοθήκη δεν χρησιμοποιήθηκε καθόλου. Η γνώση της βιβλιοθήκης είναι επομένως στενή, αλλά όπου υπάρχει επικάλυψη τα αποτελέσματα είναι θετικά. Η βιβλιοθήκη είναι το πρώτο στάδιο ενός απώτερου στόχου: ενός γενικού συστήματος τυ- ποποίησης βιβλίων με πράκτορες ΤΝ, στο οποίο ένα skill τυποποίησης παράγει τη βιβλιοθήκη και ενημερώνεται από τις καταγραφές των εκτελέσεων και από ανθρώπινες διορθώσεις, ενώ ένα benchmark μετρά τη χρησιμότητά της.