Formale Mathematik-Aussage-Kurrikulum-Learning

Wir untersuchen die Anwendung von Experten-Iteration im Kontext der Sprachmodellierung für formale Mathematik. Wir zeigen, dass bei gleichem Rechenaufwand die Experten-Iteration – verstanden als abwechselnde Durchführung von Beweissuche und Lernen – die reine Beweissuche erheblich übertrifft. Außerdem stellen wir fest, dass die Experten-Iteration, angewandt auf eine Sammlung formaler Aussagen mit ausreichend variierender Schwierigkeit, in der Lage ist, eine Curriculum-artige Folge zunehmend schwierigerer Probleme zu finden und zu lösen, ohne dass dazugehörige Referenzbeweise erforderlich sind. Schließlich erreichen wir mit dieser Methode auf einer manuell zusammengestellten Sammlung von Problemstellungen den Stand der Technik im miniF2F-Test, wobei mehrere anspruchsvolle Aufgaben aus Schul-Olympiaden automatisch gelöst werden.