Riepilogo Tecnico: MATHLIBPR – Un Benchmark per la Prontezza alla Revisione di Librerie Matematiche Formali

1. Definizione del Problema

L'ecosistema di Lean e Mathlib è diventato lo standard per il ragionamento formale assistito da modelli linguistici di grandi dimensioni (LLM), con recenti successi nella risoluzione di problemi a livello di olimpiadi (MiniF2F), nella matematica competitiva (AlphaProof) e in progetti di formalizzazione su larga scala (agente Gauss). Tuttavia, questi sistemi principalmente consumano Mathlib come dipendenza piuttosto che contribuire ad esso. Sebbene il codice generato dagli LLM possa essere verificato per correttezza dal kernel di Lean, determinare se un contributo sia "pronto per l'unione" (merge-ready) – ovvero, aderisca alle convenzioni della comunità, mantenga la coerenza della libreria e sia adatto alla manutenzione a lungo termine – richiede una revisione umana.

La revisione umana è attualmente il principale collo di bottiglia per la crescita di Mathlib, con un backlog di circa 300 pull request (PR) e tempi di attesa medi di due settimane. La domanda centrale affrontata da questo articolo è: Gli LLM possono aiutare a revisionare le PR di Mathlib? Nello specifico, possono distinguere tra codice che supera la compilazione e pronto per l'integrazione e codice che supera la compilazione ma richiede revisione o verrà rifiutato?

2. Metodologia

2.1 Costruzione del Dataset: MATHLIBPR

Gli autori introducono MATHLIBPR, un benchmark costruito da storie reali di PR di Mathlib4.

• Fonte: PR chiuse del repository leanprover-community/mathlib4 (al 5 aprile 2026).
• Criteri di Selezione: Il benchmark si concentra esclusivamente su istantanee che superano la compilazione. Questo elimina strategie banali basate su errori di sintassi o fallimenti di compilazione, costringendo i modelli a giudicare in base alla qualità del codice e alle convenzioni.
• Etichette:
  • Pronto per l'Unione: Istantanee accettate nel ramo master.
  • Non Pronto per l'Unione: Istantanee che hanno superato i controlli di compilazione ma sono state riviste prima dell'accettazione o appartenevano a PR che non sono mai state unite.
• Composizione: Il dataset finale contiene 15.895 istantanee etichettate provenienti da 12.063 PR (11.409 pronte per l'unione, 4.486 non pronte per l'unione). Include 3.687 coppie all'interno della stessa PR (un'istantanea precedente che supera la compilazione contro la versione finale accettata) per testare il riconoscimento del progresso nelle revisioni.

2.2 Protocollo di Valutazione

Gli autori propongono un protocollo di valutazione a tre stadi che fornisce progressivamente un contesto più ricco ai modelli:

