README.md

metadata

license: apache-2.0
language:
  - en
pipeline_tag: text-generation
tags:
  - math
  - lean

Model Details

$${\text{🧮}}_{\mathrm{\Delta }LoRA}={\mathrm{\Delta }}_{({\text{🧡}}_W,{\text{🧮}}_W)}🧮\_\{\Delta LoRA\}\; =\; \backslash Delta\_\{(🧡\_W,\; 🧮\_W)\}$$

$${\text{🧡}}_W+{\text{🧮}}_{\mathrm{\Delta }LoRA}={\text{🧮}}_W🧡\_W\; +\; 🧮\_\{\Delta LoRA\}\; =\; 🧮\_W\; \backslash \backslash$$

morph-prover-v0-7b

Table of Contents

1. Model Summary
2. Blog Post
3. Training Format
4. Sign Up for Hosted Use
5. Citation
6. 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.