morph-prover-v0-7b

Stream: Machine Learning for Theorem Proving

[Mark Andrew Gerads]

I recently noticed this: https://morph.so/blog/the-personal-ai-proof-engineer/
TLDR: it is an AI for math proofs in Lean.

I was able to download the AI at HuggingFace [ https://huggingface.co/morph-labs/morph-prover-v0-7b ], but have no idea how to use it.

I am asking how to use it here because I figure someone else here may be using it, and because it seems like something people here would be interested in.

I am using Kubuntu 23.10 x86_64.
When trying to install llama.cpp, I gave up at the error

mark@mark-XPS-15-9520:~/Git/llama.cpp$ python3 -m pip install -r requirements.txt
error: externally-managed-environment

× This environment is externally managed
╰─> To install Python packages system-wide, try apt install
    python3-xyz, where xyz is the package you are trying to
    install.

    If you wish to install a non-Debian-packaged Python package,
    create a virtual environment using python3 -m venv path/to/venv.
    Then use path/to/venv/bin/python and path/to/venv/bin/pip. Make
    sure you have python3-full installed.

    If you wish to install a non-Debian packaged Python application,
    it may be easiest to use pipx install xyz, which will manage a
    virtual environment for you. Make sure you have pipx installed.

    See /usr/share/doc/python3.11/README.venv for more information.

note: If you believe this is a mistake, please contact your Python installation or OS distribution provider. You can override this, at the risk of breaking your Python installation or OS, by passing --break-system-packages.
hint: See PEP 668 for the detailed specification.

Ubuntu does not have the gguf in the apt repository, so what to do?

GPT4All installed correctly, except I do not know how to use morph-prover-v0-7b with it.

[Notification Bot]

This topic was moved here from #general > morph-prover-v0-7b by Scott Morrison.

[Junyan Xu]

GPT4All only supports gguf, it seems. There's a gguf version of Morph prover here.

[Junyan Xu]

Alternatively you can join their Discord and access the model there.
The model was announced here, and Moogle is made by the same team.

[Junyan Xu]

Here is a list of clients/UI that support GGUF that you may try, including text-generation-webui, KoboldCpp, and LM Studio. I've successfully ran Mistral 7B using the firs two on Windows, but haven't tried Morph Prover yet.

BTW, it may help to paste your error messages into ChatGPT/Claude/Bing Chat/Perplexity etc.

[Mark Andrew Gerads]

I was able to get the GGUF working with https://github.com/LostRuins/koboldcpp
The LLM can indeed generate Lean 4 code, but it does not seem very helpful to me.

[Utensil Song]

Mark Andrew Gerads said:

I was able to get the GGUF working with https://github.com/LostRuins/koboldcpp
The LLM can indeed generate Lean 4 code, but it does not seem very helpful to me.

Originally I got GGUF working with LLM Studio and had some observations and feebacks. I'm sure these issues would be addressed in the next release. After the release of moogle.ai, and using it on a daily basis, I'm even more looking forward to seeing the next release of Morph Prover.