Η Anthropic κυκλοφορεί το FlashProve για κρυπτογραφικές αποδείξεις συμπερασμού από τεχνητή νοημοσύνη

Η Anthropic κυκλοφόρησε το FlashProve στις 2 Νοεμβρίου 2026: ένα πρωτότυπο ερευνητικό έργο ανοικτού κώδικα που χρησιμοποιεί κρυπτογραφικές αποδείξεις για να δείξει ότι μια απάντηση γλωσσικού μοντέλου προήλθε από συγκεκριμένα, δεσμευμένα βάρη, χωρίς να τα αποκαλύπτει. Η εταιρεία ανέφερε ότι η παραγωγή αποδείξεων για το Llama 4 Maverick της Meta έφτασε τα 110 διακριτικά (tokens) ανά δευτερόλεπτο.

Το έργο αντιμετωπίζει ένα κενό επαλήθευσης στην τεχνητή νοημοσύνη που παρέχεται μέσω φιλοξενούμενων υπηρεσιών. Μια απάντηση υψηλής ποιότητας δεν αποδεικνύει ποιο μοντέλο την παρήγαγε: μια υπηρεσία δρομολόγησης θα μπορούσε να αντικαταστήσει το μοντέλο με ένα άλλο σύστημα, ένας αξιολογητής θα μπορούσε να λάβει διαφορετικό μοντέλο από εκείνο που προοριζόταν για τη δοκιμή ή ένας εισβολέας θα μπορούσε να αλλοιώσει τη ροή των διακριτικών. Για τους χρήστες, η επαλήθευση με επανεκτέλεση του μοντέλου δεν είναι πρακτική λύση, όταν τα βάρη είναι ιδιωτικά και οι απαιτήσεις σε υλικό σημαντικές.

Σύνδεση των απαντήσεων με κρυφά βάρη

Το FlashProve χρησιμοποιεί ένα συνοπτικό επιχείρημα γνώσης μηδενικής γνώσης, ή zkSNARK, σε μια σχεδίαση που βασίζεται αποκλειστικά σε λογισμικό και όχι σε έμπιστο υλικό. Σε μια φάση εκτός σύνδεσης, ο πάροχος δημοσιεύει μια σύντομη κρυπτογραφική δέσμευση, η οποία προσδιορίζει ένα συγκεκριμένο σύνολο βαρών, ενώ τα διατηρεί μυστικά. Για ολοκληρωμένα ζεύγη προτροπής και απάντησης, το σύστημα παράγει μια απόδειξη ότι τα διακριτικά εξόδου είναι το αποτέλεσμα του μοντέλου που προσδιορίζεται από τη δέσμευση. Όποιος διαθέτει τη δέσμευση, την προτροπή και την απάντηση μπορεί να επαληθεύσει την απόδειξη χωρίς πρόσβαση στα βάρη.

Οι επιδιωκόμενες ιδιότητες είναι η πληρότητα, η ορθότητα, η μηδενική γνώση και η συνοπτικότητα. Μια έγκυρη απόδειξη θα πρέπει να γίνεται αποδεκτή, ενώ η πιστοποίηση μιας ψευδούς δήλωσης θα πρέπει να απαιτεί την κατάρριψη κρυπτογραφικών παραδοχών που θεωρούνται ευρέως αξιόπιστες. Η επαλήθευση μιας απόδειξης δεν θα πρέπει να αποκαλύπτει ούτε τα βάρη ούτε ενδιάμεσες τιμές υπολογισμών. Η σχεδίαση αποκρύπτει επίσης ποια υποδίκτυα του μείγματος ειδικών ενεργοποιήθηκαν για κάθε διακριτικό, παρότι η αρχιτεκτονική του μοντέλου παραμένει ορατή.

Η υλοποίηση αξιοποιεί τη δομή μείγματος ειδικών του Maverick. Ο φόρτος εργασίας του αποδεικνύοντος κλιμακώνεται ανάλογα με τις περίπου 17 δισεκατομμύρια παραμέτρους που είναι ενεργές για κάθε διακριτικό, αντί για το σύνολο των 400 δισεκατομμυρίων, ενώ οι επιλογές των ειδικών παραμένουν κρυφές. Τα τμηματοποιημένα βάρη μεταδίδονται από τη μνήμη του κεντρικού υπολογιστή, επιτρέποντας στον αποδεικνύοντα να λειτουργεί με μία GPU 80 GB και περίπου 290 GB μνήμης κεντρικού υπολογιστή.

Η Anthropic περιγράφει πιθανές χρήσεις για ελέγχους ακεραιότητας πελατών, ανεξάρτητες αξιολογήσεις, ρυθμιστικά εργαλεία και την επιβολή απαιτήσεων χρήσης εγκεκριμένων μοντέλων. Τα πιστοποιητικά συμπερασμού θα μπορούσαν να βεβαιώνουν ότι τα αιτήματα εξυπηρετήθηκαν από το μοντέλο που δηλώθηκε, αλλά δεν θα αποδείκνυαν ότι το ίδιο υλικό δεν χρησιμοποιούνταν ταυτόχρονα και για την εκπαίδευση ενός άλλου μοντέλου. Αυτή η διάκριση περιορίζει όσα θα μπορούσαν να αποδείξουν τέτοια πιστοποιητικά σχετικά με απαιτήσεις συμμόρφωσης που εξαρτώνται από τον τρόπο χρήσης της υπολογιστικής ισχύος.

Επιδόσεις αποδείξεων και επιβάρυνση του συμπερασμού

