A method for the automated generation of proof exercises with comparable levels of proving complexity

Questo articolo presenta un metodo per la generazione automatizzata di esercizi di dimostrazione matematica con livelli di complessità comparabili, basandosi su una procedura di estrazione meccanizzabile di regole per prove tableaux analitiche che catturano formalmente lo sforzo richiesto per la risoluzione.

L'essenziale

Immagina di essere un insegnante di matematica o logica. Il tuo compito è preparare esercizi per gli studenti. Ma c'è un problema: creare un esercizio che sia esattamente della difficoltà giusta è come cercare di indovinare il peso esatto di un pacco senza una bilancia. Se è troppo facile, gli studenti si annoiano; se è troppo difficile, si frustrano e smettono di provare.

Fino a poco tempo fa, creare centinaia di esercizi diversi ma con lo stesso livello di difficoltà richiedeva ore di lavoro manuale. Questo articolo presenta un "robot" intelligente che fa questo lavoro per te, ma con una regola d'oro: tutti gli esercizi generati devono essere ugualmente difficili da risolvere.

Ecco come funziona, spiegato con un'analogia semplice:

1. Il Problema: La "Difficoltà" è un'illusione

Spesso pensiamo che la difficoltà di un esercizio dipenda da quanto è "lungo" o "complesso" da leggere. Ma non è così. Due esercizi possono sembrare identici sulla carta, ma per risolverne uno ci vogliono 5 minuti e per l'altro 50.
I metodi vecchi di generazione automatica guardavano solo la superficie (il numero di simboli, la lunghezza della frase). Il nostro metodo, invece, guarda dentro la soluzione.

2. La Soluzione: La "Ricetta" Segreta (Le Regole)

Immagina che ogni esercizio di logica sia come un puzzle. Per risolverlo, devi seguire delle regole specifiche (come "se vedi un cerchio, togli il quadrato").
Gli autori hanno creato un sistema per:

1. Prendere un esercizio "esempio" (il modello).
2. Analizzare la sua soluzione per capire esattamente quanti "passi" servono e che tipo di passi sono.
3. Creare una "ricetta" (un insieme di regole) che descrive la struttura di quella soluzione.

3. Il Trucco: Costruire Esercizi "Gemelli"

Una volta che il computer ha capito la "struttura" della soluzione dell'esercizio originale, non si limita a cambiare le lettere (es. da A a B). Invece, usa la sua ricetta per costruire nuovi puzzle che hanno la stessa architettura interna.

L'analogia della Casa:
Immagina che la soluzione di un esercizio sia la pianta di una casa.

