发表机构
Czech Technical University（捷克理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出完全由 vibe-coding 生成并调优的 SMT 求解器 primo，在 QF-LRA 上超越 SMT-COMP 2026 冠军，证明该开发方式对自动推理工具前景广阔。
AI 中文摘要
本文介绍了 SMT 求解器 primo，它完全通过 vibe-coding 生成并进行参数调优，在线性实数算术（QF-LRA）上取得了最先进的结果。primo 的性能是通过系统的文献调研、反复的性能分析和参数调优实现的。由此产生的求解器优于 SMT-COMP~2026 中 QF-LRA 赛道的冠军。这证实了自动推理工具的 vibe-coding 将使我们能够在未来取得巨大进步。
英文摘要
This paper presents the SMT solver primo, which is fully vibe-coded and then parameter-tuned, achieving state-of-the-art results on linear real arithmetic (QF-LRA). The performance of primo is achieved by a systematic literature survey, repeated profiling, and parameter tuning. The resulting solver outperforms the winner of the QF-LRA track of SMT-COMP~2026. This confirms that vibe-coding of automated reasoning tools will enable us to make great strides in the future.
