FormalScience: Autoformalizzazione Human-in-the-Loop per Dimostrazioni Scientifiche in Lean

I ricercatori hanno introdotto FormalScience, un pipeline agentico human-in-the-loop indipendente dal dominio, progettato per autoformalizzare il ragionamento matematico informale in codice formalmente verificabile utilizzando il dimostratore di teoremi Lean4. Il sistema si rivolge a campi scientifici come la fisica, dove la notazione specifica del dominio (ad esempio, notazione di Dirac, calcolo vettoriale) pone ulteriori sfide di formalizzazione che gli attuali LLM e approcci agentici non hanno affrontato. FormalScience consente a un singolo esperto del dominio senza una profonda esperienza in linguaggi formali di produrre dimostrazioni formali sintatticamente corrette e semanticamente allineate a basso costo economico. Applicato alla fisica, il pipeline ha generato FormalPhysics, un dataset di 200 problemi e soluzioni di fisica universitaria in LaTeX—principalmente in meccanica quantistica ed elettromagnetismo—insieme alle loro rappresentazioni formali in Lean4. Questo lavoro affronta la scalabilità dell'autoformalizzazione nei domini scientifici.