Η Mistral AI Λανσάρει τον Leanstral, Ανοιχτού Κώδικα Πράκτορα Απόδειξης για το Lean 4

Zach Anderson 16 Μαρ 2026 19:13

Η Mistral κυκλοφορεί τον Leanstral, έναν AI πράκτορα 6B παραμέτρων για την επίσημη επαλήθευση Lean 4, ξεπερνώντας μεγαλύτερα μοντέλα σε κόστος 1/15 με άδεια Apache 2.0.

Η Mistral AI κυκλοφόρησε τον Leanstral στις 16 Μαρτίου 2026—τον πρώτο AI πράκτορα ανοιχτού κώδικα που κατασκευάστηκε ειδικά για την επίσημη επαλήθευση Lean 4. Το μοντέλο 120B παραμέτρων λειτουργεί με μόλις 6B ενεργές παραμέτρους και διατίθεται με άδεια Apache 2.0, καθιστώντας την απόδειξη θεωρημάτων επαγγελματικού επιπέδου προσβάσιμη χωρίς επιχειρηματικούς προϋπολογισμούς.

Γιατί αυτό έχει σημασία για τα κρυπτονομίσματα; Η επίσημη επαλήθευση—μαθηματική απόδειξη ότι ο κώδικας κάνει ακριβώς αυτό που ισχυρίζεται—έχει γίνει το χρυσό πρότυπο για την ασφάλεια έξυπνων συμβολαίων και πρωτοκόλλων blockchain. Σφάλματα στον κώδικα DeFi έχουν κοστίσει δισεκατομμύρια. Ο Leanstral θα μπορούσε να μειώσει δραματικά το εμπόδιο για έργα που αναζητούν επαληθευμένη ασφάλεια.

Αντισταθμίσεις Απόδοσης έναντι Κόστους

Η Mistral αξιολόγησε τον Leanstral έναντι τόσο ιδιόκτητων όσο και ανοιχτού κώδικα ανταγωνιστών χρησιμοποιώντας το FLTEval, μια νέα σουίτα αξιολόγησης που δοκιμάζει πραγματικές εργασίες μηχανικής απόδειξης από το έργο διατύπωσης του Τελευταίου Θεωρήματος του Fermat.

Οι αριθμοί είναι εντυπωσιακοί. Ο Leanstral στο pass@2 σημείωσε 26,3 πόντους για $36 σε κόστος υπολογισμού. Το Claude Sonnet 4.6 κατάφερε 23,7 πόντους αλλά συγκέντρωσε λογαριασμό $549—πάνω από 15 φορές το κόστος για χειρότερη απόδοση. Ακόμα και στο pass@16, όπου ο Leanstral φτάνει 31,9 πόντους για $290, εξακολουθεί να κοστίζει λιγότερο από το ένα πέμπτο της τιμής $1.650 του Claude Opus 4.6 (αν και το Opus προηγείται σε ποιότητα με 39,6).

Έναντι εναλλακτικών ανοιχτού κώδικα, το χάσμα απόδοσης διευρύνεται περαιτέρω. Τα GLM5-744B-A40B και Kimi-K2.5-1T-A32B σταθεροποιούνται γύρω στους 16-20 πόντους παρά το ότι έχουν 6-8 φορές περισσότερες ενεργές παραμέτρους. Το Qwen3.5-397B-A17B χρειάζεται τέσσερις προσπάθειες για να φτάσει τους 25,4 πόντους—ο Leanstral το ξεπερνά με δύο.

Τεχνική Αρχιτεκτονική

Ο Leanstral χρησιμοποιεί μια αραιή αρχιτεκτονική μείγματος εμπειρογνωμόνων βελτιστοποιημένη για ροές εργασίας μηχανικής απόδειξης. Το μοντέλο ενσωματώνεται με το πρωτόκολλο διακομιστή γλώσσας του Lean μέσω MCP (Model Context Protocol), ειδικά εκπαιδευμένο για μέγιστη απόδοση με εργαλεία lean-lsp-mcp.

Το ίδιο το Lean 4 κυκλοφόρησε σταθερό τον Σεπτέμβριο του 2023 και έχει δει ταχεία υιοθέτηση για την επισημοποίηση των μαθηματικών. Η βιβλιοθήκη Mathlib—μια τεράστια συλλογή μαθηματικών αποδείξεων—μεταφέρθηκε επιτυχώς στο Lean 4 το ίδιο έτος. Έργα όπως η επίσημη απόδειξη του Τελευταίου Θεωρήματος του Fermat αποδεικνύουν την ικανότητα της πλατφόρμας για σοβαρή μαθηματική εργασία.

Εφαρμογές Πραγματικού Κόσμου

Η Mistral παρουσίασε τον Leanstral να χειρίζεται μια γνήσια ερώτηση αποσφαλμάτωσης Stack Exchange σχετικά με διακοπτικές αλλαγές στο Lean 4.29.0-rc6. Ο πράκτορας διέγνωσε ένα ζήτημα ορισμικής ισότητας με ψευδώνυμα τύπων και εντόπισε σωστά ότι η αντικατάσταση του def με abbrev θα αποκαθιστούσε την αντιστοίχιση τακτικής.

Το μοντέλο επίσης επέδειξε μετάφραση μεταξύ γλωσσών, μετατρέποντας ορισμούς Rocq (πρώην Coq) σε Lean 4 διατηρώντας τη σημασιολογία απόδειξης και εφαρμόζοντας προσαρμοσμένη σημειογραφία.

Επιλογές Πρόσβασης

Υπάρχουν τρεις διαδρομές ανάπτυξης: άμεση ενσωμάτωση στο Mistral Vibe (χρησιμοποιήστε /leanstall για να ξεκινήσετε), ένα δωρεάν τελικό σημείο API στο labs-leanstral-2603 για περιορισμένη συλλογή σχολίων, ή αυτόνομη ανάπτυξη με τα βάρη Apache 2.0.

Για έργα blockchain, ο υπολογισμός είναι απλός. Η επίσημη επαλήθευση παραδοσιακά απαιτούσε είτε ακριβές εταιρείες ελέγχου είτε βαθιά εσωτερική εμπειρία. Ένας πράκτορας ανοιχτού κώδικα που μπορεί να αποδείξει την ορθότητα του κώδικα σε $36-290 ανά εργασία θα μπορούσε να αναμορφώσει τον τρόπο με τον οποίο τα πρωτόκολλα προσεγγίζουν την ασφάλεια—υποθέτοντας ότι οι αποδείξεις ανταποκρίνονται υπό συνθήκες παραγωγής.

• mistral ai
• leanstral
• lean 4
• επίσημη επαλήθευση
• ανοιχτός κώδικας