| 研究課題/領域番号 |
16K12391
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
萩原 学 千葉大学, 大学院理学研究院, 准教授 (80415728)
|
|---|
| 研究分担者 |
葛岡 成晃 和歌山大学, システム工学部, 准教授 (60452538)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| キーワード | 形式化 / 情報理論 |
|---|
| 研究実績の概要 |
本研究の目標である、情報理論の情報源符号化定理の形式化を含んでいるCoq/SSReflectライブラリである infoTheo の .v ファイル群に対し、タクティク等を自然言語へ変換するソフトウェアの開発を進めている。ソフトウェアは Python のスクリプトとして作成してきた。主なアイデアは、形式証明から自然言語へのデータベースの構築、および、形式証明の解析の組合せである。また、CoqとPython間のデータの橋渡しには、フリーソフトの proviola を参考にしてきた。これは標準出力とエラー出力をパイプとした、Coqの入力と出力をやりとりする手法である。
作成したソフトウェアは、研究体制（代表者、分担者）で協力し動作を確認してきた。また、研究協力者である名古屋大学のガリグ氏にもデモンストレーションを行い、参考意見を頂いてきた。３人の動作環境が異なることで、機能の一部が正常に動作しない状況も確認した。これは、 Windows 版の Python のバグによるところが大きい。そのため、他の OS 等を中心として開発を進めている。ただし Windows版の開発を諦めたのではなく、 Windows 10の Windows Subsystem for Linux を利用して、実質的に Windows上で実行可能な状況にできている。
これらの積み重ねにより、.v ファイルの一部に対して、ある程度まで自然言語化出来てきたと言える。実際、 infoTheo の一部のファイルでは、ほぼ全て自動的に自然言語化できたものもある。一方、すべてのファイルを完全に自然言語化するには、いくつかブレイクスルーや人力が必要であると見込みが立ってきた。その理由は進捗状況で述べる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
infoTheoは多くのファイル群により構成されること、SSReflectベースで書かれているため、単一のタクティクと異なり、タクティカルの組み合わせにより、形式化された証明の表現が複雑であることが原因で、形式証明から自然言語への対応が複雑になっていることが判明した。
|
| 今後の研究の推進方策 |
情報源符号化定理の形式証明全体を自然言語化するのではなく、主要な補題・定理や定義等に絞って、自然言語化する方法を視野に入れている。
|
