在 Modal 上构建基于强化学习的定理证明工作流

AE Studio 在 Modal 上搭建了用强化学习训练 LLM 证明数学定理的工作流，通过 vLLM 生成 Lean 证明代码、Lean 编译器在 CPU 上验证并给出奖励信号，对比了 GRPO 与 Evolution Strategies 两种更新规则。该工作流用独立镜像分离 GPU 生成、Lean 验证与编排三种运行时，并用 .map() 并行分发每次迭代的大量独立评估。