{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Neural next-step prediction \n",
    "Tutorial on neural theorem proving\\\n",
    "Author: Sean Welleck\n",
    "\n",
    "----------------"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### High-level goal\n",
    "\n",
    "In *[Generative Language Modeling for Automated Theorem Proving](https://arxiv.org/abs/2009.03393)*, Stanislas Polu and Ilya Sutskever showed that a language model called *gptf* was capable of generating novel proofs that were adopted by a formal mathematics community. Their key insight was to frame *theorem proving as language generation*: first, use a neural language model $p_\\theta(y_t|x_t)$ to model the distribution over potential next-steps to take $y_t$ given the current state of a proof $x_t$, by simply treating $x_t$ and $y_t$ as discrete token sequences; then, use the language model within a search algorithm to generate a full proof.\n",
    "\n",
    "Since their work in 2020, this approach-which we refer to as *next-step prediction*-has formed the basis for research on combining language models with formal proof assistants, which we refer to as *neural theorem proving*. \n",
    "Neural theorem proving involves *interacting* with a proof assistant in order to generate a *verifiable* formal proof. This differs from traditional language generation tasks such as long-form question answering, which are often performed without interaction and are difficult to reliably evaluate in a scalable way.\n",
    "On the other hand, formal code is extremely scarce compared to the natural language found in everyday questions, or the Python code used to benchmark language-model-based code generators.\n",
    "As a result, neural theorem proving offers a unique, yet challenging, playground for creative algorithmic development with language models.\n",
    "<!--  -->\n",
    "<!-- This approach was radically different from prior methods based on hand-crafted features or a predefined set of possible next steps to take. -->\n",
    "<!--  -->\n",
    "\n",
    "Beyond algorithmic development, neural theorem proving offers an opportunity to enable new and useful tools.\n",
    "This tutorial walks through building an interactive tool for receiving next-step suggestions from a neural language model. Doing so involves [collecting data (part 1)](./I_nextstep_lean__part1_data.ipynb), [learning a model (part 2)](./I_nextstep_lean__part2_learn.ipynb), measuring performance with [proof search (part 3)](./I_nextstep_lean__part3_proofsearch.ipynb) and [evaluation sets (part 4)](./I_nextstep_lean__part4_evaluation.ipynb), and deploying the model as an [interactive tool (part 5)](./I_nextstep_lean__part5_llmsuggest.ipynb). \n",
    "By working through these notebooks, you will see core research ideas and get a practical introduction to neural theorem proving. We hope that doing so lays a foundation for doing research in this area, and that the end product shows a glimpse of \"human-machine collaboration\" that we expect will only expand further in the future."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<br>\n",
    "<img src=\"./images/llmsuggest/llmstep_gif.gif\" width=\"400px\" />"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": []
  }
 ],
 "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.11"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}