DeepSeek brengt DeepSeek-Prover-V2 uit met recursief bewijszoeken en nieuwe ProverBench-benchmark

DeepSeek AI heeft DeepSeek-Prover-V2 aangekondigd, een open-source groot taalmodel voor formeel stelling bewijzen in Lean 4. Het model gebruikt een recursieve stellingbewijzingspijplijn die DeepSeek-V3 inzet om hoogwaardige initialisatiegegevens te genereren door complexe stellingen op te splitsen in subdoelen en deze te formaliseren. Een model met 7 miljard parameters bewijst vervolgens deze subdoelen, en de volledige bewijzen worden gekoppeld aan de chain-of-thought-redenering van DeepSeek-V3 voor training. Reinforcement learning met binaire feedback verfijnt het model verder. De versie met 671 miljard parameters behaalt 88,9% op MiniF2F-test en lost 49 van de 658 PutnamBench-problemen op. DeepSeek introduceerde ook ProverBench, een dataset van 325 problemen uit AIME-wedstrijden en studieboeken voor het evalueren van wiskundig redeneren. Het model is beschikbaar in twee groottes: 7 miljard en 671 miljard parameters.