Η μελέτη με τίτλο “arXiv:2605.01030v2” παρουσιάζει μία μηχανικά ελεγμένη τυποποίηση των αρχιτεκτονικών ροής εργασίας AI που διέπονται από διαρθρωτικούς κανόνες και αποδεικνύει ότι η διακυβέρνηση σε επίπεδο επιπτώσεων μπορεί να εφαρμοστεί χωρίς να μειωθεί η εσωτερική υπολογιστική εκφραστικότητα. Χρησιμοποιώντας τα Interaction Trees στο Rocq 8.19, ορίζεται ένας χειριστής διακυβέρνησης G που διαμεσολαβεί όλες τις εντολές που έχουν επιπτώσεις, όπως η πρόσβαση στη μνήμη, οι εξωτερικές κλήσεις και οι ερωτήσεις προς τα ορατά συστήματα (LLM).
Η ανάπτυξη της μελέτης αποτελείται από 36 ενότητες, περίπου 12.000 γραμμές Rocq, και 454 θεωρήματα, χωρίς καμία παραδοχή λημμάτων. Καθορίζονται επτά ιδιότητες: (P1) κυβερνημένη πληρότητα Turing, (P2) κυβερνημένη εκφραστικότητα ορατών συστημάτων, (P3) ένα όριο αποφασισιμότητας όπου τα κριτήρια διακυβέρνησης είναι συνολικά και κλειστά υπό τη σύνθεση Boole, ενώ οι ιδιότητες προγραμμάτων παραμένουν μη τετριμμένες και μη αποφασίσιμες, (P4) διατήρηση στόχων για επιτρεπόμενες εκτελέσεις, (P5) εκφραστική ελαχιστότητα των πρωτόγονων ικανοτήτων (υπολογισμός, μνήμη, λογική, εξωτερική κλήση, παρατηρησιμότητα), (P6) ασυμμετρία υποκατάστασης που δείχνει ότι η διαρθρωτική διακυβέρνηση υπερβαίνει αυστηρά το φιλτράρισμα σε επίπεδο περιεχομένου, και (P7) σημασιολογική διαφάνεια: σε όλες τις εκτελέσεις όπου επιτρέπεται η διακυβέρνηση, η ερμηνεία υπό διακυβέρνηση είναι παρατηρησιακά ισοδύναμη (με εξαίρεση τα γεγονότα που αφορούν μόνο τη διακυβέρνηση) με την μη κυβερνημένη ερμηνεία.
Συνολικά, τα αποτελέσματα αυτά δείχνουν ότι η διακυβέρνηση και η υπολογιστική εκφραστικότητα είναι ορθογώνιες διαστάσεις: η διακυβέρνηση περιορίζει το όριο των επιπτώσεων των προγραμμάτων, ενώ παραμένει σημασιολογικά διαφανής στην εσωτερική υπολογιστική διαδικασία.
