kfdong

STP_model_Lean_0320

The table below compares the pass@3200 performance of STP (our model) and DeepSeek-Prover-V1.5 on miniF2F-test and ProofNet-test.

We also release the dataset here, which contains:

Extracted examples from mathlib4,
Generated correct proofs of statements in LeanWorkbook,
Generated correct proofs of conjectures proposed by our model during self-play training.

Our final model is finetuned from DeepSeek-Prover-V1.5-SFT with this dataset for 1 epoch.

Available on FriendliAI

Dedicated Endpoints

Run this model inference on single tenant GPU with unmatched speed and reliability at scale.

Container

Run this model inference with full control and performance in your environment.

Model Details

Model Provider

kfdong

Model Tree

Base

deepseek-ai/DeepSeek-Prover-V1.5-SFT

Fine-tuned

this model

Input Modalities

Text

Output Modalities

Text

Supported Functionality

Dedicated EndpointsContainer

Explore FriendliAI today

The table below compares the pass@3200 performance of STP (our model) and DeepSeek-Prover-V1.5 on miniF2F-test and ProofNet-test.

We also release the dataset here, which contains:

Extracted examples from mathlib4,
Generated correct proofs of statements in LeanWorkbook,
Generated correct proofs of conjectures proposed by our model during self-play training.

Our final model is finetuned from DeepSeek-Prover-V1.5-SFT with this dataset for 1 epoch.