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

2017 年度 実施状況報告書

論理的に隙のない情報理論テキストの自動生成

研究課題

研究課題/領域番号 16K12391
研究機関千葉大学

研究代表者

萩原 学  千葉大学, 大学院理学研究院, 准教授 (80415728)

研究分担者 葛岡 成晃  和歌山大学, システム工学部, 准教授 (60452538)
研究期間 (年度) 2016-04-01 – 2019-03-31
キーワード形式化 / 情報理論
研究実績の概要

本研究の目標である、情報理論の情報源符号化定理の形式化を含んでいるCoq/SSReflectライブラリである infoTheo の .v ファイル群に対し、タクティク等を自然言語へ変換するソフトウェアの開発を進めている。ソフトウェアは Python のスクリプトとして作成してきた。主なアイデアは、形式証明から自然言語へのデータベースの構築、および、形式証明の解析の組合せである。また、CoqとPython間のデータの橋渡しには、フリーソフトの proviola を参考にしてきた。これは標準出力とエラー出力をパイプとした、Coqの入力と出力をやりとりする手法である。
作成したソフトウェアは、研究体制(代表者、分担者)で協力し動作を確認してきた。また、研究協力者である名古屋大学のガリグ氏にもデモンストレーションを行い、参考意見を頂いてきた。3人の動作環境が異なることで、機能の一部が正常に動作しない状況も確認した。これは、 Windows 版の Python のバグによるところが大きい。そのため、他の OS 等を中心として開発を進めている。ただし Windows版の開発を諦めたのではなく、 Windows 10の Windows Subsystem for Linux を利用して、実質的に Windows上で実行可能な状況にできている。
これらの積み重ねにより、.v ファイルの一部に対して、ある程度まで自然言語化出来てきたと言える。実際、 infoTheo の一部のファイルでは、ほぼ全て自動的に自然言語化できたものもある。一方、すべてのファイルを完全に自然言語化するには、いくつかブレイクスルーや人力が必要であると見込みが立ってきた。その理由は進捗状況で述べる。

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

3: やや遅れている

理由

infoTheoは多くのファイル群により構成されること、SSReflectベースで書かれているため、単一のタクティクと異なり、タクティカルの組み合わせにより、形式化された証明の表現が複雑であることが原因で、形式証明から自然言語への対応が複雑になっていることが判明した。

今後の研究の推進方策

情報源符号化定理の形式証明全体を自然言語化するのではなく、主要な補題・定理や定義等に絞って、自然言語化する方法を視野に入れている。

  • 研究成果

    (3件)

すべて 2018 2017

すべて 雑誌論文 (1件) 学会発表 (1件) (うち国際学会 1件) 図書 (1件)

  • [雑誌論文] An application of universal FV codes to source coding allowing errors2017

    • 著者名/発表者名
      Shigeaki Kuzuoka
    • 雑誌名

      IEICE Technical Report

      巻: 2017-5 ページ: 25-30

  • [学会発表] On universal FV coding allowing non-vanishing error probability2017

    • 著者名/発表者名
      Shigeaki Kuzuoka
    • 学会等名
      the 10th Asia-Europe Workshop on Information Theory (AEW10)
    • 国際学会
  • [図書] Coq/SSReflect/MathCompによる定理証明2018

    • 著者名/発表者名
      萩原 学、アフェルト・レナルド
    • 総ページ数
      224
    • 出版者
      森北出版
    • ISBN
      978-4627062412

URL: 

公開日: 2018-12-17  

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

Powered by NII kakenhi