Axiom Math satser på formell verifisering for å sikre matematisk integritet

Publisert 2026-11-05

Ingress: Oppstartsselskapet Axiom Math benytter KI-agenter for å drive formell verifisering av matematiske bevis. Dette tiltaket er et svar på den økende mengden ubekreftet materiale som genereres av store språkmodeller i akademia.

Bakgrunn Etter hvert som generativ kunstig intelligens blir mer utbredt, øker også volumet av matematisk innhold produsert av maskiner. Utfordringen er at KI-modeller ofte «hallusinerer» eller frembringer logiske feil, noe som utgjør en betydelig risiko for matematisk forskning der presisjon er et absolutt krav.

Axiom Math har nylig markert seg ved å benytte sine egne KI-agenter til å verifisere Stacks Project, et av verdens største digitale biblioteker for algebraisk geometri. Dette arbeidet innebærer å konvertere komplekse menneskeskapte bevis til et maskinlesbart format som kan kontrolleres matematisk av en datamaskin.

Formell verifisering skiller seg fra tradisjonell fagfellevurdering ved at bevisene brytes ned i logiske fundamenter. Dersom en eneste slutning i et bevis er ugyldig, vil systemet flagge dette, uavhengig av hvor overbevisende selve teksten fremstår.

Norsk kontekst For norske forskningsmiljøer ved institusjoner som NTNU og Universitetet i Oslo, representerer verktøy som Axiom Math en endring i hvordan man kan kvalitetssikre store beregningsorienterte prosjekter. Innen fagfelt som kryptografi og kompleks systemanalyse, hvor matematiske modeller ligger til grunn for kritisk infrastruktur, kan formell verifisering bli en standard snarere enn et unntak.