2N-01
命題論理の深層学習による自動証明
○金原雅典，佐藤亮介，鵜林尚靖，亀井靖高（九大）
プログラムの正しさを形式的に保証することは，そのプログラムに誤りがないということを確認する点で開発者にとって有用であり，自動化することでその証明作業の手間を減らすことができる．本研究では，深層学習を用いた命題の自動証明を試みる．その第一段階として，対象の論理を命題論理に限定し，深層学習によって学習・自動証明が可能かどうかを評価する．機械学習のモデルとしてRNNの一種であるシーケンス変換モデルを用いて，証明の手順を学習する．サイズの小さい命題論理に対して，学習に用いるデータセットの量が十分であれば，既存の機械学習手法で学習可能かどうかの評価を行なった．
footer 著作権について 倫理綱領 プライバシーポリシー セキュリティ 情報処理学会