File size: 2,591 Bytes
5829a90 35c7a1e 5829a90 35c7a1e 5829a90 f10d517 5829a90 02b2709 5829a90 35c7a1e |
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 |
---
license: apache-2.0
language:
- en
pipeline_tag: text-generation
tags:
- math
- lean
---
# **morph-prover-v0-7b**
## Table of Contents
1. **<a href="https://huggingface.co/morph-labs/morph-prover-v0-7b-gguf#model-summary" target="_blank">Model Summary</a>**
2. **<a href="https://huggingface.co/morph-labs/morph-prover-v0-7b-gguf#contact" target="_blank">Contact</a>**
3. **<a href="https://huggingface.co/morph-labs/morph-prover-v0-7b-gguf#ethical-considerations-and-limitations" target="_blank">Ethical Considerations & Limitations</a>**
# **Model Summary**
- **Developed by:** **<a href="https://www.morph.so" target="_blank">Morph Labs</a>**
- **Language(s) (NLP):** English.
- **License:** **<a href="https://www.apache.org/licenses/LICENSE-2.0" target="_blank">Apache 2.0</a>**
Morph Prover v0 7B, the first open-source model trained as a conversational assistant for Lean users. This model was trained in collaboration with **<a href="https://nousresearch.com/" target="_blank">Nous Research</a>** and the **<a href="https://cs.stanford.edu/~sanmi/" target="_blank">Safe and Trustworthy AI Research (STAIR) group at Stanford</a>** 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 **<a href="https://huggingface.co/nomic-ai" target="_blank">Nomic AI's</a>** GPT4All Vulkan support, this model can run on any consumer GPU. Morph Prover v0 7B is a chat fine-tune of **<a href="https://huggingface.co/mistralai/Mistral-7B-v0.1" target="_blank">Mistral 7B</a>** 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 **<a href="https://github.com/morph-labs/mci" target="_blank">Morph Code Index</a>**.
## Contact
**<a href="https://forms.gle/fwZhARyzrGEz9t4Q6" target="_blank">Contact Form</a>**
## 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. |