• L'esercizio originale è una casa con 3 stanze, scale al centro e un camino.
• Il nostro metodo non ti dà una casa con 4 stanze (troppo difficile) o 2 stanze (troppo facile).
• Ti dà una casa con 3 stanze, scale al centro e un camino, ma invece di mattoni rossi usa mattoni blu, e invece di un camino di pietra ne usa uno di legno.
• Risultato: Costruire la casa (risolvere l'esercizio) richiede esattamente lo stesso sforzo, gli stessi attrezzi e lo stesso tempo, anche se l'aspetto esteriore è diverso.

4. Come fa il computer a sapere che sono uguali? (Gli Alberi)

Il metodo usa una tecnica chiamata "Tabella" (o Tableau). Immagina di dover dimostrare che una frase è vera. Il computer costruisce un albero dove ogni ramo è un passo logico.

• Se l'albero dell'esercizio originale ha 10 rami che si incrociano in un certo modo, il computer cercherà di costruire nuovi alberi che abbiano esattamente la stessa forma.
• Se la forma dell'albero è identica, allora la difficoltà di "arrampicarsi" su quell'albero (risolvere il problema) è identica.

5. Perché è utile?

Questo sistema permette agli insegnanti di:

• Generare infinite varianti di un esercizio senza doverle inventare a mano.
• Garantire che uno studente non abbia un "vantaggio" o uno "svantaggio" ingiusto rispetto ai compagni solo perché gli è toccato un esercizio più facile o più difficile.
• Creare test personalizzati: se uno studente sbaglia, il sistema può generare un nuovo esercizio della stessa difficoltà per farglielo riprovare, o uno leggermente diverso per vedere se ha capito il concetto.

In sintesi

Questo articolo descrive un metodo per creare esercizi di logica "gemelli". Non sono copie esatte (quello sarebbe noioso), ma sono costruiti con lo stesso "scheletro" logico. È come se avessi un stampo magico che ti permette di creare infinite torte diverse (con gusti e decorazioni diverse), ma che richiedono esattamente lo stesso tempo e le stesse abilità per essere cotte.

Questo aiuta gli insegnanti a risparmiare tempo e gli studenti a imparare in modo più equo ed efficace.

Sommario tecnico

Ecco un riassunto tecnico dettagliato del paper in italiano, strutturato secondo le sezioni richieste.

Titolo: Un metodo per la generazione automatizzata di esercizi di dimostrazione con livelli comparabili di complessità dimostrativa

1. Il Problema

La generazione automatica di domande (Automatic Question Generation - AQG) è uno strumento promettente per ridurre il carico di lavoro degli educatori nella progettazione di esercizi. Tuttavia, l'adozione di tali sistemi in ambito pedagogico, specialmente nelle materie formali come la logica e la matematica discreta, è ostacolata dalla difficoltà di controllare la difficoltà degli esercizi generati.

• Limitazioni degli approcci esistenti: Molti sistemi AQG attuali si basano su modelli di apprendimento automatico (QDET) che stimano la difficoltà basandosi su giudizi umani o su metriche sintattiche superficiali (es. numero di connettivi, profondità della formula).
• Il gap: Queste metriche non catturano l'effettivo sforzo cognitivo richiesto per risolvere una dimostrazione. Due formule con la stessa struttura sintattica possono richiedere strategie di prova molto diverse. Inoltre, i metodi basati su ML mancano di spiegabilità e possono essere incoerenti.
• Obiettivo: Sviluppare un metodo per generare esercizi di dimostrazione (in logica del primo ordine) che abbiano un livello di complessità dimostrativa comparabile a quello di un esercizio di input, garantendo che la difficoltà sia controllata in modo rigoroso e spiegabile.

2. Metodologia

L'approccio proposto si basa sulla formalizzazione della complessità dimostrativa attraverso tableau basati sul taglio (cut-based tableaux) specifici per una teoria, privi di simboli logici.

A. Fondamenti Teorici e Definizioni

• Teorie Definitive: Il sistema opera su una "teoria definitoria" $\langle L, Ax, < \rangle$, dove $L$ è un linguaggio del primo ordine, $Ax$ è un insieme finito di assiomi definitori (es. teoria degli insiemi) e $<$ è una relazione ben fondata sui simboli predicativi.
• Regole Specifiche della Teoria: Invece di usare regole logiche generali, il metodo estrae regole lineari dai assiomi definitori. Queste regole operano su formule "specifiche della teoria" (atomiche, senza quantificatori o connettivi logici espliciti).
  • Estrazione: Gli assiomi vengono trasformati in Forma Normale Implicazionale delle Regole (RINF) tramite Prenex Normal Form, Skolemizzazione e CNF.
  • Restrizioni Analitiche: Le regole estratte devono rispettare vincoli analitici (le variabili della conclusione devono essere presenti nelle premesse; i simboli predicativi devono ridursi secondo la relazione $<$ o la profondità sintattica). Questo garantisce che le dimostrazioni siano finite e controllate.
• Tableau Specifici della Teoria: Le dimostrazioni sono rappresentate come alberi (tableau) espansi applicando queste regole. Vengono introdotti anche tagli (cut) basati su premesse "minori" e "maggiori" per gestire la chiusura dei rami in modo efficiente.

B. Definizione della Complessità Dimostrativa
La complessità non è misurata dalla lunghezza della stringa, ma dalla struttura della dimostrazione minima:

1. Isomorfismo Deduttivo: Due dimostrazioni sono considerate isomorfe se i loro "alberi di giustificazione" (che tracciano le dipendenze logiche tra i nodi fino alla chiusura) sono isomorfi, preservando l'isomorfismo sintattico delle formule.
2. Dimensione Deduttiva: È la somma dei nodi negli alberi di giustificazione di tutti i rami chiusi.
3. Complessità Comparabile: Due esercizi hanno complessità comparabile se ammettono dimostrazioni minime che sono deduttivamente isomorfe e se le formule di partenza (dati e obiettivi) sono in corrispondenza biunivoca sintattica.

C. Procedura di Generazione
Il processo di generazione avviene in due fasi principali:

1. Ricerca di Dimostrazioni Minime: Dato un esercizio di input (descritto come un insieme di formule firmate refutabili), il sistema costruisce iterativamente tableau fino a trovare tutte le dimostrazioni minime (quelle con la dimensione deduttiva più bassa).
2. Ricerca di Insiemi Isomorfi: Il sistema genera nuovi esercizi sostituendo i simboli (predicati e funzioni) nell'esercizio di input con altri simboli della stessa teoria.
   • Filtro di Rigidità: Non tutte le sostituzioni sono valide. Vengono calcolati i simboli di corrispondenza deduttiva (deductive matching symbols) basati sulla struttura della dimostrazione minima trovata. Solo le sostituzioni che preservano l'isomorfismo deduttivo della dimostrazione originale sono accettate.
   • Questo riduce drasticamente lo spazio di ricerca (es. da migliaia di casi a poche centinaia) garantendo che ogni nuovo esercizio generato abbia la stessa "struttura di sforzo" dell'originale.

3. Contributi Chiave

• Nuova Metrica di Difficoltà: Introduzione di un metodo per quantificare la difficoltà basato sulla struttura deduttiva minima (isomorfismo degli alberi di giustificazione) piuttosto che su metriche sintattiche superficiali o stime statistiche.
• Tableau senza Simboli Logici: Sviluppo di un sistema di tableau "specifico per la teoria" che elimina i simboli logici ($\neg, \land, \lor, \to$) dalle formule, operando direttamente su concetti matematici (es. appartenenza, inclusione), rendendo la complessità più vicina all'intuizione umana di un "argomento elementare".
• Procedura di Estrazione Automatizzata: Un algoritmo meccanizzabile per estrarre regole di prova dagli assiomi di una teoria (es. Teoria degli Insiemi) trasformandoli in forme implicazionali.
• Algoritmo di Generazione Isomorfa: Un metodo computazionale per generare nuovi esercizi garantendo l'isomorfismo deduttivo, evitando la generazione di esercizi "falsamente" difficili o troppo semplici.
• Implementazione Prototipale: Sviluppo di un prototipo (disponibile su GitHub) che dimostra la fattibilità del metodo sulla teoria degli insiemi.

4. Risultati

• Efficacia nella Teoria degli Insiemi: Il metodo è stato testato con successo sulla teoria degli insiemi (con operatori come $\in, \subseteq, \cup, \cap, \setminus, \times, \triangle$).
• Generazione di Esercizi Comparabili: Il sistema è stato in grado di generare esercizi come "Prova che $x \in y \cap (w \cup z) \implies x \in (y \cap w) \cup z$" e varianti strutturalmente diverse (es. sostituendo $\cap$ con $\setminus$ o $\triangle$) che, pur avendo formule diverse, richiedono esattamente lo stesso sforzo dimostrativo (stessa struttura dell'albero di giustificazione).
• Riduzione dello Spazio di Ricerca: L'uso dei "simboli di corrispondenza deduttiva" ha permesso di ridurre il numero di candidati da testare di un fattore significativo (nell'esempio citato, da potenziali migliaia a 144 casi validi), rendendo la procedura computazionalmente fattibile.
• Validazione Concettuale: L'approccio dimostra che è possibile controllare la difficoltà in modo deterministico e spiegabile, collegando direttamente la difficoltà alla struttura della soluzione.

5. Significato e Implicazioni

• Pedagogia: Questo lavoro offre agli educatori uno strumento per creare banche dati di esercizi personalizzabili per livello di difficoltà, supportando la valutazione adattiva e la formazione personalizzata senza richiedere un intervento manuale massiccio.
• Affidabilità e Spiegabilità: A differenza dei modelli di Deep Learning ("scatola nera"), questo metodo è basato su regole logiche formali. La difficoltà è spiegabile: un esercizio è difficile perché la sua dimostrazione minima richiede un certo numero di passi e una certa struttura di regole, non perché un modello statistico lo ha classificato così.
• Futuro della Ricerca: Il metodo apre la strada a sistemi AQG per materie formali (Logica, Matematica Discreta, Algebra) che possono garantire coerenza pedagogica. Le limitazioni attuali (es. la necessità che gli esercizi siano convertibili in una specifica forma normale) sono identificate come aree di miglioramento futuro, insieme alla validazione empirica in classi reali per verificare se la complessità deduttiva corrisponde alla percezione di difficoltà da parte degli studenti.

In sintesi, il paper propone un cambio di paradigma: invece di stimare la difficoltà a priori basandosi sulla superficie dell'esercizio, si definisce la difficoltà a posteriori basandosi sulla struttura della soluzione, e si usano queste strutture per generare nuovi esercizi equivalenti.