LeanAide LLAMA or Deepseek extension

Stream: general

[Frederick Pu]

I'm thinking about modifying LeanAide to work with other language models such as LLAMA and Deepseek, which lean file actual handles making the API calls?

[Jason Rute]

@Siddhartha Gadgil

[Siddhartha Gadgil]

@Frederick Pu
It is the file https://github.com/siddhartha-gadgil/LeanAide/blob/main/LeanCodePrompts/ChatClient.lean. It is already abstracted to use a couple of protocols, including the OpenAI one given a url.

Ideally I should replace my ad hoc curl calls with a dependency like LLMLean in the spirit of centralizing (and then contributing to) common resources (pinging @David Renshaw ). This is on my to-do list but I of course will welcome PRs doing this.

[Frederick Pu]

where is the ChatServer type defined?

[Siddhartha Gadgil]

In the same file at line 63

[Frederick Pu]

so which lanugage model is used to specified just by changing the auth header?

[Siddhartha Gadgil]

This is really written only for three cases I used. For others one has to use .generic and specify the url. I have only used this with local models run using vLLM.

Most likely more constructors will be needed to handle more general cases.

[Frederick Pu]

how would you pick which one to use? is it using set_option? also if your using gemini would you have to setup an api key or smth?

[Siddhartha Gadgil]

It is passed as a parameter for calls. Yes, there are some set_option parameters but mostly I experimented with using other models with compiled Lean programs.

For gemini, I used gcloud to authenticate my system. Then just calling a url worked fine.

[Siddhartha Gadgil]

The setup is really ad hoc at present, essentially to allow the 3-4 cases I used.

[Frederick Pu]

ig having a general call chatbot function instead of changing the auth header would be a good first step

[Frederick Pu]

that way you could use offline models or embedded cpp models like they do in lean copilote

[Siddhartha Gadgil]

It is convenient to abstract away the client as a term of a ChatServer type. Maybe a good way is to have a more generic constructor than what I call .generic or maybe a few cases.

[Frederick Pu]

realistically the only two types of chatbots are servers and ffi

[Frederick Pu]

cause even a locally hosted chat bot would need to be accessed via server if it isnt compiled into cpp

[Siddhartha Gadgil]

And I believe essentially all servers support the OpenAI API. So instead of generic one can have server and have an additional ffiLocal constructor. Otherwise have say openAIServer and llamaServer for two different protocols.

I don't know what arguments are needed for ffi. Maybe an enumeration is enough - each ffi takes work and one can add cases as they come.

[Hanting Zhang]

I've been toying around with this for LLMLean. Unfortunately it seems like the deepseek-reasoner API is too overloaded and I never get any responses back. deepseek-chat works though and the performance seems to be similar to gpt-4o

[Siddhartha Gadgil]

In LeanAide this is now implemented but only partially tested. To use with the command line program, use something similar to the following (this is querying o1-mini1 but as if it were a generic model). You have to give the correct url as well as model name.

lake exe translate "There are infinitely many even numbers." --auth_key "<authentication-key>" --url "https://api.openai.com/v1/chat/completions" --model "o1-mini" --temperature 10 -n 1 --no_sysprompt

Some of the parameters are because reasoning models (at least from OpenAi) need responses set to 1, temperature to $1$  and do not allow system prompts.

There are similar settings to use in the interpreter mode. Namely, one uses set_option with leanaide.translate.url?, leanaide.translate.authkey and also leanaide.translate.choices and leanaide.translate.temperature10.

I hope to have an easier to use server-client setup as well as a fully open-source option (currently the embeddings use OpenAI even if a different model is used). I will post more detailed instructions then.