Zaprzężony do pracy model wygenerował strukturę formalnego dowodu poprzez kilka iteracji rozmów i wersji argumentów, co – choć wciąż wymagało ostatecznej weryfikacji ze strony ludzi – dowodzi, iż AI może kierować się logiką matematyczną na głębszym poziomie niż dotychczas sądzono. To pierwszy udokumentowany przypadek, w którym komercyjny model językowy wniósł wkład do rozwiązania problemu będącego hipotezą. ChatGPT nie tylko powtarzał znane twierdzenia czy cytował istniejące źródła, lecz po prostu zaproponował nowe powiązania pomiędzy abstrakcyjnymi pojęciami.
Czytaj też: Futurystyczny materiał zachowuje się tak, jakby nie stworzył go człowiek. Może zmieniać kolor i teksturę
W ramach swoich działań inżynierowie zorganizowali siedem sesji z AI, w których model generował kolejne fragmenty argumentacji, a następnie ludzie nadzorowali i dopracowywali logikę, by upewnić się, iż dowód był spójny. To podejście pokazuje nową rolę sztucznej inteligencji nie tyle jako kalkulatora, ale przede wszystkim jako narzędzia pomagającego organizować i eksplorować złożone idee matematyczne.
Inne eksperymenty pokazały, że AI może również radzić sobie z klasycznymi łamigłówkami matematycznymi sprzed tysięcy lat. Naukowcy z Uniwersytetu w Cambridge i Uniwersytetu Hebrajskiego poprosili system AI o rozwiązanie starożytnego problemu geometrycznego znanego z dialogów Platona i objętego dyskusjami od ponad 2400 lat. W odpowiedzi model nie tylko rozpoznał, że klasyczne rozwiązanie polega na wykorzystaniu przekątnej kwadratu, lecz zastosował własne metody, by uporać się z postawionym przed nim zadaniem.
Czytaj też: 70 lat czekania i wreszcie ją mamy. Chemicy uchwycili cząstkę kluczową dla utleniania
Te dwa przypadki ukazują różne aspekty współczesnej współpracy ludzi i sztucznej inteligencji w matematyce. W pierwszym AI generuje formalne dowody (choć wciąż przy nadzorze ekspertów) co może przyspieszyć prace nad nierozwiązanymi problemami w czystej matematyce. W drugim projekcie jego autorzy wykorzystali AI, by zrozumieć proces myślenia nad klasycznym problemem i zaobserwować, jak generatywne modele radzą sobie z abstrakcyjnymi pojęciami, które nie są wyraźnie opisane w danych treningowych.
Źródło: University of Cambridge
