AITP 2022: AI and Theorem Proving in Aussois
In September 2022, I attended the 7th Conference on Artificial Intelligence and Theorem Proving (AITP 2022) in Aussois, France. I contributed an extended abstract and gave a talk on our work exploring graph representations and graph neural networks for Constrained Horn Clauses.
Artificial Intelligence and Theorem Proving
AITP 2022 took place from September 4–9, 2022, both in Aussois and online. The in-person meeting was hosted by the CNRS Paul-Langevin Conference Center, surrounded by the mountains of the French Alps.
The conference brought together researchers working at the intersection of artificial intelligence, automated and interactive theorem proving, and formal mathematics. Its programme explored how machine learning, large-scale data, formal reasoning, and proof systems can complement one another—from neural guidance for theorem provers and formalization of mathematics to natural-language reasoning and the verification of AI systems. The discussion-oriented format made it a particularly interesting setting for exchanging developing ideas across these closely connected communities.
My Abstract and Talk
Together with Philipp Rümmer and Marc Brockschmidt, I submitted the extended abstract “Exploring Representation of Horn Clauses using GNNs.” The contribution studied how Constrained Horn Clauses (CHCs) could be encoded as graphs for machine learning. We examined representations emphasizing either syntactic structure or program control and data flow, and investigated graph neural network architectures capable of learning from them.
The abstract was accepted for AITP’s informal, non-archival book of abstracts, and I presented the work in a 25-minute contributed talk on September 5. The extended abstract, official conference version, and presentation slides are available online.
Moments from Aussois
