AI Models

Built-In LLMs

Various different LLMs are supported by ESBMC-AI.

OpenAI

The following models require the OPENAI_API_KEY environment variable to be set.

• gpt-3.5-turbo
• gpt-3.5-16k
• gpt-4
• gpt-4-32k

Technology Innovation Institute (TII)

The following model requires the HUGGINGFACE_API_KEY environment variable to be set.

• falcon-7b: (Prototype/WIP) Uses text-generation-inference on the backend.

Custom LLM

ESBMC-AI has support of custom AI. The config supports adding custom AI models that are text-generation-inference from Hugging Face. These are specified in config.json inside the ai_custom field. The ai_model field selects which AI model to use. If the AI model is chosen and does not exist built in, then the list inside ai_custom will be checked. This means that all the entries inside ai_custom must be unique and not match any of the built-in first class AI. When adding a custom_ai entry. The name of the AI will be the entry name. The entry takes three fields, max_tokens, url, and config_message:

• The max_tokens are the acceptable max tokens that the AI can accept.
• The url is the text-generation-inference server URL that the LLM is hosted in.
• The config_message is a custom configuration message that will wrap the messages, this is used to convert text generation LLM into Chat LLMs.
• All the values mentioned are dependent on the LLM that is implemented.

There are tokens that are replaced inside the config_message in order to insert the conversation:

• {history}: The previous messages sent by the AI model.
• {user_prompt}: The last message of the user to the AI.

Examples

In order to run each LLM configuration, the ai_model entry in the config.json needs to be set to the name of the entry. Alternatively, the argument -m <name> can be passed to ESBMC-AI when running the program. The configuration entry also specifies that the maximum number of tokens that the model accepts is 1024, along with the URL describing its location and config message. The config message specified is simply the identity of the conversation. It does not manipulate the conversation at all.

Template

Here is a template example entry for custom-ai.

"example-llm": {
  "max_tokens": 1024,
  "url": "www.example.com",
  "config_message": "{history}\n{user_prompt}\n"
}

Falcon-7B

Here is an example entry for the ai_custom field in the config.json that implements the same behavior as the “falcon-7b” built-in model:

"example-llm": {
      "max_tokens": 1024,
      "url": "https://api-inference.huggingface.co/models/tiiuae/falcon-7b-instruct",
      "config_message": ">>DOMAIN<<You are a helpful assistant that answers any questions asked based on the previous messages in the conversation. The questions are asked by Human. The \"AI\" is the assistant. The AI shall not impersonate any other entity in the interaction including System and Human. The Human may refer to the AI directly, the AI should refer to the Human directly back, for example, when asked \"How do you suggest a fix?\", the AI shall respond \"You can try...\". The AI should use markdown formatting in its responses. The AI should follow the instructions given by System.\n\n>>SUMMARY<<{history}\n\n>>QUESTION<<{user_prompt}\n\n>>ANSWER<<"
},