July 2 update: The September real-world date for the conference is still the default. Since the situation changes, we will do the next evaluation only in mid-August. A combination of a real-world meeting with some online talks is an option.

March 10 update: Due to the Coronavirus travel bans, the conference has been moved to September 13-19, 2020.

The registration is now closed and the list of participants has been fixed. It was done via Easychair. Please do not provide any payment data by phone/email - it is very likely a scam!

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 and mathematics, modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented.

Confirmed Participants/Speakers (TBC)

João AraújoUniversidade Nova de Lisboa
Kevin BuzzardImperial College London
Michael R. Douglas*Stony Brook University
Vlad FiroiuDeepMind
Ben GoertzelSingularityNET
Georges GonthierINRIA
Thomas C. HalesUniversity of Pittsburgh
John HarrisonAmazon
Sean HoldenUniversity of Cambridge
Mikoláš JanotaUniversity of Lisbon
Michael KinyonUniversity of Denver
Joao Marques SilvaANITI, University of Toulouse
David McAllesterToyota Technological Institute at Chicago
Tomáš MikolovFacebook AI Research
Lawrence C. PaulsonUniversity of Cambridge
Alison PeaseUniversity of Dundee
J.D. PhillipsNorthern Michigan University
Markus RabeGoogle Research
Stephan SchulzDHBW Stuttgart
Daniel SelsamMicrosoft Research
David StanovskýCharles University in Prague
Martin SudaCzech Technical University in Prague
Christian SzegedyGoogle Research
Tuyen Trung TruongUniversity of Oslo
Robert VeroffUniversity of New Mexico
Petr VojtěchovskýUniversity of Denver
*: To be confirmed.

Invited talks (to be completed)

François Charton and Guillaume LampleDeep learning for symbolic mathematics
Michael DouglasFormal/Symbolic/Numerical Computational Methods
Ben GoertzelWhat Logic to Use for Hypothetical Scientific and Common-sense Inference?
Lawrence C. PaulsonTBA
Markus RabeTBA
Daniel SelsamThe IMO Grand Challenge

Dates

AITP solicits contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pages formatted with easychair.cls. Submission is via EasyChair. Accepted contributions will be published in an informal book of abstracts for distribution at the conference.

Contributed talks

Kshitij Bansal and Christian Szegedy: Learning alignment between formal & informal mathematics
Filip Bártek and Martin Suda: Project Proposal: Machine Learning Good Symbol Precedences
Lasse Blaauwbroek: Project Proposal: Relieving User Effort for the Auto Tactic in Coq with Machine Learning
Chad E. Brown and Thibault Gauthier: Self-Learned Formula Synthesis in Set Theory
Chad Brown, Bartosz Piotrowski and Josef Urban: Learning to Advise an Equational Prover
Karel Chvalovský and Josef Urban: From proofs to theorems
Adrián Csiszárik, Beatrix Benkő, Gergely Stomfai and Milán Vásárhelyi: Solving Arithmetic Problems on a Checkered Paper
Wesley Fussner: Computer-assisted identification of splittings in subvariety lattices
Najwa Ghannoum, Wesley Fussner, Tomáš Jakl and Carlos Simpson: Classification of Finite Semigroups and categories using Computational Methods
Aishik Ghosh and David Rousseau: Quantum Interference Measurement with Physics Aware Machine Learning at CERN
Zarathustra Goertzel, Josef Urban and Jan Jakubuv: Make E Smart Again
Thomas Hales: A Controlled Natural Language for Type Theory
Sólrún Halla Einarsdóttir and Moa Johansson: Towards Big Theory Exploration
Jesse Han: Learning cubing heuristics for SAT from DRAT proofs
Robert Kahlert, Bettina Berendt and Benjamin P. Rode: Toward a Deductive Theory of Automated Argument Maintenance
Peter Koepke, Adrian De Lon and Anton Lorenzen: ForTheL for Type Theory
David McAllester: Isomorphism Revisited
Dennis Müller and Cezary Kaliszyk: Learning Semantic Annotations for LaTeX Documents
Yutaka Nagashima: LiFtEr: Language to Encode Induction Heuristics
Miroslav Olšák, Cezary Kaliszyk and Josef Urban: Property Invariant Neural Network for Embedding Formulas in CNF
Stanisław Purgał: Learning theorem proving through self-play
Michael Rawson and Giles Reger: Autoencoding TPTP
Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki and Lawrence Paulson: Developing a Concept-Oriented Search Engine for Isabelle Based on Natural Language : Technical Challenges
Martin Suda and Sarah Winkler: Learning Strategy Design: First Lessons
Christian Szegedy, Sarah Loos, Aditya Paliwal, Markus Rabe and Kshitij Bansal: Neural Architectures for Tactic-Based Automated Theorem Proving
Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Roger Grosse and Fahiem Bacchus: Learning Clause Deletion Heuristics with Reinforcement Learning
Minchao Wu, Michael Norrish, Christian Walder and Amir Dezfouli: Reinforcement Learning for Interactive Theorem Proving in HOL4
Yuhuai Wu, Albert Jiang, Roger Grosse and Jimmy Ba: Neural Theorem Proving on Inequality Problems
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk and Josef Urban: Update on FLoP, a Reinforcement Learning based Theorem Prover
Zsolt Zombori and Josef Urban: Learning Complex Actions from Proofs in Theorem Proving

