AIAI Seminar - 5 December 2022 - Talks by Ameer Saadat-Yadzi, Richard Schmoetten and Paulius Dilkas

Speaker:        Ameer Saadat-Yadzi

Title:

Argument Understanding through Commonsense Reasoning

Abstract:

In online settings, people often make arguments to justify a position they hold, persuade others of a point of view or to reach new levels of collective understanding. In order to engage with the vast number of opinions that exist on the web today, powerful tools are needed that are capable of identifying arguments, breaking down their structure and filling in implicit information. My work focuses mainly on the last two problems: (i) What is the underlying structure of the argument? And, (ii) what knowledge has the author of the argument assumed and therefore left implicit? Often, the knowledge that is left out is assumed to be obvious and shared by both the speaker and the audience. By leveraging commonsense knowledge graphs, my work seeks to expose these implicit assumptions, and in doing so, improve the ability of automated methods to determine argument components, their structure, and their relationships.

Speaker:       Richard Schmoetten

Title:

Lie groups in Higher Order Logic (Isabelle/HOL)

Abstract:

Lie groups are elementary to the study of continuous transformations, and form a central mathematical tool for myriad modern theories of physics. This talk introduces our continuing efforts towards obtaining a formalisation of Lie groups in the proof assistant Isabelle/HOL. Beyond the benefits of formal verification, this work also presents an opportunity to explore different ways of reasoning about complex mathematical structures inside HOL.

Speaker:       Paulius Dilkas

Title:           

Generating Random Instances of Weighted Model Counting: An Empirical Analysis with Varying Primal Treewidth

Abstract:

Weighted model counting (WMC) is an extension of propositional model counting with applications to probabilistic inference and other areas of artificial intelligence. In recent experiments, WMC algorithms perform similarly overall but with significant differences on specific subsets of benchmarks. A good understanding of the differences in the performance of algorithms requires identifying key characteristics that favour some algorithms over others. In this work, we introduce a random model for WMC instances with a parameter that influences primal treewidth—the parameter most commonly used to characterise the difficulty of an instance. We then use this model to experimentally compare the performance of many WMC algorithms. Using these random instances, we show that the easy-hard-easy pattern is different for algorithms based on dynamic programming and algebraic decision diagrams than for all other solvers. We also show how all WMC algorithms scale exponentially with respect to primal treewidth and how this scalability varies across algorithms and densities. Finally, we combine insights from experiments involving both random and competition instances to determine how the best-performing WMC algorithm varies depending on clause density and primal treewidth.