Inter-GPS: Verständliches Lösen geometrischer Probleme mit formaler Sprache und symbolischer Schlussfolgerung

Die Lösung geometrischer Probleme hat in der jüngsten Zeit viel Aufmerksamkeit in der NLP-Gemeinschaft gefunden. Die Aufgabe ist herausfordernd, da sie ein abstraktes Verständnis von Problemen und symbolisches Schließen mit axiomatischem Wissen erfordert. Allerdings sind aktuelle Datensätze entweder zu klein oder nicht öffentlich zugänglich. Daher haben wir einen neuen, groß angelegten Benchmark namens Geometry3K erstellt, der 3.002 geometrische Probleme mit dichter Annotation in formaler Sprache umfasst. Zudem schlagen wir einen neuen Ansatz zur Lösung geometrischer Probleme vor, der formale Sprache und symbolisches Schließen nutzt: den interpretierbaren Geometrie-Problem-Löser (Inter-GPS). Inter-GPS analysiert zunächst automatisch den Problemtext und das Diagramm in formale Sprache, wobei für den Text eine regelbasierte Analyse und für die Objekterkennung ein neuronales Netz verwendet wird. Im Gegensatz zum impliziten Lernen bei bestehenden Methoden integriert Inter-GPS Theoremswissen als bedingte Regeln und führt das symbolische Schließen schrittweise durch. Darüber hinaus wurde ein Theorempredictor entwickelt, um die Anwendungssequenz der Theoreme zu inferieren, die dem symbolischen Löser zur Verfügung gestellt wird, um einen effizienteren und vernünftigeren Suchpfad zu gewährleisten. Umfangreiche Experimente auf den Datensätzen Geometry3K und GEOS zeigen, dass Inter-GPS erhebliche Verbesserungen gegenüber bestehenden Methoden erreicht. Das Projekt inklusive Code und Daten ist unter https://lupantech.github.io/inter-gps verfügbar.