Explore the words cloud of the SMART project. It provides you a very rough idea of what is the project "SMART" about.
The following table provides information about the project.
Coordinator |
UNIVERSITAET INNSBRUCK
Organization address contact info |
Coordinator Country | Austria [AT] |
Total cost | 1˙449˙000 € |
EC max contribution | 1˙449˙000 € (100%) |
Programme |
1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC)) |
Code Call | ERC-2016-STG |
Funding Scheme | ERC-STG |
Starting year | 2017 |
Duration (year-month-day) | from 2017-03-01 to 2022-02-28 |
Take a look of project's partnership.
# | ||||
---|---|---|---|---|
1 | UNIVERSITAET INNSBRUCK | AT (INNSBRUCK) | coordinator | 1˙449˙000.00 |
Formal proof technology delivers an unparalleled level of certainty and security. Nevertheless, applying proof assistants to the verification of complex theories and designs is still extremely laborious. High profile certification projects, such as seL4, CompCert, and Flyspeck require tens of person-years. We recently demonstrated that this effort can be significantly reduced by combining reasoning and learning in so called hammer systems: 40% of the Flyspeck, HOL4, Isabelle/HOL, and Mizar top-level lemmas can be proved automatically.
Today's early generation of hammers consists of individual systems limited to very few proof assistants. The accessible knowledge repositories are isolated, and there is no reuse of hammer components.
It is possible to achieve a breakthrough in proof automation by developing new AI methods that combine reasoning knowledge and techniques into a smart hammer, that works over a very large part of today's formalized knowledge. The main goal of the project is to develop a strong and uniform learning-reasoning system available for multiple logical foundations. To achieve this, we will develop: (a) uniform learning methods, (b) reusable ATP encoding components for different foundational aspects, (c) integration of proof reconstruction, and (d) methods for knowledge extraction, reuse and content merging. The single proof advice system will be made available for multiple proof assistants and their vast heterogeneous libraries.
The ultimate outcome is an advice system able to automatically prove half of Coq, ACL2, and Isabelle/ZF top-level theorems. Additionally we will significantly improve success rates for HOL provers and Mizar. The combined smart advice method together with the vast accumulated knowledge will result in a novel kind of tool, which allows working mathematicians to automatically find proofs of many simple conjectures, paving the way for the widespread use of formal proof in mathematics and computer science.
year | authors and title | journal | last update |
---|---|---|---|
2019 |
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark Barrett, Cesare Tinelli Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract) published pages: 18-26, ISSN: 2075-2180, DOI: 10.4204/EPTCS.301.4 |
Electronic Proceedings in Theoretical Computer Science 301 | 2019-10-29 |
2019 |
Chad E. Brown, Cezary Kaliszyk, Karol PÄ…k Higher-Order Tarski Grothendieck as aFoundation for Formal Proof published pages: , ISSN: , DOI: 10.4230/lipics.itp.2019.9 |
2019-10-29 | |
2017 |
Kaliszyk, Cezary; Urban, Josef; Vyskocil, Jirà Automating Formalization by Statistical and Semantic Parsing of Mathematics published pages: , ISSN: , DOI: |
ITP 2017 7 | 2019-09-17 |
2019 |
Cezary Kaliszyk, Karol PÄ…k Semantics of Mizar as an Isabelle Object Logic published pages: 557-595, ISSN: 0168-7433, DOI: 10.1007/s10817-018-9479-z |
Journal of Automated Reasoning 63/3 | 2019-09-17 |
2018 |
Kaliszyk, Cezary; Urban, Josef; Michalewski, Henryk; Olšák, Mirek Reinforcement Learning of Theorem Proving published pages: , ISSN: , DOI: |
NeurIPS 2018 12 | 2019-09-17 |
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 | 2019-04-18 |
2018 |
Nagashima, Yutaka; Parsert, Julian Goal-Oriented Conjecturing for Isabelle/HOL published pages: , ISSN: , DOI: |
1 | 2019-04-18 |
2018 |
Åukasz Czajka, Burak Ekici, Cezary Kaliszyk Concrete Semantics with Coq and CoqHammer published pages: 53-59, ISSN: , DOI: 10.1007/978-3-319-96812-4_5 |
2019-04-18 | |
2017 |
Färber Michael, Kaliszyk Cezary, Urban Josef Monte Carlo Tableau Proof Search published pages: , ISSN: , DOI: |
2019-04-18 | |
2017 |
Loos Sarah, Irving Geoffrey, Szegedy Christian, Kaliszyk Cezary Deep Network Guided Proof Search published pages: , ISSN: , DOI: |
2019-04-18 | |
2019 |
Gauthier Thibault, Kaliszyk Cezary Aligning Concepts across Proof Assistant Libraries published pages: , ISSN: 0747-7171, DOI: |
Journal of Symbolic Computing | 2019-04-18 |
2018 |
Wang, Qingxiang; Kaliszyk, Cezary; Urban, Josef First Experiments with Neural Translation of Informal to Formal Mathematics published pages: , ISSN: , DOI: |
2 | 2019-04-18 |
2018 |
Czajka Lukasz, Kaliszyk Cezary Hammer for Coq: Automation for Dependent Type Theory published pages: , ISSN: 0168-7433, DOI: |
Journal of Automated Reasoning | 2019-04-18 |
Are you the coordinator (or a participant) of this project? Plaese send me more information about the "SMART" 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 "SMART" are provided by the European Opendata Portal: CORDIS opendata.