新基准测智能体写形式化证明
OfirPress · x · 2026-07-09
Balaji Rao 等人发布了 s2n-bignum-bench，用来评测智能体在 HOL Light 中为 Amazon 的 s2n-bignum 仓库里的密码学汇编代码编写证明的能力。帖子提到，Codex 5.3 xhigh 目前只拿到 6.3% 的成绩，说明这个基准仍有很多可改进空间。
「编程与Agent」频道最新
- 开源 Agent Skill 2.3k 星:生成 MVP 蓝图并审计重构 agentic harness — tom_doerr · 2026-09-11
- Cognition SWE-2 用 KKT 对偶优化长度惩罚，一次 RL 推移 Pareto 曲线 — YouJiacheng · 2026-09-11
- 首届 Three.js 大会落地巴黎，AI 正缩短从想法到原型的距离 — OdinLovis · 2026-09-11
- 观点：Agent 真正的瓶颈是企业数据工程能力 — dhruv2038 · 2026-09-11
- 实测戳破 RTK 省钱神话:token 省了,账单分文未降 — Bartaseth · 2026-09-11
- GPT-6 Astra 用时 44 小时通关含敌人 Factorio,API 成本约 4500 美元 — liminal_bardo · 2026-09-11