Registration is now closed.

Background

Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that.

Topics

Sessions

There will be several focused sessions on AI for ATP, ITP, mathematics, physics, relations to general AI (AGI), Formal Abstracts, linguistic processing of mathematics/science, modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented. Most of the sessions will be scheduled in the afternoons to allow US participants.

Confirmed (Virtual) Participants/Speakers (TBC)

Kevin BuzzardImperial College London
Miles CranmerPrinceton University
Michael R. DouglasStony Brook University
Ben GoertzelSingularityNET
Georges GonthierINRIA
Thomas C. HalesUniversity of Pittsburgh
Sean HoldenUniversity of Cambridge
Mikoláš JanotaUniversity of Lisbon
Cezary KaliszykUniversity of Innsbruck
Peter KoepkeUniversity of Bonn
Michael KinyonUniversity of Denver
Ramana KumarDeepMind
David McAllesterToyota Technological Institute at Chicago
Tomáš MikolovCzech Technical University in Prague
Melanie MitchellSanta Fe Institute
Adam PeaseArticulate Software
Stanislas PoluOpenAI
Markus RabeGoogle Research
Fabian RuhleCERN
Stephan SchulzDHBW Stuttgart
David StanovskýCharles University
Martin SudaCzech Technical University in Prague
Josef UrbanCzech Technical University in Prague
Robert VeroffUniversity of New Mexico
Lucy Lu WangAllen Institute for AI
Yuhuai (Tony) WuUniversity of Toronto

Invited talks (to be completed)

Miles CranmerInterpretable Deep Learning for Physics via Symbolic Regression
Ben GoertzelOverview of Approaches to AGI for ATP
Michael Kinyon and Robert VeroffProver9 Assisted Proof of the Weak AIM Conjecture
Melanie MitchellWhat is AGI, and What Do We Need to Get There?
Fabian RuhleML applications to string theory
Lucy Lu WangMathematics in the Scholarly Literature

Dates (TBA)

AITP solicits contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pages (excluding references) formatted with easychair.cls. Submission is via EasyChair. Accepted contributions will be published in an informal book of abstracts for distribution at the conference. The extended abstracts are considered non-archival.

Contributed talks

Boris Shminke and Wesley Fussner. Mining counterexamples for wide-signature algebras with an Isabelle server
Martin Suda. One Year with Deepire: Lessons Learned and Where To Go Next?
Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi and Kyunghyun Cho. NaturalProofs: Mathematics meets Natural Language
Landon D. C. Elkind. Computer Verification for Historians of Philosophy
Jin Xing Lim, Barnabé Monnot, Georgios Piliouras and Shaowei Lin. (Auto)Complete this Proof: Decentralized Proof Generation via Smart Contracts
Jonathan Laurent and André Platzer. Designing a Theorem Prover for Reinforcement Learning and Neural Guidance
Yutaka Nagashima. Faster Smarter Proof by Induction in Isabelle/HOL with Definitional Quantifiers
Jakub Dakowski, Aleksandra Draszewska, Barbara Adamska, Dominika Juszczak, Łukasz Abramowicz and Robert Szymański. Creation of a modular proof assistant engine for a logic e-tutor
Adam Pease, Paulo Santos and Alexandre Rademaker. A Corpus of Spatial Reasoning Problems
Karel Chvalovský and Jan Jakubův. Characteristic Subsets of TPTP Benchmarks
Gergő Csaba Kertész, Péter Szeredi and Zsolt Zombori. Ordering Subgoals in a Backward Chaining Prover
David McAllester, Michael Douglas and Floris van Doorn. Handling Cryptomorphism in Proof Assistants and Automated Concept Formation
Albert Q. Jiang, Wenda Li, Jesse M. Han and Yuhuai Wu. LISA: Language models of ISAbelle proofs
Christian Szegedy, Markus Rabe and Henryk Michalewski. Retrieval-Augmented Proof Step Synthesis
Jelle Piepenbrock, Tom Heskes, Mikoláš Janota and Josef Urban. Learning Equational Theorem Proving
Jesse Han, Tao Xu, Stanislas Polu, Arvind Neelakantan and Alec Radford. Contrastive finetuning of generative language models for informal premise selection
Frederik Schmitt, Christopher Hahn, Jens U. Kreber, Markus N. Rabe and Bernd Finkbeiner. Deep Learning for Temporal Logics
Yuhuai Wu. Latent Action Space for Efficient Planning in Theorem Proving
Kristóf Szabó and Zsolt Zombori. Dreaming to Prove
Mikolas Janota, Antonio Morgado and Petr Vojtechovsky. Minimal Generating Sets in Magmas
Jan Hůla, David Mojžíšek and Mikolas Janota. Towards Graph Neural Networks for SMT Portfolios
Anton Lorenzen, Peter Koepke and Adrian De Lon. Dealing with Soft Types in Naproche’s Logical Backend
Mikoláš Janota, Jelle Piepenbrock and Bartosz Piotrowski. Learning SMT Enumeration
Thibault Gauthier. Synthesis of Recursive Functions from Sequences of Natural Numbers
Lasse Blaauwbroek and Herman Geuvers. ITP Automation in Practice: A User Study on Tactician
Karel Chvalovský, Jan Jakubuv, Miroslav Olšák and Josef Urban. Learning Reasoning Components
Zarathustra Goertzel, Jan Jakubuv and Josef Urban. Parental Guidance in E
Filip Bártek and Martin Suda. Project Proposal: Model-Based Optimization of Strategy Schedules
Edvard Holden and Konstantin Korovin. Representing First-order Problems for Heuristic Selection
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Cezary Kaliszyk and Josef Urban. Decision Trees for Tactic Prediction in Coq

