Formally Verified Approximate Policy Iteration
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917690517487616 |
|---|---|
| author | Schäffeler, Maximilian Abdulaziz, Mohammad |
| author_facet | Schäffeler, Maximilian Abdulaziz, Mohammad |
| contents | We formally verify an algorithm for approximate policy iteration on Factored Markov Decision Processes using the interactive theorem prover Isabelle/HOL. Next, we show how the formalized algorithm can be refined to an executable, verified implementation. The implementation is evaluated on benchmark problems to show its practicability. As part of the refinement, we develop verified software to certify Linear Programming solutions. The algorithm builds on a diverse library of formalized mathematics and pushes existing methodologies for interactive theorem provers to the limits. We discuss the process of the verification project and the modifications to the algorithm needed for formal verification. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_07340 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Formally Verified Approximate Policy Iteration Schäffeler, Maximilian Abdulaziz, Mohammad Artificial Intelligence Logic in Computer Science We formally verify an algorithm for approximate policy iteration on Factored Markov Decision Processes using the interactive theorem prover Isabelle/HOL. Next, we show how the formalized algorithm can be refined to an executable, verified implementation. The implementation is evaluated on benchmark problems to show its practicability. As part of the refinement, we develop verified software to certify Linear Programming solutions. The algorithm builds on a diverse library of formalized mathematics and pushes existing methodologies for interactive theorem provers to the limits. We discuss the process of the verification project and the modifications to the algorithm needed for formal verification. |
| title | Formally Verified Approximate Policy Iteration |
| topic | Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2406.07340 |