AIを含むソフトウェアのための形式検証手法

项目来源

日本学术振兴会基金(JSPS)

项目主持人

末永幸平

项目受资助机构

京都大学

项目编号

25H01113

立项年度

2025

立项时间

未公开

研究期限

未知 / 未知

项目级别

国家级

受资助金额

59800000.00日元

学科

情報科学、情報工学およびその関連分野

学科代码

未公开

基金类别

基盤研究(A)

关键词

形式検証 ; 人工知能 ; ソフトウェア ;

参与者

和賀正樹;五十嵐淳;池渕未来;関山太朗

参与机构

京都大学,情報学研究科;国立情報学研究所,アーキテクチャ科学研究系

项目标书摘要:Outline of Research at the Start:AIを用いたソフトウェアは,AIモジュールのブラックボックス性のために従来の形式検証手法をそのまま適用することが困難である.このようなソフトウェア安全性を向上させるための形式検証手法の確立に向けて,内部動作が明らかではなく,期待される動作の形式的仕様記述も困難であるモジュールを含むシステムの動作を検証するための手法を研究する.より具体的には,AIモジュールを含むソフトウェアへの適用を志向した,形式的仕様が与えられていないブラックボックスな部品を含むソフトウェアのための形式検証手法を研究する。

  • 排序方式:
  • 1
  • /
  • 1.Active Learning ofSymbolic Mealy Automata

    • 关键词:
    • Finite automata;Set theory;Active Learning;Active-learning algorithm;Automaton learning;Finite set;Learn+;Mealy automatons;Multiple outputs;Output functions;Symbolic automaton;Under-approximation
    • Irie, Kengo;Waga, Masaki;Suenaga, Kohei
    • 《22nd International Colloquium on Theoretical Aspects of Computing, ICTAC 2025》
    • 2026年
    • November 24, 2025 - November 28, 2025
    • Marrakesh, Morocco
    • 会议

    We propose ΛM∗—an active learning algorithm that learns symbolic Mealy automata, which support infinite input alphabets and multiple output characters. Each of these two features has been addressed separately in prior work. Combining these two features poses a challenge in learning the outputs corresponding to potentially infinite sets of input characters at each state. To address this challenge, we introduce the notion of essential input characters, a finite set of input characters that is sufficient to learn the output function of a symbolic Mealy automaton. ΛM∗ maintains an underapproximation of the essential input characters and refines this set during learning. We prove that ΛM∗ terminates under certain assumptions. Moreover, we provide upper and lower bounds for the query complexity. Their similarity suggests the tightness of the bounds. We empirically demonstrate that ΛM∗ is i) efficient regarding the number of queries on practical benchmarks and ii) scalable according to evaluations with randomly generated benchmarks. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.

    ...
  • 排序方式:
  • 1
  • /