Privacy Coins
DeepSeek: Νέο Ανοιχτό AI Μοντέλο από την Κίνα
Η DeepSeek λανσάρει το Prover V2, ένα νέο ανοιχτό AI μοντέλο για επαλήθευση μαθηματικών αποδείξεων, προσφέροντας προσβασιμότητα και καινοτομία.
Η κινεζική εταιρεία ανάπτυξης τεχνητής νοημοσύνης DeepSeek παρουσίασε ένα νέο μεγάλο γλωσσικό μοντέλο (LLM) ανοιχτού κώδικα. Το νέο μοντέλο, γνωστό ως Prover V2, αναρτήθηκε στην πλατφόρμα Hugging Face στις 30 Απριλίου. Διατίθεται υπό την άδεια ανοιχτού κώδικα MIT και στοχεύει στην επαλήθευση μαθηματικών αποδείξεων.
Προδιαγραφές και Δυνατότητες
Το Prover V2 διαθέτει 671 δισεκατομμύρια παραμέτρους, καθιστώντας το σημαντικά μεγαλύτερο από τους προκατόχους του, Prover V1 και Prover V1.5. Στην πρώτη του έκδοση, το μοντέλο εκπαιδεύτηκε να μεταφράζει προβλήματα μαθηματικών διαγωνισμών σε τυπική λογική χρησιμοποιώντας τη γλώσσα προγραμματισμού Lean 4. Οι προγραμματιστές επισημαίνουν ότι το Prover V2 συμπιέζει τη μαθηματική γνώση σε μορφή που επιτρέπει τη δημιουργία και επαλήθευση αποδείξεων, συμβάλλοντας στην έρευνα και την εκπαίδευση.
Τεχνικές Λεπτομέρειες
Ένα μοντέλο, συχνά αναφερόμενο λανθασμένα ως “weights” στον χώρο της AI, είναι το αρχείο ή η συλλογή αρχείων που επιτρέπει την τοπική εκτέλεση μιας AI χωρίς εξωτερικούς διακομιστές. Τα σύγχρονα LLMs απαιτούν υλικό που οι περισσότεροι δεν διαθέτουν, λόγω του μεγάλου αριθμού παραμέτρων που απαιτούν πολύ RAM ή VRAM και επεξεργαστική ισχύ. Το Prover V2 έχει μέγεθος περίπου 650 gigabytes και αναμένεται να εκτελείται από RAM ή VRAM.
Προσβασιμότητα και Καινοτομίες
Για να μειωθεί το μέγεθός του, οι παράμετροι του Prover V2 έχουν ποσοτικοποιηθεί σε ακρίβεια 8-bit, μειώνοντας το μέγεθος στο μισό από το συνηθισμένο 16-bit. Το Prover V1 βασίστηκε στο μοντέλο DeepSeekMath με επτά δισεκατομμύρια παραμέτρους και εκπαιδεύτηκε με συνθετικά δεδομένα. Το Prover V1.5 βελτίωσε την ακρίβεια και την εκτέλεση. Μέχρι στιγμής, οι βελτιώσεις του Prover V2 δεν έχουν δημοσιευθεί.
Σημασία των Ανοιχτών Μοντέλων
Η δημόσια διάθεση των παραμέτρων των LLMs είναι αμφιλεγόμενη. Από τη μία, επιτρέπει στο κοινό να έχει πρόσβαση στην AI χωρίς εξάρτηση από ιδιωτικές υποδομές. Από την άλλη, η εταιρεία δεν μπορεί να αποτρέψει την κατάχρηση του μοντέλου. Η διάθεση του R1 προκάλεσε ανησυχίες ασφαλείας, ενώ υποστηρικτές του ανοιχτού κώδικα χαιρέτησαν την κίνηση της DeepSeek.
Προσβάσιμα Γλωσσικά Μοντέλα
Χάρη σε τεχνικές όπως η απόσταξη μοντέλων και η ποσοτικοποίηση, ακόμα και χρήστες χωρίς υπερυπολογιστές μπορούν να εκτελούν LLMs τοπικά. Η απόσταξη περιλαμβάνει την εκπαίδευση ενός μικρότερου “μαθητή” μοντέλου να αναπαράγει τη συμπεριφορά ενός μεγαλύτερου “δασκάλου”, ενώ η ποσοτικοποίηση μειώνει την αριθμητική ακρίβεια για μείωση μεγέθους και αύξηση ταχύτητας. Το R1 της DeepSeek αποστάχθηκε σε μοντέλα LLaMA και Qwen με παραμέτρους από 70 δισεκατομμύρια έως 1.5 δισεκατομμύρια.