Effiziente Heuristik löst Olympiad-Geometrieprobleme ohne neuronale Netze

Automatisiertes Beweisen von Euklidischen Geometrietheoremen, insbesondere auf Olympiad-Niveau, bleibt ein zentrales Problem in der Künstlichen Intelligenz. In einer neuen Studie wird ein äußerst effizienter Ansatz vorgestellt, der komplett auf CPUs läuft und keine neuronalen Netzwerke nutzt.

Schon ein einfacher, zufälliger Ansatz zum Einfügen von Hilfspunkten erreicht laut den Autoren die Leistung eines silbermedaillen‑Niveaus bei IMO‑Problemen. Aufbauend darauf präsentiert das Team HAGeo – eine heuristikbasierte Methode zur Auswahl von Hilfskonstruktionen – die Fähigkeit, 28 von 30 Aufgaben des IMO‑30‑Benchmarks zu lösen. Damit erreicht HAGeo ein Goldmedaillen‑Niveau und übertrifft dabei AlphaGeometry, einen führenden, neuronalen Ansatz, deutlich.

Zur umfassenderen Bewertung wurden zusätzlich HAGeo‑409 und ein neuer Benchmark mit 409 Geometrieaufgaben entwickelt, die nach menschlicher Einschätzung schwieriger sind als die üblichen IMO‑30‑Aufgaben. Dieser neue Test stellt höhere Anforderungen an die Algorithmen und definiert einen neuen Standard für die Bewertung von Geometrie‑Theorem‑Proving‑Systemen.