bentleylong commited on
Commit
02b2709
1 Parent(s): f10d517

Update README.md

Browse files
Files changed (1) hide show
  1. README.md +1 -1
README.md CHANGED
@@ -25,7 +25,7 @@ tags:
25
  - **Language(s) (NLP):** English.
26
  - **License:** **<a href="https://www.apache.org/licenses/LICENSE-2.0" target="_blank">Apache 2.0</a>**
27
 
28
- 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 GPT4All</a>**, 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>**.
29
 
30
 
31
 
 
25
  - **Language(s) (NLP):** English.
26
  - **License:** **<a href="https://www.apache.org/licenses/LICENSE-2.0" target="_blank">Apache 2.0</a>**
27
 
28
+ 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>**.
29
 
30
 
31