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

2020 Fiscal Year Research-status Report

数理議論学に基づく仕様書の不整合解消支援ツールの作成

Research Project

Project/Area Number 19K11914
Research InstitutionSendai 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ソルバを拡張し,4つの外延が列挙可能であることを示した(令和二年度成果).この成果は国内会議等にて発表し,論文が掲載予定である.
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)議論フレームワーク構築法の提案に関しては,本年度は数理議論学に基づく手法や自然言語処理に基づく手法を検討した.特に自然言語処理分野における類似・対義の判定が,仕様書における有用性を確認した.しかし3)の評価の結果,仕様書独自の課題(専門用語が多い,情報が階層化されている,学習用のデータが少ない等)があり,これらを解決するための前処理などの工夫が,より精度の高い類似・対義の判定には必要であることが分かった.
2)外延列挙法の提案に関しては,本年度は外延の一階述語論理の拡張を用いた記述法を提案した(令和元年度成果).この成果である外延の記述法を基に,SMTソルバを拡張し,外延列挙法を提案した.
3)不整合解消支援手法の提案とツール試作・評価に関しては,SMTソルバの拡張を試作し,外延の抽出・列挙を行った.この成果と現在調査中の議論フレームワーク構築法(ツール)と組み合わせることで.不整合解消支援手法のための試作ツールとなる.また,議論フレームワーク構築ツールに関しては,一般的な文書に対する類似・対義の判定は十分であると考えられるが,前述した仕様書の独自性に起因する課題を克服する必要がある.

Strategy for Future Research Activity

令和三年度の研究計画では,1)議論フレームワーク構築法の提案(令和二年度まで)及び2)外延列挙法の提案(令和二年度まで)は前年度までに終了し,3)不整合解消支援手法の提案とツール試作・評価(令和三年度まで)を実施する.
1)議論フレームワーク構築法の提案に関しては,仕様書独自の課題(専門用語が多い,情報が階層化されている,学習用のデータが少ない等)があり,これらを解決するための前処理などの工夫が,より精度の高い類似・対義の判定には必要であることが分かった.これらの前処理のための工夫等を実装し,評価することで,より精度の高い議論フレームワーク構築法を提案する.
2)外延列挙法の提案に関しては,本年度は外延の一階述語論理の拡張を用いた記述法を提案した(令和元年度成果).この成果である外延の記述法を基に,SMTソルバを拡張し,外延列挙法を提案した(令和二年度成果).
3)不整合解消支援手法の提案とツール試作・評価に関しては,令和二年度の成果である2)外延列挙法の試作ツールに加え,1)議論フレームワーク構築法のツールを試作し,これらを合わせて不整合解消支援手法のためのツールとする.また各ツールの評価を継続して行い,より精度の高い不整合解消支援を提案する.

Causes of Carryover

コロナウィルスの世界的感染爆発により,国際会議や国際間での研究打合せが実現不可能となったため,旅費等が発生しなくなり,次年度使用額が生じた.他方,自然言語処理に基づく手法を実現・評価するために,自然言語処理モデルを構築・評価する環境が必要となった.次年度使用は,自然言語処理用計算機環境の整備及びオンライでの会議参加のための諸費用に使用する予定である.

  • Research Products

    (6 results)

All 2020

All Journal Article (4 results) (of which Open Access: 4 results,  Peer Reviewed: 1 results) Presentation (2 results) (of which Int'l Joint Research: 1 results)

  • [Journal Article] Bayesian Entailment Hypothesis: How Brains Implement Monotonic and Non-monotonic Reasoning2020

    • Author(s)
      Hiroyuki Kido
    • Journal Title

      CoRR

      Volume: abs/2005.00961 Pages: -

    • Open Access
  • [Journal Article] Bayes Meets Entailment and Prediction: Commonsense Reasoning with Non-monotonicity, Paraconsistency and Predictive Accuracy2020

    • Author(s)
      Hiroyuki Kido and Keishi Okamoto
    • Journal Title

      CoRR

      Volume: abs/2012.08479 Pages: -

    • Open Access
  • [Journal Article] Expressing Dung’s Extensions as FO-Formulas to Enumerate Them with an SMT Solver2020

    • Author(s)
      Keishi Okamoto, Hiroyuki Kido, Toshinori Takai
    • Journal Title

      京都大学数理解析研究所講究録

      Volume: 2170 Pages: 64-72

    • Open Access
  • [Journal Article] A Tool Generating a C# Code with Contracts of Code Contracts from a VDM++ Model with Conditions2020

    • Author(s)
      Yuma Yamano, Toshihiko Ando and Keishi Okamoto
    • Journal Title

      International Journal of Software Engineering (IJSE)

      Volume: 8 Pages: 27-39

    • Peer Reviewed / Open Access
  • [Presentation] Continuous modeling supports from business analysis to systems engineering in IoT development2020

    • Author(s)
      Toshinori Takai, Katsutoshi Shintani, Hideki Andoh and Hironori Washizaki
    • Organizer
      5th International Conference on Enterprise Architecture and Information Systems (EAIS 2020)
    • Int'l Joint Research
  • [Presentation] Enumeration of Dung ’s Extensions with an SMT Solver2020

    • Author(s)
      Keishi Okamoto
    • Organizer
      RIMS Model Theory Workshop 2020

URL: 

Published: 2021-12-27  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi