Artykuł w czasopiśmie
Brak miniatury
Licencja
ClosedAccessDostęp zamknięty
 

A study of continuous vector representations for theorem proving

Uproszczony widok
dc.abstract.enApplying machine learning to mathematical terms and formulas requires a suitable representation of formulas that is adequate for AI methods. In this paper, we develop an encoding that allows for logical properties to be preserved and is additionally reversible. This means that the tree shape of a formula including all symbols can be reconstructed from the dense vector representation. We do that by training two decoders: one that extracts the top symbol of the tree and one that extracts embedding vectors of subtrees. The syntactic and semantic logical properties that we aim to preserve include both structural formula properties, applicability of natural deduction steps and even more complex operations like unifiability. We propose datasets that can be used to train these syntactic and semantic properties. We evaluate the viability of the developed encoding across the proposed datasets as well as for the practical theorem proving problem of premise selection in the Mizar corpus.
dc.affiliationUniwersytet Warszawski
dc.contributor.authorPurgał, Stanisław
dc.contributor.authorKaliszyk, Cezary
dc.contributor.authorParsert, Julian
dc.date.accessioned2024-01-24T18:13:18Z
dc.date.available2024-01-24T18:13:18Z
dc.date.issued2021
dc.description.financePublikacja bezkosztowa
dc.identifier.doi10.1093/LOGCOM/EXAB006
dc.identifier.issn0955-792X
dc.identifier.urihttps://repozytorium.uw.edu.pl//handle/item/101882
dc.identifier.weblinkhttps://doi.org/10.1093/logcom/exab006
dc.languageeng
dc.pbn.affiliationcomputer and information sciences
dc.relation.ispartofJournal of Logic and Computation
dc.relation.pages1-27
dc.rightsClosedAccess
dc.sciencecloudnosend
dc.titleA study of continuous vector representations for theorem proving
dc.typeJournalArticle
dspace.entity.typePublication