Instructions to use markm39/openproof-tactic-2b with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use markm39/openproof-tactic-2b with Transformers:

# Use a pipeline as a high-level helper
from transformers import pipeline

pipe = pipeline("text-generation", model="markm39/openproof-tactic-2b")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# Load model directly
from transformers import AutoModel
model = AutoModel.from_pretrained("markm39/openproof-tactic-2b", dtype="auto")

PEFT
How to use markm39/openproof-tactic-2b with PEFT:
```
Task type is invalid.
```
Notebooks
Google Colab
Kaggle
Local Apps Settings

vLLM

How to use markm39/openproof-tactic-2b with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "markm39/openproof-tactic-2b"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "markm39/openproof-tactic-2b",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker

docker model run hf.co/markm39/openproof-tactic-2b

SGLang

How to use markm39/openproof-tactic-2b 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 "markm39/openproof-tactic-2b" \
    --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": "markm39/openproof-tactic-2b",
		"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 "markm39/openproof-tactic-2b" \
        --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": "markm39/openproof-tactic-2b",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Docker Model Runner
How to use markm39/openproof-tactic-2b with Docker Model Runner:
```
docker model run hf.co/markm39/openproof-tactic-2b
```

markm39 commited on Mar 31

Commit

26b4c66

verified ·

1 Parent(s): 80c278b

Update README.md

Browse files

Files changed (1) hide show

README.md +56 -181

README.md CHANGED Viewed

@@ -1,207 +1,82 @@
 ---
 base_model: Qwen/Qwen3.5-2B
-library_name: peft
 pipeline_tag: text-generation
 tags:
 - base_model:adapter:Qwen/Qwen3.5-2B
 - lora
 - transformers
 ---
