2021 Fiscal Year Annual Research 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に日本語SNLIデータセットを用いて矛盾関係を学習させたモデルを使用した．
2)外延列挙法の提案に関しては，外延の一階述語論理の拡張を用いた記述法を提案した．いくつかの外延は一階述語論理の枠組み内で記述できることが知られているが，いくつかの外延は一階述語論理の枠組み内では記述できない．本研究では．外延記述を一階述語論理で記述可能な性質と記述可能でない極大性・極小性に分離して記述した．この成果に基づき充足判定器SMTソルバを拡張し，４つの外延が列挙可能であることを示した．外延列挙は，攻撃関係の数に依存して所要時間が増大するが，実際の仕様書では，それほど多くの不整合は含まれないと仮定できる．また，攻撃関係の数が少なくとも，仕様書内に分散して現れるため，不整合は検知・解消することは依然として困難である．
3)不整合解消支援ツールとして，試作済のSMTソルバによる抽出・列挙ツールと合わせて，自然言語で記述された仕様書から議論フレームワークを構築するツールを試作した．また，列挙された外延を基に仕様書をグラフとして表現することで，不整合解消を支援するツールを試作した．さらに試作したツールを簡易な仕様書に適用し，誤記による不整合を検出・解消支援できることを確認した．これらの成果は国内会議等にて発表し，論文が掲載予定である．
|
