Thesis
masterthesis
LLM によるコミット自動分類に基づいた 開発プロセスへの形式手法適用効果の分析
  • February 2026
  • 修士学位論文 / 京都工芸繊維大学 大学院工芸科学研究科 /
  • No URL available
Abstract

形式検証はソフトウェアの正しさを数学的に証明する手法であり,安全性が重要なシステムにおいて広く採用されている.しかし,形式検証プロジェクトの開発プロセスが通常プロジェクトとどのように異なるかについて,定量的な実証研究は不足している.本研究では,形式検証プロジェクト4 件(CompCert,seL4,HACL*,CakeML) および通常プロジェクト5 件から収集した計107,006 件のGit コミットを対象に,LLM ベースのConventional Commits の10 種のコミットタイプへの自動分類とノンパラメトリック統計検定を用いた比較分析を行った.分析の結果,形式検証プロジェクトではリファクタリングの頻度が通常プロジェクトの2.74 倍と顕著に高い一方,不具合修正やドキュメントの頻度が低いことが明らかになった.変更規模ではスタイル変更およびドキュメントで中程度の効果量が観察された.開発時間については全てのコミットタイプで形式検証プロジェクト群が相対的に短い方向に偏るが,これは分布構造の違いに起因しており,絶対的なコミット間隔の短さを直接示すものではない.これらの結果は,形式検証が修正保守を削減する一方で構造的保守を増加させ,テストとは補完関係にあることを示唆している.
Files

最終版
BibTeX

Copyright © 2025 omzn.aquatan.net a.k.a. Osamu Mizuno All rights reserved.

The publications displayed in this list is related to SEL@KIT members only.