反例引导的归纳优化
人工智能
2017-04-13 v1 计算机科学中的逻辑
摘要
本文描述了一种基于可满足性模理论（SMT）求解器的反例引导归纳优化（CEGIO）方法的三种变体。具体而言，CEGIO依赖于迭代执行来约束验证过程，以便基于从SMT求解器提取的反例执行归纳泛化。CEGIO能够成功优化广泛的函数，包括基于SMT求解器的非线性和非凸优化问题，其中反例提供的数据被用于引导验证引擎，从而缩减优化域。本文算法使用一组通常用于评估优化技术的大型基准测试集进行评估。实验结果显示了所提算法的效率和有效性，其在所有评估的基准测试中找到最优解，而传统技术通常陷入局部极小值。
引用
@article{arxiv.1704.03738,
title = {Counterexample Guided Inductive Optimization},
author = {Rodrigo F. Araujo and Higo F. Albuquerque and Iury V. de Bessa and Lucas C. Cordeiro and Joao Edgar C. Filho},
journal= {arXiv preprint arXiv:1704.03738},
year = {2017}
}