Skip to content

Latest commit

 

History

History
117 lines (84 loc) · 3.36 KB

ollama-models.md

File metadata and controls

117 lines (84 loc) · 3.36 KB

Ollama Models

This document provides a list of models for proving that are available on Ollama.

miniCTX

This is the prover referenced in the main README. Again, to use it, you can pull it with the following command:

ollama pull wellecks/ntpctx-llama3-8b

and set 2 configuration variables in ~/.config/llmlean/config.toml:

api = "ollama"
model = "wellecks/ntpctx-llama3-8b"

Kimina Models

There are a few models available from Kimina, the collaboration between the Project Numina and Kimi teams.

Important configuration notes for Kimina models:

  • These models were trained to use Markdown format for inputs and outputs, so you must set prompt = "markdown" and responseFormat = "markdown"

BoltonBailey/Kimina-Prover-Distill-1.7B

To download the model:

ollama pull BoltonBailey/Kimina-Prover-Distill-1.7B

To use it, set the following configuration variables in ~/.config/llmlean/config.toml:

api = "ollama"
model = "BoltonBailey/Kimina-Prover-Distill-1.7B"
prompt = "markdown"
responseFormat = "markdown"

BoltonBailey/Kimina-Prover-Distill-8B

To download the model:

ollama pull BoltonBailey/Kimina-Prover-Distill-8B

To use it, set the following configuration variables in ~/.config/llmlean/config.toml:

api = "ollama"
model = "BoltonBailey/Kimina-Prover-Distill-8B"
prompt = "markdown"
responseFormat = "markdown"

Performance Tips for Kimina Models

  • Set numSamples to a small number: These models generate detailed reasoning chains, so using fewer samples is recommended for better performance

BFS Provers

The BFS-Prover series (BFS-Prover-V2 and BFS-Prover-V1) are open-source step-level provers developed by ByteDance Seed team.

You can pull any verison of the BFS-Prover-V2 model directly via Ollama:

7B version

ollama pull zeyu-zheng/BFS-Prover-V2-7B

Or pull the quantized q8_0 version:

ollama pull zeyu-zheng/BFS-Prover-V2-7B:q8_0

and set configuration variables in ~/.config/llmlean/config.toml:

api = "ollama"
model = "zeyu-zheng/BFS-Prover-V2-7B"
mode = "parallel"
numSamples = "5"
prompt = "tacticstate"
responseFormat = "tactic"

32B version

ollama pull zeyu-zheng/BFS-Prover-V2-32B

Or pull the quantized f16 / q8_0 version:

ollama pull zeyu-zheng/BFS-Prover-V2-32B:f16
ollama pull zeyu-zheng/BFS-Prover-V2-32B:q8_0

and set configuration variables in ~/.config/llmlean/config.toml:

api = "ollama"
model = "zeyu-zheng/BFS-Prover-V2-32B" or "zeyu-zheng/BFS-Prover-V2-32B:f16" or "zeyu-zheng/BFS-Prover-V2-32B:q8_0"
mode = "parallel"
numSamples = "5"
prompt = "tacticstate"
responseFormat = "tactic"

Tips for BFS-Prover models

  • These models were trained to use the current tactic state as input and the preceding tactic as output, so you must set prompt = "tacticstate", responseFormat = "tactic" and mode = "parallel".
  • You can increase numSamples (e.g. 5, 10, …) to sample multiple tactics for each state.
  • Currently llmqed functions the same as llmstep "".