Quantifier Instantiations: To Mimic or To Revolt?

TL;DR

This paper presents a novel SMT quantifier instantiation method that dynamically learns from existing techniques using probabilistic grammars, enhancing diversity and effectiveness in quantifier reasoning.

Contribution

It introduces a dynamic, probabilistic approach that mimics and diversifies instantiations by learning from multiple existing techniques during solving.

Findings

Improves quantifier instantiation by learning from past techniques.

Balances exploitation and exploration through probabilistic inversion.

Enhances SMT solver performance on quantified formulas.

Abstract

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.