2020 Fiscal Year Research-status Report
数理議論学に基づく仕様書の不整合解消支援ツールの作成
| Project/Area Number |
19K11914
|
|---|
| Research Institution | Sendai National College of Technology |
|---|
Principal Investigator |
岡本 圭史 仙台高等専門学校, 総合工学科, 教授 (00308214)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
高井 利憲 奈良先端科学技術大学院大学, 先端科学技術研究科, 客員准教授 (10425738)
木藤 浩之 電気通信大学, 大学院情報理工学研究科, 客員研究員 (90705287)
|
|---|
| Project Period (FY) |
2019-04-01 – 2022-03-31
|
| Keywords | 数理議論学 / 数理論理学 / SMTソルバ / 仕様 / 品質向上 |
|---|
| Outline of Annual Research Achievements |
令和二年度の研究計画では，1)議論フレームワーク構築法の提案(令和二年度まで)，2)外延列挙法の提案(令和二年度まで)，および3)不整合解消支援手法の提案とツール試作・評価(令和三年度まで)の実施を計画していた．
1)議論フレームワーク構築法の提案に関しては，数理議論学に基づく手法や自然言語処理に基づく手法を検討した．特に自然言語処理を用いた仕様書中の攻撃関係抽出法を提案するために，BERT(Bidirectional Encoder Representations from Transformers)により仕様書の文の類似度計算を行い，手法の有用性を確認した．また仕様書中の不整合検出の準備として，単語レベルでの対義や類似・対義判定の前処理として有効な処理を調査した．
2)外延列挙法の提案に関しては，外延の一階述語論理の拡張を用いた記述法を提案した．いくつかの外延は一階述語論理の枠組み内で記述できることが知られているが，集合の極小性・極大性が定義に要求されているため，いくつかの外延は一階述語論理の枠組み内では記述できない．本研究では．外延記述を一階述語論理で記述可能な性質と記述可能でない極大性・極小性に分離して記述した（令和元年度成果）．この成果に基づき充足判定器SMTソルバを拡張し，４つの外延が列挙可能であることを示した（令和二年度成果）．この成果は国内会議等にて発表し，論文が掲載予定である．
3)不整合解消支援手法の提案とツール試作・評価に関しては，SMTソルバによる抽出・列挙ツールを試作した．今後試作予定の自然言語で記述された仕様書から議論フレームワークを構築するツールの試作と合わせることで，不整合解消支援手法を実現するツールとなる．議論フレームワーク構築ツールの調査段階で，仕様書独自のいくつかの課題を抽出した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究全体としての進捗状況は，自然言語処理用計算資源の問題により議論フレームワーク構築法の提案がやや遅れ気味であるが，全体的にはおおむね予定通りの進捗状況であった．
1)議論フレームワーク構築法の提案に関しては，本年度は数理議論学に基づく手法や自然言語処理に基づく手法を検討した．特に自然言語処理分野における類似・対義の判定が，仕様書における有用性を確認した．しかし３）の評価の結果，仕様書独自の課題（専門用語が多い，情報が階層化されている，学習用のデータが少ない等）があり，これらを解決するための前処理などの工夫が，より精度の高い類似・対義の判定には必要であることが分かった．
2)外延列挙法の提案に関しては，本年度は外延の一階述語論理の拡張を用いた記述法を提案した（令和元年度成果）．この成果である外延の記述法を基に，SMTソルバを拡張し，外延列挙法を提案した．
3)不整合解消支援手法の提案とツール試作・評価に関しては，SMTソルバの拡張を試作し，外延の抽出・列挙を行った．この成果と現在調査中の議論フレームワーク構築法（ツール）と組み合わせることで．不整合解消支援手法のための試作ツールとなる．また，議論フレームワーク構築ツールに関しては，一般的な文書に対する類似・対義の判定は十分であると考えられるが，前述した仕様書の独自性に起因する課題を克服する必要がある．
|
| Strategy for Future Research Activity |
令和三年度の研究計画では，1)議論フレームワーク構築法の提案(令和二年度まで)及び2)外延列挙法の提案(令和二年度まで)は前年度までに終了し，3)不整合解消支援手法の提案とツール試作・評価(令和三年度まで)を実施する．
1)議論フレームワーク構築法の提案に関しては，仕様書独自の課題（専門用語が多い，情報が階層化されている，学習用のデータが少ない等）があり，これらを解決するための前処理などの工夫が，より精度の高い類似・対義の判定には必要であることが分かった．これらの前処理のための工夫等を実装し，評価することで，より精度の高い議論フレームワーク構築法を提案する．
2)外延列挙法の提案に関しては，本年度は外延の一階述語論理の拡張を用いた記述法を提案した（令和元年度成果）．この成果である外延の記述法を基に，SMTソルバを拡張し，外延列挙法を提案した（令和二年度成果）．
3)不整合解消支援手法の提案とツール試作・評価に関しては，令和二年度の成果である２）外延列挙法の試作ツールに加え，1)議論フレームワーク構築法のツールを試作し，これらを合わせて不整合解消支援手法のためのツールとする．また各ツールの評価を継続して行い，より精度の高い不整合解消支援を提案する．
|
| Causes of Carryover |
コロナウィルスの世界的感染爆発により，国際会議や国際間での研究打合せが実現不可能となったため，旅費等が発生しなくなり，次年度使用額が生じた．他方，自然言語処理に基づく手法を実現・評価するために，自然言語処理モデルを構築・評価する環境が必要となった．次年度使用は，自然言語処理用計算機環境の整備及びオンライでの会議参加のための諸費用に使用する予定である．
|
