Et nyt forskningsprojekt fra arXiv introducerer Euclid-Omni, en ramme der kobler formel geometri-logik med store sprogmodeller (LLM'er) og vision-sprogmodeller (VLM'er). Målet er at løse både beregnings- og bevisopgaver i geometri – helt op til olympiade-niveau. Det er første gang, en samlet tilgang kombinerer diagramforståelse, aksiomatisk deduktion og algebraisk beregning i én arkitektur.
Kernen er den symbolske solver Euclidea, som automatisk genererer ræsonnementstrin gennem deduktiv inferens og algebraisk beregning. Derudover har forskerne bygget en data-genereringspipeline, der syntetiserer symbolsk opgaver og løsninger, renderer diagrammer og oversætter dem til naturligt sprog. Det giver store, varierede datasæt til træning af både LLM'er og VLM'er.
Resultaterne viser, at VLM'er trænet på de syntetiske data klarer sig bedre på beregningsopgaver, og at LLM'er kombineret med Euclidea er konkurrencedygtige med state-of-the-art-systemer på olympiade-bevisopgaver – men med ordrer af størrelse mindre beregningskraft og træningsdata. Det er en markant forskel i ressourceforbrug, som kan have strategisk betydning for virksomheder og organisationer, der bygger AI-løsninger til matematik, uddannelse eller formel ræsonnement.
For beslutningstagere betyder det, at avancerede ræsonnementsevner ikke længere kun er forbeholdt dem med enorme compute-budgetter. Tilgangen peger på en vej mod mere effektive, specialiserede systemer, der kan integreres i produkter uden de store infrastrukturinvesteringer. Samtidig understreger den værdien af at kombinere symbolsk logik med neurale modeller – en retning, der kan få betydning langt ud over geometri, eksempelvis inden for formel verifikation, matematik-assistance og automatiseret bevisføring.
