文献
J-GLOBAL ID：201802258511017390
整理番号：18A0657236
機械学習によるCoq上の命題論理の自動証明に関する研究
-
出版者サイト
{{ this.onShowPLink() }}
複写サービスで全文入手
{{ this.onShowCLink("http://jdream3.com/copy/?sid=JGLOBAL&noSystem=1&documentNoArray=18A0657236©=1") }}
-
高度な検索・分析はJDreamⅢで
{{ this.onShowJLink("http://jdream3.com/lp/jglobal/index.html?docNo=18A0657236&from=J-GLOBAL&jstjournalNo=U0451A") }}
著者 (4件)：
,
,
,
資料名：
巻：
2018
号：
SE-198
ページ：
Vol.2018-SE-198,No.4,1-8 (WEB ONLY)
発行年：
2018年03月02日
JST資料番号：
U0451A
資料種別：
会議録 (C)
記事区分：
原著論文
発行国：
日本 (JPN)
言語：
日本語 (JA)
抄録/ポイント：
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
プログラムの正しさを形式的に保証することは,そのプログラムに誤りがないということを確認する点で開発者にとって有用である。形式的に証明することは大変であり,自動化することでその手間を減らすことができる。そこで本研究では,機械学習を用いた命題の自動証明を試みる。その第一段階として,対象の論理を命題論理に限定して既存の機械学習によって学習・自動証明が可能かどうかを評価する。命題論理式は変数の数と,命題論理式を木構造にした時の深さを限定してプログラム上で生成を行なった。本研究での“証明”は,自然言語により書かれたものではなく,定理証明支援システムCoq上での証明である。Coqとは,プログラムの正しさの証明や安全なプログラムを書くことに使用される証明支援システムである。学習は機械学習モデルの一つであるシーケンス変換モデルを用いて行う。Coq上の証明をシーケンス変換モデルに学習させることにより,学習に用いるデータセットが十分な量あれば一般の機械学習の方法でも学習可能かどうかの評価を行なった。学習結果としては,データセットと同じ範囲の入力に対しては約90%の割合で正しい出力を得られた。また,データセットの範囲を超える深さの命題論理式を入力した場合は正しい出力は約53%の割合となった。(著者抄録)
シソーラス用語：
シソーラス用語/準シソーラス用語
文献のテーマを表すキーワードです。
部分表示の続きはJDreamⅢ（有料）でご覧いただけます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
,
,
,
,
,
,
,
,
準シソーラス用語：
シソーラス用語/準シソーラス用語
文献のテーマを表すキーワードです。
部分表示の続きはJDreamⅢ（有料）でご覧いただけます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
,
分類 (2件)：
分類
JSTが定めた文献の分類名称とコードです
論理代数
, 汎用プログラミング言語
引用文献 (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件)：
タイトルに関連する用語
J-GLOBALで独自に切り出した文献タイトルの用語をもとにしたキーワードです
,
,
,
前のページに戻る
