Tree-Structure CNN for automated theorem proving

Kebin Peng; Dianfu Ma

doi:10.1007/978-3-319-70096-0_1

Tree-Structure CNN for automated theorem proving

Kebin Peng^*
, Dianfu Ma

^*Corresponding author for this work

School of Computer Science and Engineering

Beihang University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 Scopus citations

Abstract

The most difficult and heavy work of Automated Theorem Proving (ATP) is that people should search in millions of intermediate steps to finish proof. In this paper, we present a novel neural network, which can effectively help people to finish this work. Specifically, we design a tree-structure CNN, involving bidirectional LSTM. We compare our model with other neural network models and make experiments on HOLStep dataset, which is a machine learning dataset for Higher-order logic theorem proving. Being compared to previous approaches, our model improves accuracy significantly, reaching 90% accuracy on the test set.

Original language	English
Title of host publication	Neural Information Processing - 24th International Conference, ICONIP 2017, Proceedings
Editors	Dongbin Zhao, El-Sayed M. El-Alfy, Derong Liu, Shengli Xie, Yuanqing Li
Publisher	Springer Verlag
Pages	3-12
Number of pages	10
ISBN (Print)	9783319700953
DOIs	https://doi.org/10.1007/978-3-319-70096-0_1
State	Published - 2017
Event	24th International Conference on Neural Information Processing, ICONIP 2017 - Guangzhou, China Duration: 14 Nov 2017 → 18 Nov 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10635 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	24th International Conference on Neural Information Processing, ICONIP 2017
Country/Territory	China
City	Guangzhou
Period	14/11/17 → 18/11/17

Access to Document

10.1007/978-3-319-70096-0_1

Cite this

Peng, K., & Ma, D. (2017). Tree-Structure CNN for automated theorem proving. In D. Zhao, E.-S. M. El-Alfy, D. Liu, S. Xie, & Y. Li (Eds.), Neural Information Processing - 24th International Conference, ICONIP 2017, Proceedings (pp. 3-12). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10635 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-70096-0_1

Peng, Kebin ; Ma, Dianfu. / Tree-Structure CNN for automated theorem proving. Neural Information Processing - 24th International Conference, ICONIP 2017, Proceedings. editor / Dongbin Zhao ; El-Sayed M. El-Alfy ; Derong Liu ; Shengli Xie ; Yuanqing Li. Springer Verlag, 2017. pp. 3-12 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{fa35a961289a4e29946048aa6b523872,

title = "Tree-Structure CNN for automated theorem proving",

abstract = "The most difficult and heavy work of Automated Theorem Proving (ATP) is that people should search in millions of intermediate steps to finish proof. In this paper, we present a novel neural network, which can effectively help people to finish this work. Specifically, we design a tree-structure CNN, involving bidirectional LSTM. We compare our model with other neural network models and make experiments on HOLStep dataset, which is a machine learning dataset for Higher-order logic theorem proving. Being compared to previous approaches, our model improves accuracy significantly, reaching 90\% accuracy on the test set.",

author = "Kebin Peng and Dianfu Ma",

note = "Publisher Copyright: {\textcopyright} 2017, Springer International Publishing AG.; 24th International Conference on Neural Information Processing, ICONIP 2017 ; Conference date: 14-11-2017 Through 18-11-2017",

year = "2017",

doi = "10.1007/978-3-319-70096-0\_1",

language = "英语",

isbn = "9783319700953",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "3--12",

editor = "Dongbin Zhao and El-Alfy, \{El-Sayed M.\} and Derong Liu and Shengli Xie and Yuanqing Li",

booktitle = "Neural Information Processing - 24th International Conference, ICONIP 2017, Proceedings",

address = "德国",

}

Peng, K & Ma, D 2017, Tree-Structure CNN for automated theorem proving. in D Zhao, E-SM El-Alfy, D Liu, S Xie & Y Li (eds), Neural Information Processing - 24th International Conference, ICONIP 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10635 LNCS, Springer Verlag, pp. 3-12, 24th International Conference on Neural Information Processing, ICONIP 2017, Guangzhou, China, 14/11/17. https://doi.org/10.1007/978-3-319-70096-0_1

Tree-Structure CNN for automated theorem proving. / Peng, Kebin; Ma, Dianfu.
Neural Information Processing - 24th International Conference, ICONIP 2017, Proceedings. ed. / Dongbin Zhao; El-Sayed M. El-Alfy; Derong Liu; Shengli Xie; Yuanqing Li. Springer Verlag, 2017. p. 3-12 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10635 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Tree-Structure CNN for automated theorem proving

AU - Peng, Kebin

AU - Ma, Dianfu

PY - 2017

Y1 - 2017

N2 - The most difficult and heavy work of Automated Theorem Proving (ATP) is that people should search in millions of intermediate steps to finish proof. In this paper, we present a novel neural network, which can effectively help people to finish this work. Specifically, we design a tree-structure CNN, involving bidirectional LSTM. We compare our model with other neural network models and make experiments on HOLStep dataset, which is a machine learning dataset for Higher-order logic theorem proving. Being compared to previous approaches, our model improves accuracy significantly, reaching 90% accuracy on the test set.

AB - The most difficult and heavy work of Automated Theorem Proving (ATP) is that people should search in millions of intermediate steps to finish proof. In this paper, we present a novel neural network, which can effectively help people to finish this work. Specifically, we design a tree-structure CNN, involving bidirectional LSTM. We compare our model with other neural network models and make experiments on HOLStep dataset, which is a machine learning dataset for Higher-order logic theorem proving. Being compared to previous approaches, our model improves accuracy significantly, reaching 90% accuracy on the test set.

UR - https://www.scopus.com/pages/publications/85035132220

U2 - 10.1007/978-3-319-70096-0_1

DO - 10.1007/978-3-319-70096-0_1

M3 - 会议稿件

AN - SCOPUS:85035132220

SN - 9783319700953

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 12

BT - Neural Information Processing - 24th International Conference, ICONIP 2017, Proceedings

A2 - Zhao, Dongbin

A2 - El-Alfy, El-Sayed M.

A2 - Liu, Derong

A2 - Xie, Shengli

A2 - Li, Yuanqing

PB - Springer Verlag

T2 - 24th International Conference on Neural Information Processing, ICONIP 2017

Y2 - 14 November 2017 through 18 November 2017

ER -

Peng K, Ma D. Tree-Structure CNN for automated theorem proving. In Zhao D, El-Alfy ESM, Liu D, Xie S, Li Y, editors, Neural Information Processing - 24th International Conference, ICONIP 2017, Proceedings. Springer Verlag. 2017. p. 3-12. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-70096-0_1

Tree-Structure CNN for automated theorem proving

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this