Program Verification Techniques for the AI Era

AI时代的程序验证技术

基本信息

批准号：
20H05703
负责人：
小林直樹
金额：
$ 121.8万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (S)
财政年份：
2020
资助国家：
日本
起止时间：
2020-08-31 至 2025-03-31
项目状态：
未结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20H05703/
关键词：
プログラム検証高階モデル検査高階不動点論理機械学習

项目摘要

研究課題全体を(A)高階モデル検査をはじめとするプログラム検証理論・技術のさらなる発展、(B)プログラム検証への機械学習技術の応用、(C)質の変化したプログラムの検証手法、の3つの課題に分けて並行して研究を進めた。2021年度の主な研究実績（一部、繰越分として2022年度に実施した成果を含む）は以下のとおり。(A)プログラム検証技術の発展：高階モデル検査の一種である高階不動点論理HFL(Z)の真偽値判定の高速化のため、一階のケースにおいて有効な手法であるPDRと循環証明との間の理論的関係を明らかにした。さらに、リスト構造を扱うプログラムの検証のために、記号オートマトン的関係という概念を新たに導入し、それに基づいてリストに関する性質の自動推論手法の改良を行った。また、並行プログラムの検証手法として、π計算と呼ばれる並行計算モデルで記述された並行プログラムの停止性を逐次プログラムの停止性に帰着する手法を考案し、実装・評価を行った。(B)プログラム検証への機械学習技術の応用：プログラム検証において鍵となるループ不変条件等の発見のためにニューラルネットワークを用いる枠組み（NeuGus: Neural Network-Guided Synthesis）を考案・実装し、不動点論理ソルバの一種であるCHCソルバHoIceに組み込んでその有効性を確認した。(C)質の変化したプログラムの検証手法：ニューラルネットワークを組み込んだソフトウェアの検証に向け、(B)のNeuGuSの枠組みを利用して、ニューラルネットワークから通常のプログラムコンポーネントを合成する手法を考案し、その有効性を確認した。また、確率付きプログラムの検証のための基礎として、確率付き高階不動点論理について研究を行い、モデル検査が決定可能なクラスを明らかにした。

整个研究主题分为三个问题：（a）进一步开发程序验证理论和技术，包括高阶模型测试，（b）机器学习技术在程序验证中的应用，以及（c）验证方法用于更改质量计划，以及（c）研究是并行进行的。 2021财年的主要研究结果（包括2022财年的一些结果）如下：（a）计划验证技术的发展：为了加快对高阶固定点逻辑HFL（Z）的判断，这是一种高级模型检查的一种类型，我们已经阐明了PDR之间的理论关系，这是一个有效的证明方法，这是有效的方法，并且是一份有效的方法。此外，为了验证处理列表结构的程序，引入了符号自动机关系的概念，并基于此，对列表属性的自动推理方法进行了改进。此外，作为验证并行程序的一种方法，设计了一种方法来减少称为π计算的并行计算模型中描述的并行程序的垂直性，以使得顺序程序的可伸缩性，并实现和评估。（b）设计并实施了机器学习技术在程序验证中：使用神经网络（Neugus）的框架在程序验证中发现关键的循环不变条件，并将其纳入CHC求解器Hoice（一种定点逻辑求解器）中，以确认其有效性。（c）验证质量不同的程序的方法：为了验证包含神经网络的软件，我们设计了一种使用Neugus框架（b）中的Neugus框架从神经网络中合成常规程序组件的方法，并确认了其有效性。此外，作为概率验证程序的基础，我们以概率进行了有关高阶固定点逻辑的研究，并揭示了可以确定模型检查的类。