论文标题
符号执行 +模型计数 +熵最大化=自动搜索合成
Symbolic Execution + Model Counting + Entropy Maximization = Automatic Search Synthesis
论文作者
论文摘要
我们提出了一种自动合成步骤以解决搜索问题的方法。给定搜索问题的规范，我们的方法使用符号执行来分析规范，以提取一组对问题进行建模的约束。这些约束用于称为模型计数的过程，该过程被利用以计算概率分布，将搜索步骤与未知目标的谓词相关联。概率分布函数确定了基于香农熵的信息增益目标函数，当最大化时，该功能将产生搜索的下一个最佳步骤。我们证明我们的算法会收敛到正确的解决方案，并讨论计算复杂性问题。我们实施了一种特定的域语言，在其中编写搜索问题规格，从而使我们的静态分析阶段。我们的实验证明了我们的方法对受软件安全性，计算几何形状，AI的AI和用户偏好排名的领域启发的一组搜索问题案例研究的有效性。
We present a method of automatically synthesizing steps to solve search problems. Given a specification of a search problem, our approach uses symbolic execution to analyze the specification in order to extract a set of constraints which model the problem. These constraints are used in a process called model counting, which is leveraged to compute probability distributions relating search steps to predicates about an unknown target. The probability distribution functions determine an information gain objective function based on Shannon entropy, which, when maximized, yields the next optimal step of the search. We prove that our algorithm converges to a correct solution, and discuss computational complexity issues. We implemented a domain specific language in which to write search problem specifications, enabling our static analysis phase. Our experiments demonstrate the effectiveness of our approach on a set of search problem case studies inspired by the domains of software security, computational geometry, AI for games, and user preference ranking.
