以人類參與的演化式搜索證明數學定理

Proving Theorems by Using Evolutionary Search with Human Involvement

黃思誼(Szu-Yi Huang)

指導教授 ： 陳穎平

國立交通大學/資訊學院/資訊科學與工程研究所/碩士(2017年)

摘要

BHK interpretation 與 Curry-Howard isomorphism 建立了邏輯與計算的連結,藉由轉換證明過程為程式使電腦可以驗證形式證明的 Proof Assistant,在過去幾十年有重大的發展。演化式演算法作為一個搜索的策略一直以來都有很好的適應性,並且也可以被用於產生程式,因此在本實驗室之前的研究中已經成功的結合演化式演算法與 Proof Assistant,並取得初步的成果證明了這個架構的可行性。本研究將往提升搜索能力,並且嘗試更進階的定理為目的,增加讓 Proof Generator 與人類互動的機制引導演化式演算法的發展。本篇論文將詳細介紹我們所提出的理論以及演算法的設計,包含了我們證明出來的三個定理實驗結果。

關鍵字

演化計算 ； 證明助理 ； 自動定理證明 ； 人類參與 ； 證明產生器

並列摘要

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.

並列關鍵字

proof generator ； proof assistant ； Coq ； evolutionary algorithm ； automatic theorem proving ； human involvement

參考文獻

[1] A. S. Troelstra, “History of constructivism in the twentieth century,” University of Amsterdam, Tech. Rep. ML-91-05, April 1991.

[2] H. B. Curry, “Functionality in combina tory logic,” Proceedings of the National Academy of Sciences, vol. 20, no. 11, pp. 584–590, 1934, doi:10.1073/pnas.20.11.584.

[3] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: http://homotopytypetheory.org/book, 2013.

[4] P. Hudak, J. Hughes, S. Peyton Jones, and P. Wadler, “A history of Haskell: Being lazy with class,” in Proceedings of the Third ACM SIGPLAN Conference on History of Programming Languages, ser. HOPL III. New York, NY, USA: ACM, 2007, pp. 12–1–12–55.[Online].Available:http://doi.acm.org/10.1145/1238844.1238856

[5] “Haskell: An advanced purely-functional programming language,” https://www.haskell.org/, accessed: 2017-01-30.