Instructions to use typeof/morph-prover-v0-7b-sharded with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use typeof/morph-prover-v0-7b-sharded with Transformers:

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

pipe = pipeline("text-generation", model="typeof/morph-prover-v0-7b-sharded")

# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("typeof/morph-prover-v0-7b-sharded")
model = AutoModelForCausalLM.from_pretrained("typeof/morph-prover-v0-7b-sharded")

Notebooks
Google Colab
Kaggle
Local Apps

vLLM

How to use typeof/morph-prover-v0-7b-sharded with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "typeof/morph-prover-v0-7b-sharded"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "typeof/morph-prover-v0-7b-sharded",
		"prompt": "Once upon a time,",
		"max_tokens": 512,
		"temperature": 0.5
	}'

Use Docker

docker model run hf.co/typeof/morph-prover-v0-7b-sharded

SGLang

How to use typeof/morph-prover-v0-7b-sharded 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 "typeof/morph-prover-v0-7b-sharded" \
    --host 0.0.0.0 \
    --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "typeof/morph-prover-v0-7b-sharded",
		"prompt": "Once upon a time,",
		"max_tokens": 512,
		"temperature": 0.5
	}'

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 "typeof/morph-prover-v0-7b-sharded" \
        --host 0.0.0.0 \
        --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "typeof/morph-prover-v0-7b-sharded",
		"prompt": "Once upon a time,",
		"max_tokens": 512,
		"temperature": 0.5
	}'

Docker Model Runner
How to use typeof/morph-prover-v0-7b-sharded with Docker Model Runner:
```
docker model run hf.co/typeof/morph-prover-v0-7b-sharded
```

morph-prover-v0-7b

This is the sharded version of https://huggingface.co/morph-labs/morph-prover-v0-7b

Most recent commit b6e98c1

Model Summary
Blog Post
Training Format
Sign Up for Hosted Use
Citation
Ethical Considerations & Limitations

Model Summary

Developed by: Morph Labs
Language(s) (NLP): English.
License: Apache 2.0

Morph Prover v0 7B, the first open-source model trained as a conversational assistant for Lean users. This model was trained in collaboration with Nous Research and the Safe and Trustworthy AI Research (STAIR) group at Stanford led by professor Sanmi Koyejo, with major contributions by Brando Miranda of Stanford and help from Peter Holderrieth of MIT and Jin Peng Zhou of Cornell. Thanks to Nomic AI's GPT4All Vulkan support, this model can run on any consumer GPU. Morph Prover v0 7B is a chat fine-tune of Mistral 7B which achieves state of the art results in autoformalization while performing better than the original Mistral model on benchmarks like AGIEval and MMLU. It was trained with a proprietary synthetic data pipeline with code data generated by the Morph Code Index.

Blog Post

https://morph.so/blog/the-personal-ai-proof-engineer/

Training Format

The model was trained for chat using the Llama 2 chat format. Example as follows:

[INST] <<SYS>>\n You are a helpful assistant. \n<</SYS>>\n\n  What is the curry howard isomorphism? [/INST]

Sign Up for Hosted Use

Sign Up Form

Citation

@misc{morphprover2023, title={Morph Prover v0 7B: the first open-source chat assistant for Lean}, author={Morph Labs, Jesse Michael Han, Eric Yu, Bentley Long, Pranav Mital, Brando Miranda, Peter Holderrieth, Jin Peng Zhou, Sanmi Koyejo}, year={2023}, }

Ethical Considerations and Limitations

Morph Prover v0 7B, as with all Large Language Models, carries inherent risks with use. Testing has been solely conducted in English, and our testing has not been fully comprehensive nor could be fully comprehensive of all use scenarios. The model may be prone to producing inaccurate, unsatisfactory, or otherwise undesirable outputs, and thus we encourage all developers to test and tune to their specific use case prior to deployment.

Downloads last month: 6

Safetensors

Model size

7B params

Tensor type

BF16

typeof
/

morph-prover-v0-7b-sharded