Machine-learning-based algorithm selection has demonstrated improvements in SMT solving by exploiting solver complementarity across diverse problem families. Existing SMT algorithm selectors primarily rely on handcrafted syntactic features to represent problem instances for machine-learning models. In this work, we explore whether high-level natural-language descriptions of SMT instances can provide additional useful information. We present SMT-Select, an SMT algorithm selection framework that combines traditional syntactic features with semantic embeddings derived from natural-language descriptions using pretrained transformer models. It further improves upon the algorithm selection pipeline of the state-of-the-art selector MachSMT. Evaluated on SMT-COMP 2024 benchmarks across 9 logics, SMT-Select achieves improved performance in 7 logics when description-based features are added, while performance degrades in the remaining two logics, where the SMT-LIB descriptions exhibit very limited variability. To address this limitation, we outline future work on LLM-based agents for generating higher-quality SMT instance descriptions, supported by preliminary demos.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Learning SMT Algorithm Selection with High-Level Natural-Language Descriptions

  • Zhengyang Lu,
  • Paul Sarnighausen-Cahn,
  • Jiahao Chen,
  • Arie Gurfinkel,
  • Florin Manea,
  • Vijay Ganesh

摘要

Machine-learning-based algorithm selection has demonstrated improvements in SMT solving by exploiting solver complementarity across diverse problem families. Existing SMT algorithm selectors primarily rely on handcrafted syntactic features to represent problem instances for machine-learning models. In this work, we explore whether high-level natural-language descriptions of SMT instances can provide additional useful information. We present SMT-Select, an SMT algorithm selection framework that combines traditional syntactic features with semantic embeddings derived from natural-language descriptions using pretrained transformer models. It further improves upon the algorithm selection pipeline of the state-of-the-art selector MachSMT. Evaluated on SMT-COMP 2024 benchmarks across 9 logics, SMT-Select achieves improved performance in 7 logics when description-based features are added, while performance degrades in the remaining two logics, where the SMT-LIB descriptions exhibit very limited variability. To address this limitation, we outline future work on LLM-based agents for generating higher-quality SMT instance descriptions, supported by preliminary demos.