Opendata, web and dolomites

AI4REASON SIGNED

Artificial Intelligence for Large-Scale Computer-Assisted Reasoning

Total Cost €

0

EC-Contrib. €

0

Partnership

0

Views

0

Project "AI4REASON" data sheet

The following table provides information about the project.

Coordinator
CESKE VYSOKE UCENI TECHNICKE V PRAZE 

Organization address
address: JUGOSLAVSKYCH PARTYZANU 1580/3
city: PRAHA
postcode: 160 00
website: www.cvut.cz

contact info
title: n.a.
name: n.a.
surname: n.a.
function: n.a.
email: n.a.
telephone: n.a.
fax: n.a.

 Coordinator Country Czech Republic [CZ]
 Project website http://ai4reason.org/
 Total cost 1˙499˙500 €
 EC max contribution 1˙499˙500 € (100%)
 Programme 1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC))
 Code Call ERC-2014-CoG
 Funding Scheme ERC-COG
 Starting year 2015
 Duration (year-month-day) from 2015-09-01   to  2020-08-31

 Partnership

Take a look of project's partnership.

# participants  country  role  EC contrib. [€] 
1    CESKE VYSOKE UCENI TECHNICKE V PRAZE CZ (PRAHA) coordinator 1˙499˙500.00

Map

 Project objective

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.

 Publications

year authors and title journal last update
List of publications.
2017 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
2017 Josef Urban
AI at CADE/IJCAR
published pages: 33-28, ISSN: , DOI: 10.29007/26gg
EPiC Series in Computing volume 51 2020-04-23
2016 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
2016 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
2016 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
2017 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
2016 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
2017 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
2017 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
2016 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
2016 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
2015 Josef Urban
BliStr: The Blind Strategymaker
published pages: 312-303, ISSN: , DOI: 10.29007/8n7m
EPiC Series in Computing volume 36 2020-04-23
2016 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
2016 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 (fabio@fabiodisconzi.com) 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.

More projects from the same programme (H2020-EU.1.1.)

MADEFUN (2019)

Regulation of Brain Macrophage Development and Function

Read More  

NanoBeam (2019)

Quantum Coherent Control: Self–Interference of Electron Beams with Nanostructures

Read More  

H I C I (2020)

Transcriptional and epigenetic control of tissue regenerative HB-EGF in autoimmune CNS inflammation

Read More