让SMT求解器学会模仿和创新，自动优化量化公式求解
Quantifier Instantiations: To Mimic or To Revolt?
- 用概率上下文无关语法学习已有成功实例的生成模式
- 能复制有效实例，也能反转概率探索新解法
- 适合做逻辑推理与自动化验证的研究者
量化公式给满足模理论（SMT）求解器带来显著挑战，因其固有的不可判定性。现有实例化技术如e-matching、语法引导、基于模型、冲突驱动及枚举方法常相互补充。本文提出一种新方法，在求解过程中动态学习这些技术的经验。将观察到的实例视为潜在语言的样本，利用概率上下文无关语法生成相似新项。该方法不仅能模仿过往成功的实例，还可通过可选地反转学习到的项概率来探索多样性，旨在平衡量化推理中的利用与探索。
原文摘要 · Abstract (English)
Quantified formulas pose a significant challenge for Satisfiability Modulo Theories (SMT) solvers due to their inherent undecidability. Existing instantiation techniques, such as e-matching, syntax-guided, model-based, conflict-based, and enumerative methods, often complement each other. This paper introduces a novel instantiation approach that dynamically learns from these techniques during solving. By treating observed instantiations as samples from a latent language, we use probabilistic context-free grammars to generate new, similar terms. Our method not only mimics successful past instantiations but also explores diversity by optionally inverting learned term probabilities, aiming to balance exploitation and exploration in quantifier reasoning.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。