Hulplijnen
Bewijs dat in een gelijkbenige driehoek de basishoeken gelijk zijn.
Het is een opgave uit de vlakke meetkunde, (begin) middelbare school – in elk geval in mijn HBS-tijd (dus voor 1968). Het schoolbewijs -toen- maakte gebruik van een hulplijn (de middelloodlijn vanuit de top), zonder die extra lijn zou je het bewijs niet kunnen leveren werd gezegd.
Toen AI nog kunstmatige intelligentie heette en vooral rule-based was, was de stelling een ultieme test. Zou een computer die hulplijn kunnen vinden of het bijltje er bij neer moeten gooien? De anekdote, veel anders kan het niet zijn, is mij altijd bijgebleven. Het vraagstuk werd aan de computer voorgelegd, de onderzoekers waren in gespannen afwachting van de reactie van de computer en voorbereid op een error of time-out. Maar het antwoord kwam snel en was verrassend: In de gegeven situatie (A is de top) is 
BCA congruent met CBA, immers AB=AC dus twee zijden zijn gelijk en de ingesloten (top)hoek A is gelijk (want gelijk aan zichzelf). Bijgevolg zijn alle overeenkomende elementen gelijk, dus 
ABC = BCA. QED, geen hulplijn nodig.
Gisteren, 17 januari 2024, is in Nature (625, pages 476–482 (2024)) het artikel Solving olympiad geometry without human demonstrations verschenen. De auteurs introduceren in het artikel AlphaGeometry, de nieuwste telg in de AlphaX-familie waarvan AlphaGo, AlphaZero, AlphaFold beroemde leden zijn.
Op de foto zie je auteurs van het artikel bij een schoolbord waarop een van de olympiade problemen is uitgewerkt. Bron: New York Times 17 januari 2024.
AlphaGeometry kan stellingen bewijzen in de Euclidische vlakke meetkunde. Net als bij AlphaZero is er geen menselijke input of labeling geweest, het is een op synthetische data getraind systeem dat gebruik maakt van een GPT-achtig taalmodel (maar kleiner) in combinatie met een symbolic deduction engine.
Om te laten zien wat het systeem kan hebben ze het een test-set voorgelegd van 30 meetkunde vraagstukken uit recente internationale wiskunde olympiades (IMO in het Engels). AlphaGeometry kon er 25 foutloos oplossen en staat daar mee op het niveau van de gemiddelde gouden medaillewinnaar bij zo’n olympiade.
Vanuit een zeker standpunt is het een indrukwekkende prestatie, als je je ooit zelf gewaagd hebt aan opgaven uit een wiskunde olympiade dan zal je dat willen bevestigen. Gedacht vanuit AI ontwikkeling is het een proof-of-concept, niet meer en niet minder, van een neuro-symbolic systeem. In de toekomst mogen we ook andere toepassingen van dit, of een eruit afgeleid, systeem verwachten.
Ik wil er nog meer over uitzoeken, met name de manier waarop de synthetische dataset is ontworpen en gerealiseerd. Het is nodig om met synthetische data te werken (er wordt gezegd 100 miljoen meetkundige bewijzen) omdat de beschikbare verzameling veel te klein is om in machine learning te gebruiken. Het geldt bijvoorbeeld ook voor AlphaFold dat nieuwe eiwitten kan voorspellen, maar dat ook op synthetische gegevens getraind moest worden omdat er simpelweg niet genoeg bekende eiwitten aanwezig zijn.
Hoe slim is AlphaGeometry? Nou, ongeveer het eerste probleem dat getackled werd is dat van de hoeken van de gelijkbenige driehoek. Zie het plaatje. Het systeem komt niet met de zelfongruentie-redenering, maar trekt zowaar de fameuze hulplijn!
Als ik het goed begrijp wordt eerst de symbolic deduction engine losgelaten op het probleem. Als die het kan oplossen, prima, maar zo niet dan wordt via het taalmodel de suggestie gedaan om een punt toe te voegen en de deductie opnieuw te proberen. Hoe dat toevoegen gaat weet ik nog niet, maar op enig moment komt er een configuratie waarin het bewijs geleverd kan worden.
Kennelijk zaten symmetrie overwegingen (de basis van de congruentie van de driehoek en zijn spiegelbeeld) niet in het bereik van de deduction engine.
Hulppunten zetten en hulplijnen trekken horen dus tot het standaard arsenaal van AlphaGeometry, precies zo als het op de HBS geleerd werd.