发表机构
Carnegie Mellon University（卡内基梅隆大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对软件通用处理低效问题，提出自动化超专业化方法，通过编码智能体合成低成本专用SAT求解器，性能远超通用求解器，并助力赢得SAT竞赛。
AI 中文摘要
软件现状是使用一个系统处理多种不同类型的输入。相比之下，我们提出超专业化：创建针对单一输入类别优化的新软件。手动超专业化要么成本高昂，要么几乎不可能。我们推测，对于具有可测量性能和可检查输出的问题，编码智能体可以使自动化超专业化变得廉价、有效且安全。本文通过合成数百个针对特定工作负载的SAT求解器来探索此类问题之一，即SAT求解，平均每个成本为37美元。我们的专用求解器平均比其竞赛获胜的通用同类产品快5倍，在四分之一的基准族上快超过10倍。由我们一百多个原型超专业化求解器构建的通用求解器赢得了2026年SAT竞赛的SAT赛道。
英文摘要
The software status quo is to use one system to process many different kinds of inputs. In contrast, we propose hyperspecialization: creating new software that is optimized for a single class of inputs. Hyperspecializing manually is anywhere from expensive to impossible. We conjecture that coding agents make automated hyperspecialization cheap, effective, and safe for problems with measurable performance and checkable output. This paper explores one such problem, SAT solving, by synthesizing hundreds of workload-specific SAT solvers at an average cost of \$37 each. Our specialists outperform their competition-winning, general-purpose cousins by 5$\times$ on average, and by over $10\times$ on a quarter of benchmark families. A general-purpose solver constructed from over a hundred of our prototype hyperspecialists won the SAT track at the 2026 SAT Competition.