Post-proceedings

We will consider an open call for post-proceedings in an established series of conference proceedings (LIPIcs, EPiC, JMLR) or a journal (AICom, JAR, JAIR).

Program Committee (TBC)

Jasmin Christian BlanchetteINRIA Nancy
Ulrich FurbachUniversity of Koblenz
Thibault GauthierCzech Technical University in Prague
Michael R. Douglas (co-chair)Stony Brook University
Thomas C. Hales (co-chair)University of Pittsburgh
Sean HoldenUniversity of Cambridge
Cezary Kaliszyk (co-chair)University of Innsbruck
Michael KinyonUniversity of Denver
Peter KoepkeUniversity of Bonn
Michael KohlhaseFAU Erlangen-Nürnberg
Konstantin KorovinThe University of Manchester
Ramana Kumar (co-chair)DeepMind
Adam PeaseArticulate Software
Stephan Schulz (co-chair)DHBW Stuttgart
Geoff SutcliffeUniversity of Miami
Christian SzegedyGoogle Research
Josef Urban (co-chair)Czech Technical University in Prague
Sarah WinklerUniversity of Innsbruck
Yuhuai (Tony) WuUniversity of Toronto
Zsolt ZomboriAlfréd Rényi Institute of Mathematics

Program (preliminary)



September 5
19:30 dinner


September 6
14:00-16:30 Chair: Michael Douglas video of the whole session

Welcome

Fabian Ruhle
ML applications to string theory (45m)

Miles Cranmer
Interpretable Deep Learning for Physics via Symbolic Regression (45m)

Frederik Schmitt, Christopher Hahn, Jens U. Kreber, Markus N. Rabe and Bernd Finkbeiner
Deep Learning for Temporal Logics (30m)

Jonathan Laurent and André Platzer
Designing a Theorem Prover for Reinforcement Learning and Neural Guidance (30m)

16:30-17:00 coffee break
17:00-19:10 Chair: Peter Koepke video of the whole session

Michael Kinyon and Robert Veroff
Prover9 Assisted Proof of the Weak AIM Conjecture (50m)

Jelle Piepenbrock, Tom Heskes, Mikoláš Janota and Josef Urban
Learning Equational Theorem Proving (30m)

Mikolas Janota, Antonio Morgado and Petr Vojtechovsky
Minimal Generating Sets in Magmas (20m)

Boris Shminke and Wesley Fussner
Mining counterexamples for wide-signature algebras with an Isabelle server (30m)

19:30 dinner


September 7
14:00-16:10 Chair: Stephan Schulz video of the whole session

Martin Suda
One Year with Deepire: Lessons Learned and Where To Go Next? (40m)

Zarathustra Goertzel, Jan Jakubuv and Josef Urban
Parental Guidance in E (30m)

Gergő Csaba Kertész, Péter Szeredi and Zsolt Zombori
Ordering Subgoals in a Backward Chaining Prover (20m)

Filip Bártek and Martin Suda
Project Proposal: Model-Based Optimization of Strategy Schedules (20m)

Yutaka Nagashima
Faster Smarter Proof by Induction in Isabelle/HOL with Definitional Quantifiers (20m)

16:30-17:00 coffee break
17:00-19:35 Chair: Christian Szegedy video of the whole session

Lucy Lu Wang
Mathematics in the Scholarly Literature (45m)

Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi and Kyunghyun Cho
NaturalProofs: Mathematics meets Natural Language (30m)

Jesse Han, Tao Xu, Stanislas Polu, Arvind Neelakantan and Alec Radford
Contrastive finetuning of generative language models for informal premise selection (30m)

Anton Lorenzen, Peter Koepke and Adrian De Lon
Dealing with Soft Types in Naproche’s Logical Backend (30m)

David McAllester, Michael Douglas and Floris van Doorn
Handling Cryptomorphism in Proof Assistants and Automated Concept Formation (20m)

19:35 dinner
September 8
14:00-16:30 Chair: Martin Suda video of the whole day

