Model językowy otrzymuje nieformalne sformułowanie (np. treść twierdzenia po angielsku) i generuje jego odpowiednik w języku formalnym (np. Lean), a często także szkic dowodu. Wygenerowany kod jest przekazywany do asystenta dowodzenia, który sprawdza jego poprawność; błędy i komunikaty weryfikatora wracają do modelu jako sygnał do poprawy (pętla generuj–weryfikuj–popraw). Trening i dostrajanie wykorzystują pary nieformalne↔formalne oraz uczenie ze wzmocnieniem na podstawie wyniku weryfikacji.
Formalizacja matematyki ręcznie jest bardzo pracochłonna, a LLM-y potrafią halucynować w rozumowaniu. Autoformalizacja automatyzuje przekład do postaci formalnej, którą można maszynowo zweryfikować, łącząc skalę AI z pewnością dowodu.
Generuje formalne sformułowania i dowody z treści nieformalnych.
Oficjalna
Weryfikator (np. Lean) sprawdzający poprawność wygenerowanego kodu.
Oficjalna
Komunikaty weryfikatora kierują poprawą kolejnych prób.
Oficjalna
Wu i in. pokazują, że LLM potrafią tłumaczyć matematykę na język formalny.
System łączący autoformalizację i Lean osiąga poziom medalowy na IMO.
