Lernen, in großen Theorien ohne Imitation zu argumentieren

In dieser Arbeit zeigen wir, wie automatisches Theorembeweisen in Anwesenheit einer umfangreichen Wissensbasis potenzieller Voraussetzungen ohne das Lernen von menschlichen Beweisen durchgeführt werden kann. Wir schlagen einen Explorationsmechanismus vor, der zusätzliche Voraussetzungen einmischt, die durch eine tf-idf (Term Frequency-Inverse Document Frequency)-basierte Suche in einem Szenario des tiefen Reinforcement Learnings ausgewählt werden. Dies unterstützt die Exploration und das Lernen, welche Voraussetzungen für den Beweis eines neuen Theorems relevant sind. Unsere Experimente erweisen, dass der Theorembeweiser, der mit diesem Explorationsmechanismus trainiert wurde, Beweisern überlegen ist, die nur auf menschlichen Beweisen trainiert wurden. Er nähert sich der Leistung eines Beweisers an, der durch eine Kombination von Imitations- und Reinforcement Learning trainiert wurde. Wir führen mehrere Experimente durch, um die Bedeutung der zugrundeliegenden Annahmen zu verstehen, die unseren Explorationsansatz erfolgreich machen, und damit unsere Gestaltungswahl zu erklären.