• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2017 Fiscal Year Research-status Report

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

Research Project

Project/Area Number 16K12391
Research InstitutionChiba University

Principal Investigator

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

Co-Investigator(Kenkyū-buntansha) 葛岡 成晃  和歌山大学, システム工学部, 准教授 (60452538)
Project Period (FY) 2016-04-01 – 2019-03-31
Keywords形式化 / 情報理論
Outline of Annual Research Achievements

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

Current Status of Research Progress
Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

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

Strategy for Future Research Activity

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

  • Research Products

    (3 results)

All 2018 2017

All Journal Article (1 results) Presentation (1 results) (of which Int'l Joint Research: 1 results) Book (1 results)

  • [Journal Article] An application of universal FV codes to source coding allowing errors2017

    • Author(s)
      Shigeaki Kuzuoka
    • Journal Title

      IEICE Technical Report

      Volume: 2017-5 Pages: 25-30

  • [Presentation] On universal FV coding allowing non-vanishing error probability2017

    • Author(s)
      Shigeaki Kuzuoka
    • Organizer
      the 10th Asia-Europe Workshop on Information Theory (AEW10)
    • Int'l Joint Research
  • [Book] Coq/SSReflect/MathCompによる定理証明2018

    • Author(s)
      萩原 学、アフェルト・レナルド
    • Total Pages
      224
    • Publisher
      森北出版
    • ISBN
      978-4627062412

URL: 

Published: 2018-12-17  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi