DeepSeek, yinelemeli kanıt aramalı DeepSeek-Prover-V2'yi ve yeni ProverBench kıyaslamasını yayınladı

DeepSeek AI, formal teorem kanıtlama için Lean 4'te kullanılmak üzere DeepSeek-Prover-V2 adında açık kaynaklı büyük bir dil modeli duyurdu. Model, karmaşık teoremleri alt hedeflere ayırıp bunları biçimlendirerek yüksek kaliteli başlatma verileri oluşturmak için DeepSeek-V3'ü kullanan yinelemeli bir teorem kanıtlama hattı kullanıyor. 7 milyar parametreli bir model bu alt hedefleri kanıtlıyor ve tam kanıtlar, eğitim için DeepSeek-V3'ün düşünce zinciri muhakemesiyle eşleştiriliyor. İkili geri bildirimle pekiştirmeli öğrenme modeli daha da iyileştiriyor. 671 milyar parametreli versiyon MiniF2F-test'te %88,9 başarı oranına ulaşıyor ve 658 PutnamBench probleminden 49'unu çözüyor. DeepSeek ayrıca matematiksel muhakemeyi değerlendirmek için AIME yarışmalarından ve ders kitaplarından 325 problemin yer aldığı bir veri kümesi olan ProverBench'i tanıttı. Model iki boyutta sunuluyor: 7 milyar ve 671 milyar parametre.