Informal proceedings

The (extended) abstracts of all the invited and contributed talks are now available online.

Program Committee

Jasmin Christian BlanchetteINRIA Nancy
Ulrich FurbachUniversity of Koblenz
Tibault GauthierCzech Technical University in Prague
Thomas C. Hales (co-chair)University of Pittsburgh
Sean HoldenUniversity of Cambridge
Mikoláš JanotaUniversity of Lisbon
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
Sarah LoosGoogle Research
Stephan Schulz (co-chair)DHBW Stuttgart
Geoff SutcliffeUniversity of Miami
Josef Urban (co-chair)Czech Technical University in Prague
Sarah WinklerUniversity of Innsbruck

Program (preliminary)



September 13
19:30 dinner


September 14
14:00-16:30 (video) video of the whole session

Welcome - Josef Urban

Lawrence C. Paulson
Machine Learning and the Formalisation of Mathematics: Research Challenges (55m)

Yiannos Stathopoulos
Developing a Concept-Oriented Search Engine for Isabelle Based on Natural Language : Technical Challenges

Yutaka Nagashima
LiFtEr: Language to Encode Induction Heuristics

Minchao Wu
Reinforcement Learning for Interactive Theorem Proving in HOL4

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

Thibault Gauthier
Self-Learned Formula Synthesis in Set Theory

Lasse Blaauwbroek
Project Proposal: Relieving User Effort for the Auto Tactic in Coq with Machine Learning

Zsolt Zombori
Learning Complex Actions from Proofs in Theorem Proving

Adrián Csiszárik
Solving Arithmetic Problems on a Checkered Paper

19:30 dinner


September 15
14:00-16:30 (video) Chair: Georges Gonthier video of the whole session

François Charton
Deep learning for symbolic mathematics (50m)

Yuhuai Wu
Neural Theorem Proving on Inequality Problems (25m)

Stanislas Polu
Generative Language Modeling for Automated Theorem Proving (25m)

Miroslav Olšák
Property Invariant Neural Network for Embedding Formulas in CNF (25m)

Christian Szegedy
Learning alignment between formal & informal mathematics (25m)

16:30-17:00 coffee break
17:00-19:30 (video) Chair: David Stanovsky video of the whole session

Daniel Selsam
The IMO Grand Challenge (55m)

Anton Lorenzen
ForTheL for Type Theory

Dennis Müller
Learning Semantic Annotations for LaTeX Documents

David McAllester:
Isomorphism Revisited

19:30 dinner
September 16
12:00-12:30 (video) Holger Hoos
Ten theses on AI in Europe

