OpenAI übersetzte Mathematik für Navier-Stokes-Beweis falsch in Code

OpenAI scheint bei der Veröffentlichung seiner Beweise für das Navier-Stokes-Problem einen subtilen Fehler gemacht zu haben, behauptet ein Team von Mathematikern. Der Fehler bedeutet nicht, dass die Beweise falsch sind oder dass OpenAI das Problem nicht korrekt gelöst hat, aber er stellt infrage, ob man sich auf von KI-Modellen generierte mathematische Ergebnisse immer verlassen kann.

„Was mit all diesen von großen Sprachmodellen generierten Beweisen geschehen muss, ist, dass sie von Menschen gelesen werden müssen, und das stellt eine enorme zusätzliche Belastung für Mathematiker dar“, sagt Anders Hansen von der University of Cambridge.

Am 8. September gab OpenAI bekannt, dass es eine Lösung für das Navier-Stokes-Problem gefunden hat, eines der berühmtesten offenen Probleme der Mathematik. Es veröffentlichte den Beweis in zwei Versionen – eine in „natürlicher Sprache“, also einer Kombination aus Englisch und mathematischen Symbolen, wie sie ein menschlicher Mathematiker schreiben würde, und eine weitere in dem Computercode Lean. Der Lean-Beweis soll eine Formalisierung der Version in natürlicher Sprache sein, die es einem Computer ermöglicht, mechanisch zu verifizieren, dass alle seine logischen Aussagen wahr sind. Das Problem ist, so Hansen und sein Team, dass sie nicht übereinstimmen.