Albert Q. Jiang, Wenda Li, Jesse M. Han and Yuhuai Wu
LISA: Language models of ISAbelle proofs (30m)

Kristóf Szabó and Zsolt Zombori
Dreaming to Prove (30m)

Yuhuai Wu and Minchao Wu
Latent Action Space for Efficient Planning in Theorem Proving (30m)

Kunhao Zheng, Jesse Michael Han, and Stanislas Polu
miniF2F: a cross-system benchmark for formal Olympiad-level mathematics (15m)

Miroslav Olšák
Project proposal: Puzzle games and reasoning (15m)

Thibault Gauthier
Synthesis of Recursive Functions from Sequences of Natural Numbers (30m)

16:30-17:00 coffee break
17:00-19:30 Chair: Josef Urban video of the whole day

Ben Goertzel
Overview of Approaches to AGI for ATP (45m)

Melanie Mitchell
What is AGI, and What Do We Need to Get There? (45m)

Panel Discussion (B. Goertzel, M. Mitchell, T. Mikolov, S. Schulz, C. Szegedy, T. Gauthier)
AGI and AI for TP/Math/Science (60m)

19:30 dinner


September 9
14:00-16:30 Chair: Cezary Kaliszyk video of the whole day

Edvard Holden and Konstantin Korovin
Representing First-order Problems for Heuristic Selection (30m)

Karel Chvalovský and Jan Jakubův
Characteristic Subsets of TPTP Benchmarks (20m)

Jan Hůla, David Mojžíšek and Mikolas Janota
Towards Graph Neural Networks for SMT Portfolios (30m)

Mikoláš Janota, Jelle Piepenbrock and Bartosz Piotrowski
Learning SMT Enumeration (30m)

Jin Xing Lim, Barnabé Monnot, Georgios Piliouras and Shaowei Lin
(Auto)Complete this Proof: Decentralized Proof Generation via Smart Contracts (20m)

Lasse Blaauwbroek and Herman Geuvers
ITP Automation in Practice: A User Study on Tactician (20m)

16:30-17:00 coffee break
17:00-19:25 Chair: Mikolas Janota video of the whole day

Adam Pease, Paulo Santos and Alexandre Rademaker
A Corpus of Spatial Reasoning Problems (30m)

Jakub Dakowski, Aleksandra Draszewska, Barbara Adamska, Dominika Juszczak, Łukasz Abramowicz and Robert Szymański
Creation of a modular proof assistant engine for a logic e-tutor (25m)

Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Cezary Kaliszyk and Josef Urban
Decision Trees for Tactic Prediction in Coq (30m)

Karel Chvalovský, Jan Jakubuv, Miroslav Olšák and Josef Urban
Learning Reasoning Components (30m)

19:30 dinner


September 10
10:00-12:30 Discussions in groups
12:30-14:00 lunch and departure from the center


September 11 (optional for participants staying in Aussois)
10:00-16:30 Excursion/Discussions in groups


Picture from the conference

Pictures from the previous conferences

Location, Prices and Further Local Information

The conference will take place from September 5 to September 10 2021 in the CNRS Paul-Langevin Conference Center located in the mountain village of Aussois in Savoy. Dominated by the "Dent Parrachée", one of the highest peaks of La Vanoise, Aussois is located on a sunny plateau at 1500 m altitude, offering a magnificent panorama of the surrounding mountains and a direct access to the downhill ski slopes or cross country slopes in winter. The total price for accommodation, food and registration for the five days will be around 600 EUR. Online participation will be most likely for free but may be limited to relevant participants.

Arrival/Departure:

Aussois is less than 2h from the airports of Lyon, Geneve, Chambery, Annecy, Grenoble and Turin. There are trains and buses to Modane from these airports. Aussois is 8km from the Modane TGV station with direct trains from/to Paris. We will organize a bus for the participants from there to Aussois. Further buses to these airports / station can be found here and it is easy to get a taxi from Modane to Aussois and back.

The first meal is dinner on September 5 and the last meal is lunch on Friday September 10 . There will be a full morning session on Friday. The planned departure of our bus from Modane to Aussois is at around 19:15 pm on Sunday, September 5 . The bus will wait for the TGV train from Paris arriving to Modane at 18:46. The train starts at 14:40 in Paris Gare de Lyon, and it also stops in Lyon-St Exupery at 16:38 and in Chambery-Challes-E at 17:44. The distance from Modane to Aussois is 8km and there are taxis and alternative buses.

We have not yet set the time for the departure of the bus after lunch on September 10 . This will be optimized based on your departure flights during the conference (but taking taxi back to Modane is easy). The center will close after our last session on Friday. If you want to stay for the weekend, the center recommends Hotel des Mottets which is 5 minutes from the center and their prices are very reasonable: https://www.hotel-lesmottets.com/ . If you registered, please fill in this Google form to indicate if you plan to take our bus to Modane, your food preferences, whom you want to share a room with, if you plan to stay longer, etc.