Formal Primal-Dual Algorithm Analysis
Mohammad Abdulaziz, Thomas Ammer, Christoph Madlener
TL;DR
This paper discusses developing a formal framework in Isabelle/HOL for primal-dual algorithm analysis, covering classical and modern algorithms like Hungarian and Adwords.
Contribution
It introduces a formalisation framework and library for primal-dual algorithms, enabling rigorous proofs in Isabelle/HOL.
Findings
Formalisation of the Hungarian Method in Isabelle/HOL
Formalisation of the Adwords algorithm in Isabelle/HOL
A unified framework for primal-dual algorithm analysis
Abstract
We present an ongoing effort to build a framework and a library in Isabelle/HOL for formalising primal-dual arguments for the analysis of algorithms. We discuss a number of example formalisations from the theory of matching algorithms, covering classical algorithms like the Hungarian Method, widely considered the first primal-dual algorithm, and modern algorithms like the Adwords algorithm, which models the assignment of search queries to advertisers in the context of search engines.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.