Enabling vllm-based prover - Githubissues

lean-dojo / ReProver

Retrieval-Augmented Theorem Provers for Lean

https://leandojo.org

MIT License

218 stars 48 forks source link

Enabling vllm-based prover #40

Closed albertqjiang closed 6 months ago

albertqjiang commented 9 months ago

[x] VLLM-based prover
[x] Saving progress so that theorems don't need to be rerun
[x] Solving memory issues
[x] Making batch_generate more efficient

yangky11 commented 6 months ago

Thanks!