AI και Μαθηματική απόδιξη

[mklabgr]

Όταν μια απόδειξη είναι σωστή αλλά κανείς δεν την καταλαβαίνει

[i]Τι σημαίνει «απόδειξη» όταν ο επαληθευτής είναι μηχανή και όχι άνθρωπος[/i]

---

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

«Επαληθευμένη» δεν σημαίνει πάντα το ίδιο πράγμα
Αν ένας βοηθός απόδειξης όπως το Lean ή το Coq έχει ελέγξει κάθε βήμα συλλογισμού έναντι ενός μικρού, πλήρως κατανοητού λογικού πυρήνα, αυτό αποτελεί ισχυρή εγγύηση — η εμπιστοσύνη δεν στηρίζεται καθόλου στο ίδιο το AI, αλλά στον πυρήνα αυτό, τον οποίο οι άνθρωποι κατανοούν πλήρως. Είναι εντελώς διαφορετικό από το «το AI δοκίμασε την απόδειξη σε αρκετές περιπτώσεις-ελέγχου και άντεξε», κάτι που αποτελεί πολύ ασθενέστερη ένδειξη — πιο κοντά σε ισχυρή εμπειρική στήριξη παρά σε απόδειξη.

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

Το επόμενο βήμα με το AI
Μια εκδοχή παραγόμενη από AI πάει αυτό ένα βήμα παραπέρα, γιατί ακόμη και το δίχτυ ασφαλείας του κατανεμημένου ανθρώπινου ελέγχου μπορεί να λείπει — κανείς, ούτε καν συλλογικά, δεν κατέχει τη δομή του επιχειρήματος. Στο σημείο αυτό εμπιστευόμαστε τη διαδικασία (την ορθότητα του επαληθευτή, ίσως στατιστικούς ελέγχους συνέπειας, ίσως ανεξάρτητες προσπάθειες επανα-παραγωγής) και όχι την κατανόηση κάποιου ανθρώπου για το γιατί το θεώρημα είναι αληθές.

Τι θα συνέβαινε στην πράξη

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

• Κάποιοι ίσως αρνηθούν να τη χαρακτηρίσουν πλήρως ως «μαθηματική γνώση» μέχρι να υπάρξει επεξηγηματική εκδοχή — αντιμετωπίζοντάς την περισσότερο ως ισχυρή εικασία με μηχανική βεβαιότητα, παρά ως θεώρημα με την παραδοσιακή έννοια.
  

Μια παλιά φιλοσοφική ανησυχία
Υπάρχει μια παλιά φιλοσοφική ανησυχία — που διατυπώθηκε με διαφορετικές μορφές από τον Wittgenstein και αργότερα από φιλοσόφους όπως ο Thomas Tymoczko στην περίπτωση των τεσσάρων χρωμάτων — ότι μια απόδειξη οφείλει να είναι επισκοπήσιμη: ένας άνθρωπος πρέπει να μπορεί να τη διατρέξει και να πειστεί προσωπικά. Αν αυτή η απαίτηση εγκαταλειφθεί, τα μαθηματικά αρχίζουν να μοιάζουν λίγο περισσότερο με πειραματική επιστήμη: δεν κατανοούμε πάντα γιατί ένα φάρμακο δρα σε μοριακό επίπεδο, αλλά εμπιστευόμαστε τα κλινικά δεδομένα. Μια επαληθευμένη αλλά ακατανόητη απόδειξη θα ωθούσε τα καθαρά μαθηματικά ένα βήμα προς αυτή την κατεύθυνση — αλήθεια που στηρίζεται σε μια αξιόπιστη μηχανική διαδικασία, όχι σε ανθρώπινη διαίσθηση.

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