DeepSeek Prover V2
accounts/fireworks/models/deepseek-prover-v2
DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3.
DeepSeek Prover V2 can be fine-tuned on your data to create a model with better response quality. Fireworks uses low-rank adaptation (LoRA) to train a model that can be served efficiently at inference time.
On-demand deployments allow you to use DeepSeek Prover V2 on dedicated GPUs with Fireworks' high-performance serving stack with high reliability and no rate limits.