★ 3
OpenFrontiers 发布 12151 个开放科研问题与数学再发现基准
研究者推出跨学科资源 OpenFrontiers，收录 12,151 个开放研究问题的结构化语料，并构建 200 道数学题的回顾性基准（110 道 2026 年已解决、90 道仍开放），每题配 Lean 4 形式化陈述。在 HQ-50 子集上评测七个 LLM 智能体，闭卷再发现最多仅解出 40 题…
arXiv cs.AI3 天前
#Lean 4
共 6 篇相关资讯，按重要度与时间排序，每 3 小时更新。
★ 3
h1 框架：简单智能体循环在 Lean 4 定理证明达 SOTA
论文提出 h1，一个仅给模型提供高效 Lean 4 接口、依靠验证器反馈与自我反思持续迭代的简单框架，不预设分解或搜索结构。h1 在 PutnamBench、FATE-X、FormalConjectures100-Solved 上取得 SOTA，并解决 FormalConjectures 中 8 …
arXiv cs.LG5 天前
★ 3
ReuF2F：244 道本科科研开放题 Lean 4 基准发布
研究者推出 ReuF2F，收录 244 道来自本科生科研项目（REU）的 Lean 4 形式化开放问题，用于端到端评测编码智能体的开放问题求解能力。基于 mini-SWE-agent 构建 Leanimum-agent 统一评测框架，结果显示最强模型仅解出约 40% 的题目。
arXiv cs.AI12 天前
★ 3
LeanPolish：Lean证明压缩的验证监督
论文提出LeanPolish符号化Lean 4流水线，发布33402条被接受的局部编辑与65596条同状态失败尝试，研究模型从验证监督中学到什么。实验表明延续菜单评估可消除排序捷径，迭代符号化处理将miniF2F节省率从19.7%提升至27.5%，微调将PutnamBench验证token缩减从2…
arXiv cs.LG32 天前
★ 2
新方法用 Lean 4 编译器报错修复定理证明，解出率提升 32%
论文提出有界在线步骤级修复模块：每步采样 K 个策略，失败时把 Lean 4 编译器错误信息喂给预训练修复模型就地修正，而非丢弃重采样。在 LeanDojo 1990 条定理子集上最多取得 32% 相对提升、多解出 82 条定理，收益主要来自浅层策略执行错误。该方法在 Lean Workbook …
arXiv cs.AI12 天前
★ 2
LeanLLM：面向 Lean 4 应用的 LLM SDK 开源
开发者发布 LeanLLM，一个面向 Lean 4 语言的统一 LLM 客户端库，支持 Anthropic Claude、OpenAI、Google Gemini、DeepSeek、Qwen、Mistral 等多家模型，并兼容 OpenRouter、AWS Bedrock、Azure OpenAI…
Hacker News – LLM19 天前
这个主题的相关资产
相关公司OpenAI1