Proving Theorems Using Deep Learning

Abstract

Interaktive teorembevissystemer (ITP-systemer) er symbolbaserte programvaresystemer som brukes til å skrive og verifisere formelle matematiske bevis. Disse systemene inneholder ofte store datasett med menneskeskrevne formaliserte bevis, strukturert som trinnvise applikasjoner av bevis-strategier kalt taktikker. Rommet av mulige taktikker er veldefinert og inneholder en kombinasjon av kjernetaktikker og taktikkargumenter. Taktikkargumenter refererer som regel enten til allerede beviste teoremer eller termer og hypoteser i den lokale beviskonteksten. Nylig har flere forskningsgrupper fokusert på automatisering av ITP-systemer ved å trene maskinlæringsmodeller til å forutsi hvilken neste taktikk som skal brukes i bevissøket. Dette har resultert i rammeverk utviklet for mer tilgjengelig forskning på maskinlæringsmodeller som automatiserer underliggende ITP-systemer. En slik automatisering av ITP-systemer lar modeller utføre formell resonnering på et høyt abstraksjonsnivå, lignende menneskelig matematisk resonnering.

Denne masteroppgaven utvikler en ny bevisagent for ende-til-ende bevissøk i ITP-systemer. Agenten transformerer bevisproblemet til tre separate klassifiseringsproblemer, noe som gir en mer naturlig maskinlæringstolkning av bevisproblemet enn tidligere tilnærminger.

I tillegg til modeller som imiterer mennesskrevne bevis via veiledet læring, anvendes også dyp forsterkningslæring – implementert ved hjelp av dyp Q-læring. Dette har to fordeler: (1) det håndterer knappheten av annotert data, og (2) agenten har muligheten til å utvikle sin egen bevisstrategi, noe som lar den omgå støy i menneskeskrevne bevis. Videre testes to nye dyplæringsteknikker: Konvolusjonelle nevrale nettverk for grafstrukturer (GCNs) og Bidirectional Encoder Representations from Transformers (BERT) arkitekturen. Mer generelle ikke-konvolusjonelle nevrale nettverk for grafstrukturer er nylig vist å fungere godt på formell logikk og blitt brukt til å bevise teoremer i ITP-systemer. BERT har vist overlegne resultater på flere problemer innen språkbehandlings-feltet (Natural Language Processing). I tillegg har andre Transformer-modeller nylig vist lovende resultater på relaterte problemer innen formell logikk.

GCN- og BERT-baserte agenter beviser henholdsvis 37,3 % og 16,3 % flere teoremer enn tilsvarende agenter basert på tilfeldig gjetting, når de blir trent til å imitere menneskeskrevne bevis. Dyp forsterkningslæring forbedrer resultatene ytterligere. Disse agentene er i stand til å bevise 7,6 % flere teoremer enn tilsvarende veiledete agenter og 47,7 % flere teoremer enn tilsvarende agenter basert på tilfeldig gjetting. Dette er første gang GCN, Transformers og dyp forsterkningslæring er brukt til å automatisere taktisk-baserte ITP-systemer.

Interactive Theorem Proving (ITP) systems are symbolic-based software systems used to write and verify formal mathematical proofs. These systems often contain large datasets of human-written formalized proofs, structured as step-by-step applications of high-level proof strategies called tactics. The space of tactics is well-defined and contains a combination of core tactics and tactic arguments. Tactic arguments generally refer to either already proven theorems or terms and hypotheses in the local proof search context. Recently, several research groups have focused on automating ITP systems by training machine learning models to predict what next tactic to apply in any given proof state. This has resulted in whole frameworks developed for more accessible research into machine learning models automating underlying ITP systems. Such ITP automation allows the model to perform high-level formal reasoning similar to human mathematical reasoning.

This Master's Thesis develops a new theorem proving agent for end-to-end ITP theorem proving. The agent transforms the theorem proving task into three separate multi-class classification problems, allowing a more natural machine learning interpretation of the theorem proving task than previous approaches.

In addition to models imitating human proofs via supervised learning, deep reinforcement learning – implemented using deep Q-learning – is deployed. This has two advantages: (1) it deals with data scarcity, and (2) it allows the agent to develop its own proof style, effectively circumventing noisy human-written proofs. Furthermore, two novel deep learning embedding techniques are tested: Graph Convolutional Networks (GCNs) and the Bidirectional Encoder Representations from Transformers (BERT) architecture. More general non-convolutional Graph Neural Networks have recently been shown to work well on formal logic and been used successfully for ITP theorem proving. BERT has shown state-of-the-art results on several Natural Language Processing tasks. In addition, Transformer-based models have recently shown promising results on related mathematical reasoning tasks.

When trained to imitate human proofs, GCN and BERT-based agents significantly outperform corresponding random guessing agents, proving 37.3% and 16.3% more theorems, respectively. Deep reinforcement learning improves results further. These agents are capable of proving 7.6% more theorems than corresponding supervised agents and 47.7% more theorems than corresponding random guessing agents. This is the first time GCN, Transformers, and deep reinforcement learning have been used for tactic-based formal theorem proving.