Lernen, Sätze zu beweisen, durch Lernen, Sätze zu generieren

Wir betrachten die Aufgabe des automatisierten Beweisens von Sätzen, einer zentralen Aufgabe im Bereich Künstliche Intelligenz. Tiefes Lernen hat vielversprechende Ergebnisse bei der Ausbildung von Satzbeweisern gezeigt, doch stehen für das überwachte Lernen nur begrenzte Mengen an menschlich verfassten Sätzen und Beweisen zur Verfügung. Um diese Einschränkung zu überwinden, schlagen wir vor, einen neuronalen Generator zu lernen, der automatisch Sätze und deren Beweise synthetisiert, um einen Satzbeweiser zu trainieren. Experimente auf realen Aufgaben zeigen, dass synthetische Daten aus unserem Ansatz den Satzbeweiser verbessert und den Stand der Technik im Bereich des automatisierten Beweisens in Metamath voranbringt. Der Quellcode ist unter https://github.com/princeton-vl/MetaGen verfügbar.