Riassunto Tecnico: APE-Bench: Valutare l'Ingegneria Automatica delle Prove per Librerie di Matematica Formale

Definizione del Problema

Gli attuali benchmark di valutazione per la matematica formale basata su Large Language Model (LLM), come miniF2F e FATE, si concentrano principalmente sulla dimostrazione di teoremi isolati. Questi benchmark richiedono che gli agenti sintetizzino un termine di prova per un dato enunciato formale che sia tipicamente corretto (type-checks). Tuttavia, la pratica dello sviluppo della matematica formale in ambienti di produzione (ad esempio, Mathlib) si è evoluta in ingegneria delle prove su scala di repository. Lo sviluppo reale comporta la coordinazione tra più file, l'evoluzione della libreria, la gestione delle dipendenze tra file diversi e la manutenzione sotto variazione — compiti che i benchmark di dimostrazione di teoremi isolati non riescono a catturare. Gli strumenti esistenti per la manutenzione delle prove (ad esempio, iCoq, REPLICA) rimangono ampiamente euristici e richiedono un significativo sforzo manuale. Vi è una mancanza di un framework sistematico per valutare gli agenti IA sulle attività di ingegneria su scala di repository che caratterizzano lo sviluppo reale della matematica formale.

Metodologia

1. Formulazione dell'Ingegneria Automatica delle Prove (APE)

Gli autori introducono l'Automated Proof Engineering (APE) come una formulazione del compito che operazionalizza l'ingegneria delle prove su scala di repository. Un compito APE è definito da tre componenti:

• Ambiente Fissato (Pinned Environment): Un commit specifico del repository e una versione della toolchain.
• Istruzione in Linguaggio Naturale: Una descrizione dell'obiettivo di ingegneria (ad esempio, "refactor", "aggiungi automazione").
• Doppia Verifica:
  • Correttezza Sintattica: Il codice modificato deve compilare con successo all'interno dell'ambiente fissato.
  • Correttezza Semantica: La soluzione deve soddisfare i requisiti in linguaggio naturale e mantenere il controllo dello scope (evitando modifiche superflue), validata tramite un LLM-as-Judge.

Questa formulazione rispecchia il paradigma SWE-bench per l'ingegneria del software, ma lo adatta alla matematica formale sostituendo i test unitari con la validazione basata sul giudizio, poiché i compiti di prova spesso mancano di suite di test preesistenti.

2. Infrastruttura APE-Harness

Per supportare una valutazione sistematica, gli autori hanno costruito l'infrastruttura di esecuzione APE-Harness, basata sull'Astrazione del Contratto del Compito (Task Contract Abstraction).

