Nvidia fellowship proposal - Sketching: a Cognitively inspired Compositional Theorem Prover that Learns

Brando Miranda

Permalink

https://hdl.handle.net/2142/109175 Copy

Description

Title

Nvidia fellowship proposal - Sketching: a Cognitively inspired Compositional Theorem Prover that Learns

Author(s)

Brando Miranda

Issue Date

2020-09-11

Keyword(s)

• meta-learning
• agi
• machine learning
• theorem proving

Abstract

Vision & motivation: Theorem proving has important applications in hardware and software verification. In hardware verification, it has been used for integrated circuit design [7, 8]. For software verification, a major success with theorem provers has been with the creation of CertC; a verified compiler for C; [9]. In the past, companies like Intel have made major investments in formal methods to guarantee the processors they manufacture do not have major floating-point bugs -- an important example of this is the Pentium FDIV bug in 1994 that cost them $500M [11]. As a consequence, theorem proving has been used to verify floating-point firmware [10]. But to effectively use this tool one requires highly trained human experts in the corresponding theorem prover and its area of application (e.g. using the HOL Light theorem prover for hardware verification). However, learnable automated theorem proving promises to revolutionize hardware and software verification by: 1) increasing the automatization of the challenging task of theorem proving and 2) by increasing the adaptability of such methods and therefore widening their use and applicability through learning. With this I envision that Nvidia can be a leader in this field by providing high quality verified GPU hardware, safe compilation of CUDA code, verified CUDA kernels, and exemplary verified interfaces of Nvidia GPU code for higher-level languages like python. With these vast immediately impactful applications I can see Nvidia leading the way to the highest quality products and saving millions of dollars in a fiercely competitive industry with increasing demands from gaming and deep learning applications. In addition, theorem proving has had a major role in human history with the development of the scientific method, mathematics and technology. Thus, the last major part of my vision is to further empower humanity with powerful automation tools that can take all those areas even further. In addition, with a system that is capable of learning its applications are nearly endless. For example, it could play the crucial role of guaranteeing safe AI. Nvidia can become one of the first to pave the way forward in this exciting field and have a long-lasting impact for a richer, safer future.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/109175

Owning Collections