С повече от 20 години опит ние променяме вашето цифрово присъствие. Специализирани сме в разработването на уебсайтове и електронни магазини, SEO и цифров маркетинг, ERP софтуер и интелигентна автоматизация, които извеждат бизнеса ви на следващото ниво.
Адрес:
Егнатия 154, Солун 546 36
Телефон:
+30 231 231 4095
Електронна поща:
[email protected]
Готови ли сте за следващата стъпка?;
Το ProofEvolve διατηρεί kernel-checked ενδιάμεσα βήματα, τα οργανώνει σε proof DAGs και τα επαναχρησιμοποιεί χωρίς να χαλαρώνει την τυπική ορθότητα.
Το ProofEvolve κρατά τα επαληθευμένα ενδιάμεσα βήματα, τα οργανώνει σε γράφους Lean 4 και τα επαναχρησιμοποιεί σε νέες αποδείξεις. Η αξία του δεν είναι μια αόριστη «μνήμη AI», αλλά μια μνήμη όπου κάθε αποθηκευμένο βήμα έχει περάσει ανεξάρτητο τυπικό έλεγχο.
Τι θα γινόταν αν ένα σύστημα τεχνητής νοημοσύνης δεν ξεχνούσε ό,τι έμαθε από μια αποτυχημένη προσπάθεια; Στην τυπική απόδειξη θεωρημάτων, μια λύση μπορεί να μη φτάσει μέχρι το τέλος, αλλά να περιέχει σωστά λήμματα, χρήσιμες διασπάσεις και βήματα που έχουν ήδη ελεγχθεί. Το ProofEvolve σχεδιάστηκε ακριβώς γύρω από αυτή την ιδέα: να κρατά τη γνώση που έχει πιστοποιηθεί, ακόμη και όταν η συνολική απόδειξη παραμένει ανολοκλήρωτη.
Η εργασία των Wenqian Ye και συνεργατών προτείνει ένα νευρο-συμβολικό πλαίσιο για αυτοματοποιημένη απόδειξη στο Lean 4. Το γλωσσικό μοντέλο προτείνει κινήσεις, αλλά ο πυρήνας του Lean αποφασίζει ποια κίνηση είναι μαθηματικά αποδεκτή. Αντί να αποθηκεύει την εμπειρία μόνο στα βάρη ενός μοντέλου ή να τη χρησιμοποιεί μόνο μέσα στο τρέχον πρόβλημα, το ProofEvolve οργανώνει τα επαληθευμένα αποτελέσματα σε ρητές δομές που μπορούν να μεταφερθούν σε επόμενες αποδείξεις.
Πολλά συστήματα απόδειξης αξιολογούν μια προσπάθεια με ένα δυαδικό σήμα: είτε έκλεισε ολόκληρο το θεώρημα είτε όχι. Αυτό είναι σαφές, αλλά φτωχό ως πληροφορία. Μια προσπάθεια μπορεί να έχει λύσει τρία δύσκολα υποπροβλήματα και να έχει κολλήσει στο τέταρτο. Αν το σύστημα κοιτάζει μόνο το τελικό αποτέλεσμα, αντιμετωπίζει αυτή την προσπάθεια σχεδόν όπως μια εντελώς άστοχη απάντηση.
Οι μέθοδοι που βασίζονται σε εκπαίδευση μπορούν να ενσωματώσουν εμπειρία στα βάρη του μοντέλου, όμως αυτό απαιτεί νέο κύκλο ενημέρωσης. Οι agentic προσεγγίσεις μπορούν να μοιραστούν λήμματα ανάμεσα σε κλάδους της ίδιας αναζήτησης, αλλά συνήθως η μνήμη παραμένει δεμένη με τον τρέχοντα στόχο. Οι συγγραφείς θεωρούν ότι αυτή η απώλεια επιβεβαιωμένης προόδου περιορίζει την πραγματική αυτοβελτίωση.
Η διάκριση έχει σημασία πέρα από τα μαθηματικά. Σε κάθε διαδικασία όπου υπάρχουν αυστηροί έλεγχοι, μια αποτυχημένη συνολική εκτέλεση μπορεί να περιέχει έγκυρα υποαποτελέσματα. Η επιχειρηματική ανάγνωση δεν είναι ότι το ProofEvolve αποτελεί έτοιμο εργαλείο για γενικά workflows, αλλά ότι δείχνει μια αρχιτεκτονική αρχή: η επιβεβαιωμένη ενδιάμεση εργασία αξίζει να γίνεται μόνιμο, επαναχρησιμοποιήσιμο περιουσιακό στοιχείο.
Βλέπει μόνο αν έκλεισε ολόκληρο το θεώρημα. Μια προσπάθεια με τρία ελεγμένα λήμματα και έναν ανοιχτό στόχο καταγράφεται απλώς ως αποτυχία.
Μετρά πόση δομή έχει κλείσει με kernel-accepted βήματα, χωρίς να παρουσιάζει μια ανολοκλήρωτη απόδειξη ως σωστή.
Κρατά κλειστούς υπογράφους ως τυποποιημένα, επαναχρησιμοποιήσιμα αποτελέσματα και ελέγχει ξανά κάθε εφαρμογή τους σε νέο στόχο.
Στο ProofEvolve, το νευρωνικό μοντέλο δεν έχει την τελική εξουσία. Προτείνει αποσυνθέσεις ενός στόχου, διορθώσεις αποτυχημένων βημάτων και συνδυασμούς παλαιότερων σχημάτων απόδειξης. Κάθε προτεινόμενη μετάβαση περνά από τον kernel του Lean 4 στο ίδιο, παγωμένο περιβάλλον Mathlib. Μια αποδεκτή απόδειξη δεν πρέπει να περιέχει άλυτες μεταμεταβλητές ή placeholders.
Ο πυρήνας λειτουργεί ως σαφές όριο εμπιστοσύνης. Μια απόρριψη αφήνει αμετάβλητη την έμπιστη κατάσταση του συστήματος και αποθηκεύεται μαζί με το σφάλμα του Lean για πιθανή επισκευή. Μια αποδοχή προσθέτει μόνο έναν τυποποιημένο, ελεγμένο δεσμό στη δομή της απόδειξης. Έτσι, η παραγωγική ευελιξία του μοντέλου χωρίζεται από την αυστηρή πιστοποίηση του συμβολικού συστήματος.
Οι ερευνητές αναφέρουν επίσης ανεξάρτητο επανέλεγχο κάθε λύσης με περιορισμένο έλεγχο αξιωμάτων. Σε περισσότερους από 400 επανελέγχους δεν εντόπισαν ψευδώς θετική λύση. Αυτό δεν αποδεικνύει ότι κάθε πιθανή υλοποίηση είναι αλάνθαστη, αλλά τεκμηριώνει ότι τα αποτελέσματα που δηλώθηκαν ως λυμένα πέρασαν τον καθορισμένο έλεγχο.
Κρίσιμη αρχή
Το παραγωγικό μοντέλο προτείνει· ο ανεξάρτητος verifier αποφασίζει τι γίνεται μόνιμη γνώση
Στο ProofEvolve ο Lean 4 kernel είναι το όριο εμπιστοσύνης. Για ένα επιχειρηματικό AI workflow, η αντίστοιχη ασφάλεια απαιτεί deterministic validation, authoritative δεδομένα, provenance και σαφή απόρριψη όταν οι προϋποθέσεις δεν ικανοποιούνται.
Η απόδειξη αναπαρίσταται ως πεπερασμένος, άκυκλος AND-OR γράφος. Ένας OR κόμβος εκφράζει εναλλακτικές κινήσεις: αρκεί μία από αυτές να οδηγήσει σε λύση. Ένας AND δεσμός εκφράζει ότι πρέπει να λυθούν όλα τα επιμέρους υποπροβλήματα που δημιούργησε μια συγκεκριμένη διάσπαση. Αυτή η μορφή επιτρέπει στο σύστημα να διατηρεί πολλές στρατηγικές χωρίς να συμπιέζει όλη την αναζήτηση σε ένα γραμμικό κείμενο.
Κλειδί είναι ότι ένας κλειστός εσωτερικός υπογράφος αποτελεί έγκυρο αποτέλεσμα ακόμη κι αν η ρίζα του συνολικού θεωρήματος είναι ανοιχτή. Ο μηχανισμός συναρμολόγησης ακολουθεί τους ελεγμένους δεσμούς και παράγει όρο απόδειξης για τον συγκεκριμένο κόμβο. Άρα, η μερική επιτυχία έχει σαφή συμβολική μορφή και δεν εξαρτάται από μια ασαφή περίληψη που έγραψε το ίδιο το μοντέλο.
Για να μη γεμίσει το αρχείο μόνο με παραλλαγές της ίδιας στρατηγικής, το ProofEvolve χρησιμοποιεί συμπεριφορικούς δείκτες, όπως το βάθος, την κυρίαρχη οικογένεια tactics και την περιοχή του schema index. Σε κάθε «κελί» κρατά τον καλύτερο υποψήφιο, ενώ η επιλογή επηρεάζεται από το πόση επαληθευμένη πρόοδο έχει ήδη επιτευχθεί.
Η verified closure, με σύμβολο ρ, μετατρέπει τη δομή του γράφου σε βαθμιαίο σήμα επιλογής. Ένας κλειστός κόμβος παίρνει τιμή 1 και ένα ανοιχτό φύλλο τιμή 0. Στους OR κόμβους κρατείται η καλύτερη εναλλακτική, ενώ στους AND δεσμούς υπολογίζεται σταθμισμένος συνδυασμός των παιδιών. Στα πειράματα χρησιμοποιούνται ομοιόμορφα βάρη.
Η βαθμολογία δεν αντικαθιστά τον τελικό έλεγχο ούτε δηλώνει ότι μια μισοτελειωμένη απόδειξη είναι «κατά το ήμισυ σωστή». Μετρά πόση από την επιλεγμένη δομή έχει ήδη κλείσει με kernel-accepted βήματα. Οι συγγραφείς αποδεικνύουν ότι η τιμή 1 ισοδυναμεί με κλειστή ρίζα και ότι η βαθμολογία δεν μειώνεται όταν ο γράφος επεκτείνεται χωρίς να αλλοιώνονται τα παλαιότερα βήματα.
Η ίδια λογική χρησιμοποιείται για την προτεραιότητα των ανοιχτών μετώπων. Το σύστημα εκτιμά ποιο υποπρόβλημα θα αύξανε περισσότερο τη συνολική closure αν λυνόταν και το προωθεί στην αναζήτηση. Στις καταγεγραμμένες τροχιές, οι επιτυχημένες εκτελέσεις ανεβαίνουν σταδιακά μέχρι το 1, ενώ αποτυχημένες εκτελέσεις σταθεροποιούνται χαμηλότερα. Το δυαδικό σήμα, αντίθετα, μένει στο μηδέν μέχρι το τελευταίο βήμα.
Η διάσπαση μετατρέπει έναν δύσκολο στόχο σε μικρότερες, ρητές υποχρεώσεις. Η επισκευή δίνει στο μοντέλο μια απορριφθείσα πρόταση μαζί με το μήνυμα σφάλματος του Lean, ώστε να επιχειρήσει διορθωμένη μετάβαση. Ο ανασυνδυασμός αναζητά ένα προηγουμένως επαληθευμένο schema που ταιριάζει στον τρέχοντα στόχο.
Το schema δεν αντιγράφεται τυφλά. Οι ελεύθερες μεταβλητές γενικεύονται, οι χρησιμοποιούμενες υποθέσεις γίνονται ρητές προκείμενες και η εφαρμογή πρέπει να ταιριάξει τυπικά με τον νέο στόχο. Όποιες προκείμενες δεν μπορούν να αποδειχθούν άμεσα εμφανίζονται ως νέα υποπροβλήματα. Ολόκληρη η εφαρμογή ελέγχεται ξανά από το Lean πριν γίνει δεκτή.
Η μελέτη αφαίρεσης σε 60 προβλήματα του IMO-LeanProofBench δείχνει ότι και οι τρεις λειτουργίες συνεισφέρουν. Το πλήρες σύστημα έλυσε κατά μέσο όρο 32 από τα 60. Χωρίς διάσπαση έλυσε 11, χωρίς ανασυνδυασμό 14 και χωρίς επισκευή 9. Η πτώση ήταν εντονότερη στο Advanced split, όπου το πλήρες σύστημα έλυσε 10 από τα 30 προβλήματα, έναντι 2 χωρίς διάσπαση, 3 χωρίς ανασυνδυασμό και 2 χωρίς επισκευή.
Η κύρια σύγκριση έγινε στα PutnamBench, IMO-LeanProofBench και CombiBench, με Claude Opus 4.8 ως κοινό βασικό μοντέλο για τα agentic συστήματα και αντιστοιχισμένο budget. Ο μέσος όρος προέρχεται από τρεις ανεξάρτητες εκτελέσεις. Το ProofEvolve πέτυχε μέσο solve rate 57,8%, έναντι 50,5% για το LEAP και 45,9% για το Hilbert.
Αναλυτικά, το ProofEvolve έφτασε 71,2% στο PutnamBench και 53,3% στο IMO-LeanProofBench. Το LEAP κατέγραψε αντίστοιχα 64,7% και 36,7%. Στο CombiBench, όμως, το ProofEvolve έφτασε 49,0%, μία μονάδα κάτω από το 50,0% του LEAP. Επομένως, το αποτέλεσμα δεν είναι ομοιόμορφη υπεροχή σε κάθε σύνολο, αλλά ο υψηλότερος μέσος όρος και ιδιαίτερα μεγάλη διαφορά στο benchmark με προβλήματα που συχνά απαιτούν σύνθεση πολλών λημμάτων.
Τα απλά inference-only μοντέλα ήταν πολύ χαμηλότερα στο συγκεκριμένο πρωτόκολλο. Για παράδειγμα, το Claude Opus 4.8 με pass@16 χωρίς agentic search είχε 0% στα Putnam και IMO-Lean και 10% στο Combi. Η σύγκριση υπογραμμίζει ότι η αρχιτεκτονική της αναζήτησης και ο έλεγχος των ενδιάμεσων βημάτων μπορούν να είναι εξίσου κρίσιμα με την επιλογή του βασικού μοντέλου.
Τέσσερα τεκμηριωμένα σημεία αναφοράς
Οι τιμές αφορούν τα συγκεκριμένα benchmarks, τα μοντέλα, τα budgets και τις συνθήκες που δηλώνει η εργασία.
Σε ελεγχόμενες συνθετικές οικογένειες προβλημάτων, όπου μεταγενέστεροι στόχοι χτίζονται πάνω σε προηγούμενα λήμματα, η βιβλιοθήκη που μεγάλωνε από στόχο σε στόχο οδήγησε σε solve rate 19,8%. Όταν η βιβλιοθήκη μηδενιζόταν πριν από κάθε στόχο, το ποσοστό ήταν 7,3%. Οι συγγραφείς το περιγράφουν ως 2,7 φορές περισσότερους λυμένους στόχους, με τα υπόλοιπα στοιχεία σταθερά.
Η μεγαλύτερη μελέτη χρησιμοποίησε Lean Workbook. Μετά από επανεπαλήθευση παρέμειναν 20.554 ζεύγη δήλωσης και απόδειξης και, μετά την αποδιπλοποίηση, 10.968 διαφορετικά θεωρήματα. Από αυτά, 1.000 κρατήθηκαν για αξιολόγηση και 9.968 χρησιμοποιήθηκαν ως ροή πηγής. Το Qwen3.5-397B-A17B-FP8 παρήγαγε 5.546 kernel-accepted αποδείξεις για τη βιβλιοθήκη.
Μετά από έλεγχο πιθανής επικάλυψης από πέντε ανεξάρτητους language-model judges, έμειναν 744 θεωρήματα αξιολόγησης. Με retrieval βάθους K=8, το solve rate αυξήθηκε από 49,5% σε 53,4%, δηλαδή κατά 3,9 ποσοστιαίες μονάδες. Τυχαίο retrieval από την ίδια βιβλιοθήκη έδωσε 49,6%. Ακόμη και βιβλιοθήκη 1.000 αποδείξεων πρόσθεσε 3,3 μονάδες, ενώ στο K=64 η αύξηση έφτασε 5,3 μονάδες.
Σε τρεις εκτελέσεις με K=8, το σχετικό retrieval έκλεισε 351 περιπτώσεις που έμεναν ανοιχτές στο zero-shot. Στις 322 από αυτές, ποσοστό 91,7%, η αποδεκτή απόδειξη δεν αναπαρήγαγε κατά λέξη καμία από τις εμφανιζόμενες αποδείξεις. Οι συγγραφείς το ερμηνεύουν ως ένδειξη μεταφοράς δομής και όχι απλής ανάκλησης απαντήσεων. Σημαντική διευκρίνιση: αυτό το πείραμα απομονώνει τη συνεισφορά της βιβλιοθήκης και απενεργοποιεί repair, decomposition, DAG archive και τη closure ως σήμα επιλογής.
Η εργασία δοκίμασε επίσης open-weight μοντέλα με διαφορετικά budgets ανά στόχο. Το όριο περιλάμβανε κλήσεις μοντέλου, κλήσεις του Lean kernel, tokens και χρόνο. Επτά από τις οκτώ ρυθμίσεις παρήγαγαν περισσότερες επαληθευμένες μεταβάσεις καθώς το budget αυξανόταν. Η εξαίρεση ήταν το gpt-oss-120b με low reasoning effort, που παρέμεινε επίπεδο.
Από 0,25× έως 2× budget, τα solve events αυξήθηκαν από 28 σε 44 και η ένωση διαφορετικών λυμένων στόχων από 2 σε 10. Οι ίδιοι οι συγγραφείς προειδοποιούν ότι τα arms ήταν ξεχωριστές στοχαστικές εκτελέσεις και ότι οι αριθμοί δεν αποδεικνύουν μονοτονική κλιμάκωση για κάθε μοντέλο ούτε απομονώνουν την επίδραση ενός μόνο πόρου.
Το υπολογιστικό κόστος είναι ουσιαστικό. Για open-weight hosting χρησιμοποιήθηκαν κόμβοι με οκτώ NVIDIA B200 των 192 GB και οι μεγαλύτερες εκτελέσεις έφτασαν έως 28 κόμβους ή 224 GPUs ταυτόχρονα. Αυτό θέτει σαφές όριο στη γενίκευση: το ερευνητικό αποτέλεσμα δεν ισοδυναμεί με οικονομικά βιώσιμη εγκατάσταση για κάθε οργανισμό.
Σε ένα εξελικτικό σύστημα υπάρχει πάντα ο φόβος ότι μια νέα παραλλαγή θα καταστρέψει ένα προηγουμένως σωστό αποτέλεσμα. Η σχεδίαση του ProofEvolve αποφεύγει αυτή την παγίδα με μονότονες επεκτάσεις. Ένας νέος γράφος μπορεί να προσθέσει κόμβους και δεσμούς, αλλά δεν αλλάζει τις ετικέτες και τους realizers των υπαρχόντων βημάτων. Εφόσον κάθε νέος δεσμός έχει ελεγχθεί, η παλαιότερη πιστοποιημένη γνώση παραμένει διαθέσιμη.
Η εργασία διατυπώνει τρεις βασικές invariants: κάθε αποθηκευμένος δεσμός έχει kernel-checked realizer, κάθε κλειστός κόμβος μπορεί να συναρμολογηθεί σε έγκυρη απόδειξη και κάθε schema της βιβλιοθήκης συνοδεύεται από έγκυρο όρο απόδειξης. Αν μια πρόταση απορριφθεί, ενημερώνεται μόνο το error store. Αν γίνει δεκτή, η βιβλιοθήκη μπορεί μόνο να μεγαλώσει με νέα ελεγμένα schemas.
Αυτό είναι ουσιαστικά διαφορετικό από μια μνήμη όπου το μοντέλο ξαναγράφει ελεύθερα παλιές σημειώσεις. Η γνώση εδώ έχει provenance, τύπο και ελέγξιμη αλυσίδα παραγωγής. Η έννοια μπορεί να εμπνεύσει και άλλες εφαρμογές υψηλής αξιοπιστίας, αλλά μόνο εφόσον υπάρχει πραγματικός μηχανισμός επιβεβαίωσης αντίστοιχος με το είδος του αποτελέσματος.
Παράλληλα, η διατήρηση διαφορετικών στρατηγικών στο archive μειώνει τον κίνδυνο να κυριαρχήσει νωρίς ένα μόνο μονοπάτι αναζήτησης. Το σύστημα δεν επιβραβεύει απλώς την ποσότητα των παραγόμενων βημάτων· επιλέγει ανάμεσα σε δομικά διαφορετικούς, ήδη ελεγμένους υποψηφίους και συνεχίζει από εκείνους που εμφανίζουν ουσιαστική πρόοδο.
Η πρώτη πρακτική αρχή είναι ο διαχωρισμός proposer και verifier. Το γενετικό μοντέλο μπορεί να προτείνει δημιουργικά βήματα, αλλά μια ανεξάρτητη, ντετερμινιστική διαδικασία πρέπει να επικυρώνει ό,τι περνά στη μόνιμη γνώση. Στα μαθηματικά αυτός ο ρόλος ανήκει στον Lean kernel. Σε άλλα πεδία θα απαιτούνταν διαφορετικός, πραγματικά αξιόπιστος μηχανισμός ελέγχου· δεν αρκεί ένα δεύτερο LLM που απλώς δηλώνει ότι «φαίνεται σωστό».
Η δεύτερη αρχή είναι ότι τα intermediate artifacts χρειάζονται δομή. Ένα αρχείο με συνομιλίες ή μια περίληψη δεν προσφέρει την ίδια εγγύηση με ένα τυποποιημένο schema που δηλώνει προϋποθέσεις, συμπέρασμα και αποδεικτικό όρο. Για επιχειρηματικές ροές αυτό μεταφράζεται σε σαφείς εισόδους, ελέγχους, dependencies και provenance πριν ένα υποαποτέλεσμα γίνει επαναχρησιμοποιήσιμο.
Η τρίτη αρχή είναι ότι το retrieval πρέπει να είναι σχετικό και ελεγχόμενο. Η τυχαία επιλογή αποδείξεων δεν βελτίωσε ουσιαστικά το zero-shot αποτέλεσμα, ενώ η σημασιολογική ανάκτηση το βελτίωσε. Το μάθημα για knowledge bases και agent memory είναι ότι η αποθήκευση από μόνη της δεν δημιουργεί αξία. Χρειάζονται καλή ευρετηρίαση, μηχανισμός επιλογής και έλεγχος συμβατότητας στο σημείο εφαρμογής.
Checklist για μνήμη AI που αποθηκεύει μόνο ελεγμένη πρόοδο
Μην αποθηκεύετε μια ασαφή «καλή απάντηση». Καταγράψτε εισόδους, προϋποθέσεις, έξοδο, έκδοση εργαλείων και το αποδεικτικό validation που επιτρέπει τη μελλοντική χρήση.
Το ίδιο μοντέλο δεν πρέπει να παράγει και να επικυρώνει μόνο του τη μόνιμη γνώση. Χρησιμοποιήστε schema checks, tests, policy rules ή authoritative APIs ανάλογα με το domain.
Κάθε unresolved premise πρέπει να παραμένει ρητό task. Η μερική επιτυχία δεν επιτρέπεται να μετατραπεί σιωπηρά σε τελική έγκριση.
Η μελέτη έδειξε ότι το τυχαίο retrieval δεν πρόσφερε ουσιαστική βελτίωση. Η ομοιότητα δεν αρκεί: οι προϋποθέσεις του παλιού αποτελέσματος πρέπει να ισχύουν και στο νέο context.
Καταγράψτε από ποιο run προήλθε το artifact, ποιος verifier το δέχθηκε και ποια δεδομένα χρησιμοποίησε, ώστε η ομάδα να μπορεί να το ελέγξει ή να το ανακαλέσει.
Παρακολουθήστε accepted artifacts, rejected proposals, retrieval precision, ανοιχτές προϋποθέσεις και compute cost. Ένα μεγαλύτερο budget δεν εγγυάται γραμμική ή οικονομικά αποδοτική πρόοδο.
Η αξιολόγηση βρίσκεται στο αυστηρό αλλά ειδικό περιβάλλον τυπικών μαθηματικών στο Lean 4. Εκεί υπάρχει kernel που μπορεί να απορρίψει κάθε μη έγκυρη μετάβαση. Σε marketing, customer experience ή γενική επιχειρηματική στρατηγική, η «σωστή» απάντηση συχνά δεν έχει τυπικό τύπο και δεν υπάρχει ισοδύναμος verifier. Η μεταφορά της αρχιτεκτονικής απαιτεί λοιπόν προσοχή και δεν πρέπει να παρουσιάζεται ως ήδη αποδεδειγμένη γενική λύση.
Τα ισχυρά αποτελέσματα συνδέονται επίσης με συγκεκριμένα benchmarks, μοντέλα, budgets και περιβάλλον Mathlib. Στο CombiBench το ProofEvolve δεν ήταν πρώτο, ενώ στην open-weight μελέτη κανένας από τους 11 διαφορετικούς λυμένους στόχους δεν προερχόταν από το IMO-LeanProofBench. Η κλιμάκωση του compute αύξησε τη συνολική κάλυψη, αλλά όχι με τρόπο που να εγγυάται σταθερή βελτίωση σε κάθε ρύθμιση.
Τέλος, η εργασία δείχνει συσσώρευση επαληθευμένης γνώσης χωρίς ενημέρωση των βαρών του μοντέλου, όχι ένα πλήρως αυτόνομο σύστημα επιστημονικής ανακάλυψης. Η αναφορά των συγγραφέων σε φυσική και χημεία είναι προοπτική για μελλοντική έρευνα, όχι πειραματικά επιβεβαιωμένο αποτέλεσμα της παρούσας μελέτης.
Η σημαντικότερη συμβολή του ProofEvolve δεν είναι απλώς ένα ακόμη υψηλότερο benchmark score. Είναι η αλλαγή της μονάδας μνήμης. Το σύστημα δεν κρατά μόνο prompts, απαντήσεις ή ένα ενημερωμένο μοντέλο. Κρατά επαληθευμένες δομές που μπορούν να συνδυαστούν ξανά χωρίς να χαλαρώσει η τυπική ορθότητα.
Για όσους σχεδιάζουν AI agents με ρητή κατάσταση, αυτό προσφέρει ένα πιο απαιτητικό πρότυπο για τον όρο «μαθαίνει από την εμπειρία». Η εμπειρία έχει αξία όταν μπορεί να απομονωθεί, να πιστοποιηθεί, να ανακτηθεί τη σωστή στιγμή και να εφαρμοστεί με έλεγχο των προϋποθέσεών της. Το ProofEvolve δείχνει ότι ακόμη και μια ανολοκλήρωτη προσπάθεια μπορεί να επεκτείνει το όριο γνώσης, αρκεί το σύστημα να γνωρίζει με ακρίβεια ποιο μέρος της είναι πράγματι σωστό.
Автоматизация на бизнеса и AI
Σχεδιάστε AI workflows που κρατούν μόνο ελεγμένη γνώση
Η TWO DOTS χαρτογραφεί deterministic validators, authoritative πηγές, traceable memory, retrieval controls και ανθρώπινα σημεία έγκρισης, ώστε κάθε επαναχρησιμοποιούμενο αποτέλεσμα να έχει σαφείς προϋποθέσεις και provenance.
Често задавани въпроси
Είναι ένα νευρο-συμβολικό πλαίσιο αυτοματοποιημένης απόδειξης θεωρημάτων. Ένα γλωσσικό μοντέλο προτείνει βήματα και ο kernel του Lean 4 επαληθεύει κάθε μετάβαση πριν προστεθεί στη δομή γνώσης.
Επειδή μια ανολοκλήρωτη απόδειξη μπορεί να περιέχει λήμματα και υποστόχους που έχουν ήδη αποδειχθεί. Η verified closure αξιοποιεί αυτή την πρόοδο χωρίς να χαρακτηρίζει σωστή την πλήρη λύση.
Είναι άκυκλος γράφος όπου οι OR κλάδοι αναπαριστούν εναλλακτικές στρατηγικές και οι AND κλάδοι σύνολα υποπροβλημάτων που πρέπει να λυθούν όλα.
Στον μέσο όρο PutnamBench, IMO-LeanProofBench και CombiBench, το ProofEvolve πέτυχε solve rate 57,8%, έναντι 50,5% για το LEAP και 45,9% για το Hilbert.
Στη μελέτη 744 Lean Workbook θεωρημάτων και με K=8, το σχετικό retrieval αύξησε το solve rate από 49,5% σε 53,4%. Το τυχαίο retrieval έφτασε 49,6%.
Όχι στα κύρια πειράματα αναζήτησης. Τα base-model parameters παραμένουν παγωμένα και η συσσώρευση γίνεται σε ρητούς, kernel-checked γράφους και schemas.
Όχι χωρίς προσαρμογή. Η αρχή του ανεξάρτητου verifier και της δομημένης μνήμης είναι χρήσιμη, αλλά τα περισσότερα επιχειρηματικά πεδία δεν διαθέτουν τυπικό kernel αντίστοιχο του Lean.
Τα αποτελέσματα προέρχονται από συγκεκριμένο περιβάλλον Lean, συγκεκριμένα benchmarks, μοντέλα και υψηλό υπολογιστικό κόστος. Δεν αποδεικνύουν γενική, οικονομικά βιώσιμη αυτοβελτίωση.
