★ 3
arXiv 发布 Lean4AgenticRL 框架与 LAR-9B/27B 智能体模型
Lean4AgenticRL 是首个将多级过程奖励建立在统一 Lean4 形式化体系上的开放式智能体强化学习框架，结合问题专属工作流与工作流阶段归一化 GRPO 算法。基于该框架训练的 LAR-9B/27B 中，LAR-27B 在 TerminalBench-2.1 上达到 77.3%，平均超越基…
arXiv cs.LG14 天前
#Lean4
共 2 篇相关资讯，按重要度与时间排序，每 3 小时更新。
★ 3
IneqAgent：结合符号计算在 Lean4 中证明不等式
论文提出 IneqAgent，将 LLM 推理与符号计算结合用于 Lean4 不等式证明，通过引理级蒙特卡洛树搜索协调引理构造、目标改写与符号后端选择。使用 DeepSeek-V4-Flash 时在四个基准上解决 186 题中的 175 题（94.09%），并在四维和五维上获得 Dittert 猜…
arXiv cs.AI17 天前
这个主题的相关资产
相关公司深度求索（DeepSeek）1