• Stadio 1: Evidenza locale al codice (diff, file modificati) e riassunti compatti delle linee guida di Mathlib (nomenclatura, stile, documentazione).
• Stadio 2: Aggiunge diagnosi strutturate (linting, import, posizionamento delle dichiarazioni, adattamento all'API) derivate da registri storici di controlli GitHub o ricostruiti localmente.
• Stadio 3: Aggiunge titolo e descrizione della PR come intento dichiarato.

2.3 Sistemi Valutati

Il benchmark valuta due classi di sistemi:

1. Modelli LLM: DeepSeek-R1-Distill-Qwen, Qwen3-8B, Goedel-Prover-V2-32B (pre-addestrato su Mathlib) e Kimina-Prover-Distill-8B.
2. Agenti LLM: Codex (GPT-5.4) e Claude Code (Claude Sonnet 4.6). Gli agenti operano in un checkout locale del repository in sola lettura, limitati dal modificare file, accedere al web o recuperare esiti delle PR.

2.4 Schema di Output e Metriche

Ai sistemi è richiesto di produrre una revisione strutturata in JSON invece di testo libero. Lo schema include:

• Verdetto: merge_ready, not_merge_ready o uncertain.
• Punteggio: Un punteggio scalare di prontezza all'unione ($p_{merge\_ready}$).
• Assi: Valutazioni su otto dimensioni della rubrica (nomenclatura, documentazione, struttura locale, posizionamento dei file, import, leggibilità delle prove, adattamento all'API, sovrapposizione con il repository).

Metriche:

• Recall MR/NMR: Recall per le classi pronte per l'unione e non pronte per l'unione (trattando uncertain e output non validi come errori).
• Accuratezza Bilanciata: Media del recall MR e NMR.
• Tasso di Output Validi: Percentuale di output conformi allo schema entro i budget di tempo di esecuzione.
• AUROC: Area sotto la curva ROC basata sui punteggi scalari.

3. Risultati Chiave

3.1 Prestazioni Complessive

• Bassa Accuratezza: Nessun sistema distingue in modo affidabile le istantanee pronte per l'unione da quelle non pronte. Il modello con le prestazioni migliori (DeepSeek) ha raggiunto un'Accuratezza Bilanciata del 36,0% allo Stadio 3, significativamente al di sotto della baseline casuale del 50% per un compito bilanciato (sebbene il dataset sia sbilanciato, le metriche di recall evidenziano il fallimento).
• Asimmetria delle Classi: I sistemi mostrano un forte pregiudizio verso la previsione di merge_ready.
  • DeepSeek (Stadio 3): 69,8% di Recall MR, ma solo 2,3% di Recall NMR.
  • Qwen (Stadio 3): 48,3% di Recall MR, 0,0% di Recall NMR.
  • Codex (Agente): 92,0% di Recall MR, ma solo 12,0% di Recall NMR.
• Impatto del Contesto: L'aggiunta di diagnosi e intento della PR (Stadio 2 e 3) ha prodotto guadagni limitati e disomogenei. Ad esempio, l'accuratezza bilanciata di DeepSeek è migliorata dal 18,1% al 36,0%, ma la sua capacità di identificare codice non pronto per l'unione è rimasta vicina allo zero.

3.2 Prestazioni Agente vs Modello

• Agenti: Sebbene Codex abbia mostrato un'alta affidabilità operativa (99,9% di tasso di output validi) e un alto Recall MR, non è riuscito a identificare codice non pronto per l'unione. Claude Code ha avuto un'affidabilità inferiore (56,4% di tasso valido) e un simile scarso Recall NMR.
• Modelli Specializzati: Goedel e Kimina, nonostante siano addestrati su prove formali, hanno performato male. Il tasso di output validi di Goedel è crollato dal 68,3% (Stadio 1) al 13,5% (Stadio 3), e entrambi i modelli hanno prodotto frequentemente output non validi (prosa o blocchi di codice) invece dello schema JSON richiesto.

3.3 Analisi All'interno della PR

In un confronto controllato tra istantanee precedenti che superano la compilazione e istantanee finali accettate dalla stessa PR:

• I modelli hanno appena battuto il caso. L'accuratezza pairwise di DeepSeek si è stabilizzata al 51,1% (Stadio 3), e Qwen è rimasta vicina al 49,1%.
• Ciò indica che i modelli non riescono a rilevare in modo affidabile i miglioramenti specifici che hanno portato all'accettazione di una PR, anche confrontando due versioni dello stesso contributo.

3.4 Analisi degli Errori

• Astensione: I sistemi spesso si astengono (uncertain) sugli assi di documentazione o leggibilità delle prove.
• Output Non Validi: Una porzione significativa di output dai modelli specializzati (Goedel, Kimina) e dagli agenti (Claude Code) è stata non valida a causa di violazioni dello schema, timeout o fallimenti nella produzione di JSON. Ciò suggerisce una discrepanza tra gli obiettivi di addestramento dei modelli (prova di teoremi) e l'interfaccia di revisione strutturata.

4. Contributi

1. Benchmark MATHLIBPR: Il primo benchmark per valutare gli LLM sulla prontezza all'unione di contributi a Mathlib che superano la compilazione, derivato da storie reali di PR.
2. Protocollo di Valutazione a Stadi: Un protocollo che testa sistematicamente se un contesto più ricco (diagnosi, intento della PR) migliora il giudizio simile a quello di un revisore.
3. Studio Empirico: Una valutazione completa che mostra come gli attuali LLM e agenti faticino a distinguere il codice pronto per l'unione dal codice che supera la compilazione ma richiede revisione, evidenziando un divario tra correttezza del codice e qualità dell'integrazione nella libreria.

5. Significato e Affermazioni

L'articolo afferma che MATHLIBPR fornisce un passo verso assistenti per revisori e modelli di ricompensa per librerie matematiche formali.

• Stato Attuale: I risultati dimostrano che giudicare la prontezza all'unione è una capacità sostanzialmente più difficile rispetto al rilevamento di errori di sintassi o fallimenti di compilazione. Gli attuali sistemi non riescono a catturare le norme di revisione sfumate necessarie per curare una libreria matematica integrata.
• Utilità Futura: Il benchmark è destinato a essere utilizzato per:
  • Assistenza al Revisore: Triaggio e individuazione di probabili ostacoli per i revisori umani.
  • Modellazione della Ricompensa: Addestramento di modelli di ricompensa utilizzando la struttura delle coppie all'interno della PR (preferendo l'istantanea finale accettata rispetto a una precedente che supera la compilazione) per orientare gli LLM verso la generazione di codice non solo corretto, ma anche manutenibile e pronto per l'unione.
• Limitazioni: Gli autori riconoscono che il benchmark copre una fetta selettiva della storia delle PR e che le etichette sono derivate da decisioni storiche dei manutentori, che possono includere fattori non tecnici. Affermano esplicitamente che l'obiettivo non è sostituire i revisori umani, ma fornire un segnale consultivo.

In conclusione, sebbene gli LLM abbiano avuto successo nella generazione di prove corrette, la transizione verso il contributo a Mathlib richiede un livello di giudizio riguardo allo stile del codice, alla documentazione e all'adattamento alla libreria che i modelli attuali non hanno ancora padroneggiato. MATHLIBPR stabilisce la baseline per misurare i progressi in questa direzione.