AI-assistenten

Ten opzichte van andere academische disciplines neemt de wiskunde een bijzondere plaats in: wiskundigen kunnen hun gelijk halen door te bewíjzen dat ze gelijk hebben. Maar ieder voordeel heeft een nadeel: een stelling is pas een stelling als je een volledig kloppend bewijs hebt. En dat legt de lat hoog. Als je bewijs niet klopt –ook wiskundigen zien wel eens iets over het hoofd – dan schieten door oplettende collega’s het onverbiddelijk lek. Er resteert dan niets dan je ongelijk ruiterlijk te erkennen.

Af en toe zijn bewijzen zo ingewikkeld dat nauwelijks nog iemand alle details overziet. Hoe weet je dan of zo’n bewijs klopt? Bij gebrek aan beter werd het tot voor kort door de wiskundegemeenschap geaccepteerd als enkele vooraanstaande wiskundigen aangaven te geloven dat alles klopt: proof by authority. Hierin kwam verandering met de opkomst van formal proofchecking. Met behulp van speciale hiervoor ontwikkelde programmeertalen zoals Lean is het mogelijk om bewijzen (die in de regel in informeel Engels geschreven zijn) te formaliseren en vervolgens volledig te herleiden tot de axioma’s waarop de wiskunde gebaseerd is.

Bekende voorbeelden van stellingen die op deze wijze gecontroleerd zijn, zijn de priemgetalstelling (het aantal priemgetallen onder een gegeven getal N schaalt als N/ln(N)), het vierkleurenprobleem (iedere landkaart kan met vier kleuren zodanig worden ingekleurd dat landen met een gemeenschappelijke grens verschillende kleuren krijgen), en het Keplervermoeden (de stapeling van sinaasappels bij de marktkraam is de meest efficiënte). Eenvoudig ogende beweringen, althans voor een wiskundige, maar alle drie heel lastig te bewijzen. Een leuke quizvraag: welke van de drie is het moeilijkst?

Een leuke quizvraag: welke van de drie is het moeilijkst?

Formal proofchecking is nu nog het exclusieve domein van een klein groepje afficinado’s, maar door de opkomst van generatieve AI begint hier verandering in te komen: de code waarmee je een bewijs kunt proofchecken kun je proberen te genereren met large language models (LLM) zoals ChatGPT. Dit is slechts één van de vele fascinerende state-of-the-art toepassingen van generatieve AI.

Veel wetenschappers gebruiken de commerciële LLM’s inmiddels al als personal assistant bij hun onderzoek. Ik heb hier ook enige ervaring mee opgebouwd: het voelt als samenwerken met een PhD-student die weliswaar soms fouten maakt, maar ongelofelijk veel weet en bijzonder snel is. Ook als docent kun je je voordeel met LLM’s doen: ze kunnen bijvoorbeeld in een mum van tijd modeluitwerkingen van opgaven genereren. Veel studenten gebruiken een LLM als persoonlijke teaching assistant: je kunt vragen om hints en je antwoorden laten controleren en becommentariëren.

Fascinerende mogelijkheden doemen op, maar ook tal van ethische vragen. Mogen we in het onderzoek samenwerken met een LLM? Mogen we het schrijven van de inleiding van een artikel delegeren aan een LLM? Mogen we LLM inzetten bij het schrijven van grant proposals?

Ik vermoed dat velen, inclusief ondergetekende, weinig principiële problemen zien in het eerste scenario, mits zorgvuldig toegepast – het zal niet lang duren tot LLM’s gewoon als een tool wordt gezien. Bij de tweede vraag begint het al flink te wringen, en bij de derde begeven we ons duidelijk op een hellend vlak. In het onderwijs dienen zich soortgelijke vragen aan; daar zal het bijvoorbeeld lastig worden de scheidslijn met fraude helder te trekken.

Studenten hebben AI massaal omarmd. In mijn wetenschappelijke omgeving zie ik een aantal enthousiaste early adopters, veel mensen met een afwachtende houding of voorzichtige belangstelling, en een enkeling die uitgesproken sceptisch is. Het brede debat moet nog beginnen.