Quantifier Instantiations: To Mimic or To Revolt?
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918127246245888 |
|---|---|
| author | Jakubův, Jan Janota, Mikoláš |
| author_facet | Jakubův, Jan Janota, Mikoláš |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_13811 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Quantifier Instantiations: To Mimic or To Revolt? Jakubův, Jan Janota, Mikoláš Artificial Intelligence Logic in Computer Science 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. |
| title | Quantifier Instantiations: To Mimic or To Revolt? |
| topic | Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2508.13811 |