量子科技中心_量科网

随着量子程序日益受到关注，确保其正确性成为一项基础性挑战。虽然约束求解技术可以克服传统测试与验证方法的某些局限性，但这类技术在量子程序领域的应用尚未得到充分探索。为解决这一空白，该研究团队提出了首个量子约束求解器QSolver。该工具提供了结构化框架来处理五种量子约束类型，并集成自动化断言生成模块以验证量子态。QSolver将量子程序和多时刻约束转化为符号化表示，利用SMT求解器获取满足这些约束的量子态。为验证生成输入态的正确性，该系统能自动生成与每个约束对应的断言程序。实验结果表明，QSolver能高效处理常用量子门，并在不同规模的量子程序中展现出良好的可扩展性。