12:30-14:00 lunch
14:00-16:30 (videos linked to talks) Chair: Cezary Kaliszyk Zarathustra Goertzel
Make E Smart Again (video)

Pashootan Vaezipoor
Learning Clause Deletion Heuristics with Reinforcement Learning (video)

Zsolt Zombori
Update on FLoP, a Reinforcement Learning based Theorem Prover (video)

Filip Bártek
Project Proposal: Machine Learning Good Symbol Precedences (video)

Sarah Winkler
Learning Strategy Design: First Lessons (video)

16:30-17:00 coffee break
17:00-19:30 (video)Chair: Martin Suda video of the whole session

Ben Goertzel
What Logic to Use for Hypothetical Scientific and Common-sense Inference? (55m)

Joao Araujo
Algebra and ATP (25m)

Wesley Fussner
Computer-assisted identification of splittings in subvariety lattices

Najwa Ghannoum
Classification of Finite Semigroups and categories using Computational Methods

David Stanovsky
ATP in algebra: several observations from practice (10m)

19:30 dinner


September 17
14:00-16:30 (videos linked to the talks) Chair: Mikolas Janota Michael Douglas
Formal/Symbolic/Numerical Computational Methods (55m) (video)

Aishik Ghosh
Quantum Interference Measurement with Physics Aware Machine Learning at CERN (video)

Sólrún Halla Einarsdóttir
Towards Big Theory Exploration (video - starts at 24:00)

Jesse Han
Learning cubing heuristics for SAT from DRAT proofs (video)

16:30-17:00 coffee break
17:00-19:30 Chair: Stephan Schulz video of the whole session

Markus Rabe
Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning (35m)

Martin Suda
Deepire: First Experiments with Neural Guidance in Vampire

Stanisław Purgał
Learning theorem proving through self-play (25m)

Michael Rawson
Autoencoding TPTP (25m)

Bartosz Piotrowski
Learning to Advise an Equational Prover

19:30 dinner


September 18
14:00-16:30 Discussions in groups
16:30-17:00 coffee break
17:00-19:00 Discussions in groups


September 19
14:00-16:30 Excursion/Discussions in groups
16:30-17:00 coffee break
17:00-19:00 Excursion/Discussions in groups


Picture from the conference

Location, Prices and Further Local Information

The conference will take place from March 22 to March 27 September 13 to September 19 2020 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.

Registration

The registration is now closed and the list of participants has been fixed. It was done via Easychair. Please do not provide any payment data by phone/email - it is very likely a scam! We have a limited block of rooms in the Aussois conference center and we have to confirm them by February 7th (after that reservation will be difficult or impossible). The pictures of the center and the rooms are here. There are twin rooms, either with double (shared) or single occupancy. The price for a double/shared room for five nights (March 22-27 September 13-18) is 550 EUR and the price for single occupancy is 640 EUR. The price includes full board, coffee breaks, the lecture rooms and our bus Modane<->Aussois. Prices for accompanying persons are the same as for conference participants. Receipts and invoices can be downloaded from EasyChair.

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 March 22nd September 13 and the last meal is lunch on Friday March 27th September 18 . 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, March 22 September 13 . The bus will wait for the TGV train from Paris arriving to Modane at 18:47. The train starts at 14:38 in Paris Gare de Lyon, and it also stops in Lyon-St Exupery at 16:37 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 March 27 September 18 . This will be optimized based on your departure flights during the conference (but taking taxi back to Modane is easy). It may be possible to stay in the center (as normal tourists) also on Saturday/Sunday (March 28-29 September 19-20) if you are interested in more skiing enjoying the Alps some more. Either arrange this with the center yourself or let us know and we will ask the center about the availability. 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 until Saturday/Sunday, etc.

Ski Rental and Passes (data from 2018)

Skiing equipment could be rented at the center for 18.70 € per day or 80.70 € for the week. A ski pass was 29 € per day or 26 € for 4 consecutive hours or 116 € for 4 days or 129 € for 5 days.