以演化式搜索輔助轉換數學證明為形式化證明

Formalizing Mathematical Proof by Using Evolutionary Search

楊平(Yang, Ping)

指導教授 ： 陳穎平

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

摘要

演化演算法作為一個搜索策略在各領域皆有良好的適應性，而數學中的形式化證明可視為一顆證明樹，因此可藉由演化計算搜索並生成證明。在本實驗室之前的研究當中，結合演化演算法以及證明輔助系統(Coq)，已經可以自動證明一些邏輯中的恆真式；再加上人類介入引導與互動，更進一步證明了一些數論中的定理，展示了研究方向的可行性。但這些研究中，人類的介入常是細節並且無法預期的，且要求其對證明輔助系統有一定程度的了解。本研究將專注於規範人類介入的方式，加強人類在其中的作用，不須理會形式化過程的細節，亦無需了解證明輔助系統。研究直接的結果之一就是當人類清楚知道如何證明時，可以快速的形式化並驗證其證明，亦可作為未來全自動證明的基礎。

關鍵字

演化式搜索 ； 演化計算 ； 基因演算法 ； 數學證明 ； 形式化證明 ； 證明輔助系統

並列摘要

In mathematics, generating a formalized Proofs can be considered as searching a proof tree. As a search method with remarkable feasibility in many field, evolutionary algorithm is suitable for searching proof tree and generating formalized proof automatically. In our previous proposal, some tautology in propositional logic can be automatically proved with our framework which combines evolutionary algorithm and proof assistant. It also can prove simple theorems in number theory with additional human involvement. Despite attaining these results, the necessary human involvement for this framework is detail and unpredictable, and the profound understanding in proof assistant is required. In this thesis, to ameliorate these problem, we aim to enhance and regulate human involvement in the framework, and reduce the requirement of understanding of proof assistant. The direct results of our research is that one can formalizing and validating mathematical proof rapidly without deep understanding of proof assistant.

並列關鍵字

Evolutionary Search ； Genetic Algorithm ； Formalized Proof ； Proof Assistant ； Coq

參考文獻

[1] H.B. Curry, “Functionality in Combinatory Logic.” Proceedings of the National Academy of Sciences, vol.20, no.11, pp. 584-590, 1934, doi:10.1073/pnas.20.11.584.

[3] Kurt. Gödel, “Über Formal Unentscheidbare Sätze Der Principia Mathematica Und Verwandter Systeme I.” Monatshefte Für Mathematik Und Physik, vol. 38-38, no. 1, 1931, pp. 173–198., doi:10.1007/bf01700692.

[4] Peter B. Andrews, Matthew Bishop, and Chad E. Brown “System Description: TPS: A Theorem Proving System for Type Theory.” Automated Deduction - CADE-17 Lecture Notes in Computer Science, 2000, pp. 164–169., doi:10.1007/10721959_11.

[5] Christoph Benzmüller, and Michael Kohlhase. “System Description: Leo — A Higher-Order Theorem Prover.” Automated Deduction — CADE-15 Lecture Notes in Computer Science, 1998, pp. 139–143., doi:10.1007/bfb0054256.

[6] B. Kutzler, and S. Stifter “Automated Geometry Theorem Proving Using Buchbergers Algorithm.” Proceedings of the Fifth ACM Symposium on Symbolic and Algebraic Computation - SYMSAC 86, 1986, doi:10.1145/32439.32480.