Opendata, web and dolomites

SMART SIGNED

Strong Modular proof Assistance: Reasoning across Theories

Total Cost €

0

EC-Contrib. €

0

Partnership

0

Views

0

 SMART project word cloud

Explore the words cloud of the SMART project. It provides you a very rough idea of what is the project "SMART" about.

conjectures    additionally    uniform    zf    accumulated    content    works    repositories    atp    single    combining    automatically    reusable    prove    made    proof    demonstrated    learning    reuse    certainty    extremely    40    tool    isabelle    reasoning    hol    isolated    mathematics    outcome    ultimate    techniques    person    vast    ai    combined    mathematicians    theories    generation    certification    smart    advice    proved    profile    mizar    reconstruction    unparalleled    integration    half    extraction    formalized    significantly    rates    few    flyspeck    tens    theorems    lemmas    logical    sel4    automation    multiple    assistants    security    libraries    combine    nevertheless    acl2    computer    proofs    designs    hammer    formal    foundations    consists    effort    coq    encoding    hammers    hol4    limited    science    compcert    paving    verification    heterogeneous    laborious    accessible    provers    components    delivers    individual    foundational    breakthrough   

Project "SMART" data sheet

The following table provides information about the project.

Coordinator
UNIVERSITAET INNSBRUCK 

Organization address
address: INNRAIN 52
city: INNSBRUCK
postcode: 6020
website: http://www.uibk.ac.at

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 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

 Partnership

Take a look of project's partnership.

# participants  country  role  EC contrib. [€] 
1    UNIVERSITAET INNSBRUCK AT (INNSBRUCK) coordinator 1˙449˙000.00

Map

 Project objective

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.

 Publications

year authors and title journal last update
List of publications.
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.

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

RECON (2019)

Reprogramming Conformation by Fluorination: Exploring New Areas of Chemical Space

Read More  

ArtHistCEE (2018)

Art Historiographies in Central and Eastern EuropeAn Inquiry from the Perspective of Entangled Histories

Read More  

UNITY (2020)

A Single-Photon Source Featuring Unity Efficiency And Unity Indistinguishability For Scalable Optical Quantum Information Processing

Read More