Questions on 7B model

[vadimkantorov]

Hi! Thanks for the awesome model release and paper write-up!

I have a few minor questions about the paper (mainly 7B setups)

1. What do you mean by the 7B-non CoT setup? Is this model of the expert iteration stage?

2. What do you mean by the 7B-CoT setup? Is it the output of the distillation step (from subsection 2.3)?

3. Do you only train a 7B model during the expert iteration step? If so, what model do you use as the initial weights and for the initial unsolved statement filtering? DeepSeek-Prover-V1.5-Base (7B)? DeepSeek-Prover-V1.5-SFT (7B)? DeepSeek-Prover-V1.5-RL (7B)?

4. Have you used the V3 or V3-0324 as the frozen model for high-level proof sketch generation?

Thank you!