• Contratti del Compito (Task Contracts): Specifiche dichiarative che separano i requisiti del compito (obiettivi, confini, vincoli dell'ambiente, protocolli di verifica) dalle strategie di esecuzione. Ciò consente a diversi scaffold di agenti di eseguire lo stesso compito sotto identici vincoli.
• Servizi di Infrastruttura:
  • Servizi di Esecuzione (Execute Services): Compilano il codice dell'agente contro installazioni della libreria target immutabili.
  • Servizi di Recupero (Retrieve Services): Consentono la ricerca semantica limitata a specifiche versioni della libreria.
  • Isolamento del Workspace: Impone l'accesso in sola lettura alle librerie target e l'accesso in scrittura agli spazi di lavoro (scratch workspaces).
• Efficienza Multi-Versione: Il sistema utilizza l'archiviazione content-addressable (hashing crittografico) per deduplicare file identici attraverso 67 diverse versioni della libreria, ottenendo risparmi di ordini di grandezza nelle risorse di archiviazione e nei costi di embedding.

3. Costruzione di APE-Bench

APE-Bench è una pipeline automatizzata che estrae compiti di ingegneria delle prove dalle cronologie dei commit reali di Mathlib.

• Processo: Filtra i commit per modifiche sostanziali a livello di file (5–100 righe), poi utilizza un agente per sintetizzare istruzioni in linguaggio naturale dai diff.
• Validazione: La pipeline assicura che i compiti siano risolvibili e che la patch originale soddisfi l'istruzione generata sotto doppia verifica.
• Dataset: Il rilascio iniziale contiene 100 compiti estratti da 67 commit (datati dal 2026-01-01 in poi) per garantire lo zero training data contamination per i modelli frontier.

4. Scaffold di Valutazione

Il framework supporta l'intercambiabilità degli scaffold. Gli autori forniscono APE-Agent (uno scaffold di tipo ReAct con verifica integrata) e lo valutano insieme a Claude Code e Codex CLI per dimostrare che l'infrastruttura può confrontare equamente diverse implementazioni di agenti.

Contributi Chiave

1. Formulazione e Benchmark APE: La prima infrastruttura completa per la valutazione dell'ingegneria delle prove su scala di repository, dotata di una pipeline automatizzata (APE-Bench) che estrae compiti dall'evoluzione reale delle librerie.
2. Benchmark di Validazione LLM-as-Judge: Un dataset di 64 soluzioni di agenti annotate da esperti con valutazioni tridimensionali della qualità (correttezza semantica, allineamento ai requisiti, controllo dello scope) per validare l'affidabilità dei giudici LLM.
3. APE-Harness: Un'infrastruttura di esecuzione basata su contratti di compito che consente una valutazione unificata di diversi agenti, supporta workflow funzionali (come la sintesi delle istruzioni) e permette l'intercambiabilità degli scaffold.
4. APE-Agent: Uno scaffold white-box, di tipo ReAct, con strumenti di sistema di file e verifica integrati per facilitare la ricerca e il confronto.
5. Servizi di Esecuzione Multi-Versione: Implementazione di servizi di compilazione e recupero efficienti attraverso molteplici versioni della libreria utilizzando la deduplicazione del contenuto.

Risultati

Prestazioni dei Modelli

Gli autori hanno valutato i modelli frontier (GPT-5.2, Gemini 3 Pro, Gemini 3 Flash) su APE-Bench, miniF2F e miniCTX utilizzando un budget fisso di $3 per compito.

• Difficoltà di APE-Bench: L'ingegneria su scala di repository si è rivelata significativamente più difficile della dimostrazione isolata. Su APE-Bench, Gemini 3 Flash ha raggiunto un tasso di successo del 47,0%, superando GPT-5.2 (27,0%) e Gemini 3 Pro (24,0%).
• Confronto con la Dimostrazione Isolata: Su miniF2F e miniCTX, i modelli hanno raggiunto tassi di successo molto più elevati (73–94%), indicando che la difficoltà in APE-Bench deriva dalla complessità dell'ingegneria (coordinazione, controllo dello scope) piuttosto che dalla pura capacità di dimostrazione dei teoremi.
• Efficienza: I gap di prestazione sono stati guidati dall'efficienza dei costi. Gemini 3 Flash ha ottenuto tassi di successo più elevati non grazie a un ragionamento superiore per turno, ma evitando l'esaurimento prematuro del budget causato da chiamate a strumenti costose o prompt verbali.

Analisi di Scaffold e Strumenti

• Intercambiabilità dello Scaffold: APE-Agent ha superato significativamente Claude Code e Codex CLI (di 15–23 punti percentuali) su compiti identici.
  • Ragioni: La verifica integrata di APE-Agent (edit atomico + compilazione) ha ridotto le chiamate ridondanti. Al contrario, Claude Code e Codex hanno incoraggiato costi più elevati a causa di prompt verbali, chiamate di esecuzione separate e pattern di recupero conservativi.
• Ablazione degli Strumenti: Rimuovere il recupero, la shell o le operazioni sui file ha portato solo a cali di prestazione marginali (nell'ordine del 44–47%). Ciò suggerisce che il collo di bottiglia principale è la capacità di ragionamento dei modelli per compiti su scala di repository, non la disponibilità di strumenti specifici.

Affidabilità del Giudice

La pipeline LLM-as-Judge ha dimostrato un'elevata accuratezza (90,6% complessivo) rispetto alle annotazioni degli esperti umani attraverso le dimensioni di correttezza semantica, allineamento ai requisiti e controllo dello scope, validando il suo uso per la valutazione automatizzata.

Efficienza dell'Infrastruttura

La deduplicazione del contenuto ha ridotto i requisiti di archiviazione per 67 versioni della libreria da 480GB a 71GB (riduzione dell'85%) e ha ridotto i costi di embedding per i servizi di recupero del 98,5% (\12,9K a \197).

Significato

Il paper sostiene di aver stabilito una base per la valutazione sistematica degli agenti IA sull'ingegneria della matematica formale su scala di repository. Spostando il paradigma della valutazione dalla dimostrazione di teoremi isolati all'ingegneria delle prove, APE-Bench colma il divario tra le attuali capacità dell'IA e le reali richieste di manutenzione delle librerie formali in produzione. Il lavoro dimostra che:

1. L'ingegneria delle prove su scala di repository è un compito distinto e significativamente più impegnativo rispetto alla dimostrazione di teoremi isolati.
2. L'astrazione del contratto del compito consente un confronto equo e standardizzato di diverse architetture di agenti.
3. Gli attuali modelli frontier mostrano promessa ma affrontano ostacoli sostanziali nella disciplina ingegneristica, nel controllo dello scope e nell'efficienza dei costi quando applicati alla manutenzione reale delle librerie.

Gli autori rilasciano tutto il codice e il dataset del benchmark come open-source per facilitare ulteriori ricerche in questo dominio.