arXiv cs.AI· Bobber Cheng·· 10 小时前AI 评分31
Vexorium-Agent 用 GPT-6.1 与 Gemini 4 分步编译门控，Lean 证明重构赛获 86.31 分
Compile-Gated Lean Proof Refactoring with Enterprise Agent Practices: A Model per Step under a US\$3 Cap, Followed by Programmatic Rewrite Rules
AI 导读
Vexorium-Agent 在 Lean Refactor Arena 闭赛道上以 86.31 分位列第 8，60 道决赛题总花费 US$166.33，单题均值 US$2.772、最高 US$2.874，未超 US$3 上限。
正文 · AI 翻译
摘要：我们的封闭赛道参赛作品（Arena 用户名 Vexorium-Agent）在 60 道决赛题目的最终榜单上获得 86.31 分（L = 77.07，H = 81.86，Z = 100），参考证明为 33.33 分，截止时排名第 8（最高：92.57），按标价计算总花费 US$166.33，所有调用均计入（每题：平均 US$2.772，最高 US$2.874；上限 US$3）。该作品依赖三项实践。第一，每个付费阶段都在我们自建测试框架中测试过的 9 个模型里，选用该阶段每美元表现最好的模型：早期会话用 GPT-6.1 Sol，后期会话和尾部用 GPT-6.1 Terra，其每轮成本为 Sol 的 70%，审查与修复用 Gemini 4 Argon；风格重写也由 Sol 执行。第二，我们的开发和研究运行所学到的内容以编译器检查的程序化重写规则形式交付，而非提示文本（发布前修复的规则贡献 +0.93 分；发布后构建或启用的轮次在样本内贡献 +0.26 和 +0.30 分）。第三，每次调用都被记录，并在每次变更前接受审查（全部 9 个榜单分数与我们的计量预测相差在 -0.063 到 +0.015 分之间）。该测试框架、门控以及其中许多规则也服务于我们的开放赛道参赛作品。我们报告完整账单以及三次运行的分布。
| 评论： | 20 页。Vexorium-Agent 团队关于 Lean Refactor Arena 封闭赛道的技术报告，该竞赛属于 NeurIPS 2026 可验证编码 AI 研讨会 |
| 主题： | 软件工程（cs.SE）；人工智能（cs.AI）；计算机科学逻辑（cs.LO） |
| 引用为： | arXiv:2611.13011 [cs.SE] |
| （或 arXiv:2611.13011v1 [cs.SE] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2611.13011 arXiv 颁发的 DOI 通过 DataCite（待注册） |
提交历史
来自：Bobber Cheng [查看电子邮件]
[v1]
2026 年 11 月 9 日星期一 03:12:45 UTC（65 KB）
来源：arXiv cs.AI · arxiv.org