| Project/Area Number |
21K12028
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 61030:Intelligent informatics-related
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
蟻坂 竜大 京都大学, 情報学研究科, 講師 (00774580)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
伊藤 孝行 京都大学, 情報学研究科, 教授 (50333555)
川本 裕輔 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (60760006)
|
|---|
| Project Period (FY) |
2021-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2023: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2022: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2021: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | 詭弁検証 / 議論検証 / 数理議論 / 議論進行サポート / 形式検証 / 自動証明 / プログラム検証 / 信用 / separation logic |
|---|
| Outline of Research at the Start |
機械学習の手法を用いた議論AIの開発が進む中、AIの挙動が議論の趣旨に合致するか、その公正性・適切生を保障することが課題になってきている。現状、人が議論の社会実験を行い、それに基づいてAIの挙動を調整しているが、調整に係る人的コストは非常に大きく、汎用性の問題もある。そこで、AIの挙動の統制を自動化するために、本研究では、「議論検証」という、プログラム検証の枠組みと数理議論の枠組みを融合させる研究領域を創出する。具体的には、議論の仕様を任意に記述可能とする形式言語を導入し、議論が仕様に沿うかを自動で検証する手法を構築する。これを通して、AIの発言の公正性・適切性の自動検証を実現する。
|
| Outline of Annual Research Achievements |
誤謬や詭弁の検出手法に関して、議論ではしばしば統計を用いることも多く、健全な議論では統計に関わる誤謬を避ける必要がある。そこで、統計における誤謬の有無について推論するためのプログラム論理（BHL）を構築した。この研究成果は論文誌Artificial Intelligenceで発表した。
前年度までに構築した誤謬・詭弁検出のための議論モデルでモデル化された対話や議論に、通常数理議論で考察される容認意味論（議論中のどの主張を受け入れるかを決定するための意味論）を適用することで、その対話や議論中に生じる論理に依る誤謬・詭弁を検知することができる。しかし、従来の数理議論の容認意味論の定義方法では、主張の容認性を柔軟に決定することが難しく、議論のオーガナイザなどが自身の想定する議論進行形式に沿って自由に容認性を指定することができない。この問題を緩和するため、容認性をtuple relational calculus（部分的な一階述語論理）を用いて行い、柔軟な定義を可能にした。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
前年度に言及した遷移意味論の研究課題については、プログラム検証の理論に従って、統計における誤謬の有無について推論するためのプログラム論理（BHL）を構築したことで、成果がでている。論理に基づく誤謬・詭弁の検出に関わる論理的な手法の構築も行なった。さらに、誤謬・詭弁一般を扱う遷移意味論の構築も進んでおり、発表の用意を進めている。
|
| Strategy for Future Research Activity |
得られた研究成果を発表することを中心に行う。
ルクセンブルク大学との国際共同研究も開始した。（１）純粋に論理的な検証手法を言語モデルなどで置き換えて、詭弁検証にかかる計算量の問題を緩和する手法開発を進めている。（２）対話プロトコルに基づく形式対話理論の構築も進めている。
|
