[Proof Complexity] MIAO seminar Thu May 28 at 15:15 CEST with Randal E. Bryant: Checkable proofs for model counting and knowledge compilation

[Jakob Nordström]

Dear all,

It is our pleasure to announce that next Thursday May 28 at 15:15 CEST (note the time!) we will have the opportunity to listen to a seminar with Randal E. Bryant from Carnegie Mellon University, who will give a talk titled "Checkable proofs for model counting and knowledge compilation". You find the abstract at the bottom of this message.

We will run this as a MIAO hybrid seminar at Lund University. Local participants are warmly welcome to seminar room E:2405 at Ole Römers väg 3, while other participants are equally warmly welcome to join virtually at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch for people who would like to hear the talk but cannot attend.

More information about the MIAO seminar series can be found at https://jakobnordstrom.se/miao-seminars/ . If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk.

Best regards,
Jakob Nordström

**********

/Thursday May 28 at 15:15 (note the time!) in seminar room E:2405, Ole Römers väg 3, Lund University, and on Zoom
*Checkable proofs for model counting and knowledge compilation
*(Randal E. Bryant, Carnegie Mellon University)
/
Automated reasoning tools, such as Boolean and Pseudo-Boolean satisfiability solvers, provide powerful capabilities that can be applied to a variety of tasks. As with any complex software system, however, these tools can have errors in their underlying algorithms and in their implementations. Certifying tools overcome this limitation by also generating checkable proofs that the answers they provide are correct.

Knowledge compilers convert Boolean formulas, given in conjunctive normal form (CNF), into representations that enable efficient evaluation of unweighted and weighted model counts, as well as a variety of other useful properties. Certifying the correctness of a knowledge compiler's output requires proving that 1) the generated formula is logically equivalent to the input formula, and 2) the generated formula satisfies the structural properties that enable efficient model counting.

Our Certified Partitioned-Operation Graph (CPOG) proof framework provides a way to encode the output of a knowledge compiler as well as a set of steps providing a checkable proof of correctness. We have developed two formally verified checkers for CPOG, one in Lean4 and the other in CakeML/HOL. In doing so, we formally verified the soundness of the frameworks.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se