Explore the words cloud of the AI4REASON project. It provides you a very rough idea of what is the project "AI4REASON" about.
The following table provides information about the project.
CESKE VYSOKE UCENI TECHNICKE V PRAZE
|Coordinator Country||Czech Republic [CZ]|
|Total cost||1˙499˙500 €|
|EC max contribution||1˙499˙500 € (100%)|
1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC))
|Duration (year-month-day)||from 2015-09-01 to 2020-08-31|
Take a look of project's partnership.
|1||CESKE VYSOKE UCENI TECHNICKE V PRAZE||CZ (PRAHA)||coordinator||1˙499˙500.00|
The goal of the AI4REASON project is a breakthrough in what is considered a very hard problem in AI and automation of reasoning, namely the problem of automatically proving theorems in large and complex theories. Such complex formal theories arise in projects aimed at verification of today's advanced mathematics such as the Formal Proof of the Kepler Conjecture (Flyspeck), verification of software and hardware designs such as the seL4 operating system kernel, and verification of other advanced systems and technologies on which today's information society critically depends.
It seems extremely complex and unlikely to design an explicitly programmed solution to the problem. However, we have recently demonstrated that the performance of existing approaches can be multiplied by data-driven AI methods that learn reasoning guidance from large proof corpora. The breakthrough will be achieved by developing such novel AI methods. First, we will devise suitable Automated Reasoning and Machine Learning methods that learn reasoning knowledge and steer the reasoning processes at various levels of granularity. Second, we will combine them into autonomous self-improving AI systems that interleave deduction and learning in positive feedback loops. Third, we will develop approaches that aggregate reasoning knowledge across many formal, semi-formal and informal corpora and deploy the methods as strong automation services for the formal proof community.
The expected outcome is our ability to prove automatically at least 50% more theorems in high-assurance projects such as Flyspeck and seL4, bringing a major breakthrough in formal reasoning and verification. As an AI effort, the project offers a unique path to large-scale semantic AI. The formal corpora concentrate centuries of deep human thinking in a computer-understandable form on which deductive and inductive AI can be combined and co-evolved, providing new insights into how humans do mathematics and science.
|year||authors and title||journal||last update|
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
TacticToe: Learning to Reason with HOL4 Tactics
published pages: 125-105, ISSN: , DOI: 10.29007/ntlb
|EPiC Series in Computing volume 46||2020-04-23|
AI at CADE/IJCAR
published pages: 33-28, ISSN: , DOI: 10.29007/26gg
|EPiC Series in Computing volume 51||2020-04-23|
Alex A. Alemi, FranÃ§ois Chollet, Geoffrey Irving, Christian Szegedy, Josef Urban
DeepMath - Deep Sequence Models for Premise Selection
published pages: 2235--2243, ISSN: , DOI:
|Advances in Neural Information Processing Systems 29 (NIPS 2016) 29, NIPS 2016||2020-04-23|
John Harrison, Josef Urban, Freek Wiedijk
Preface: Twenty Years of the QED Manifesto
published pages: 1-2, ISSN: 1972-5787, DOI: 10.6092/issn.1972-5787/5974
|Journal of Formalized Reasoning 9||2020-04-23|
Cezary Kaliszyk, Josef Urban, Jiri Vyskocil
Improving Statistical Linguistic Algorithms for Parsing Mathematics
published pages: 27-16, ISSN: 2398-7340, DOI: 10.29007/8c2m
|EPiC Series in Computing volume 40 vol 40, pages 27-36||2020-04-23|
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
Initial Experiments with Statistical Conjecturing over Large Formal Corpora
published pages: 219-228, ISSN: , DOI:
|Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016||2020-04-23|
Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban
Hammering towards QED
published pages: 101-148, ISSN: 1972-5787, DOI: 10.6092/issn.1972-5787/4593
|Journal of Formalized Reasoning vol9, no 1||2020-04-23|
Jan Jakubuv, Martin Suda, Josef Urban
Automated Invention of Strategies and Term Orderings for Vampire
published pages: 121-107, ISSN: , DOI: 10.29007/xghj
|EPiC Series in Computing volume 50||2020-04-23|
THOMAS HALES, MARK ADAMS, GERTRUD BAUER, TAT DAT DANG, JOHN HARRISON, LE TRUONG HOANG, CEZARY KALISZYK, VICTOR MAGRON, SEAN MCLAUGHLIN, TATÂ THANG NGUYEN, QUANG TRUONG NGUYEN, TOBIAS NIPKOW, STEVEN OBUA, JOSEPH PLESO, JASON RUTE, ALEXEY SOLOVYEV, THI HOAI AN TA, NAM TRUNG TRAN, THI DIEP TRIEU, JOSEF URBAN, KY VU, ROLAND ZUMKELLER
A FORMAL PROOF OF THE KEPLER CONJECTURE
published pages: , ISSN: 2050-5086, DOI: 10.1017/fmp.2017.1
|Forum of Mathematics, Pi 5||2020-04-23|
Geoff Sutcliffe, Josef Urban
The CADE-25 Automated Theorem Proving system competitionÂ â€“ CASC-25
published pages: 423-433, ISSN: 0921-7126, DOI: 10.3233/AIC-150691
|AI Communications 29/3||2020-04-23|
Josef Urban, Robert Veroff
Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry
published pages: 122-116, ISSN: , DOI: 10.29007/pqh1
|EPiC Series in Computing volume 40||2020-04-23|
BliStr: The Blind Strategymaker
published pages: 312-303, ISSN: , DOI: 10.29007/8n7m
|EPiC Series in Computing volume 36||2020-04-23|
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel KÃ¼hlwein, Josef Urban
A Learning-Based Fact Selector for Isabelle/HOL
published pages: 219-244, ISSN: 0168-7433, DOI: 10.1007/s10817-016-9362-8
|Journal of Automated Reasoning 57/3||2020-04-23|
Freek Wiedijk, Herman Geuvers, Josef Urban
Een wiskundig bewijs correct bewezen: De meest efficiÃ«nte manier om bollen op te stapelen
published pages: 177-183, ISSN: 0028-9825, DOI:
|Nieuw Archief voor Wiskunde 5/17||2020-04-23|
Are you the coordinator (or a participant) of this project? Plaese send me more information about the "AI4REASON" project.
For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.
Send me an email (firstname.lastname@example.org) and I put them in your project's page as son as possible.
Thanks. And then put a link of this page into your project's website.
The information about "AI4REASON" are provided by the European Opendata Portal: CORDIS opendata.