• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2019 年度 実施状況報告書

数学の自動化を推進するための機械学習を用いた定理自動証明手法

研究課題

研究課題/領域番号 19K22842
研究機関京都大学

研究代表者

末永 幸平  京都大学, 情報学研究科, 准教授 (70633692)

研究分担者 塚田 武志  東京大学, 大学院情報理工学系研究科, 助教 (50758951)
関山 太朗  国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
研究期間 (年度) 2019-06-28 – 2022-03-31
キーワード機械学習 / 定理証明 / 強化学習 / ホーン節ソルバ
研究実績の概要

数学的な定理の自動証明手法への機械学習の適用について検討を行った.今年度は主に強化学習によって自動証明器,特にホーン節ソルバを従来手法より高性能化できるかどうかについて実験を行った.その結果,ホーン節ソルバの内部状態の情報を用いて,ホーン節ソルバの動作を誘導するポリシーを学習することで,従来手法の証明器の性能を向上することができる見込みが得られた.ポリシーを手動で作り込むことで証明器の性能が向上することは確認できており,少なくともこのポリシーを学習することができれば高性能化が可能になると期待される.そこで今後は,この方向の研究を進め,(1) ポリシーの学習に有用な内部状態情報の同定と (2) 本問題でのポリシーの学習に適した手法の検討を進めたいと考えており,最終的にホーン節ソルバのためのベンチマークで実験的に有用性を確認したいと考えている.
また,付随する研究として RNN からその動作を模倣する重み付き有限状態オートマトン (WFA) を抽出する研究を行い,その成果をAAAI'20にて発表した.この研究は,オートマトン学習手法であるAngluinのアルゴリズムに着想を得て,これをRNNからのWFAの抽出に応用したものであり,その有効性を実験的に確認した.本研究は直接的に定理を機械学習によって証明しようとする手法ではないものの,RNN という機械学習における道具と,オートマトンという記号を扱う道具を結びつける手法としての意義がある.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

強化学習によるホーン節ソルバの高性能化に関する予備実験が進んでおり,これを今後成果に結びつけることができると考えている.

今後の研究の推進方策

今年度行ったホーン節ソルバの高性能化の実験を進め,強化学習に基づく自動証明手法の研究として結実させることを検討している.また,別途末永が代表となって進めている基盤Bの研究においても,自動証明に類する研究の発想が出つつあり,そちらとのシナジーを得ることも考えている.

次年度使用額が生じた理由

国際会議参加が見込みより少なかったために次年度使用額が生じた.来年度は実験に要する費用と国際会議参加を積極的に行う予定である.新型コロナウイルスの影響により国際会議の参加が難しい場合は,実験用の計算機を購入し,より実験を効率的に行うことを検討する.

  • 研究成果

    (2件)

すべて 2020

すべて 雑誌論文 (1件) (うち査読あり 1件) 学会発表 (1件) (うち国際学会 1件)

  • [雑誌論文] Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces2020

    • 著者名/発表者名
      Takamasa Okudono, Masaki Waga, Taro Sekiyama, and Ichiro Hasuo
    • 雑誌名

      Proceedings of AAAI'20

      巻: - ページ: -

    • 査読あり
  • [学会発表] Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces2020

    • 著者名/発表者名
      Takamasa Okudono
    • 学会等名
      AAAI'20
    • 国際学会

URL: 

公開日: 2021-01-27  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi