Datamaskiner kan teste matematiske formodninger

Avhandlingen viser at datamaskiner kan brukes til automatisk å bevise eller avkrefte grafteoretiske formodninger for hele familier av grafer med avgrenset struktur. Rammeverket gir nye teoretiske grenser for størrelsen på slike automatiske bevis og motbevis og gjør det mulig å lete systematisk etter konkrete moteksempler.

Grafer er matematiske modeller for nettverk og består av punkter og forbindelser. Metoden bruker et mål som kalles grafbredde, og som grovt sagt beskriver hvor sammensatt forbindelsesmønsteret i en graf er. Grafer med liten bredde kan deles inn i små, trelignende deler som analyseres trinn for trinn ved hjelp av dynamisk programmering. For en fast breddegrense kan systemet avgjøre om en påstand gjelder for alle grafer innenfor denne grensen.

To teknikker gjør metoden langt mer effektiv i praksis ved å redusere antallet unødvendige beregninger. Dermed kan systemet undersøke større og mer krevende tilfeller.

Rammeverket ble brukt til å undersøke formodninger om fargelegging av trekantfrie grafer. Det verifiserte automatisk Reed-grensen for trekantfrie grafer i alle de undersøkte grafklassene med begrenset trebredde og stibredde. Systemet fant også moteksempler på ugyldige, sterkere varianter av formodningen.

Resultatene viser at automatisert teorembevisning for breddebegrensede grafklasser kan bli et nyttig verktøy for matematikere. Metoden kan bekrefte resultater for strukturerte grafklasser, avdekke påstander som er for sterke, og identifisere tilfeller som krever videre teoretisk arbeid.

Personalia

Sam Urmian er forsker ved Centre for the Science of Learning & Technology (SLATE) ved Universitetet i Bergen. Forskningen omfatter algoritmedesign, automatisert teorembevisning og algoritmisk læringsteori. Doktorgradsarbeidet er utført ved Institutt for informatikk under veiledning av Mateus de Oliveira Oliveira. Urmian leder også den norske olympiaden i kunstig intelligens (NOKI).