TY - GEN
T1 - Proving theorems by using evolutionary search with human involvement
AU - Huang, Szu Yi
AU - Chen, Ying-Ping
PY - 2017/7/5
Y1 - 2017/7/5
N2 - The link between logic and computation has been established by the BHK interpretation and the Curry-Howard isomorphism, based on which proof assistants capable of verifying formal proofs by transforming proofs into programs and by computationally evaluating the programs have been developed for the past few decades. Because evolutionary algorithms are search methods with remarkable feasibility and can be used to automatically generate programs, in our previous proposal, evolutionary algorithms and proof assistants were integrated to create a framework able to automatically prove simple theorems. In the present work, we aim to enhance the search ability of the proof generator such that proofs of slightly advanced, complicated theorems can be generated via evolutionary search with human involvement. This article describes in detail the algorithmic design of the proposed proof generator, how and why humans are involved in the process of proof development, and the test runs, in which proofs as Coq formalization of three theorems, the divisibility rule for 3, the sum of an arithmetic series, and the inequality of arithmetic and geometric means, were successfully generated. The developed source code with the obtained experimental results, including the human created rules and the software generated proofs, are released as open source.
AB - The link between logic and computation has been established by the BHK interpretation and the Curry-Howard isomorphism, based on which proof assistants capable of verifying formal proofs by transforming proofs into programs and by computationally evaluating the programs have been developed for the past few decades. Because evolutionary algorithms are search methods with remarkable feasibility and can be used to automatically generate programs, in our previous proposal, evolutionary algorithms and proof assistants were integrated to create a framework able to automatically prove simple theorems. In the present work, we aim to enhance the search ability of the proof generator such that proofs of slightly advanced, complicated theorems can be generated via evolutionary search with human involvement. This article describes in detail the algorithmic design of the proposed proof generator, how and why humans are involved in the process of proof development, and the test runs, in which proofs as Coq formalization of three theorems, the divisibility rule for 3, the sum of an arithmetic series, and the inequality of arithmetic and geometric means, were successfully generated. The developed source code with the obtained experimental results, including the human created rules and the software generated proofs, are released as open source.
KW - Automatic theorem proving
KW - Coq
KW - Evolutionary algorithm
KW - Human involvement
KW - Proof assistant
KW - Proof generator
UR - http://www.scopus.com/inward/record.url?scp=85027877540&partnerID=8YFLogxK
U2 - 10.1109/CEC.2017.7969480
DO - 10.1109/CEC.2017.7969480
M3 - Conference contribution
AN - SCOPUS:85027877540
T3 - 2017 IEEE Congress on Evolutionary Computation, CEC 2017 - Proceedings
SP - 1495
EP - 1502
BT - 2017 IEEE Congress on Evolutionary Computation, CEC 2017 - Proceedings
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 5 June 2017 through 8 June 2017
ER -