DeepSeek heeft DeepSeek-Prover-V2 geïntroduceerd, een baanbrekend open-source large language model (LLM) dat zorgvuldig is ontworpen voor het complexe domein van formeel theorema bewijzen binnen het Lean 4 framework. Dit nieuwe model maakt gebruik van een recursieve theorema bewijs pipeline, waarbij gebruik wordt gemaakt van de kracht van DeepSeek’s geavanceerde DeepSeek-V3 foundation model. Lean 4, de nieuwste iteratie van de Lean theorema prover, is een interactieve bewijs assistent ontwikkeld door Microsoft Research. Deze geavanceerde functionele programmeertaal en interactieve theorema bewijs systeem stelt wiskundigen en computer wetenschappers in staat om formele bewijzen te construeren met ongeëvenaarde machine gecontroleerde verificatie.
Het project betekent een monumentale stap voorwaarts in het overbruggen van de kloof tussen formele en informele wiskundige redenering. Door te profiteren van de inherente mogelijkheden van general-purpose LLM’s, probeert het effectief het zeer gestructureerde domein van formeel theorema bewijzen aan te pakken. Het DeepSeek onderzoeksteam stelt dat hun innovatieve aanpak de cognitieve processen weerspiegelt die door menselijke wiskundigen worden gebruikt bij het construeren van bewijzen, waarbij complexe theorema’s nauwgezet worden ontleed in meer beheersbare en begrijpelijke componenten.
Uitbreiding van het Evaluatie Framework: Introductie van ProverBench
In een belangrijke stap om de nauwkeurigheid van hun onderzoek te verbeteren, heeft het DeepSeek team hun evaluatie framework aanzienlijk uitgebreid met de introductie van ProverBench, een geheel nieuwe benchmark collectie die zorgvuldig is ontworpen specifiek voor de uitgebreide beoordeling van formele theorema bewijs mogelijkheden. Deze uitgebreide collectie dient als een waardevolle bron voor het evalueren van de prestaties van LLM’s in de context van formele wiskunde.
"Naast de conventionele benchmarks introduceren we met trots ProverBench, een zorgvuldig samengestelde collectie van 325 geformaliseerde problemen, om ons evaluatieproces te verrijken. Deze collectie bevat 15 zorgvuldig geselecteerde problemen die rechtstreeks afkomstig zijn van de recente American Invitational Mathematics Examination (AIME) competities, specifiek uit de jaren 24-25," lichtten de onderzoekers toe.
De opname van AIME problemen in de ProverBench dataset is bijzonder opmerkelijk, omdat het een reeks uitdagende en gevestigde wiskundige problemen introduceert die algemeen worden erkend binnen de wiskundige gemeenschap. Dit biedt een gestandaardiseerde en rigoureuze basis voor het evalueren van de prestaties van DeepSeek-Prover-V2 en het vergelijken ervan met andere benaderingen.
Veelbelovende Eerste Resultaten: Het Aanpakken van AIME Problemen
De eerste resultaten die voortkomen uit rigoureuze tests op deze uitdagende AIME problemen hebben uitzonderlijk veelbelovende prestaties onthuld van hun zorgvuldig ontworpen gespecialiseerde theorema bewijs model. Het DeepSeek team meldt met trots dat DeepSeek-Prover-V2 zijn bekwaamheid demonstreerde door met succes een indrukwekkende 6 van de 15 AIME problemen op te lossen die aan het waren voorgelegd. Ter vergelijking: het general-purpose DeepSeek-V3 model, bij het gebruik van majority voting technieken, slaagde erin om succesvol 8 problemen op te lossen.
Deze bevindingen benadrukken het potentieel van zowel gespecialiseerde als general-purpose LLM’s bij het aanpakken van complexe wiskundige problemen. Hoewel het general-purpose model in deze specifieke benchmark een iets hoger succespercentage vertoonde, demonstreerde het gespecialiseerde theorema bewijs model zijn bekwaamheid in formele wiskundige redenering.
Het Nabootsen van Menselijke Bewijs Constructie: Een Chain-of-Thought Benadering
"Gezien de goed gedocumenteerde uitdagingen die general-purpose modellen vaak tegenkomen bij het proberen om complete Lean bewijzen te produceren, hebben we DeepSeek-V3 strategisch geïnstrueerd om alleen een high-level bewijs schets te genereren, waarbij de ingewikkelde details opzettelijk werden weggelaten. De resulterende chain of thought culmineert in een Lean theorema dat bestaat uit een reeks have statements, elk zorgvuldig afgesloten met een sorry placeholder, wat effectief een subdoel aangeeft dat moet worden opgelost. Deze innovatieve aanpak weerspiegelt op elegante wijze de menselijke stijl van bewijs constructie, waarin een complex theorema stapsgewijs wordt gereduceerd tot een reeks van meer beheersbare lemma’s," legde het DeepSeek team uit.
Deze innovatieve aanpak van het genereren van high-level bewijs schetsen sluit aan bij hoe wiskundigen complexe bewijzen vaak benaderen. Door zich te concentreren op de algehele structuur en de belangrijkste stappen, kan het model effectief de daaropvolgende verfijning en voltooiing van het bewijs begeleiden.
Een Methodische Strategie: Het Individueel Aanpakken van Elke Bewijscomponent
Het systeem maakt vervolgens zorgvuldig gebruik van een methodische en gestructureerde strategie om elke individuele component van het bewijs aan te pakken. Deze systematische aanpak zorgt ervoor dat elk aspect van het bewijs zorgvuldig wordt overwogen en op een logische en coherente manier wordt aangepakt. Het systeem creëert een zeer gestructureerde aanpak van theorema bewijzen, voortbouwend op eerder vastgestelde resultaten om een solide basis te garanderen voor elke volgende stap.
"Gebruikmakend van de subdoelen die door DeepSeek-V3 worden gegenereerd, hanteren we een recursieve oplosstrategie om systematisch elke tussenliggende bewijsstap op te lossen. We extraheren subdoel expressies uit have statements om ze te substitueren voor de oorspronkelijke doelen in de gegeven problemen en nemen vervolgens de voorgaande subdoelen op als premissen. Deze constructie stelt in staat dat latere subdoelen kunnen worden opgelost met behulp van de tussenliggende resultaten van eerdere stappen, waardoor een meer gelokaliseerde afhankelijkheidsstructuur wordt bevorderd en de ontwikkeling van eenvoudigere lemma’s wordt vergemakkelijkt," beschreven de onderzoekers.
De recursieve oplosstrategie is een belangrijk aspect van het vermogen van het systeem om complexe bewijzen te verwerken. Door het probleem op te splitsen in kleinere, meer beheersbare subdoelen, kan het systeem effectief zijn redeneervermogen toepassen op elke individuele component.
Het Optimaliseren van Computationele Resources: Een Gespecialiseerd 7B Parameter Model
Om computationele resources effectief te optimaliseren en een efficiënte verwerking te garanderen, maakt het systeem strategisch gebruik van een kleiner, zeer gespecialiseerd 7B parameter model voor het verwerken van de ontbonden lemma’s. Deze aanpak is cruciaal voor het effectief beheren van de computationele eisen die gepaard gaan met uitgebreide bewijs zoekopdrachten, waardoor wordt gegarandeerd dat het systeem efficiënt kan werken zonder te worden overweldigd door de complexiteit van de zoekruimte. De aanpak culmineert uiteindelijk in een automatisch afgeleid compleet bewijs wanneer alle ontbonden stappen met succes zijn opgelost.
"Het algoritmische framework werkt in twee verschillende fasen, waarbij gebruik wordt gemaakt van twee complementaire modellen: DeepSeek-V3 voor lemma ontbinding en een 7B prover model om de overeenkomstige formele bewijs detailste voltooien," beschreven de onderzoekers.
Deze tweefasige aanpak stelt het systeem in staat om te profiteren van de sterke punten van zowel een groot general-purpose model als een kleiner gespecialiseerd model. Het grote model wordt gebruikt om high-level bewijs schetsen te genereren, terwijl het kleinere model wordt gebruikt om de details in te vullen en het formele bewijs te voltooien.
Het Synthetiseren van Formele Redeneergegevens: Een Natuurlijk Pad
Deze zorgvuldig ontworpen architectuur creëert effectief een natuurlijk en intuïtief pad voor het synthetiseren van formele redeneergegevens, waarbij high-level wiskundige redenering naadloos wordt samengevoegd met de strenge en rigoureuze eisen van formele verificatie. Deze integratie is essentieel voor het waarborgen van de betrouwbaarheid en betrouwbaarheid van de resultaten van het systeem.
"We cureren een subset van uitdagende problemen die onopgelost blijven door het 7B prover model op een end-to-end manier, maar waarvoor alle ontbonden subdoelen met succes zijn opgelost. Door de bewijzen van alle subdoelen samen te stellen, construeren we een compleet-formeel bewijs voor het oorspronkelijke probleem," legden de onderzoekers uit.
Deze aanpak stelt het systeem in staat om van zijn fouten te leren en zijn vermogen om complexe problemen op te lossen te verbeteren. Door de specifieke subdoelen te identificeren die moeilijkheden veroorzaken, kan het systeem zijn inspanningen richten op het verbeteren van zijn prestaties op die gebieden.
Zorgen en Uitdagingen: Implementatiedetails Onder de Loep
Ondanks de onmiskenbare technische prestaties die door DeepSeek-Prover-V2 worden gedemonstreerd, hebben sommige experts in het veld pertinente zorgen geuit over bepaalde implementatiedetails. Elliot Glazer, een zeer gerespecteerd Lead wiskundige bij Epoch AI, heeft gewezen op potentiële problemen die verder onderzoek rechtvaardigen.
Some concerns about the DeepSeek-Prover-V2 paper. Potentially misformalized examples, and discussion on the Lean zulip suggests the PutnamBench proofs are nonsense and use an implicit sorry (possibly hidden in the apply? tactic) not reported in their read-eval-print-loop.
Deze zorgen benadrukken levendig de voortdurende uitdagingen die inherent zijn aan de formele verificatieruimte, waar zelfs de meest minuscule en ogenschijnlijk onbeduidende implementatiedetails een onevenredig grote impact kunnen hebben op de algehele validiteit en betrouwbaarheid van de resultaten. Het formele verificatieproces vereist onwrikbare aandacht voor detail en nauwgezette naleving van gevestigde normen.
Het potentieel voor verkeerd geformaliseerde voorbeelden en de mogelijkheid van verborgen "sorry" tactieken in de PutnamBench bewijzen roepen belangrijke vragen op over de nauwkeurigheid en volledigheid van het verificatieproces. Deze zorgen onderstrepen de noodzaak van voortdurende controle en onafhankelijke verificatie van de resultaten.
Beschikbaarheid en Resources: Het Democratiseren van Toegang tot Formeel Theorema Bewijzen
DeepSeek heeft zijn Prover-V2 beschikbaar gesteld in twee verschillende modelgroottes, inspelend op een divers scala aan computationele resources en onderzoeksdoelstellingen. De eerste versie is een 7B parameter model dat is gebouwd op hun vorige Prover-V1.5-Base, met een uitgebreide contextlengte tot 32K tokens. De tweede versie is een aanzienlijk groter 671B parameter model dat is getraind op DeepSeek-V3-Base. Beide modellen zijn nu gemakkelijk toegankelijk op HuggingFace, een toonaangevend platform voor het delen en samenwerken aan machine learning modellen.
Naast de modellen zelf heeft DeepSeek ook de volledige ProverBench dataset, met 325 zorgvuldig geformaliseerde problemen voor evaluatiedoeleinden, beschikbaar gesteld op HuggingFace. Deze uitgebreide dataset biedt onderzoekers en ontwikkelaars een waardevolle resource voor het evalueren van de prestaties van hun modellen en het vergelijken ervan met DeepSeek-Prover-V2.
Door deze resources vrij beschikbaar te stellen, democratiseert DeepSeek de toegang tot formele theorema bewijs technologie en bevordert het de samenwerking binnen de onderzoeksgemeenschap. Deze open-source aanpak zal waarschijnlijk de vooruitgang in het veld versnellen en leiden tot nieuwe doorbraken in geautomatiseerde redenering en verificatie.
Deze release stelt onderzoekers en ontwikkelaars in staat met de nodige resources om zich te verdiepen in de mogelijkheden en beperkingen van deze technologie. Door open toegang te bieden tot de modellen en de ProverBench dataset, moedigt DeepSeek verder onderzoek en gezamenlijke inspanningen aan om de zorgen van experts in het veld weg te nemen. Deze gezamenlijke aanpak is de sleutel tot het ontrafelen van de complexiteiten van formeel theorema bewijzen en het consolideren van de betrouwbaarheid van deze baanbrekende vooruitgang.