您尚未登录账户
您的企业账号申请正在审核中
Lean Co-pilo让你可以在Lean使用LLM
这个创新系统利用LLM在Lean定理证明器中提出证明策略，为人工干预和修改提供了一个无缝的环境。
LeanDojo团队和加州理工学院推出了Lean Co-pilot，这是一个为LLM与人类互动而设计的协作工具，用于构建100%准确的形式数学证明。
这个创新系统利用LLM在Lean定理证明器中提出证明策略，为人工干预和修改提供了一个无缝的环境。
自动化定理证明的挑战性领域长期以来一直受到当前LLM在数学和推理任务中的不可靠性的阻碍，这些经常会出错和产生幻觉。传统上，数学证明主要依赖于手工推导，需要细致的验证。
Lean是一个强大的定理证明器，但人类在编写Lean时会发现这是一个繁琐的任务。Lean Co-pilot通过利用LLM来自动化推荐Lean证明策略，显著加快了速度。该系统仅在必要时允许人类输入，提供了机器智能与人类智能之间的平衡合作。
Lean Co-pilot的关键特点包括由LLM驱动的证明步骤建议，搜索证明，以及从广泛的数学库中选择有用的引理。该工具无缝集成到Lean的Visual Studio Code工作流程中，确保了用户友好的体验。
用户可以将Lean Co-pilot设置为Lean包，使用内置的LeanDojo模型，或者集成可以在本地或云上运行的自定义模型。
LeanDojo，支持Lean Co-pilot的平台，通过提供MIT许可下的开源模型和工具来支持可访问性。该工具可以在各种平台上运行，包括Linux、macOS和Windows WSL，可选地支持CUDA启用的GPU。
Lean Co-pilot的要求包括Git LFS，CUDA和cuDNN（推荐用于GPU支持）以及用于构建Lean Co-pilot本身的CMake>= 3.7和C++17兼容编译器。
Lean Co-pilot的引入旨在使LLM对Lean用户更加易于访问，促进积极的反馈循环，在该反馈循环中，证明自动化有助于提高数据质量，最终推动LLM在数学任务中的改进。
