AxQM: un benchmark su scala di manuale per la sintesi di dimostrazioni formali in una libreria di meccanica quantistica a dimensione finita

Abstract degli autori

La formalizzazione della matematica in un assistente di dimostrazione, in cui una macchina controlla ogni definizione, enunciato e dimostrazione, ha stabilito un nuovo standard di rigore. Oggi i modelli linguistici di grandi dimensioni sono in grado di formalizzare autonomamente, persino su scala di interi manuali. Applichiamo questo standard di rigore alla fisica, dove gli argomenti teorici incorporano idealizzazioni che raramente vengono esplicitate per intero e qualsiasi lacuna logica potrebbe avere effetti a cascata su risultati interdipendenti. Riconoscendo la necessità di valutare i sistemi di autoformalizzazione per la fisica, rendiamo disponibile AxQM: 1.019 compiti di sintesi di dimostrazioni verificabili dal kernel, relativi a 479 voci tratte dal manuale Quantum Computation and Quantum Information di Nielsen e Chuang. I compiti sono formulati in una libreria personalizzata di Lean dedicata alla meccanica quantistica a dimensione finita. In termini di numero di compiti, è il più grande benchmark di sintesi di dimostrazioni in fisica, con un numero di compiti quattro volte superiore a quello del benchmark successivo. AxQM deriva da una formalizzazione quasi completa delle parti formali del manuale, perciò è garantito che ogni compito abbia una soluzione, che manteniamo riservata. La valutazione del benchmark è eseguita in modo deterministico dal kernel di Lean, che verifica che la dimostrazione venga compilata, che non contenga sorry né questo compaia in alcuna dichiarazione da cui essa dipende, e che non introduca nuovi assiomi.