Arrow Research search

Author name cluster

Mohammad Abdulaziz

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

11 papers
2 author rows

Possible papers

11

AAAI Conference 2025 Conference Paper

Formally Verified Approximate Policy Iteration

  • Maximilian Schäffeler
  • Mohammad Abdulaziz

We present a methodology based on interactive theorem proving that facilitates the development of verified implementations of algorithms for solving factored Markov Decision Processes. As a case study, we formally verify an algorithm for approximate policy iteration in the proof assistant Isabelle/HOL. We show how the verified algorithm can be refined to an executable, verified implementation. Our evaluation on benchmark problems shows that it is practical. As part of the development, we build verified software to certify linear programming solutions. We discuss the verification process and the modifications we made to the algorithm during formalization.

PDF Details DOI

AAAI Conference 2024 Conference Paper

Interactive Theorem Provers: Applications in AI, Opportunities, and Challenges

  • Mohammad Abdulaziz

Interactive theorem provers (ITPs) are computer programs in which axioms and a conjecture are stated in a formal language, and a user provides the ITP with relatively high-level steps of a formal proof for the conjecture. Then, by invoking automated theorem provers, the ITP tries to generate low-level steps that fill the gaps between the steps provided by the user, thus forming a complete formal proof of the conjecture. The ITP also checks the entire formal proof against the axioms, thus confirming the soundness of all derivations in the formal proof. In this talk, I will discuss the existing opportunities and potential benefits to applying ITPs to reason about and verify AI concepts, algorithms, and software. I will also discuss the challenges we have to being able to apply ITPs in AI and reap those benefits. I will do so by discussing a number of my previous projects on the application of ITPs to different AI concepts, algorithms, and software systems. These projects span different areas of planning (classical planning, temporal planning, and planning under uncertainty) as well as algorithms with applications in algorithmic game theory, like general graph matching and online matching.

PDF Details DOI

AAAI Conference 2023 Conference Paper

Formally Verified SAT-Based AI Planning

  • Mohammad Abdulaziz
  • Friedrich Kurz

We present an executable formally verified SAT encoding of ground classical AI planning problems. We use the theorem prover Isabelle/HOL to perform the verification. We experimentally test the verified encoding and show that it can be used for reasonably sized standard planning benchmarks. We also use it as a reference to test a state-of-the-art SAT-based planner, showing that it sometimes falsely claims that problems have no solutions of certain lengths.

PDF Details DOI

AAAI Conference 2023 Conference Paper

Formally Verified Solution Methods for Markov Decision Processes

  • Maximilian Schäffeler
  • Mohammad Abdulaziz

We formally verify executable algorithms for solving Markov decision processes (MDPs) in the interactive theorem prover Isabelle/HOL. We build on existing formalizations of probability theory to analyze the expected total reward criterion on finite and infinite-horizon problems. Our developments formalize the Bellman equation and give conditions under which optimal policies exist. Based on this analysis, we verify dynamic programming algorithms to solve tabular MDPs. We evaluate the formally verified implementations experimentally on standard problems, compare them with state-of-the-art systems, and show that they are practical.

PDF Details DOI

AAAI Conference 2022 Conference Paper

Formal Semantics and Formally Verified Validation for Temporal Planning

  • Mohammad Abdulaziz
  • Lukas Koller

We present a simple and concise semantics for temporal planning. Our semantics are developed and formalised in the logic of the interactive theorem prover Isabelle/HOL. We derive from those semantics a validation algorithm for temporal planning and show, using a formal proof in Isabelle/HOL, that this validation algorithm implements our semantics. We experimentally evaluate our verified validation algorithm and show that it is practical.

PDF Details

AAAI Conference 2021 Conference Paper

Computing Plan-Length Bounds Using Lengths of Longest Paths

  • Mohammad Abdulaziz
  • Dominik Berger

We devise a method to exactly compute the length of the longest simple path in factored state spaces, like state spaces encountered in classical planning. Although the complexity of this problem is NEXP-hard, we show that our method can be used to compute practically useful upper-bounds on lengths of plans. We show that the computed upper-bounds are significantly (in many cases, orders of magnitude) better than bounds produced by previous bounding techniques and that they can be used to improve the SAT-based planning.

PDF Details

SoCS Conference 2020 Conference Paper

Computing Plan-Length Bounds Using Lengths of Longest Paths

  • Mohammad Abdulaziz
  • Dominik Berger

We devise a method to exactly compute the length of the longest simple path in factored state spaces, like state spaces encountered in classical planning. Although the complexity of this problem is NEXP-Hard, we show that our method can be used to compute practically useful upper-bounds on lengths of plans. We show that the computed upper-bounds are significantly (in many cases, orders of magnitude) better than bounds produced by previous bounding techniques and that they can be used to improve the SAT-based planning.

Details

AAAI Conference 2019 Conference Paper

Plan-Length Bounds: Beyond 1-Way Dependency

  • Mohammad Abdulaziz

We consider the problem of compositionally computing upper bounds on lengths of plans. Following existing work, our approach is based on a decomposition of state-variable dependency graphs (a. k. a. causal graphs). Tight bounds have been demonstrated previously for problems where key dependencies flow in a single direction—i. e. manipulating variable v1 can disturb the ability to manipulate v2 and not vice versa. We develop a more general bounding approach which allows us to compute useful bounds where dependency flows in both directions. Our approach is practically most useful when combined with earlier approaches, where the computed bounds are substantially improved in a relatively broad variety of problems. When combined with an existing planning procedure, the improved bounds yield coverage improvements for both solvable and unsolvable planning problems.

PDF Details

MFCS Conference 2019 Conference Paper

Trustworthy Graph Algorithms (Invited Talk)

  • Mohammad Abdulaziz
  • Kurt Mehlhorn
  • Tobias Nipkow

The goal of the LEDA project was to build an easy-to-use and extendable library of correct and efficient data structures, graph algorithms and geometric algorithms. We report on the use of formal program verification to achieve an even higher level of trustworthiness. Specifically, we report on an ongoing and largely finished verification of the blossom-shrinking algorithm for maximum cardinality matching.

Details

ICAPS Conference 2017 Conference Paper

A State-Space Acyclicity Property for Exponentially Tighter Plan Length Bounds

  • Mohammad Abdulaziz
  • Charles Gretton
  • Michael Norrish

We investigate compositional bounding of transition system diameters, with application in bounding the lengths of plans. We establish usefully-tight bounds by exploiting acyclicity in state-spaces. We provide mechanised proofs in HOL4 of the validity of our approach. Evaluating our bounds in a range of benchmarks, we demonstrate exponentially tighter upper bounds compared to existing methods. Treating both solvable and unsolvable benchmark problems, we also demonstrate the utility of our bounds in boosting planner performance. We enhance an existing planning procedure to use our bounds, and demonstrate significant coverage improvements, both compared to the base planner, and also in comparisons with state-of-the-art systems.

Details

IJCAI Conference 2015 Conference Paper

Exploiting Symmetries by Planning for a Descriptive Quotient

  • Mohammad Abdulaziz
  • Michael Norrish
  • Charles Gretton

We eliminate symmetry from a problem before searching for a plan. The planning problem with symmetries is decomposed into a set of isomorphic subproblems. One plan is computed for a small planning problem posed by a descriptive quotient, a description of any such subproblem. A concrete plan is synthesized by concatenating instantiations of that one plan for each subproblem. Our approach is sound.

PDF Details