議論の形式検証を実現する論理的手法の研究

Research Project

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 – 2024-03-31
Project Status	Granted (Fiscal Year 2022)
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	健全な議論進行においては、誤謬や詭弁などを極力検出して排除できる必要がある。前年度で行った追加研究テーマ（２）「並行的に進行する議論をモデル化する数学的な議論理論の構築・理論性質究明」で構築した議論モデルについて、健全な議論で満たされるべき、もしくは場合によっては満たされるべき、要件を20制定し、「要件が不成立＝詭弁」、とする形式的詭弁検出法を考案し定式化した。詳細:当該の議論モデルはグラフ構造部と意味構造部から成り、20の要件のうちの5つはグラフ構造のみにかかる要件、残りの15は意味構造に及ぶ要件となる。４つのグラフ構造に対する要件が満たされる場合には必ず8つの意味構造に及ぶ要件を成立される意味構造が存在し、その逆も成り立つことを証明した。構築した議論モデル並びに各要件をPythonで実装した。これによって、モデル化された議論中の詭弁の有無の自動検証を可能とした。各要件の検証にかかる計算複雑性も求めた。その結果であるが、定めた要件群を検証することは一般的に多項式時間で行えない。大規模議論に提案手法を応用する際には、当該の議論モデルを簡素化するもしくは抽象化などの手法を構築する必要がある。これについては今後研究を進めていき解決策を考案する予定である。人工知能の議論研究における本研究成果の位置付け：形式的な議論研究を進める数理議論分野においては、グラフ構造のみから推論を進める抽象議論と、意味構造から抽象議論を抽出する構造議論を中心に研究が進められている。前者においては、意見主張間の関係は与えられたものとみなされ、例えばグラフ上の批判関係が、意見主張の意味を考慮した際に本当に批判関係を成しているかを判断できない。後者では実際の議論上の意見主張間の繋がりが考慮されないに加え、ほぼ論理矛盾＝批判を押し通すため、現実の批判関係を反映できていない。本研究成果はこの部分の解決の道を示した
Current Status of Research Progress	Current Status of Research Progress 2: Research has progressed on the whole more than it was originally planned. Reason 本研究提案当初の計画案に追加した研究テーマを深掘りしたところ、議論進行をサポートする上で、健全な議論進行を妨げる「詭弁」を排斥する必要が明らかになった。そのため、詭弁を形式的に検証するに必要な要件を定め、詭弁の自動検出を行う方法論を構築するに至った。成果として、詭弁検出の要件を定めた。実装も終えた。要件成立の検証にかかる計算の複雑性も確認した。したがって、追加研究テーマに関して大幅な進歩が認められる。この追加の研究成果を議論遷移意味論に落とし込むことが重要になる。この部分を今年度の研究においての取り組みとする。
Strategy for Future Research Activity	上述の成果を踏まえ、議論遷移意味論および議論検証の枠組みの構築を進める予定である。