OpenAI ‘GPT-f’ levert SOTA-prestaties bij het automatisch testen van wiskundige stellingen

Het in San Francisco gevestigde AI-onderzoekslaboratorium OpenAI heeft nog een lid toegevoegd aan zijn populaire GPT-familie (Generative Pre-training Transformer). In een nieuw artikel introduceren OpenAI-onderzoekers GPT-f, een geautomatiseerde bewaarder en bewijsassistent voor de Metamath-formalisatietaal.

Hoewel kunstmatige neurale netwerken aanzienlijke vooruitgang hebben geboekt op het gebied van computervisie, natuurlijke taalverwerking, robotica enzovoort, gelooft OpenAI dat ze ook potentieel hebben op het relatief onderbelichte gebied van redeneertaken. Het nieuwe onderzoek verkent dit potentieel door een transformatortaalmodel toe te passen op geautomatiseerde stellingonderzoek.

Geautomatiseerd bewijzen van stellingen vereist doorgaans een algemene en flexibele redenering om de juistheid van bewijzen efficiënt te controleren. Dit maakt het een aantrekkelijk domein om de redeneervaardigheden van taalmodellen te controleren en om redenering in het algemeen te bestuderen. De mogelijkheid om bewijzen te verifiëren, helpt onderzoekers ook, omdat hierdoor automatisch nieuwe problemen kunnen worden gegenereerd die als trainingsgegevens kunnen worden gebruikt.

De onderzoekers ontdekten overeenkomsten tussen het leren bewijzen van stellingen en het leren spelen van het oude bordspel Go, aangezien beide geautomatiseerde manieren bieden om succes te bepalen en nieuwe gegevens te genereren via zelfspelbenaderingen. Het succes van AlphaZero in Go suggereert dus dat het automatisch bewijzen van stellingen een vruchtbaar domein zou kunnen zijn voor de studie van redeneren in neurale netwerken.

Metamath is een taal- en computerprogramma voor het archiveren, verifiëren en bestuderen van wiskundige bewijzen. De onderzoekers gebruiken Metamath – aangedreven door een eenvoudig meta-logisch systeem gebaseerd op een enkele substitutieregel – als hun formele omgeving, met behulp van alleen-decoder-transformatoren vergelijkbaar met GPT-2 en GPT-3 om modellen te maken met verschillende pre-training datasets en in verschillende groottes. Hun grootste model heeft 36 lagen en 774 miljoen trainbare parameters.

De onderzoekers creëerden de GPT-f online proefassistent om interactieve proefconstructies mogelijk te maken met behulp van hun modellen. In experimenten behaalde GPT-f een nieuw SOTA-resultaat op de Metamath-bibliotheek, waarbij 56,22 procent van de bewijzen van een vastgehouden testset werd afgesloten versus 21,16 procent voor het huidige SOTA-model MetaGen-IL om het potentieel van transformatorarchitectuur in formeel redeneren te demonstreren.

GPT-f vond ook nieuwe korte bewijzen die zijn geaccepteerd in de hoofdbibliotheek van Metamath. De onderzoekers zeggen dat dit de eerste keer is dat een op diep leren gebaseerd systeem bewijzen heeft geleverd die zijn overgenomen door een formele wiskundegemeenschap.

“Onze resultaten suggereren dat de nauwe koppeling van een deep learning-systeem met een formeel systeem interessante mogelijkheden biedt voor verder onderzoek, met als doel de generatieve kracht van het eerste en de verificatiemogelijkheden van het laatste beter te benutten”, concluderen de onderzoekers. .

De papieren Generative Language Modeling for Automated Theorem Proving staat op arXiv.

Verslaggever : Yuan Yuan | Editor : Michael Sarazen

Gesynchroniseerd rapport | Een onderzoek naar de kunstmatige intelligentie-oplossingen in China als reactie op de COVID-19-pandemie – 87 casestudy’s van meer dan 700 AI-leveranciers

Dit rapport biedt een blik op hoe China kunstmatige-intelligentietechnologieën heeft gebruikt in de strijd tegen COVID-19. Het is ook beschikbaar op Amazon Kindle. Samen met dit rapport hebben we ook een databank geïntroduceerd met 1428 aanvullende kunstmatige intelligentieoplossingen uit 12 pandemische scenario’s.

Klik hier voor meer rapporten van ons.

We weten dat u geen enkel laatste nieuws of doorbraken op het gebied van onderzoek wilt missen. Abonneer u op onze populaire nieuwsbrief Synced Global AI Weekly om wekelijkse AI-updates te ontvangen.