Generative Language Modeling für das automatisierte Beweisen von Sätzen

Wir untersuchen die Anwendung transformerbasierter Sprachmodelle auf das automatisierte Beweisen von Sätzen. Diese Arbeit wird motiviert durch die Möglichkeit, dass eine wesentliche Einschränkung automatisierter Beweissysteme im Vergleich zu Menschen – die Erzeugung origineller mathematischer Begriffe – möglicherweise durch die Generierung mittels Sprachmodelle überwunden werden könnte. Wir präsentieren einen automatisierten Beweiser und Beweishilfssystem, GPT-f, für die formale Sprache Metamath, und analysieren dessen Leistung. GPT-f fand neue, kurze Beweise, die in die Hauptbibliothek von Metamath aufgenommen wurden – soweit uns bekannt, das erste Mal, dass ein auf tiefen Lernverfahren basierendes System Beweise beigetragen hat, die von einer formalen Mathematikgemeinschaft übernommen wurden.