Oct, 2023

LLMSTEP: Lean中的LLM证明步骤建议

HTML
PDF
TL;DRLLMSTEP是将语言模型整合到Lean证明助手中的工具，它将用户的证明状态发送到托管语言模型的服务器，语言模型生成建议并在Lean中检查后显示给用户在其开发环境中。我们提供了基准语言模型，以及用于微调和评估的代码，以支持进一步的开发。我们提供了在CPU、CUDA GPU或Google Colab笔记本上运行的服务器实现，这是快速有效的语言模型建议的一小步。