Text Generation
Transformers
PyTorch
English
qwen3
formal-mathematics
lean4
data-synthesis
problem-generation
formal-statement-synthesis
conversational
text-generation-inference
Instructions to use purewhite42/DExplorer-8B with libraries, inference providers, notebooks, and local apps. Follow these links to get started.
- Libraries
- Transformers
How to use purewhite42/DExplorer-8B with Transformers:
# Use a pipeline as a high-level helper from transformers import pipeline pipe = pipeline("text-generation", model="purewhite42/DExplorer-8B") messages = [ {"role": "user", "content": "Who are you?"}, ] pipe(messages)# Load model directly from transformers import AutoTokenizer, AutoModelForCausalLM tokenizer = AutoTokenizer.from_pretrained("purewhite42/DExplorer-8B") model = AutoModelForCausalLM.from_pretrained("purewhite42/DExplorer-8B") messages = [ {"role": "user", "content": "Who are you?"}, ] inputs = tokenizer.apply_chat_template( messages, add_generation_prompt=True, tokenize=True, return_dict=True, return_tensors="pt", ).to(model.device) outputs = model.generate(**inputs, max_new_tokens=40) print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:])) - Notebooks
- Google Colab
- Kaggle
- Local Apps
- vLLM
How to use purewhite42/DExplorer-8B with vLLM:
Install from pip and serve model
# Install vLLM from pip: pip install vllm # Start the vLLM server: vllm serve "purewhite42/DExplorer-8B" # Call the server using curl (OpenAI-compatible API): curl -X POST "http://localhost:8000/v1/chat/completions" \ -H "Content-Type: application/json" \ --data '{ "model": "purewhite42/DExplorer-8B", "messages": [ { "role": "user", "content": "What is the capital of France?" } ] }'Use Docker
docker model run hf.co/purewhite42/DExplorer-8B
- SGLang
How to use purewhite42/DExplorer-8B with SGLang:
Install from pip and serve model
# Install SGLang from pip: pip install sglang # Start the SGLang server: python3 -m sglang.launch_server \ --model-path "purewhite42/DExplorer-8B" \ --host 0.0.0.0 \ --port 30000 # Call the server using curl (OpenAI-compatible API): curl -X POST "http://localhost:30000/v1/chat/completions" \ -H "Content-Type: application/json" \ --data '{ "model": "purewhite42/DExplorer-8B", "messages": [ { "role": "user", "content": "What is the capital of France?" } ] }'Use Docker images
docker run --gpus all \ --shm-size 32g \ -p 30000:30000 \ -v ~/.cache/huggingface:/root/.cache/huggingface \ --env "HF_TOKEN=<secret>" \ --ipc=host \ lmsysorg/sglang:latest \ python3 -m sglang.launch_server \ --model-path "purewhite42/DExplorer-8B" \ --host 0.0.0.0 \ --port 30000 # Call the server using curl (OpenAI-compatible API): curl -X POST "http://localhost:30000/v1/chat/completions" \ -H "Content-Type: application/json" \ --data '{ "model": "purewhite42/DExplorer-8B", "messages": [ { "role": "user", "content": "What is the capital of France?" } ] }' - Docker Model Runner
How to use purewhite42/DExplorer-8B with Docker Model Runner:
docker model run hf.co/purewhite42/DExplorer-8B
Update README.md
Browse files
README.md
CHANGED
|
@@ -40,7 +40,7 @@ This model is fine-tuned from [Goedel-Prover-V2-8B](https://huggingface.co/Goede
|
|
| 40 |
|
| 41 |
This model is SFTed for the **DExploration** task: given the current exploration state (introduced variables/hypotheses and Lean 4 context), the model proposes the next exploration step — either introducing a new variable/hypothesis, deriving a new fact, or submitting a conclusion.
|
| 42 |
|
| 43 |
-
See the [📺GitHub repo](https://github.com/Purewhite2019/dexploration_main) for prompt templates and detailed usage
|
| 44 |
|
| 45 |
## 📄 Citation
|
| 46 |
|
|
|
|
| 40 |
|
| 41 |
This model is SFTed for the **DExploration** task: given the current exploration state (introduced variables/hypotheses and Lean 4 context), the model proposes the next exploration step — either introducing a new variable/hypothesis, deriving a new fact, or submitting a conclusion.
|
| 42 |
|
| 43 |
+
See the [📺GitHub repo](https://github.com/Purewhite2019/dexploration_main) for prompt templates and detailed usage.
|
| 44 |
|
| 45 |
## 📄 Citation
|
| 46 |
|