論文の概要: Towards Bridging Formal Methods and Human Interpretability
- arxiv url: http://arxiv.org/abs/2506.09759v1
- Date: Wed, 11 Jun 2025 14:03:35 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-06-13 06:35:03.030666
- Title: Towards Bridging Formal Methods and Human Interpretability
- Title（参考訳）: ブリッジング形式法と人間の解釈可能性
- Authors: Abhijit Paul, Proma Chowdhury, Kazi Sakib,
- Abstract要約: ラベリード・トランジション・システムズの重要性にもかかわらず、これらの設計の人間の理解について事前の研究は行われていない。
我々は148 LTS の設計データセットを作成し、324 対の比較で48 をサンプリングし、Bradley-Terry モデルを用いてそれらをランク付けした。
その結果、Albinの複雑性(tau = 0.444$)、状態空間サイズ(tau = 0.420$)、サイクロマティック複雑性(tau = 0.366$)、冗長性(tau = 0.315$)はLTS設計の人間の理解を最も正確に反映していることがわかった。
- 参考スコア（独自算出の注目度）: 1.433758865948252
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Labeled Transition Systems (LTS) are integral to model checking and design repair tools. System engineers frequently examine LTS designs during model checking or design repair to debug, identify inconsistencies, and validate system behavior. Despite LTS's significance, no prior research has examined human comprehension of these designs. To address this, we draw on traditional software engineering and graph theory, identifying 7 key metrics: cyclomatic complexity, state space size, average branching factor, maximum depth, Albin complexity, modularity, and redundancy. We created a dataset of 148 LTS designs, sampling 48 for 324 paired comparisons, and ranked them using the Bradley-Terry model. Through Kendall's Tau correlation analysis, we found that Albin complexity ($\tau = 0.444$), state space size ($\tau = 0.420$), cyclomatic complexity ($\tau = 0.366$), and redundancy ($\tau = 0.315$) most accurately reflect human comprehension of LTS designs. To showcase the metrics' utility, we applied the Albin complexity metric within the Fortis design repair tool, ranking system redesigns. This ranking reduced annotators' comprehension time by 39\%, suggesting that metrics emphasizing human factors can enhance formal design interpretability.
- Abstract（参考訳）: ラベル付きトランジションシステム(LTS)は、モデル検査および設計修理ツールに不可欠なものである。
システムエンジニアは、モデルチェック中のLTS設計を頻繁に調べ、デバッグ、不整合の特定、システムの振る舞いの検証を行う。
LTSの重要性にもかかわらず、これらの設計の人間の理解について事前の研究は行われていない。
これを解決するために、私たちは、サイクロマティックな複雑さ、状態空間のサイズ、平均分岐係数、最大深さ、アルビンの複雑さ、モジュラリティ、冗長性の7つの主要な指標を特定し、従来のソフトウェアエンジニアリングとグラフ理論に基づいています。
我々は148 LTS の設計データセットを作成し、324 対の比較で48 をサンプリングし、Bradley-Terry モデルを用いてそれらをランク付けした。
KendallのTau相関分析により、Albin complexity(\tau = 0.444$), state space size(\tau = 0.420$), cyclomatic complexity(\tau = 0.366$),redundancy(\tau = 0.315$)はLTS設計の人間の理解を最も正確に反映していることがわかった。
メトリクスの実用性を示すために、Fortis設計修復ツールにAlbinの複雑性メトリクスを適用し、ランキングシステムを再設計した。
このランキングは、アノテータの理解時間を39 %削減し、人間の要因を強調する指標が形式的設計の解釈可能性を高めることを示唆している。
関連論文リスト
- Unveiling Hybrid Cyclomatic Complexity: A Comprehensive Analysis and Evaluation as an Integral Feature in Automatic Defect Prediction Models [0.5461938536945723]
本稿では,新しい複雑性指標であるHybrid Cyclomatic Complexity(HCC)の解析と,欠陥予測モデルの特徴としての有効性について述べる。
HCCメトリックとその2つのコンポーネントの比較研究、継承された複雑性とオブジェクト指向の文脈におけるクラスの実際の複雑さについて述べる。
論文 参考訳（メタデータ） (2025-04-01T07:07:17Z) - ZeroLM: Data-Free Transformer Architecture Search for Language Models [54.83882149157548]
現在の自動プロキシ発見アプローチは、検索時間の拡張、データの過度なオーバーフィットへの感受性、構造的な複雑さに悩まされている。
本稿では,効率的な重み統計によるモデルキャパシティの定量化を目的とした,新しいゼロコストプロキシ手法を提案する。
本評価は,FlexiBERT ベンチマークで Spearman's rho 0.76 と Kendall's tau 0.53 を達成し,このアプローチの優位性を示すものである。
論文 参考訳（メタデータ） (2025-03-24T13:11:22Z) - Integrating Expert Knowledge into Logical Programs via LLMs [3.637365301757111]
ExKLoPは、大規模言語モデルが専門家の知識を論理的推論システムに統合する方法を評価するために設計されたフレームワークである。
この能力は特にエンジニアリングにおいて有用であり、製造業者が推奨する運用範囲などの専門家の知識を、自動化された監視システムに直接組み込むことができる。
論文 参考訳（メタデータ） (2025-02-17T19:18:23Z) - SyMANTIC: An Efficient Symbolic Regression Method for Interpretable and Parsimonious Model Discovery in Science and Beyond [3.4191590966148824]
シンボリック回帰(SR)アルゴリズムであるSyMANTICを導入する。
Symanticは、多数の候補から低次元記述子を効率的に識別する。
我々はSyMANTICが既存のSR手法のコストのごく一部で類似またはより正確なモデルを明らかにすることを示す。
論文 参考訳（メタデータ） (2025-02-05T17:05:25Z) - Complexity in Complexity: Understanding Visual Complexity Through Structure, Color, and Surprise [6.324765782436764]
人間がどのように視覚の複雑さを知覚するかを理解することは、視覚認知において重要な研究領域である。
複雑性を正確にモデル化することは、これまで考えられていたほど単純ではなく、データセットのバイアスに対処するために、知覚的および意味的な要素を追加する必要がある。
我々のモデルは、解釈可能性を維持しながら予測性能を改善し、視覚的複雑さの認識と評価についてより深い洞察を提供する。
論文 参考訳（メタデータ） (2025-01-27T09:32:56Z) - AnalogXpert: Automating Analog Topology Synthesis by Incorporating Circuit Design Expertise into Large Language Models [10.986618360243526]
本稿では,実用的なトポロジ合成問題の解決を目的としたLLMベースのエージェントであるAnalogXpertを提案する。
まず、アナログトポロジをSPICEコードとして表現し、設計空間を減らすためにサブ回路ライブラリを導入する。
第2に、CoTと非コンテキスト学習技術を用いて、問題を2つのサブタスクに分解する。
第3に,LLMが初期設計の誤りを漸進的に修正できる証明読解戦略を導入する。
論文 参考訳（メタデータ） (2024-12-17T09:08:08Z) - Restore Anything Model via Efficient Degradation Adaptation [129.38475243424563]
RAMは、様々な劣化にまたがる固有の類似性を活用して、効率的で包括的な復元を可能にする統一された経路を取る。
RAMのSOTA性能はRAMのSOTA性能を確認し、トレーニング可能なパラメータで約82%、FLOPで約85%のモデルの複雑さを減少させる。
論文 参考訳（メタデータ） (2024-07-18T10:26:53Z) - Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
カリキュラムベースの論理認識型チューニングフレームワークであるLACTを提案する。
具体的には、任意の一階論理クエリをバイナリツリー分解によって拡張する。
広く使われているデータセットに対する実験では、LATは高度な手法よりも大幅に改善(平均+5.5% MRRスコア)し、新しい最先端技術を実現している。
論文 参考訳（メタデータ） (2024-05-02T18:12:08Z) - Computational-Statistical Gaps in Gaussian Single-Index Models [77.1473134227844]
単次元モデル(Single-Index Models)は、植木構造における高次元回帰問題である。
我々は,統計的クエリ (SQ) と低遅延多項式 (LDP) フレームワークの両方において,計算効率のよいアルゴリズムが必ずしも$Omega(dkstar/2)$サンプルを必要とすることを示した。
論文 参考訳（メタデータ） (2024-03-08T18:50:19Z) - Scalable Learning of Item Response Theory Models [48.91265296134559]
項目応答理論(IRT)モデルは、分類データから、$m$テスト項目の遅延困難特性とともに、$n$試験の潜時能力を評価することを目的としている。
我々はこれらのモデルの類似性をロジスティック回帰に利用し、コアセットと呼ばれる小さな重み付き部分集合を用いて正確に近似することができる。
論文 参考訳（メタデータ） (2024-03-01T17:12:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。