2018 Fiscal Year Annual Research Report
Automated Generation of No Logical Gap Readable Proof for Information Theory
| Project/Area Number |
16K12391
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
萩原 学 千葉大学, 大学院理学研究院, 准教授 (80415728)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
葛岡 成晃 和歌山大学, システム工学部, 准教授 (60452538)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | Coq / Coqtop / Proviola / Python / 定理証明 |
|---|
| Outline of Annual Research Achievements |
本研究の目標である、情報理論の情報源符号化定理の形式化を含んでいるCoq/SSReflectライブラリである infoTheo の .v ファイル群に対し、タクティク等を自然言語へ変換するソフトウェアの開発を進めた。
ソフトウェアは Python のスクリプトとして作成してきた。主なアイデアは、形式証明から自然言語へのデータベースの構築、および、形式証明の解析の組合せである。また、CoqとPython間のデータの橋渡しには、フリーソフトの proviola を参考にしてきた。これは標準出力とエラー出力をパイプとした、Coqの入力と出力をやりとりする手法である。
作成したソフトウェアは、研究体制（代表者、分担者）で協力し動作を確認してきた。動作環境が異なることで、機能の一部が正常に動作しない状況も確認した。これは、PythonとCoqのOSに依存した動作によるところが大きい。どのOSでも同一のもしくは同様の動作を実現するのは非常に困難である。Coqの入出力に対する操作に関するこのような知見は、本研究を経験しなければ得られなかったと感じている。
昨年度同様、.v ファイルの一部に対して、ある程度まで自然言語化出来たがすべてのファイルを完全に自然言語化するには、いくつかブレイクスルーや人力が必要である。検討の結果、自然言語化をスムースに実現するには、.vファイル作成時からフォーマット等のルールを定めて行うべきという知見に達した。
|
