En ny benchmark, TREAT, viser at selv de bedste AI-modeller kun genkender det korrekte matematiske teorem i 60,73% af tilfældene, når formlen præsenteres i en ækvivalent, men anderledes form. Dette rejser spørgsmål om pålideligheden af AI-systemer, der arbejder med formel viden i videnskabelige og tekniske domæner.
TREAT er designet til at teste, om sprogmodeller kan genkende et kendt teorem, når betingelsen transformeres ækvivalensbevarende – for eksempel ved at udtrykke resultatet som residualligninger, optimeringsidentiteter eller mængderelationer i stedet for standardformuleringen. Dette er ikke en simpel parafrase, men en ændring af den matematiske form i sig selv. Korpuset indeholder 737 teoremidentiteter og 29.480 transformerede rækker, hvilket giver et solidt grundlag for evaluering.
For beslutningstagere, der overvejer at implementere AI i forskning, ingeniørarbejde eller kvalitetskontrol, er dette en vigtig advarsel: Modeller kan være skrøbelige, når input repræsenteres på uventede måder. Selvom modellen er trænet på store mængder matematisk tekst, viser resultaterne, at viden ikke nødvendigvis er robust over for ækvivalente ændringer i repræsentationen. Dette kan have konsekvenser for systemer, der skal validere eller generere formelle beviser, hvor præcision er afgørende.
TREAT tilbyder også et kontrolleret testmiljø med eksplicitte ækvivalensrelationer, valideringsprocedurer og auditérbar scoring, hvilket gør det muligt at måle og forbedre modellernes repræsentationsrobusthed. For virksomheder, der bygger værktøjer til matematisk eller logisk ræsonnement, er dette en ressource til at evaluere og vælge modeller med større pålidelighed.
