一句话：提出 LasT，用重训练-微调与数据增强驱动 LLM 生成 SMT 公式来模糊测试求解器，发现 65 个真实缺陷。
SMT 求解器广泛用于软件验证、测试生成和程序合成，但其内部缺陷会导致严重后果，而如何生成有效测试公式仍是难题。本文提出将大型语言模型用于 SMT 公式生成，以模糊测试求解器，并设计重训练-微调流水线，结合数据增强提升生成效果。作者实现工具 LasT，对 Z3、cvc5 和 Bitwuzla 等先进求解器进行大规模测试。结果显示，LasT 已发现 65 个真实缺陷，其中 45 个被开发者修复，表明 LLM 可有效增强 SMT 求解器验证。
SMT solvers are utilized to check the satisfiability of logic formulas and have been applied in various crucial domains, including software verification, test case generation, and program synthesis. However, bugs hidden in SMT solvers can lead to severe consequences, causing erroneous results in these domains. Therefore, ensuring the reliability and robustness of SMT solvers is of critical importance. Despite several testing approaches proposed for SMT solvers, generating effective test formulas to comprehensively test SMT solvers remains a challenge. To address this challenge, in this study, we propose to port large language models (LLMs) to generate SMT formulas for fuzzing solvers. Specifically, the study presents a novel retrain-finetune pipeline to unleash the potential of language models to generate effective SMT formulas and improve their generation performance through data augmentation. We implemented our approach as a practical fuzzing tool, named LasT,and then extensively tested the state-of-the-art SMT solvers, namely Z3, cvc5, and Bitwuzla. To date, Last has successfully uncovered 65 genuine bugs for the solvers, of which 45 have been fixed by the developers.
@inproceedings{SunYWWJZ23,
title = {SMT Solver Validation Empowered by Large Pre-Trained Language Models},
author = {Maolin Sun and Yibiao Yang and Yang Wang and Ming Wen and Haoxiang Jia and Yuming Zhou},
booktitle = {ASE},
year = {2023},
doi = {10.1109/ase56229.2023.00180}
}