Das System erzeugt Hilfskonstruktionen und prüft geometrische Folgerungen symbolisch. In einem Testset löste es 25 von 30 ausgewählten Olympiade-Aufgaben innerhalb der vorgegebenen Zeitbedingungen. Der Vergleich betrifft einen begrenzten Bereich formaler Geometrie und keine allgemeine mathematische Intelligenz.
Forschungsfrage
Wie können kreative geometrische Konstruktionen mit streng überprüfbaren Beweisschritten verbunden werden?
Ansatz
Ein neuronales Modell schlägt zusätzliche Punkte, Linien oder Kreise vor. Eine symbolische Engine leitet daraus formal gültige Aussagen ab und sucht einen vollständigen Beweis.
Veröffentlichte Ergebnisse
- 25 von 30 Aufgaben des IMO-AG-30-Testsets gelöst
- Vorheriger Vergleichsansatz löste 10 Aufgaben
- Beweise wurden in symbolisch nachvollziehbarer Form erzeugt
Bedeutung
- Verbindung generativer Vorschläge mit formaler Verifikation
- Synthetische Trainingsdaten statt menschlicher Lösungsdemonstrationen
- Forschung zu maschinellem Theorembeweisen und mathematischen Assistenzsystemen
Grenzen
- Spezialisiert auf euklidische Olympiade-Geometrie
- Testset und Vergleich erlauben keine Aussage über gesamte Mathematik
- Formale Übersetzung und geeignete Werkzeuge bleiben für andere Gebiete schwierig