| 研究課題/領域番号 |
20H05703
|
|---|
| 研究種目 |
基盤研究(S)
|
| 配分区分 | 補助金 |
|---|
| 審査区分 |
大区分J
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
|
|---|
| 研究分担者 |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
塚田 武志 千葉大学, 大学院理学研究院, 准教授 (50758951)
吉仲 亮 東北大学, 情報科学研究科, 准教授 (80466424)
海野 広志 東北大学, 電気通信研究所, 教授 (80569575)
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476)
佐藤 一誠 東京大学, 大学院情報理工学系研究科, 教授 (90610155)
佐藤 亮介 東京農工大学, 学内共同利用施設等, 准教授 (10804677)
|
|---|
| 研究期間 (年度) |
2020-08-31 – 2025-03-31
|
| 研究課題ステータス |
交付 (2024年度)
|
| 配分額 *注記 |
190,320千円 (直接経費: 146,400千円、間接経費: 43,920千円)
2024年度: 39,260千円 (直接経費: 30,200千円、間接経費: 9,060千円)
2023年度: 39,260千円 (直接経費: 30,200千円、間接経費: 9,060千円)
2022年度: 39,260千円 (直接経費: 30,200千円、間接経費: 9,060千円)
2021年度: 39,780千円 (直接経費: 30,600千円、間接経費: 9,180千円)
2020年度: 32,760千円 (直接経費: 25,200千円、間接経費: 7,560千円)
|
|---|
| キーワード | プログラム検証 / 高階モデル検査 / 高階不動点論理 / 機械学習 |
|---|
| 研究開始時の研究の概要 |
プログラム検証とは、プログラムが正しく振る舞うかどうかを実行前に網羅的に検証する技術であり、ソフトウェアの信頼性向上のために欠かせないものである。本研究課題では、近年の機械学習技術の台頭とそれに伴うコンピュータによって制御されたシステムの社会への普及を踏まえ、（１）代表者らがこれまで研究を進めてきた高階モデル検査などの自動プログラム検証技術や理論をさらに発展させるとともに、（２）プログラム検証技術のさらなる飛躍のために機械学習技術を活用し、さらに（３）機械学習技術の台頭に伴うソフトウェアの質と量の変化に対応するための、新たなプログラム検証技術の確立を目指す。
|
| 研究実績の概要 |
研究課題全体を(A)高階モデル検査をはじめとするプログラム検証理論・技術のさらなる発展、(B)プログラム検証への機械学習技術の応用、(C)質の変化したプログラムの検証手法、の3つの課題に分けて並行して研究を進めた。2022年度の主な研究実績(一部、繰越分として2023年度に実施した成果を含む)は以下のとおり。
(A)プログラム検証技術の発展: 高階モデル検査の一種である高階不動点論理HFL(Z)の真偽値判定の高速化のため、さまざまな改良方法について研究を行った。具体的には、（１）不動点論理式の展開畳み込み変換を非同期に行うための拡張、（２）最小不動点演算子の近似によるHFL(Z)論理式のνHFL(Z)論理式（最大不動点のみからなるHFL(Z)論理式）への変換、（３）不動点論理式の証明側と反証側の情報共有による高速化、などについて研究を行った。また、扱えるプログラム機能の拡張の研究の一環として、代数的データ構造や代数的エフェクト、スマートコントラクトなどのためのプログラム検証手法の改良、および新しい手法の考案・実装を行った。
(B)プログラム検証への機械学習技術の応用:プログラム検証において鍵となるループ不変条件等の発見のためにニューラルネットワークを用いる枠組みNeuGuS (Neural Network-Guided Synthesis) を拡張し、リストに関する再帰的述語をニューラルネットワークを用いて合成する手法を考案・実装した。
(C)質の変化したプログラムの検証手法: ニューラルネットワークなどを用いた機械学習プログラムにおける、テンソルデータの処理の整合性を静的に検証するため、漸進的型システムと詳細型を組み合わせた型システムを構築・実装し、その有効性を確認した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究実績の概要に述べた通り順調に研究成果が出ており、一流の雑誌や国際会議に論文を発表している。
|
| 今後の研究の推進方策 |
検証対象のプログラムのクラスを拡張するとともに、機械学習技術のさらなる応用を探っていく。
|
| 評価記号 |
中間評価所見 (区分)
A: 研究領域の設定目的に照らして、期待どおりの進展が認められる
|
