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
- AI and big-data methods in theorem proving and mathematics
- Collaboration between automated and interactive theorem proving, in particular their AI/ML aspects
- Common-sense reasoning and reasoning in science
- Alignment and joint processing of formal, semi-formal, and informal libraries, Formal Abstracts
- Methods for large-scale computer understanding of mathematics and science
- Combinations of linguistic/learning-based and semantic/reasoning methods
- Formal verification of AI and machine learning algorithms, explainable AI
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 Buzzard | Imperial College London |
| Miles Cranmer | Princeton University |
| Michael R. Douglas | Stony Brook University |
| Ben Goertzel | SingularityNET |
| Georges Gonthier | INRIA |
| Thomas C. Hales | University of Pittsburgh |
| Sean Holden | University of Cambridge |
| Mikoláš Janota | University of Lisbon |
| Cezary Kaliszyk | University of Innsbruck |
| Peter Koepke | University of Bonn |
| Michael Kinyon | University of Denver |
| Ramana Kumar | DeepMind |
| David McAllester | Toyota Technological Institute at Chicago |
| Tomáš Mikolov | Czech Technical University in Prague |
| Melanie Mitchell | Santa Fe Institute |
| Adam Pease | Articulate Software |
| Stanislas Polu | OpenAI |
| Markus Rabe | Google Research |
| Fabian Ruhle | CERN |
| Stephan Schulz | DHBW Stuttgart |
| David Stanovský | Charles University |
| Martin Suda | Czech Technical University in Prague |
| Josef Urban | Czech Technical University in Prague |
| Robert Veroff | University of New Mexico |
| Lucy Lu Wang | Allen Institute for AI |
| Yuhuai (Tony) Wu | University of Toronto |
Invited talks (to be completed)
| Miles Cranmer | Interpretable Deep Learning for Physics via Symbolic Regression |
| Ben Goertzel | Overview of Approaches to AGI for ATP |
| Michael Kinyon and Robert Veroff | Prover9 Assisted Proof of the Weak AIM Conjecture |
| Melanie Mitchell | What is AGI, and What Do We Need to Get There? |
| Fabian Ruhle | ML applications to string theory |
| Lucy Lu Wang | Mathematics in the Scholarly Literature |
Dates (TBA)
- Submission deadline:
May 5Extended: May 12, 2021 - Author notification: June 20
- Conference registration: TBA
- Camera-ready versions: TBA
- Conference: September 5-11, 2021
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 |
Informal proceedings
The (extended) abstracts of all the invited and contributed talks are now available online.
Program Committee (TBC)
| Jasmin Christian Blanchette | INRIA Nancy |
| Ulrich Furbach | University of Koblenz |
| Thibault Gauthier | Czech Technical University in Prague |
| Michael R. Douglas (co-chair) | Stony Brook University |
| Thomas C. Hales (co-chair) | University of Pittsburgh |
| Sean Holden | University of Cambridge |
| Cezary Kaliszyk (co-chair) | University of Innsbruck |
| Michael Kinyon | University of Denver |
| Peter Koepke | University of Bonn |
| Michael Kohlhase | FAU Erlangen-Nürnberg |
| Konstantin Korovin | The University of Manchester |
| Ramana Kumar (co-chair) | DeepMind |
| Adam Pease | Articulate Software |
| Stephan Schulz (co-chair) | DHBW Stuttgart |
| Geoff Sutcliffe | University of Miami |
| Christian Szegedy | Google Research |
| Josef Urban (co-chair) | Czech Technical University in Prague |
| Sarah Winkler | University of Innsbruck |
| Yuhuai (Tony) Wu | University of Toronto |
| Zsolt Zombori | Alfré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 |
| 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.