文献

J-GLOBAL ID：201802258511017390   整理番号：18A0657236

機械学習によるCoq上の命題論理の自動証明に関する研究

著者 (4件)： 金原雅典 ,  佐藤亮介 ,  鵜林尚靖 ,  亀井靖高
資料名： 情報処理学会研究報告(Web)  (IPSJ Technical Report (Web))
巻： 2018  号： SE-198  ページ： Vol.2018-SE-198,No.4,1-8 (WEB ONLY)  発行年： 2018年03月02日 
JST資料番号： U0451A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： プログラムの正しさを形式的に保証することは,そのプログラムに誤りがないということを確認する点で開発者にとって有用である。形式的に証明することは大変であり,自動化することでその手間を減らすことができる。そこで本研究では,機械学習を用いた命題の自動証明を試みる。その第一段階として,対象の論理を命題論理に限定して既存の機械学習によって学習・自動証明が可能かどうかを評価する。命題論理式は変数の数と,命題論理式を木構造にした時の深さを限定してプログラム上で生成を行なった。本研究での“証明”は,自然言語により書かれたものではなく,定理証明支援システムCoq上での証明である。Coqとは,プログラムの正しさの証明や安全なプログラムを書くことに使用される証明支援システムである。学習は機械学習モデルの一つであるシーケンス変換モデルを用いて行う。Coq上の証明をシーケンス変換モデルに学習させることにより,学習に用いるデータセットが十分な量あれば一般の機械学習の方法でも学習可能かどうかの評価を行なった。学習結果としては,データセットと同じ範囲の入力に対しては約90%の割合で正しい出力を得られた。また,データセットの範囲を超える深さの命題論理式を入力した場合は正しい出力は約53%の割合となった。(著者抄録)

シソーラス用語： 機械学習 ,  *プログラミング言語 ,  *命題論理 ,  *証明 ,  ソフトウェア ,  論理 ,  自然言語 ,  計算機利用システム ,  *自動化 ,  *Coq【言語】 ,  *改変
準シソーラス用語： 支援システム

分類 (2件)： 論理代数  (JB03000H) ,  汎用プログラミング言語  (JD03051H)

引用文献 (14件)：

• Bahdanau, D., Cho, K. and Bengio, Y.: Neural Machine Translation by Jointly Learning to Align and Translate, CoRR, Vol. abs/1409.0473 (online), available from <http://arxiv.org/abs/1409.0473> (2014).
• Cho, K., van Merrienboer, B., G?l?ehre, ?., Bougares, F., Schwenk, H. and Bengio, Y.: Learning Phrase Representations using RNN Encoder-Decoder for Statistical Machine Translation, CoRR, Vol. abs/1406.1078 (online), available from <http://arxiv.org/abs/1406.1078> (2014).
• Dahl, G. E., Yu, D., Deng, L. and Acero, A.: ContextDependent Pre-Trained Deep Neural Networks for LargeVocabulary Speech Recognition, IEEE Trans. Audio, Speech & Language Processing, Vol. 20, No. 1, pp. 30-42 (online), DOI: 10.1109/TASL.2011.2134090 (2012).
• Denton, E. L., Chintala, S., Szlam, A. and Fergus, R.: Deep Generative Image Models using a Laplacian Pyramid of Adversarial Networks, CoRR, Vol. abs/1506.05751 (online), available from <http://arxiv.org/abs/1506.05751> (2015).
• Gonthier, G.: The Four Colour Theorem: Engineering of a Formal Proof, Computer Mathematics, 8th Asian Symposium, ASCM 2007, Singapore, December 15-17, 2007. Revised and Invited Papers, p. 333 (2007).

タイトルに関連する用語 (4件)： 機械学習 ,  命題論理 ,  証明 ,  研究