Mechanically Proving Guarantees of Generalized Heuristics: First Results and Ongoing Work

Abdulaziz, Mohammad and Pommerening, Florian and Corrêa, Augusto B.. (2022) Mechanically Proving Guarantees of Generalized Heuristics: First Results and Ongoing Work. ICAPS 2022 Workshop on Heuristics and Search for Domain-independent Planning (HSDIP 2022). Proceedings.

[img] PDF - Submitted Version

Official URL: https://edoc.unibas.ch/93498/

Downloads: Statistics Overview


The goal of generalized planning is to find a solution that works for all tasks of a specific planning domain. Ideally, this solution is also efficient (i.e., polynomial) in all tasks. One possible approach is to learn such a solution from training examples and then prove that this generalizes for any given task. However, such proofs are usually pen-and-paper proofs written by a human. In our paper, we aim at automating these proofs so we can use a theorem prover to show that a solution generalizes for any task. Furthermore, we want to prove that this generalization works while still preserving efficiency. Our focus is on generalized potential heuristics encoding tiered measures of progress, which can be proven to lead to a find in a polynomial number of steps in all tasks of a domain. We show our ongoing work in this direction using the interactive theorem prover Isabelle/HOL. We illustrate the key aspects of our implementation using the Miconic domain and then discuss possible obstacles and challenges to fully automating this pipeline.
Faculties and Departments:05 Faculty of Science > Departement Mathematik und Informatik > Informatik > Artificial Intelligence (Helmert)
UniBasel Contributors:Pommerening, Florian and Blaas Corrêa, Augusto
Item Type:Other
Publisher:AAAI Press
Note:Publication type according to Uni Basel Research Database: Other publications
edoc DOI:
Last Modified:08 May 2023 12:09
Deposited On:08 May 2023 12:09

Repository Staff Only: item control page