Nowe badanie z arXiv pokazuje, że autonomiczne agenty AI przy konstruowaniu formalnych dowodów matematycznych zachowują się fundamentalnie inaczej niż ludzie - nawet gdy pracują nad tymi samymi zadaniami. Naukowcy zgłębili to zjawisko poprzez analizę 4,7 miliona definicji z ponad 6 tysięcy zmian w dziewięciu głównych projektach wspólpracy człowieka i AI w systemie Lean, najpopularniejszym asystencie dowodzenia twierdzeń.
AI agenty wykazują trzy kluczowe różnice w podejściu. Po pierwsze, znacznie bardziej przyciągają je jawnie zaznaczone luki w dowodach, podczas gdy ludzie skupiają się na głębszych strukturach. Po drugie, unikają gęsto połączonych sekcji dowodów i skomplikowanych celów - systemy AI są konserwatywne tam, gdzie ludzie chętnie idą w nieznane. Po trzecie, agenty są fascynowane zaskakującymi elementami dowodów, ale mają tendencję do ich ujednolicania i regularyzacji zamiast zachowywania oryginalnej elegancji.
Wyniki ujawniają ważne słabe punkty obecnych systemów AI w matematyce formalnej. Choć modele językowe generujące dowody przyczyniają się do eksplozji nowych twierdzeń, rzeczywista współpraca człowieka z AI wymaga głębszego zrozumienia tych rozbieżności w podejściu. Badania sugerują, że przyszłe systemy powinny lepiej łączyć ludzką intuicję z mocnymi stronami AI, zamiast pozwalać agentom działać w całkowitej autonomii.