support external models: vllm huggingface openai

[hsz0403]

Hi, I tested current sota llms for lean code and made a simple prompt to output tactics via vllm, huggingface and openai.

[objecti0n]

def _prompt_fewshot(state):
    prompt = f"My LEAN 4 state is:\n```lean\n" + state + \
        "```\nPlease predict a possible tactic to help me prove the theorem."
    prompt = [{"role": "user", "content": prompt}]
    return prompt

This prompt is used for SFT in Internlm-math-plus models.

[hsz0403]

fixed

[hsz0403]

Other model APIs e.g. Claude, Gemini, and Mistral will soon be tested and implemeted.

[hsz0403]

For now, Gemini and Claude APIs only support one sequence output, so the (str, float) list has only one element.

[Peiyang-Song]

Hi @hsz0403 , thanks again for the efforts! I am currently reviewing your code in order to merge and publish in the upcoming release. I was wondering if your code changes in any way the previous instructions to run external models, that is, e.g. run uvicorn server:app --port 23337 from ./python and then uncomment the code in ModelAPIs.lean.

Do your additional code require different steps to run, or would the original steps still work?

[hsz0403]

Hi, My previous changes include the file python/external_models for new models and server.py. No additional steps. I commented on the usage of new models in ModelAPIs.lean. According to the failing information, I guess CTranslate2 causes the error?

[Peiyang-Song]

Yes, the CI run itself is a bit buggy right now. For this PR we don't need the second CI check to pass.

[Peiyang-Song]

Thanks for confirming. Since there are no additional steps, I suppose running the code in this PR is as simple as going to ./python and start a server, then uncomment the corresponding code in ModelAPIs.lean. Did everything work as expected with these steps on your end?

E.g. in the first step, when trying your code by running uvicorn server:app --port 23337 from ./python, I saw the error

  File "/home/peiyangsong/LeanCopilot/python/server.py", line 6, in <module>
    from external_models import *
  File "/home/peiyangsong/LeanCopilot/python/external_models/__init__.py", line 1, in <module>
    from oai_runner import OpenAIRunner
ModuleNotFoundError: No module named 'oai_runner'

which I suppose can be fixed by changing the import statements in your __init__.py to relative imports, e.g. from oai_runner to .oai_runner. If the code in this PR has not been tested yet, it would be good to have it tested on your local end first; otherwise if the testing steps are different from the above, feel free to let me know.

[hsz0403]

Sorry for this mistake, each model should work well now in codespace

[Peiyang-Song]

Thanks! Can you update the requirement in python/README.md to reflect the new ones added with your PR? You can alternatively make a requirement.txt and use that if the requirement list becomes too long and you think would make the README messy.

[Peiyang-Song]

The code runs well, thank you! I will now go a pass reviewing it for code cleanness.

Meanwhile I notice that there are unused package imports, could you remove them and only keep the necessary ones, as you go through the requirements?

[hsz0403]

Hi, the unused package imports is because models not declared in python/server.py , all the packages in python/external_models/requirement.txt are required.

[Peiyang-Song]

Sounds great, thanks!

[Peiyang-Song]

By the way, is the requirement list in requirements.txt comprehensive? In addition, I suggest we move the requirements.txt to the outside folder, on the same level of python/README.md. Then after ensuring the requirement list is comprehensive we can replace the install command in the README with pip install -r requirements.txt.

[Peiyang-Song]

I will have this PR merged in the next official release.

[Peiyang-Song]

I made some minor comments in the code too. Thank you for the nice work!

A meta comment is that let us try to not leave commented-out code in there. If they are necessary we should make them options for users to pick. If they are not we should just delete the dead code. Also let's make sure the requirements are comprehensive -- more in the specific comments.

[Peiyang-Song]

Let's double check that all comments above are addressed. You can "resolve" a comment after you address it.

[Peiyang-Song]

@hsz0403 Let me know when it's ready for final review. I will merge it and publish with the upcoming new release.

[Peiyang-Song]

Changes look great, merging soon. Thanks!