Gdy agent zastępuje matematyka: system autoformalizacji zdobywa twierdzenia z Putnam i STOC
Wielkie modele językowe potrafią rozwiązywać zadania matematyczne, ale też produkują subtelne błędy, które umykają ludzkiej kontroli. Badacze proponują system, który omija ten problem - z pomocą języka formalnego Lean 4, agentowego potoku i nowatorskiej techniki…
