Text Generation
Transformers
Safetensors
PEFT
English
mathematics
conjectures
theorem-proving
reasoning
qlora
lora
formal-math
lean
research
conversational
Instructions to use NorthernTribe-Research/math-conjecture-model with libraries, inference providers, notebooks, and local apps. Follow these links to get started.
- Libraries
- Transformers
How to use NorthernTribe-Research/math-conjecture-model with Transformers:
# Use a pipeline as a high-level helper from transformers import pipeline pipe = pipeline("text-generation", model="NorthernTribe-Research/math-conjecture-model") messages = [ {"role": "user", "content": "Who are you?"}, ] pipe(messages)# Load model directly from transformers import AutoModelForCausalLM model = AutoModelForCausalLM.from_pretrained("NorthernTribe-Research/math-conjecture-model", dtype="auto") - PEFT
How to use NorthernTribe-Research/math-conjecture-model with PEFT:
Task type is invalid.
- Notebooks
- Google Colab
- Kaggle
- Local Apps Settings
- vLLM
How to use NorthernTribe-Research/math-conjecture-model with vLLM:
Install from pip and serve model
# Install vLLM from pip: pip install vllm # Start the vLLM server: vllm serve "NorthernTribe-Research/math-conjecture-model" # Call the server using curl (OpenAI-compatible API): curl -X POST "http://localhost:8000/v1/chat/completions" \ -H "Content-Type: application/json" \ --data '{ "model": "NorthernTribe-Research/math-conjecture-model", "messages": [ { "role": "user", "content": "What is the capital of France?" } ] }'Use Docker
docker model run hf.co/NorthernTribe-Research/math-conjecture-model
- SGLang
How to use NorthernTribe-Research/math-conjecture-model 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 "NorthernTribe-Research/math-conjecture-model" \ --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": "NorthernTribe-Research/math-conjecture-model", "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 "NorthernTribe-Research/math-conjecture-model" \ --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": "NorthernTribe-Research/math-conjecture-model", "messages": [ { "role": "user", "content": "What is the capital of France?" } ] }' - Docker Model Runner
How to use NorthernTribe-Research/math-conjecture-model with Docker Model Runner:
docker model run hf.co/NorthernTribe-Research/math-conjecture-model
File size: 1,718 Bytes
e69a71a | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 | global:
output_root: model_development/runs/math-conjecture-scratch
seed: 17
tokenizer:
tokenizer_dir: model_development/runs/math-conjecture-scratch/tokenizer
vocab_size: 32768
min_frequency: 2
max_train_rows: 220000
special_tokens:
- <pad>
- <unk>
- <s>
- </s>
- <|system|>
- <|user|>
- <|assistant|>
model:
n_layer: 12
n_head: 12
n_embd: 768
n_positions: 2048
use_bf16: true
resid_pdrop: 0.1
embd_pdrop: 0.1
attn_pdrop: 0.1
initializer_range: 0.02
data:
train_file: data/releases/v1/train.parquet
validation_file: data/releases/v1/validation.parquet
prompt_field: prompt
target_field: target
final_answer_field: final_answer
proof_field: proof_formal
max_seq_length: 2048
max_train_samples: 240000
max_eval_samples: 4500
system_prompt: |
You are NorthernTribe Research's math-conjecture solver.
Recover answers for solved conjectures, produce checkable reasoning, and
preserve formal consistency suitable for Lean verification.
training:
output_dir: model_development/runs/math-conjecture-scratch/checkpoints
num_train_epochs: 1
max_steps: null
per_device_train_batch_size: 1
per_device_eval_batch_size: 1
gradient_accumulation_steps: 32
learning_rate: 2.0e-4
weight_decay: 0.1
warmup_ratio: 0.03
lr_scheduler_type: cosine
max_grad_norm: 1.0
gradient_checkpointing: true
logging_steps: 10
save_steps: 250
eval_steps: 250
save_total_limit: 3
dataloader_num_workers: 2
hub:
push_to_hub: false
repo_id: NorthernTribe-Research/math-conjecture-model
private: false
commit_message: Upload scratch-trained math-conjecture solver model.
credentials:
path: huggingface-api-key.json
|