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

Abstract

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.