h1: Un assaggio della lezione amara nella dimostrazione automatica di teoremi

Abstract degli autori

Mentre i progressi nella matematica informale sono derivati in gran parte dall’aumento delle risorse dedicate al chain-of-thought e al ragionamento agentico dei modelli linguistici di frontiera, la dimostrazione formale di teoremi si è affidata sempre più a flussi di lavoro progettati da esseri umani intorno a questi modelli, come la pianificazione, la scomposizione e il coordinamento di dimostratori specializzati. Questo solleva una domanda legata alla lezione amara: un semplice ciclo agentico, a cui si destinano risorse di calcolo crescenti in fase di test, può eguagliare questi flussi di lavoro? La risposta conta, perché la verifica formale deve crescere di scala per tenere il passo con i modelli di frontiera che producono matematica di ricerca. Eppure i nuovi flussi di lavoro raramente chiariscono la questione, poiché spesso non è possibile distinguere i loro miglioramenti dagli effetti di modelli più potenti o di maggiori risorse di calcolo. Studiamo questa domanda con h1, una semplice infrastruttura che offre a un modello un’interfaccia efficiente per Lean 4 e gli consente di continuare a lavorare grazie al feedback del verificatore e all’autoriflessione, senza imporre una struttura di scomposizione o di ricerca. h1 ottiene risultati all’avanguardia su PutnamBench, FATE-X e FormalConjectures100-Solved, risolve otto problemi aperti in FormalConjectures e, a parità di modelli, eguaglia o supera flussi di lavoro specializzati come Goedel-Architect e AlphaProof Nexus. Mostra, sorprendentemente, che spesso è possibile aumentare le risorse dedicate a un singolo tentativo (pass@1) fino a risolvere problemi aperti. Attraverso studi di ablazione e confronti a parità di modello con Claude Code e AxProverBase, riscontriamo che la sola semplicità non basta: un’interfaccia efficiente per Lean determina in larga misura i costi e il tasso di risoluzione. Raccomandiamo quindi che i lavori futuri valutino i modelli di frontiera con un feedback di esecuzione efficiente prima di prescrivere flussi di lavoro, per non rischiare amare lezioni.