partI_nextstep/notebooks/I_nextstep_lean__part6_llmsuggest.ipynb

{
 "cells": [
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Neural next-step prediction | part 6: LLMLean suggestion tool\n",
    "Tutorial on neural theorem proving\\\n",
    "Author: Sean Welleck\n",
    "\n",
    "----------------"
   ]
  },
  {
   "attachments": {},
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### High-level goal\n",
    "\n",
    "Finally, we will make an interactive tool that uses our context-dependent generator to suggest next-steps in VS Code:\n",
    "\n",
    "<img src=\"./images/llmsuggest/llmstep_gif.gif\" width=\"400px\" />"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "\n",
    "Concretely, we will use [LLMLean](https://github.com/cmu-l3/llmlean), which provides tools for running LLMs in Lean on your laptop (or calling external LLM APIs).\n",
    "\n",
    "<img src=\"images/llmlean.png\" width=600px>\n",
    "\n",
    "For tutorial purposes, we will make a simple  server that hosts our model from the tutorial. Conceptually, our simple server will take the place of the \"cloud LLM API\" in the diagram above. \n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "LLMLean consists of Lean **tactics** that communicate with language models.\n",
    "\n",
    "For example, the `llmstep` tactic in LLMLean:\n",
    "1. Sends the current proof state and file contents to a server\n",
    "2. Checks the resulting generations in Lean and displays them\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "vscode": {
     "languageId": "plaintext"
    }
   },
   "source": [
    "#### Run a server"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "!cd ../ntp-server && python server.py"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Set environment variables\n",
    "\n",
    "Now open the [llmlean example](https://github.com/wellecks/llmlean-example) in VS Code. By default, LLMLean does not communicate with our custom server, so we need to set environment variables.\n",
    "\n",
    "Set the following environment variables:\n",
    "\n",
    "<img src=\"images/env-variables.png\" width=\"500px\">\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Be sure to restart Lean. Now you can call `llmstep` within a Lean file in the project, e.g.:\n",
    "\n",
    "<img src=\"images/llmlean-example.png\">"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Take a look at the LLMLean documentation to see how to use a LLM such as Llemma-7b via `ollama`, which does not require manually running the server above. Also take a look at LLMLean's implementation if you are curious how it works."
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.10.13"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}