Riepilogo Tecnico: LeanSearch v2

Definizione del Problema: Recupero Globale delle Premesse

Il documento individua una lacuna critica nella dimostrazione automatica di teoremi all'interno dell'ecosistema Lean 4. Sebbene gli strumenti esistenti eccellano nella ricerca semantica (trovare singole dichiarazioni corrispondenti a una query) o nella selezione delle premesse (prevedere lemma utili per un singolo passo di tattica), falliscono nel recupero globale delle premesse.

Il recupero globale delle premesse è definito come il compito di identificare l'insieme completo e logicamente coerente dei lemma della libreria necessari per dimostrare un intero teorema. Ciò si distingue dalla ricerca di un singolo documento rilevante per i seguenti motivi:

1. Non-località: I lemma necessari risiedono spesso in moduli distanti della libreria (Mathlib) e non condividono alcuna sovrapposizione lessicale con l'enunciato del problema.
2. Dipendenza Strategica: La connessione tra il problema e i lemma non è semantica ma strutturale, basandosi sull'"architettura logica" di una strategia di dimostrazione (ad esempio, rimodellare un obiettivo per corrispondere all'interfaccia di un teorema).
3. Completezza: L'omissione di un singolo lemma essenziale da un insieme di tre o quattro rende la dimostrazione incompleta, un modo di fallimento non catturato dalle metriche standard di rilevanza dei documenti.

Gli autori sostengono che, senza un recupero efficace delle premesse globali, i dimostratori AI sprecano risorse computazionali nel riprovare lemma locali esistenti e faticano a generare dimostrazioni efficienti e idiomatiche.

Metodologia: LeanSearch v2

LeanSearch v2 è un sistema di recupero a due modalità progettato per affrontare questa sfida.

1. Modalità Standard (Il Substrato di Recupero)

La modalità Standard funge da motore di ricerca ad alte prestazioni per le singole dichiarazioni di Mathlib e costituisce la base per la modalità di ragionamento.

• Costruzione del Corpus: Il sistema utilizza Jixia, uno strumento di analisi statica, per estrarre tutte le dichiarazioni da Mathlib. Costruisce un grafo delle dipendenze ed esegue l'informalizzazione gerarchica dal basso verso l'alto. Questo processo genera descrizioni in linguaggio naturale per ciascuna dichiarazione incorporando le descrizioni già informalizzate delle sue dipendenze, assicurando che le descrizioni siano radicate in concetti matematici piuttosto che in identificatori opachi.
• Pipeline: Adotta una pipeline a due stadi embedding–reranker utilizzando modelli pronti all'uso (Qwen3-Embedding-8B e Qwen3-Reranker-8B) senza affinamento specifico per il dominio.
  • Embedding: Le query e gli elementi del corpus sono codificati utilizzando un template di passaggio strutturato che include il tipo di dichiarazione, la firma del tipo e la descrizione informalizzata.
  • Reranking: Un reranker consapevole del tipo assegna un punteggio alle coppie query-candidato, gestendo specificamente definizioni e istanze per superare le difficoltà di recupero osservate nei sistemi precedenti.

2. Modalità di Ragionamento (Recupero Globale delle Premesse)

La modalità di Ragionamento si basa sulla Modalità Standard per recuperare insiemi di premesse attraverso un ciclo iterativo schizzo-recupero-riflessione.

• Generazione dello Schizzo: Dato l'enunciato di un teorema, un generatore (Claude Sonnet 4.5) propone una bozza di dimostrazione passo dopo passo, decomponendo il teorema in sotto-query. Non scrive codice ma definisce le mosse matematiche e le intenzioni di recupero.
• Recupero e Filtraggio: Ogni sotto-query viene inviata alla Modalità Standard. Un modello filtro (Kimi K2 Instruct) valuta i migliori candidati, permettendo esplicitamente insiemi vuoti se nessun lemma recuperato è genuinamente utile per un passo specifico.
• Giudizio di Fattibilità e Riflessione: Un modello giudice esamina i risultati filtrati.
  • Se l'insieme dei lemma supporta la strategia di dimostrazione, il ciclo termina.
  • Se l'insieme è insufficiente (ad esempio, manca una premessa o suggerisce un percorso non valido), il giudice fornisce feedback strutturato a un revisionatore dello schizzo, che modifica la bozza di dimostrazione e rientra nel ciclo.
• Aggregazione: Gli output finali vengono aggregati utilizzando una regola di sconto basato sul rango attraverso le sotto-query per formare un elenco unificato di lemma di supporto.

Contributi Chiave

1. Formulazione del Compito: Il documento definisce formalmente il recupero globale delle premesse come una sfida distinta che richiede il recupero di insiemi di premesse logicamente coerenti piuttosto che di singoli documenti.
2. Benchmark: Vengono introdotti due benchmark curati da esperti:
   • MathlibQR: 200 dichiarazioni e 946 query per valutare la ricerca a query singola (Modalità Standard).
   • MathlibMPR: 69 teoremi da pull request fuse con gruppi di premesse annotati da esperti (1–8 per teorema) per valutare il recupero globale delle premesse (Modalità di Ragionamento).
3. Prestazioni del Sistema: LeanSearch v2 ottiene risultati all'avanguardia senza affinamento specifico per il dominio.
   • Modalità Standard: Raggiunge un nDCG@10 di 0,62 su MathlibQR, superando il sistema successivo migliore (0,53).
   • Modalità di Ragionamento: Su MathlibMPR, recupera il 46,1% dei gruppi di premesse di verità fondamentale tra i primi 10 candidati, superando significativamente le linee di base di recupero per ragionamento (38,0%) e i sistemi di selezione delle premesse (9,3%).
4. Validazione a valle: In un esperimento controllato con un ciclo di dimostratore fisso, sostituire altri recuperatori con la modalità di ragionamento di LeanSearch v2 ha aumentato i tassi di successo delle dimostrazioni al 20% (contro il 16% del successivo migliore e il 4% senza recupero), dimostrando che la qualità del recupero si propaga direttamente alla generazione della dimostrazione.

Significato e Affermazioni

Il documento posiziona questo lavoro come il primo ad applicare tecniche di recupero-ragionamento specificamente al problema del recupero delle premesse in Lean. Gli autori affermano che, sebbene sistemi agenti potenti possano talvolta compensare un recupero debole attraverso la riformulazione ripetuta delle query o la dimostrazione locale, il divario tra una dimostrazione semplicemente compilabile e una efficiente e idiomatica dipende fondamentalmente dall'identificazione e dal riutilizzo dei risultati esistenti della libreria.

Il significato risiede nell'istituire il recupero come un asse distinto di progresso per la matematica formale. Disaccoppiando il substrato di recupero dal ciclo di generazione della dimostrazione, il sistema permette il miglioramento indipendente delle strategie di recupero. Gli autori notano che, sebbene la metodologia sia agnostica rispetto al linguaggio nel design, la valutazione attuale è esclusiva per Lean 4/Mathlib, e il comportamento di tali sistemi all'interno di architetture di agenti altamente capaci su compiti complessi a livello di repository rimane un'area aperta per future esplorazioni.

Il documento conclude che la combinazione di un corpus con gerarchia informalizzata, una pipeline di recupero consapevole del tipo e un ciclo iterativo schizzo-recupero-riflessione fornisce una soluzione robusta alla sfida di trovare i lemma sparsi e non locali necessari per le dimostrazioni formali moderne.