DeepSeek julkaisee DeepSeek-Prover-V2:n rekursiivisella todistuksenhaulla ja uudella ProverBench-vertailuarvolla

DeepSeek AI on julkaissut DeepSeek-Prover-V2:n, avoimen lähdekoodin suurikielisen mallin muodolliseen lauseentodistukseen Lean 4:ssä. Se käyttää rekursiivista putkea harjoitusdatan tuottamiseen DeepSeek-V3:n avulla, saavuttaa huipputulokset MiniF2F:ssä ja PutnamBenchissä ja esittelee ProverBenchen, uuden 325 ongelman vertailuarvon.

DeepSeek AI julkisti DeepSeek-Prover-V2:n, avoimen lähdekoodin suuren kielimallin muodolliseen teoreemantodistukseen Lean 4:ssä. Malli käyttää rekursiivista teoreemantodistusputkea, joka hyödyntää DeepSeek-V3:aa korkealaatuisen alustusdatan tuottamiseen jakamalla monimutkaisia teoreemoja osatavoitteiksi ja formalisoimalla ne. 7B parametrin malli todistaa nämä osatavoitteet, ja täydelliset todistukset yhdistetään DeepSeek-V3:n ajatusketjupäättelyn kanssa harjoitusta varten. Vahvistusoppiminen binääripalautteella hienosäätää mallia edelleen. 671B parametrin versio saavuttaa 88,9 % MiniF2F-testissä ja ratkaisee 49 PutnamBench-ongelmaa 658:sta. DeepSeek esitteli myös ProverBench-tietoaineiston, joka sisältää 325 ongelmaa AIME-kilpailuista ja oppikirjoista matemaattisen päättelyn arvioimiseksi. Malli on saatavilla kahdessa koossa: 7B ja 671B parametria.

Lähde: Synced — Alkuperäinen