Vexorium-Agent 的 Lean 证明重构方案：每个阶段用不同模型、单题不超过 $3 上限，并以编译器校验的改写规则落地经验
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 团队在 NeurIPS 2026 Lean Refactor Arena 闭源赛道的技术报告中写道，其方案在 60 道决赛题上得 86.31 分（参考证明 33.33 分），deadline 时排第 8（最高 92.57），总花费 $166.33，单题平均 $2.772、上限 $3。
正文 · 原文
Abstract:Our closed-track entry (Arena username Vexorium-Agent) scored 86.31 points on the final board (L = 77.07, H = 81.86, Z = 100) over the 60 final problems, against 33.33 for the reference proofs, 8th at the deadline (top: 92.57), for US\$166.33 at list prices with every call counted (per problem: mean US\$2.772, at most US\$2.874; US\$3 cap). Three practices carry the entry. First, each paid stage runs the model that measured best per dollar for it among the 9 we tested in our own harness: GPT-6.1 Sol the early sessions, GPT-6.1 Terra the later ones and the tail at 70% of Sol's cost per turn, and Gemini 4 Argon the review and repair; Sol also runs the style rewrite. Second, what our development and research runs learned ships as compiler-checked programmatic rewrite rules rather than prompt text (+0.93 points from rules fixed before the release; +0.26 and +0.30, in sample, from passes built or switched on after the release). Third, every call is recorded and reviewed before each change (all 9 board scores came within -0.063 to +0.015 points of our meter's prediction). The harness, gate and many of these rules also serve our open-track entry. We report the full bill and the spread of three runs.
| Comments: | 20 pages. Technical report of team Vexorium-Agent for the closed track of the Lean Refactor Arena, a competition at the NeurIPS 2026 Workshop on AI for Verifiable Coding |
| Subjects: | Software Engineering (cs.SE); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO) |
| Cite as: | arXiv:2611.13011 [cs.SE] |
| (or arXiv:2611.13011v1 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2611.13011 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Bobber Cheng [view email]
[v1]
Mon, 9 Nov 2026 03:12:45 UTC (65 KB)
来源：arXiv cs.AI · arxiv.org