Η αξιολόγηση της Anthropic χρησιμοποίησε μια έκδοση του μοντέλου με κβαντισμό 4 bit, διαθέσιμη στο κοινό. Ένας διακομιστής με μία H100 και 24 πυρήνες CPU παρήγαγε αποδείξεις για μια παρτίδα 24 αιτημάτων σε περίπου 223 δευτερόλεπτα, δημιουργώντας απόδειξη 18,78 MB για κάθε αίτημα. Το βήμα δέσμευσης εκτός σύνδεσης διήρκεσε περίπου 39 λεπτά.

Από την πλευρά της επαλήθευσης, ο πελάτης κατεβάζει μια δέσμευση περίπου 6,5 MB και επαληθεύει τις αποδείξεις σε CPU, χωρίς GPU. Η Anthropic μέτρησε χρόνο επαλήθευσης 17 δευτερολέπτων με 24 νήματα και 21 δευτερολέπτων με ένα νήμα, συμπεριλαμβανομένων των ελέγχων της φάσης εκτός σύνδεσης.

Οι μετρήσεις αυτές διαχωρίζουν τη διαδικασία επαλήθευσης αποκλειστικά σε CPU από την πολύ πιο απαιτητική διαδικασία παραγωγής αποδείξεων. Στη σύγκριση της Anthropic με συμπερασμό FP8 σε οκτώ H100 που εκτελούσαν το vLLM, η παραγωγή αποδείξεων απαιτούσε περίπου 72 φορές περισσότερο χρόνο ανά GPU για την ίδια παρτίδα και περίπου 94 φορές περισσότερο στο υψηλότερο φορτίο vLLM που δοκιμάστηκε. Επομένως, η απόδοση αυτή συνεπάγεται σημαντικό κόστος σε σύγκριση με την εξυπηρέτηση του μοντέλου χωρίς αποδείξεις.

Τυπική επαλήθευση και πρακτικοί περιορισμοί

Το αποθετήριο του FlashProve περιλαμβάνει έναν αποδεικνύοντα, έναν γρήγορο επαληθευτή C++, έναν πιο αργό επαληθευτή Lean, αποδείξεις Lean για βασικές μαθηματικές προτάσεις και ένα διαδραστικό εργαλείο οπτικοποίησης θεωρημάτων, με άδεια Apache 2.0. Χαρακτηρίζει την έκδοση 0.16.0 ως μη συντηρούμενο ερευνητικό έργο, στο οποίο δεν γίνονται δεκτές συνεισφορές.

Η εργασία σε Lean εξετάζει την πληρότητα, την ορθότητα και τη μηδενική γνώση στο μοντέλο τυχαίου μαντείου. Οι τυπικές διατυπώσεις εξακολουθούν να απαιτούν χειροκίνητη εξέταση, ώστε να διαπιστωθεί αν εκφράζουν τις εγγυήσεις που προορίζονται. Ο επαληθευτής Lean συνδέεται τυπικά με το θεώρημα ορθότητας, αλλά ο επαληθευτής C++, που προορίζεται για τακτική χρήση, δεν συνοδεύεται από τυπική εγγύηση και, αντί γι’ αυτό, δοκιμάστηκε ως προς τη συμφωνία του με τον επαληθευτή Lean.

Η τεκμηρίωση του έργου για τους γνωστούς περιορισμούς αναφέρει ότι συστήματα τεχνητής νοημοσύνης, υπό ανθρώπινη καθοδήγηση, συνέταξαν σχεδόν όλο το λογισμικό, τις αποδείξεις Lean και την τεκμηρίωση, ενώ εκτέλεσαν και τις αναφερόμενες δοκιμές. Δεν έχει πραγματοποιηθεί ανεξάρτητος έλεγχος ασφάλειας, ενώ οι δοκιμές σχετικά με την απόκρυψη των βαρών και τις κακόβουλες αποδείξεις παραμένουν περιορισμένες.

Οι αποδείξεις καλύπτουν μια ακριβή ακέραια εκδοχή των βαρών, με άπληστη αποκωδικοποίηση. Ο συμπερασμός κινητής υποδιαστολής ή η αποκωδικοποίηση με δειγματοληψία μπορεί να αποκλίνει από τον υπολογισμό που αποδεικνύεται, ενώ οι γενικές δοκιμές σφαλμάτων δεν καλύπτουν προτροπές σχεδιασμένες κακόβουλα. Τα συμφραζόμενα περιορίζονται στα 1.024 διακριτικά, ενώ οι επιθέσεις χρονισμού και άλλες επιθέσεις πλευρικού καναλιού δεν καλύπτονται από την εγγύηση. Η παραγωγή αποδείξεων εκ των υστέρων συνεπάγεται επίσης επανυπολογισμό, καθυστερημένες διαβεβαιώσεις και μη ντετερμινισμό σε σύγκριση με την παραγωγή αποδείξεων παράλληλα με τον συμπερασμό.

Για να γίνει η αποδείξιμη συμπερασματολογία ένας τακτικός έλεγχος της εξυπηρετούμενης κίνησης, οι εργασίες που απομένουν επικεντρώνονται στα κενά που αναδεικνύει αυτή η κυκλοφορία: στη μείωση του κόστους παραγωγής αποδείξεων, στην κάλυψη λιγότερο περιοριστικών μεθόδων αποκωδικοποίησης και μεγαλύτερων συμφραζομένων, καθώς και στην ισχυρότερη σύνδεση της γρήγορης υλοποίησης με το τυπικό πρωτόκολλο.