Nieuws

Oplossen van (sommige) formele wiskundeproblemen uit olympiades

OpenAI heeft een neurale theorema-prover ontwikkeld voor Lean die in staat is om een verscheidenheid aan uitdagende wiskundeproblemen op te lossen, waaronder problemen uit de AMC12 en AIME-competities, evenals twee problemen die zijn aangepast van de IMO. Het team bereikte een nieuw state-of-the-art resultaat op de miniF2F-benchmark met een score van 41,2 procent. De methode, genaamd statement curriculum learning, maakt gebruik van iteratief leren op basis van steeds moeilijkere problemen om de prestaties van de prover te verbeteren.