In het kort:
De doorbraak toont aan hoe AI nu daadwerkelijk kan bijdragen aan geavanceerd wiskundig onderzoek door problemen volledig zelfstandig op te lossen.
- Wiskundige Dawei Chen probeerde vijf jaar lang tevergeefs een algebraïsch probleem op te lossen, totdat AxiomProver binnen een dag een bewijs leverde.
- Het AI-systeem vond een verband met een numeriek fenomeen uit de 19e eeuw dat alle menselijke onderzoekers hadden gemist.
- AxiomProver loste ook Fel's Conjecture op, een probleem dat formules bevat uit de legendarische notitieboeken van Srinivasa Ramanujan van meer dan 100 jaar geleden.
Het grote plaatje:
Axiom combineert grote taalmodellen met een gespecialiseerd AI-systeem dat getraind is om wiskundige problemen stap voor stap door te redeneren tot bewezen correcte oplossingen.
- In tegenstelling tot ChatGPT kan AxiomProver bewijzen verifiëren met behulp van de wiskundige programmeertaal Lean, waardoor het echt nieuwe oplossingsmethoden kan ontwikkelen.
- Scott Kominers van Harvard Business School noemt het "verbijsterend" hoe het systeem niet alleen problemen oplost, maar ook elegante en mooie wiskundige bewijzen produceert.
- De technieken kunnen ook buiten de wiskunde worden toegepast, bijvoorbeeld voor het ontwikkelen van cyberbeveiliging-resistente software.
