xcz0/lean4-eval-pipeline

Check out the configuration reference at https://huggingface.co/docs/hub/spaces-config-reference

功能概览

本项目提供一个 Streamlit 页面：输入自然语言数学题 → 调用 Hugging Face Inference 生成 PLAN: + 一个 lean4 代码块 → 通过 lake env <repl> 在内置的 Mathlib 项目中编译验证（无 error 且无 sorry 才算通过）。

Hugging Face Spaces 配置

必需 Secrets

• —HF_TOKEN：调用 Hugging Face Inference 必需。未设置会直接在 UI 中报错并停止。

可选 Variables

• —HF_MODEL_ID：要调用的模型 ID。
• —默认：deepseek-ai/DeepSeek-Prover-V2-7B
• —说明：并非所有模型都支持 HF Serverless Inference 的 text-generation/chat-completion。如果出现 provider 相关报错，优先尝试换一个确认可用的模型或使用 Endpoint。

• —HF_BASE_URL：自定义 Inference Endpoint Base URL（当你使用专用 Endpoint 时设置）。
• —用途：绕开 Serverless Inference 对“模型/任务”的限制，稳定性通常更好。

• —HF_PROVIDER：显式指定推理提供方（provider）。
• —示例：hf-inference
• —说明：不同 huggingface_hub 版本/运行环境可用的 provider 可能不同；不确定时可以先不设置。

• —LEAN_REPL_BIN：repl 可执行文件路径。
• —容器默认：/app/repl/.lake/build/bin/repl
• —一般不需要修改。

常见问题（Troubleshooting）

1) StopIteration / 找不到 provider

这通常表示：当前模型 + 任务（比如 text-generation）在你的推理环境里没有可用 provider。你可以：

1. 1.将 HF_MODEL_ID 换成一个已在 Hugging Face Inference 上可用的模型；
2. 2.使用专用 Inference Endpoint：设置 HF_BASE_URL 并保证 HF_TOKEN 有权限；
3. 3.需要时设置 HF_PROVIDER（例如 hf-inference）来显式选择 provider。

2) 模型输出无法解析（没生成标准代码块）

本项目解析逻辑要求：

• —先输出以 PLAN: 开头的计划段落；
• —再输出且仅输出一个 fenced code block，且语言标记为 lean/lean4。

如果 UI 提示“未能生成标准的 Lean 代码块”，可在页面底部查看模型原始输出并据此调整提示词或更换模型。