-# Model Card for Model ID
-<!-- Provide a quick summary of what the model is/does. -->
-## Model Details
-### Model Description
-<!-- Provide a longer summary of what this model is. -->
-- **Developed by:** [More Information Needed]
-- **Funded by [optional]:** [More Information Needed]
-- **Shared by [optional]:** [More Information Needed]
-- **Model type:** [More Information Needed]
-- **Language(s) (NLP):** [More Information Needed]
-- **License:** [More Information Needed]
-- **Finetuned from model [optional]:** [More Information Needed]
-### Model Sources [optional]
-<!-- Provide the basic links for the model. -->
-- **Repository:** [More Information Needed]
-- **Paper [optional]:** [More Information Needed]
-- **Demo [optional]:** [More Information Needed]
-## Uses
-<!-- Address questions around how the model is intended to be used, including the foreseeable users of the model and those affected by the model. -->
-### Direct Use
-<!-- This section is for the model use without fine-tuning or plugging into a larger ecosystem/app. -->
-[More Information Needed]
-### Downstream Use [optional]
-<!-- This section is for the model use when fine-tuned for a task, or when plugged into a larger ecosystem/app -->
-[More Information Needed]
-### Out-of-Scope Use
-<!-- This section addresses misuse, malicious use, and uses that the model will not work well for. -->
-[More Information Needed]
-## Bias, Risks, and Limitations
-<!-- This section is meant to convey both technical and sociotechnical limitations. -->
-[More Information Needed]
-### Recommendations
-<!-- This section is meant to convey recommendations with respect to the bias, risk, and technical limitations. -->
-Users (both direct and downstream) should be made aware of the risks, biases and limitations of the model. More information needed for further recommendations.
-## How to Get Started with the Model
-Use the code below to get started with the model.
-[More Information Needed]
-## Training Details
-### Training Data
-<!-- This should link to a Dataset Card, perhaps with a short stub of information on what the training data is all about as well as documentation related to data pre-processing or additional filtering. -->
-[More Information Needed]
-### Training Procedure
-<!-- This relates heavily to the Technical Specifications. Content here should link to that section when it is relevant to the training procedure. -->
-#### Preprocessing [optional]
-[More Information Needed]
-#### Training Hyperparameters
-- **Training regime:** [More Information Needed] <!--fp32, fp16 mixed precision, bf16 mixed precision, bf16 non-mixed precision, fp16 non-mixed precision, fp8 mixed precision -->
-#### Speeds, Sizes, Times [optional]
-<!-- This section provides information about throughput, start/end time, checkpoint size if relevant, etc. -->
-[More Information Needed]
-## Evaluation
-<!-- This section describes the evaluation protocols and provides the results. -->
-### Testing Data, Factors & Metrics
-#### Testing Data
-<!-- This should link to a Dataset Card if possible. -->
-[More Information Needed]
-#### Factors
-<!-- These are the things the evaluation is disaggregating by, e.g., subpopulations or domains. -->
-[More Information Needed]
-#### Metrics
-<!-- These are the evaluation metrics being used, ideally with a description of why. -->
-[More Information Needed]
-### Results
-[More Information Needed]
-#### Summary
-## Model Examination [optional]
-<!-- Relevant interpretability work for the model goes here -->
-[More Information Needed]
-## Environmental Impact
-<!-- Total emissions (in grams of CO2eq) and additional considerations, such as electricity usage, go here. Edit the suggested text below accordingly -->
-Carbon emissions can be estimated using the [Machine Learning Impact calculator](https://mlco2.github.io/impact#compute) presented in [Lacoste et al. (2019)](https://arxiv.org/abs/1910.09700).
-- **Hardware Type:** [More Information Needed]
-- **Hours used:** [More Information Needed]
-- **Cloud Provider:** [More Information Needed]
-- **Compute Region:** [More Information Needed]
-- **Carbon Emitted:** [More Information Needed]
-## Technical Specifications [optional]
-### Model Architecture and Objective
-[More Information Needed]
-### Compute Infrastructure
-[More Information Needed]
-#### Hardware
-[More Information Needed]
-#### Software
-[More Information Needed]
-## Citation [optional]
-<!-- If there is a paper or blog post introducing the model, the APA and Bibtex information for that should go in this section. -->
-**BibTeX:**
-[More Information Needed]
-**APA:**
-[More Information Needed]
-## Glossary [optional]
-<!-- If relevant, include terms and calculations in this section that can help readers understand the model or model card. -->
-[More Information Needed]
-## More Information [optional]
-[More Information Needed]
-## Model Card Authors [optional]
-[More Information Needed]
-## Model Card Contact
-[More Information Needed]
-### Framework versions
-- PEFT 0.18.1

 ---
 base_model: Qwen/Qwen3.5-2B
 pipeline_tag: text-generation
 tags:
 - base_model:adapter:Qwen/Qwen3.5-2B
 - lora
 - transformers
+- lean4
+- theorem-proving
+- tactic-prediction
+- formal-verification
+- mathlib
+- peft
+license: mit
+datasets:
+- markm39/openproof-tactic-pairs
 ---
+# OpenProof Tactic 2B
+A Lean 4 tactic prediction model fine-tuned from [Qwen/Qwen3.5-2B](https://huggingface.co/Qwen/Qwen3.5-2B) on 190K+ Mathlib tactic pairs.
+Given a Lean 4 proof goal state, the model predicts the next tactic to apply. Designed for use in best-first search (BFS) proof engines like [OpenProof](https://github.com/mxthematic/openproof).
+## Usage
+```python
+from transformers import AutoModelForCausalLM, AutoTokenizer
+from peft import PeftModel
+import torch
+base = "Qwen/Qwen3.5-2B"
+tokenizer = AutoTokenizer.from_pretrained(base)
+model = AutoModelForCausalLM.from_pretrained(base, torch_dtype=torch.bfloat16, device_map="cuda")
+model = PeftModel.from_pretrained(model, "markm39/openproof-tactic-2b")
+# Input: goal state followed by :::
+prompt = "n m : Nat\\n⊢ n + m = m + n:::"
+inputs = tokenizer(prompt, return_tensors="pt").to("cuda")
+with torch.no_grad():
+    out = model.generate(**inputs, max_new_tokens=64, do_sample=True, temperature=0.6, top_k=10)
+print(tokenizer.decode(out[0][inputs.input_ids.shape[1]:], skip_special_tokens=True))
+# Output: induction m with | zero => simp | succ m ih => simp [Nat.add_assoc, ih, Nat.add_comm]
+```
+## Training
+- **Base model**: Qwen/Qwen3.5-2B
+- **Method**: SFT with LoRA (rank 64, alpha 128)
+- **Trainable params**: 43.6M / 1.93B (2.3%)
+- **Data**: [markm39/openproof-tactic-pairs](https://huggingface.co/datasets/markm39/openproof-tactic-pairs) -- 190K+ Lean 4 goal-tactic pairs extracted from Mathlib
+- **Input format**: `{goal_state}:::`
+- **Output format**: tactic string
+- **Epochs**: ~1.8 (12,500 steps)
+- **Batch size**: effective 128 (2 per device x 32 gradient accumulation)
+- **Learning rate**: 2e-5 cosine schedule
+- **Best eval loss**: 0.5492 (checkpoint-12500)
+- **Hardware**: RunPod GPU instance
+- **Framework**: HuggingFace TRL + PEFT
+## Intended Use
+Tactic prediction for automated theorem proving in Lean 4. The model generates candidate tactics given a proof goal state, which are then verified by the Lean type checker. Designed to be used with beam search -- sample multiple candidates and verify each.
+Not intended for general-purpose text generation.
+## Limitations
+- Trained on Mathlib tactics only -- may not generalize to custom Lean libraries
+- LoRA adapter (must be loaded on top of Qwen3.5-2B base)
+- SFT only (no RL/GRPO refinement yet)
+- May hallucinate lemma names that don't exist in Mathlib
+## Links
+- [OpenProof](https://github.com/mxthematic/openproof) -- the theorem prover that uses this model
+- [Training code](https://github.com/mxthematic/openproof-ml)
+- [Training data](https://huggingface.co/datasets/markm39/openproof-tactic-pairs)
+## Acknowledgments
+Training data derived from [LeanDojo](https://leandojo.org/) (Yang et al.), [Lean Workbook](https://huggingface.co/datasets/internlm/Lean-Workbook) (InternLM), and [Goedel-Pset](https://huggingface.co/datasets/Goedel-LM/Goedel-Pset) (Goedel-LM). Tactic extraction from whole proofs uses [Pantograph](https://github.com/leanprover/Pantograph) kernel-level invocations.