arXiv雑要約
プログラム - 2026/07/31 公開
実践におけるプロンプト連鎖:自動化された学術レポート生成の事例研究 [cs.CL, cs.AI, cs.CE, cs.DL, cs.SE]目的:学術レポートの自動生成手法
- 学術論文の爆発的な増加に対応するため,情報統合の自動化が不可欠である。
- 単純なプロンプトでは,複雑な情報統合タスクに必要な信頼性と品質が不足する。
- 複数段階のプロンプト連鎖による,より信頼性の高い生成手法を確立すること。
- 提案手法であるプロンプト連鎖は,単発プロンプトと比較して100%の成功率を達成し,信頼性で顕著な差を示した。
- 品質評価では,ROUGE-L F1スコアで優位性を示し(0.507 vs 0.486),特に適合率の高さが貢献した。
- 複雑な生成タスクにおいて,プロンプト連鎖は単一プロンプトよりも依存性が高く,効果的な手法である。
OwlPath:LLMによるバグ修正のための損失のない知識圧縮 [cs.SE]目的:LLMを用いたバグ修正における知識圧縮手法
- LLMは強力だが,扱うことのできるコンテキスト長には限界があるため,効率的な情報提供が重要である。
- 従来のコード検索手法はテキストとして扱うため,複雑な依存関係の解決に時間がかかるという課題がある。
- ソースコードをOWL2オントロジーに変換することで,構造的クエリを効率化し,必要なコード断片のみを抽出する。
- OwlPathは,既存のCodeGraphと比較して,厳密な適用率で優位性を示し,トークン使用量と実行時間を削減した。
- オフライン検索テストでは,リコール率が2.06倍に向上し,ヒット率も大幅に改善された。
- 構造的検索ベンチマークにおいて,リコール率は4.4%から28.8%へと大幅に向上し,高い精度を達成した。
コンテキストファイルはコーディングエージェントに役立つか?実リポジトリにおける二エージェントアブレーションスタディ [cs.SE, cs.AI]目的:コーディングエージェントの性能に対するコンテキストファイルの有効性の検証
- AIコーディングエージェントの活用は,ソフトウェア開発の効率化に不可欠である。
- コンテキストファイルの有効性に関する証拠は一貫しておらず,その効果に疑問が残る。
- エージェントがリポジトリの知識不足で失敗するのではなく,実装スキルに問題があることを明らかにすること。
- コンテキストファイルの注入戦略は,Claude CodeおよびCodexのいずれのエージェントにおいても,正答率に有意な影響を与えなかった。
- 失敗モードの分析から,エージェントの失敗は機能設計やパターン選択といった実装スキルに起因することが示された。
- タスクの難易度はエージェントによって異なり,先行研究で矛盾が生じた原因として,エージェント固有の得意分野が考えられる。
CircuitProver:再利用可能な回路証明ライブラリによる,ハードウェア検証のためのエージェント型Lean 4定理証明 [cs.LO, cs.AR]目的:ハードウェア検証のための,エージェント型定理証明システムの開発と評価
- 現代の集積回路は複雑化の一途を辿っており,その機能検証は重要な課題となっている。
- 従来のモデル検査法では,検証結果のみが得られ,証明の根拠が再利用されない。
- 本研究は,証明の蓄積とパラメータ化された検証を可能にし,ハードウェア検証の効率化を目指す。
- CircuitProverは,パラメータ化されたハードウェア設計と自然言語仕様をLean 4モデルに自動変換する。
- 本フレームワークは,検証タスクにおいて全てのベンチマークを成功裏に証明した。
- 蓄積された証明知識により,関連する検証タスクでの証明長を16.3%,検証時間を23.2%削減した。
BMOA:コンパイラによる数値ずれの要因帰属のためのベースライン-メカニズム-結果の帰属 [cs.PL]目的:コンパイラによる数値ずれの診断と要因分析
- 科学計算の信頼性確保は重要であり,数値計算の正確性が不可欠である。
- コンパイラの最適化が数値計算に影響を与え,正確性を損なう可能性がある。
- 数値ずれの原因を特定し,コンパイラの挙動と計算結果の関係を明確にすること。
- BMOAフレームワークは,数値ずれの診断を,ベースライン,メカニズム,結果の3つの要素に分離する。
- 実験の結果,ベースラインの選択が診断結果に影響を与え,数値ずれが必ずしも精度低下を意味するわけではないことが示された。
- BMOAは,監査可能な証拠に基づいた記録を作成し,コンパイラに配慮した数値的な正しさを検証するための基盤を提供する。
パフォーマンスフィードバックからの強化学習によるコード生成 (RLPF) [cs.LG, cs.SE]目的:コード生成におけるパフォーマンスの最適化
- コード生成AIの性能向上は,ソフトウェア開発の効率化に不可欠である。
- 既存手法では,コードの正当性のみが重視され,実行速度の最適化が課題である。
- 実行速度を考慮した学習手法を確立し,より効率的なコード生成を実現すること。
- RLPFは,実行結果を段階的な報酬に変換することで,効率的な学習を可能にした。
- PerfCodeBenchデータセットでの実験により,正しく実行可能なコードの生成率が大幅に向上した。
- 学習済みモデルは,他のオープンソースモデルと同等の性能を示し,EffiBench-Xへの応用も確認された。
残差のベンチマーク:マッチングされた短期タスクのパフォーマンスを超えた長期評価がもたらすもの [cs.LG, cs.AI, cs.SE]目的:長期タスクにおけるエージェントの失敗要因の分析
- AIエージェントの複雑なタスク遂行能力評価は,実用化に向けて不可欠である。
- 長期タスクの評価では,単純にパフォーマンスが低下するだけで,その原因が不明瞭になりがちである。
- 短期タスクの予測と長期タスクの実際の成功率の差を「ホライズン残差」として定量化し,問題点を明確化する。
- 長期タスクのパフォーマンス低下は,単なるエラーの積み重ねだけでなく,履歴や環境変化による影響も考慮する必要がある。
- 「ホライズン残差」を用いることで,長期タスクの失敗が予測との乖離として明確に示され,さらなる分析を促す。
- ベンチマークは,エージェント設定やステージ選択方法を事前に明示し,公平な比較を可能にする必要がある。
PIE-APT: 時間的計画と矛盾検出のための統一的フレームワーク - 増分直接導出アブダクションによる [cs.AI, cs.LO]目的:動的知識グラフにおける時間的計画と矛盾検出
- 知識グラフは,現実世界の複雑な情報を表現する上で不可欠である。
- 不完全な知識や動的な変化への対応が困難である。
- 効率的なアブダクションと時間的推論を統合することで,その課題を克服する。
- 本研究では,記述論理上で動作するPIE-AbducerとPIE-APTという統合的フレームワークを提案する。
- PIE-Abducerは,従来の最小ヒット集合列挙を回避し,直接反駁の結果を利用して欠損前提を抽出する。
- 実験結果は,提案手法が古典的プランナーよりも優れており,アブダクションによる知識拡張において,最小ヒット集合に忠実なベースラインよりも定量的に優れていることを示している。
AgentS4D:LLMベースのワークスペースエージェントの実行ライフサイクルにおける実行時リスクのベンチマーク [cs.SE]目的:LLMベースのワークスペースエージェントにおける実行時安全性の評価
- 近年,LLMを活用したエージェントが普及し,その安全性確保が重要課題となっている。
- 既存の安全性評価は限定的であり,リスク発生源,行動誘発,悪影響,証拠の関連性が明確でない。
- 実行ライフサイクル全体を通して,リスクを網羅的に評価するフレームワークを確立すること。
- AgentS4Dは,リスク発生源,誘導戦略,標的となる悪影響を組み合わせた,ライフサイクル全体を通じた実行時安全性評価ベンチマークである。
- 20通りの構成で6,560回の実行を行った結果,4,461回 (68.0%) で事前に定義された安全でない信号がトリガーされた。
- タスクの完了だけでは実行時の安全性を保証できず,リスクの一側面だけをテストしても弱点を隠蔽する可能性があることが示された。
講義ノートからLeanへ:確率論の教科書を形式化する [cs.LO]目的:確率論の教科書の形式化
- AIの数学補助が発展する中で,数学的根拠の信頼性が重要となる。
- 大規模言語モデルの出力の検証と,数学的知識の再利用が課題である。
- 教科書の内容を形式化し,AIによる数学の信頼性を高める。
- 確率論の教科書「測度論的確率論」をLeanで形式化し,検証可能な数学的基盤を構築した。
- 教科書と既存のMathlibライブラリ間のインターフェースを整備し,再利用性を高めた。
- 形式化された教科書が,教育,数学的仮定の明確化,信頼性の高いAI支援数学に貢献することを示唆した。
人間とロボットのチームワーク要件の分類 [cs.SE]目的:人間とロボットのチームワーク要件
- 安全性が求められる分野で,人間とロボットの協働が不可欠となっている。
- 人間とロボットの連携に関する要件が散在しており,統一的な枠組みが存在しない。
- 人間とロボットの協働における要件の体系化を目指す。
- 学術文献や業界標準等の分析から361の要件を抽出し,二層構造の分類体系を構築した。
- この分類体系は,情報提供,関係制御,意思決定支援,安全機構,性能監視,基盤システム能力の6つのカテゴリと21のサブカテゴリを含む。
- 専門家による評価と,別途収集した448要件への適用により,分類体系の有効性が確認された。
SIGIL:エージェントのスキルを型付きハーネスにコンパイル [cs.SE]目的:エージェントのスキルを型付きハーネスに変換する手法
- AIエージェントの能力向上には,柔軟なスキル獲得が不可欠である。
- プロシージャ記述のスキルは実行時に解釈され,検証が省略される場合がある。
- プロシージャをプログラム構造化するハーネスの自動生成を目指す。
- SIGILは,プロシージャ形式のスキルを型付きハーネスにコンパイルする。
- コンパイルされたハーネスは,必要なステップの実行率が86%に向上した。
- モデル世代に関わらず,一貫して高い実行率を維持することが示された。
TrustChain-Review: 信頼性の高いAI支援コードレビューのためのリスク適応型ブロックチェーンおよびゲーム理論的フレームワーク [cs.SE]目的:AI支援コードレビューにおける信頼性向上
- ソフトウェア開発の効率化が求められる中で,AIの活用が不可欠となっている。
- AI支援コードレビューでは,責任の所在が不明確になりやすく,品質管理が課題である。
- ブロックチェーンとゲーム理論を用いて,より信頼性の高いコードレビューを実現すること。
- 完全な証拠記録構成は,レピュテーション,信頼性,検出能力において最も高い性能を示した。
- リスク適応型構成は,証拠記録構成と比較してガバナンスコストを削減し,費用対効果を向上させた。
- 高リスクな変更には厳格なガバナンスが適しており,日常的な変更には選択的なガバナンスが現実的である。
プロパティ誘導回帰探索による意味的誤り検出 [cs.SE]目的:意味的誤り検出のためのプロパティ誘導回帰探索
- ソフトウェアの信頼性確保において,テストは不可欠であり,特に複雑なプログラム構造を効率的に検証することが重要である。
- 従来の回帰テスト生成は,既存の誤りを期待される動作とみなしてしまうという課題がある。
- 本研究は,意図に基づいたプロパティをテスト生成に組み込み,より深い状態への到達と誤りの検出を目指す。
- PROGRESSは,回帰テスト生成と比較して,現在のバージョンにおけるバグを328/562個(58%)検出した。
- PROGRESSは,到達困難なプロパティの事前条件を70/150個満たしたのに対し,スタンドアロンのjqwikは18個にとどまった。
- ドキュメントや呼び出し元/呼び出し先コンテキストが,有効な実行可能プロパティ生成に不可欠であることが示された。
バックログ項目からセキュリティガイダンスへ:継続的なセキュリティコンプライアンスに向けて [cs.SE, cs.CR]目的:セキュリティ関連バックログ項目の検出と,関連するセキュリティ要件へのリンク
- 規制対象分野では,開発ライフサイクル全体を通してセキュリティを考慮する必要があり,その重要性は増している。
- バックログ項目にセキュリティ要件を明示的に記述することが難しく,エンジニアは推測に頼らざるを得ない。
- バックログ項目のセキュリティ関連性を自動的に検出し,適切な要件を提示することで,開発者の支援を目指す。
- セキュリティ専門家によるラベル付けデータセットを公開し,セキュリティ関連性の判断において高い合意率(Fleiss' κ=0.787)が得られた。
- セキュリティ関連性分類器は,F2スコア0.774を達成し,既存の古典的な機械学習モデルやオープンソースGPTモデルと同等またはそれ以上の性能を示した。
- RAGパイプラインの予備的な評価では,提示されたセキュリティ条項の半数が,関連性4/5以上と評価され,実用的な可能性が示唆された。
自由な拡張型 [cs.LO, math.AT, math.CT, math.LO]目的:依存型理論における拡張型の統一的枠組みの構築
- 型理論は,数学基礎や計算機科学における厳密なモデリングに不可欠であり,その拡張は表現力を高める。
- 既存の拡張型はそれぞれ異なる枠組みで定義されており,統一的な理解と比較が困難である。
- 二段階型理論を用いて,既存の拡張型を統一的に定義し,型理論間の比較を可能にすること。
- 既存の拡張型(経路型,名前付与型,制御アンフォールド)が,二段階型理論において一貫して定義可能であることが示された。
- 二段階型理論はHoTTの標準モデルを自動的にモデル化し,保守性を保つ。
- 立方体接着とユニバレンスが同値であることが証明され,立方体型理論の保守性に関する考察に繋がった。
SWE-NFI:非機能改善のためのコーディングエージェントの研究とベンチマーク [cs.SE, cs.AI]目的:非機能改善を行うコーディングエージェントの評価基準
- ソフトウェア開発において,機能修正だけでなく品質向上が不可欠である。
- 既存のベンチマークは機能要件に偏っており,品質改善の評価が困難である。
- 非機能改善能力を定量的に評価し,エージェント開発の指針を示す。
- SWE-NFIベンチマークは,実際のオープンソースPythonプロジェクトのプルリクエストから188のタスクを構築している。
- 最先端のエージェントは機能要件で70.0%の正答率を達成するも,非機能改善能力では人間開発者に劣る。
- 特に構造的改善において顕著な差が見られ,エージェントのスコアは0.0〜1.3に対し,人間のスコアは1.5である。
非シグナリング支援を持つブロードキャストチャネルの容量領域 [cs.IT, math.IT, quant-ph]目的:非シグナリング支援下におけるブロードキャストチャネルの容量領域の完全な特徴付け
- 通信システムの効率化において,ブロードキャストチャネルの容量限界の理解は不可欠である。
- 従来のブロードキャストチャネルの容量領域は完全には解明されておらず,性能向上の余地がある。
- 本研究は,非シグナリング支援を利用することで,ブロードキャストチャネルの容量領域を明確化することを目指す。
- 非シグナリング支援を持つブロードキャストチャネルの容量領域は,佐藤領域と一致することが示された。
- 佐藤領域は,各部分集合における受信機の完全な協調を仮定した和レート上限によって定義される。
- この結果は,非シグナリング支援がブロードキャストチャネルの性能向上に役立つことを示唆する。
Tweeスタイル目標指向性に関する実験 [cs.LO, cs.SC]目的:飽和推論における次に行う節の選択戦略
- 定理証明は,数学的推論の自動化において不可欠であり,その効率性が重要である。
- 従来の節選択戦略では,効率的な証明探索が困難な場合がある。
- 本研究では,Tweeの考え方を拡張し,より効率的な節選択を実現することを目指す。
- 本研究では,Tweeの考え方を一階述語論理に適用し,共有項に基づく新たな実装を提案した。
- 提案手法は,問題を変形するために等式定義を追加するアプローチを採用している。
- 実験結果から,提案手法が非常に有望な結果を示すことが明らかになった。
展開なしの認証済みシーケンシャルスイープ [cs.RO, cs.CL, cs.LO]目的:リタイミング後の追加シーケンシャル再合成ステップの検証
- 回路設計の最適化において,リタイミングは性能向上に不可欠である。
- 既存の検証ツールでは,リタイミングと再合成を組み合わせた検証が困難である。
- リタイミングおよび強力なシーケンシャル再合成下での等価性検証を効率的に実現する。
- 本研究では,IC3ベースの手法を用いて,リタイミングを前処理とし,シミュレーションにより仮説的な不変条件を生成する。
- 提案手法は,リタイミングおよび任意のシーケンシャル再合成の下での等価性検証を効率的に行い,証明書も生成する。
- オープンソース回路設計の検証において,最新のHardware Model Checking Competition優勝者のツールを大きく上回る性能を示した。
ThreatForest:プラグ可能なTTPフレームワークマッピングによるマルチエージェント攻撃ツリー生成 [eess.SY, cs.SY, cs.CR, cs.AI, cs.CL, cs.SE]目的:クラウドネイティブアーキテクチャに対する攻撃ツリーの自動生成と,それに対応する対策の提示
- ソフトウェアの安全な開発には脅威モデリングが不可欠であり,クラウド環境でのセキュリティ確保は重要である。
- クラウドネイティブアーキテクチャの脅威モデリングは手動では時間がかかり,専門知識を持つ人材が不足している。
- ソースコードから攻撃ツリーを生成し,TTPフレームワークに基づいて具体的な対策を提示することで,脅威モデリングの効率化を目指す。
- ThreatForestは,ソースコードリポジトリから攻撃ツリーを生成し,MITRE ATT&CK等のTTPフレームワークにマッピングするマルチエージェントシステムである。
- 脅威モデリングのプロセスを段階的なエージェントパイプラインに分解し,人間による検証ポイントを設けることで,信頼性を高めている。
- TTPマッピングの精度がボトルネックであり,特に埋め込みエンコーダの性能が課題であることが示された。
LimICE:効率的なループ不変条件推論のためのLLMをICEフレームワークに統合 [cs.SE]目的:ループ不変条件の効率的な推論
- プログラム検証における基礎問題であり,ソフトウェアの信頼性向上に不可欠である。
- 機械学習の活用が進むも,複雑な問題に対する完全な不変条件の生成が困難である。
- LLMとICE-DTを組み合わせ,より多くの問題を迅速に解決することを目指す。
- 提案手法LimICEは,線形ベンチマーク367件中349件を平均15.2秒で解決した。
- 非線形ベンチマーク50件中47件を平均8.8秒で解決し,最先端のLLMベースラインを12-24%上回る性能を示した。
- 従来の非LLMベースラインと比較しても,線形・非線形ベンチマークともに優れた結果が得られた。
HALO:安全なエージェント実行のための局所的義務による異種承認 [cs.AI, cs.RO, cs.SE]目的:異種応答におけるコンポーネントのサポート維持と,依存関係を考慮した承認プロトコル
- エージェントAIの発展に伴い,多様な応答形式が求められる状況が生じている。
- 応答の各コンポーネントが独立して変化し,依存関係が崩れるリスクがある。
- 応答全体を拒否することなく,依存関係を維持しつつ安全に実行可能なコンポーネントを選別する。
- HALOは,96件の承認期待と20件のプロトコルテスト全てを満たした。
- 構造化された応答再生実験では,248/248のサポートされたコンポーネントを維持し,うち128/128は無関係な変更の影響を受けなかった。
- PX4/Gazeboセッションでは,全ての古いルートをブロックし,対応する古いセットポイントは観測されず,全ての新しい回復に成功した。
同じ意味でも形式が異なれば違う:LLMドキュメントワークフローにおける形式堅牢性に関する実証研究 [cs.IR, cs.IR, cs.SE]目的:LLMドキュメントワークフローにおける形式堅牢性の評価
- LLMの利用拡大に伴い,テキストだけでなくドキュメント処理が重要になっている。
- ドキュメント形式の違いがLLMワークフローの信頼性に及ぼす影響は未解明である。
- ドキュメント形式の変化がLLMの挙動に与える影響を明らかにし,対策を提案する。
- 形式を変更するだけで,精度が最大53.63%低下し,意思決定のずれが41%以上で発生することが判明した。
- ユーザー視点での軽量な緩和策により,形式に起因する意思決定のずれの最大44.21%を回復できることが示された。
- ドキュメント形式は単なるラッパーではなく,LLMシステム信頼性に影響する重要な要素であることが示唆された。
大規模言語モデルは実際のJavaマージコンフリクトを解決できるか?キャリブレーションされたLLM-as-Judgeによる評価 [cs.CL, cs.SE]目的:Javaマージコンフリクトに対する大規模言語モデルの解決能力の評価
- 共同ソフトウェア開発において,マージコンフリクトは常に発生するコストであるため,効率的な解決方法が求められている。
- 従来のツールは,ヒューリスティックが適用されない場合に解決を諦めるため,多くのコンフリクトを未解決のままにしてしまう。
- 大規模言語モデルを用いてコンフリクト解決の自動化を目指し,その性能を客観的に評価すること。
- 大規模言語モデルを用いた解決器は,開発者の解決と約55%の確率で一致し,既存のツール(AutoMerge)を18-22ポイント上回る性能を示した。
- この性能向上は,解決可能なコンフリクトの網羅性によるものが大きく,生の精度によるものではない。
- 構造的妥当性のチェックに合格しない解決策のうち,大規模言語モデルによる判断は4/5で合格しており,構造的検証はLLMに委ねるべきではないことが示唆された。
ガウス型部分巡回行列に対する改良された制限等距性境界 [cs.DS, math.PR]目的:ガウス型部分巡回行列の制限等距性境界の改善
- 近年,信号処理や機械学習において,高次元データの効率的な処理が重要視されている。
- ランダム行列の制限等距性(RIP)は,高次元データ処理の理論的基盤となるが,十分な条件が不明確である。
- 本研究は,ガウス型部分巡回行列に対するRIPのより緩い条件を導き出すことを目指す。
- 任意の標本集合を持つガウス型部分巡回行列に対して,改善された制限等距性境界が導かれた。
- その境界は,既存の結果よりも緩い条件で成立し,より実用的な応用を可能にする。
- 証明には,非可換ヒンチーンの不等式とシャッテンモーメント推定を組み合わせた洗練された手法が用いられた。
多デポ容量制車両経路問題に対するグラフマッチングに基づくアプローチ [cs.DS, cs.DM]目的:多デポ容量制車両経路問題の低コスト配送ルートの構築
- 物流効率化において重要な問題であり,配送コスト削減に貢献する。
- 問題規模が大きくなると,最適な解を効率的に求めることが困難である。
- グラフマッチングを用いて,効率的な近似解法を提案し,実用的な速度で解を求める。
- 提案手法は,最大2つの配送先の場合に多デポ容量制車両経路問題を多項式時間で厳密に解く。
- 構造化された条件下では,2を上限とする近似率を保証する。
- 1000顧客,20デポのインスタンスにおいて,既存手法と同等以上の性能をミリ秒単位で実現した。
ISACのためのグリーンセルフリーMassive MIMO:クラウド,フロントホール,無線資源の共同割り当て [cs.IT, math.IT]目的:セルフリーMassive MIMOと統合センシング・通信(ISAC)システムにおける,ネットワーク全体の消費電力の最小化
- 次世代6Gネットワークにおいて,センシング技術を活用した新たなアプリケーションの実現が期待されている。
- 従来の送信電力最適化手法では,センシング機能の統合による無線,フロントホール,クラウド領域における電力消費増加に対応できない。
- 分散マルチターゲット検出とクロスレイヤー最適化により,ISACシステムの電力効率を向上させる。
- 提案手法は,従来の送信電力最適化と比較して,総消費電力を大幅に削減する。
- 特に,総消費電力は50%以上,無線資源最適化と比較して13-15%の削減を達成した。
- 検出性能を維持しつつ,通信とセンシングの両方の制約を満たすことが確認された。
クラスタLPにおける近似二重分離:相関クラスタリングに対する1.387近似 [cs.DS]目的:相関クラスタリング問題に対する近似解の精度向上
- 相関クラスタリングは,データ間の関係性を明らかにする重要な課題である。
- 既存手法では,十分な精度での近似解を得ることが困難であった。
- 新たなアルゴリズムにより,より精度の高い近似解を効率的に求めることを目指す。
- 相関クラスタリング問題に対し,$(1.3865+\varepsilon)$近似アルゴリズムを提案した。
- 二重分離オラクルと新しい丸めスキームが,本研究の主要な貢献である。
- 提案手法は,既存の最良結果である$1.485+\varepsilon$よりも精度が高い。
セキュリティバグ報告の特定のための自動化技術の比較分析 [cs.SE]目的:セキュリティバグ報告の特定のための自動化技術の比較
- ソフトウェアの脆弱性対策において,迅速なバグ報告の特定は不可欠である。
- 手動による選別は時間がかかり,誤りやすく,大規模システムでは非効率である。
- 既存手法の有効性を比較し,最適な技術選択の指針を示すことを目指す。
- SetFitがF1スコア0.80で最も優れた性能を示し,4つのデータセットのうち3つで他の技術を上回った。
- RoBERTaも競争力があり,一部のプロジェクトではSetFitに匹敵する性能を示した。一方,GPT-5.2は性能が低い。
- プロジェクトごとの実験では,転移学習がデータ不足を補える一方,固有の特徴が強いプロジェクトでは性能が低下する場合がある。
バイブモデリングの必要性:AIベースの信頼性のあるソフトウェア開発における不可欠なステップ [cs.CL, cs.RO, cs.SE]目的:AIベースのソフトウェア開発における信頼性向上のためのバイブモデリングの有効性
- AIによるソフトウェア開発は加速するが,理解・検証・トレーサビリティ等の課題が存在する。
- 従来のAI開発はコード生成に偏り,人間の意図やシステム挙動の推論を妨げている。
- バイブモデリングを導入し,AI開発の信頼性と説明可能性を向上させる。
- 学生調査の結果,LLM生成コードの理解度や検証努力,信頼度においてバイブモデリングの有用性が示唆された。
- バイブモデリングは,自然言語との対話とコード生成の中間表現として機能し,人間の意図を保持する。
- 本研究は,バイブモデリングを通じて,信頼性と説明可能なAIベースのソフトウェアエンジニアリングの将来研究を促進する。
例からの形状学習:再帰的SHACLにおける形状学習の基礎 [cs.AI, cs.LO]目的:形状学習の基礎
- 知識グラフの応用において,データ整合性確認が重要であり,自動形状学習はその鍵となる。
- 既存手法では,正例と負例から適切な形状表現を効率的に導出することが課題である。
- 正例は検証し,負例は検証しない形状表現を,効率的に計算することを目指す。
- 正例と負例の集合から形状表現を導出する「fitting」アプローチを調査し,その計算可能性を検討した。
- fitting問題と最も特異なfitting問題の計算複雑性を解析し,指数時間の上界と,特定のケースにおける多項時間上界を確立した。
- SHACLの断片言語ELIと,well-founded,stable,supportedの3つの意味論に基づいて議論を行った。
準多項式性を通して見たオイラー向きえ数のLPアルゴリズム [cs.CC, cs.DS]目的:オイラー向きえ数問題の計算複雑性
- Holant問題の複雑度分類において,オイラー向きえ数問題は重要な役割を果たす。
- 準多項式性を持つ関数の場合,FPに属するか不明であった。
- FPNP側の問題を全て多項式時間で解くアルゴリズムを開発する。
- 本研究により,重み付きオイラー向きえ数問題に対する完全なFP対#Pの分離が達成された。
- 線形計画緩和を構造的ツールとして活用し,準多項式性を通常の多項式性に置き換える。
- 制約関数のアフィン局所構造を明らかにし,計算可能性を示す。
大規模言語モデルを用いたデッドロックフリーな通信プロトコル改善の仕様駆動型合成 [cs.SE, cs.AI]目的:通信プロトコルのデッドロックフリーな改善手法
- 分散ソフトウェアシステムにおいて,通信プロトコルの正当性は重要であり,わずかな不整合がデッドロックを引き起こす可能性がある。
- 形式仕様は厳密な保証を提供するものの,プロトコル改善を自動的に構築する支援は限られていた。
- 大規模言語モデルのコード生成能力と形式仕様の厳密性を組み合わせ,安全なプロトコル改善を自動化すること。
- 提案手法Syntropyは,MPST仕様と大規模言語モデルを組み合わせることで,デッドロックフリーなプロトコル改善を可能にする。
- Syntropyは,95.6%-99.5%の有効性と高い構文的正確性を達成し,多様な改善案を生成する。
- 改善制約を生成プロセスに直接組み込むことで,生成されたプロトコルが保証を満たすことを確実にする。
グラフと群を用いた線形符号の構成 [cs.IT, math.CO, math.GR, math.IT]目的:グラフ及びダイグラフを用いた線形符号の構成法
- 符号理論は,通信やデータ保存における誤り検出・訂正に不可欠な技術である。
- 既存の符号化方式では,効率性と性能の向上が課題となっている。
- グラフ構造を利用し,より高性能な符号を構成することで,この課題を解決する。
- 本研究では,Cayley符号の一般化であるグラフ符号とダイグラフ符号を提案した。
- これらの符号はCayley符号と同等の性質を持ちつつ,より柔軟な設計が可能である。
- グラフの拡張性に着目した解析により,KaufmanとLubotzkyの結果を改善し,良好なダイグラフ符号の無限族を構成した。
幾何学的刺突問題に対する厳密なUGC閾値 [cs.CG, cs.CC, cs.DM, cs.DS]目的:幾何学的刺突問題におけるUGC(Unique Games Conjecture)の下限を示すこと
- 幾何学的問題の近似アルゴリズムの性能限界を評価する上で,UGCのような計算複雑性仮説は重要である。
- 既存研究では,幾何学的刺突問題に対する近似アルゴリズムの性能限界が明確に示されていなかった。
- 本研究は,特定の問題クラスにおいて,UGCに基づいた厳密な近似性能限界を導き出すことを目指す。
- 本研究では,幾何学的刺突問題に対するUGCを用いた証明を通じて,既存の近似アルゴリズムの限界を明らかにした。
- 特に,軸平行d次元キューブの刺突問題の閾値がdであることが示され,矩形や正方形の刺突問題の閾値も2と特定された。
- 水平線分に対する水平・垂直線の刺突問題の閾値がe/(e-1)であり,分離d-interval transversalの閾値がdであることも証明された。
クラウドベースIoTアクセス制御ポリシーにおける情報フローの検証(拡張版) [cs.CR, cs.LO, cs.SE]目的:IoTアクセス制御ポリシーにおける不要な情報フローによるセキュリティ脆弱性の特定
- IoTデバイスの普及に伴い,セキュリティ確保の重要性が増している。
- IoT環境では,デバイス間の信頼度やサブシステムによる区分が存在するため,単独での権限検証では不十分である。
- アクセス制御ポリシーに起因するデバイス間情報漏洩リスクを形式手法を用いて検証する。
- AWS IoT Coreのコンポーネントを形式的にモデル化し,アクセス制御ポリシーによるデバイス間の通信を情報フローグラフで表現した。
- SMTソルバーを活用してグラフの有限表現を構築し,デバイス間の情報フローを検証できるツールIOT:POKERを実装した。
- 現実的なシナリオと実世界のポリシーに対する評価により,本アプローチの有効性を示した。
q-CSP再構成の近似の最適PSPACE困難性 [cs.CC, cs.DM, cs.DS]目的:Maxmin q-CSP再構成問題における近似の困難性
- 制約充足問題は,AIやオペレーションズリサーチにおいて重要な役割を担う
- q-CSP再構成問題の効率的な近似アルゴリズムは未だ存在しない
- Maxmin q-CSP再構成問題の近似困難性の限界を示す
- 本研究により,Maxmin q-CSP再構成問題は,任意のq ≥ 2 および ε > 0 に対して,(1/2^(q-1) + ε)の範囲で近似することがPSPACE困難であることが証明された。
- 完全なケースにおいては,(1/2^(q-1) - ε)の近似アルゴリズムがNPに属することが示された。
- これらの結果は,q ≥ 2 の任意のqに対して,Maxmin q-CSP再構成問題の近似の最適PSPACE困難性を確立する。
k^2木に対する拡張深さ優先表現 [cs.DS, cs.IR, cs.PF]目的:k^2木のメモリ局所性と運用効率を向上させるための静的圧縮形式
- グラフの圧縮は,大規模データセットの取り扱いや効率的な計算のために不可欠である。
- k^2木の伝統的なレベルごとの配置は,局所性が低く,キャッシュ性能が悪いという課題がある。
- 深さ優先表現によってk^2木の配置を改善し,圧縮と計算性能の両方を向上させる。
- 提案された深さ優先表現は,従来のレベルごとの配置と比較して競争力があり,しばしば優れた性能を示す。
- 特に,CEDFは圧縮率が最も高く,EDF-1とCEDFはピークメモリ使用量を一貫して削減する。
- 性能はワークロードによって異なり,異なるレイアウトが異なる操作やデータにおいて効果を発揮する。
高性能CPUおよびGPU処理のための不規則配列の高度化 [eess.SY, cs.SY, cs.SE]目的:高エネルギー物理学におけるネストされた可変長データの表現と処理
- 高エネルギー物理学分析は,複雑なデータ構造に依存しており,高速処理が不可欠である。
- 従来の数値配列はGPUに最適化されているが,不規則なデータ構造のGPU処理は困難である。
- 不規則なワークロードに対するGPUスループットを向上させること。
- Awkward ArrayのGPUバックエンドが開発され,NVIDIA CUDA Core Compute Libraries (CCCL)が利用されている。
- 最適化されたメモリ管理と,ラギッド配列に対するセグメント化された削減アルゴリズムが実装された。
- Pythonプログラミングモデルを維持しつつ,不規則なワークロードにおけるGPUスループットが大幅に向上した。
ブロックグラフにおける文字列マッチング:歩数による完全分類 [cs.HC, cs.CL, eess.SY, cs.SY, cs.DS]目的:ブロックグラフにおける文字列パターン検索の計算複雑性の分類
- ゲノムのような大規模類似データセットのコンパクトな表現としてグラフ構造が活用されている。
- 既存研究では,グラフ全体の長さを歩数とする前提で計算量の下限が示されている。
- 歩数を制限することで,既存の下限を回避できる可能性があり,その複雑性を明確化する。
- 歩数が3のブロックグラフに対する文字列マッチングは,ほぼ線形時間で実行可能である。
- ブロック数bが4以上の場合は,既存の計算量の上限を改善する組合せアルゴリズムは存在しない。
- 定数個のブロックの場合,高速行列乗算に基づいたアルゴリズムにより改善が期待できる(条件付き最適)。
相関情報源に対する最も識別力の高いブール関数について [cs.IT, math.IT]目的:相関情報源を個別に圧縮した場合に得られる2つの分布間のカルバック・ライブラー情報量(KLダイバージェンス)を最大化するブール関数のペアの特定
- 情報理論において,情報源符号化や情報伝達の限界を明らかにする上で,相互情報量の最大化は重要な課題である。
- KLダイバージェンスの最大化は計算が困難であり,効率的な手法や最適な関数の特定が課題となっている。
- ブール関数のペアがKLダイバージェンスを最大化する条件を特定し,AmariとKobayashiの予想を部分的に解決すること。
- 独立な情報源を基準とした場合,この問題は相互情報量の最大化に帰着し,辞書関数が最適であることが知られている。
- 非バイアスなブール関数と,非負の相関領域における同一のペアに対して,KLダイバージェンスとFisher情報はレベル-$k$関数によって最大化されることが証明された。
- ベイズ分散型1ビット仮説検定の枠組みにおいて,レベル-$k$関数が最適なペアであることが示された。
ソフトウェア工学教育におけるAIの要件品質学習への統合:TPACKに基づく経験的研究 [cs.SE, cs.AI]目的:ソフトウェア工学教育におけるAI統合の教育的アプローチ
- ソフトウェア工学分野では,AI技術の急速な進化に対応した教育が不可欠である。
- AI技術の教育的活用に関する体系的な研究が不足している。
- AIツールを用いた要件品質分析の教育効果を検証し,指導方法を提案する。
- 学生はAIツールを分析・評価の支援として選択的に使用した。
- 要件の価値明確性やテスト可能性といった具体的な側面での改善が認められた。
- 学生はAIに対する条件付き信頼と能動的な改善意欲を示し,要件品質基準への意識が高まった。
再帰型グラフニューラルネットワークにおける過剰平滑化の防止:持続的なガウス摂動 [cs.LG, cs.AI, cs.IT, math.IT]目的:深層グラフニューラルネットワークにおける過剰平滑化現象の防止機構
- グラフ構造データに対する機械学習は,様々な分野で応用が広がっている重要な研究領域である。
- 深層グラフニューラルネットワークは,層を深くするとノード表現が均質化し,識別能力が低下する過剰平滑化問題に直面する。
- ガウスノイズの持続的な注入により,過剰平滑化を抑制し,表現の多様性を維持することを目指す。
- 各伝播ステップ後に独立なガウスノイズを注入する再帰型グラフニューラルネットワークを解析した結果,隠れ表現は幾何学的にエルゴードなマルコフ連鎖を形成することが示された。
- 理論的解析により,期待される定常ディリクレエネルギーに正の下限が導き出され,表現の崩壊を防ぐことが保証された。
- 数値実験は,理論的予測と一致し,ノイズ強度に対する限界ディリクレエネルギーの依存関係が確認された。
古典的な手法,新たなモデル:単純な画像変換が最新のAIベースコンテンツモデレーションを欺く方法 [cs.AI, cs.CR, cs.SE]目的:AIベースの画像コンテンツモデレーションシステムの脆弱性
- 有害コンテンツの拡散防止は重要であり,大規模なコンテンツモデレーションが求められる。
- 従来のコンテンツモデレーションは,ポリシーの網羅性と文脈理解に限界がある。
- 大規模基盤モデルを用いたモデレーションAPIの信頼性と安全性を評価する。
- 3つの商用画像モデレーションサービスは,勾配や代替モデルを必要としない単純な画像変換によって回避可能である。
- 色反転やグレースケール変換などの固定変換でも,人間には認識可能なコンテンツを維持しながら,安全でないと判断される場合がある。
- マルチモーダルコンテンツや自傷行為に関するコンテンツは,特に脆弱性が高いことが示された。
構造を用いた学習の改善:最小一貫部分集合の微細な複雑性 [cs.HC, cs.DS, cs.CC]目的:大規模教師ありクラスタリングにおける最近傍探索分類の計算ボトルネックを軽減するためのインスタンス選択
- 大規模データセットの解析において,計算効率の良い分類手法の確立が重要である。
- 最小一貫部分集合問題の計算複雑性は高く,現実的な規模の問題への適用が困難である。
- グラフ構造に着目し,最小一貫部分集合問題の計算複雑性の限界を厳密に明らかにする。
- 重み付きグラフにおける最小一貫部分集合問題を解くためのアルゴリズムを開発し,既存手法を大幅に改善した。
- ツリー幅twを持つグラフにおいて,$3^{c \cdot(\mathrm{tw}+1)}\cdot n^{\mathrm{tw}+\mathcal{O}(1)}$の実行時間を持つアルゴリズムを提案した。
- 指数時間仮説のもとで,さらなる計算時間改善の限界を示す下界を導出した。
エージェント型メタバースサービス:新たなAs-a-Serviceパラダイム [cs.SE, cs.AI, cs.MA]目的:エージェント型メタバースサービスとMeta-AaaSの形態,特性,原理の提示
- メタバースは,人々の生活,仕事,創作,娯楽を支える仮想生態系であり,重要性が増している。
- 従来のメタバースサービスは,多様なニーズへの対応や高度な自律性に課題があった。
- 生成AIを活用したエージェント型サービスをメタバースに導入し,新たなサービスパラダイムを確立すること。
- 生成AIの進化により,自律学習,マルチモーダル対話,コンテンツ生成能力を備えたエージェントが登場した。
- これらのエージェント能力をカプセル化し,メタバース上で提供するAgent-as-a-Service(AaaS)が,新たなサービス形態として注目されている。
- エージェント型メタバースサービス(AMServ)は,メタバースビジネス処理を促進し,AI時代のサービス産業の発展に貢献すると期待される。
レガシーコード移行の決定論的検証のためのエージェント手法 [eess.SY, cs.SY, cs.SE, cs.AI]目的:レガシーCOBOLプログラムからJavaへの移行における機能の正確性保証
- レガシーシステムは企業にとって重要な資産であり,現代的な環境への移行は不可欠である。
- 移行後のテストには十分なテストデータや全てのコーナーケースの検証が困難な場合がある。
- エージェントによるテスト合成手法を用いて,網羅的な検証と正確性の保証を目指す。
- 提案手法「Locksmith Loop」は,COBOLとJavaの実行環境をそれぞれ計装し,入力モックを用いた探索によりプログラム分岐を深く網羅する。
- 3つのCOBOL-Javaケーススタディにおいて,既存のテスト手法が停滞した状況下でも,カバレッジが向上し,特にオープンソースプログラムではほぼ完全なカバレッジを達成した。
- 生成されたJavaコードは,決定論的パリティチェックにおいてCOBOL参照と同等の結果を示し,エージェントによるコーディング出力の検証手法の有効性を実証した。
大規模AIモデルと意味認識型ハイブリッドビームフォーミングによる汎用的なクエリ指向画像意味符号化 [cs.IT, cs.SY, eess.IV, eess.SY, math.IT]目的:クエリ指向画像意味符号化フレームワーク
- データ伝送において,意味を保持する意味通信の重要性が高まっている。
- 既存の符号化設計では,ユーザーの意図が考慮されていない場合が多い。
- 未学習のオブジェクトカテゴリに対しても汎化性能を持つ符号化手法の確立。
- 提案手法は,従来のコーデックや最新のセマンティック符号化方式と比較して,優れた性能を示すことがシミュレーションにより確認された。
- 大規模 MIMO-OFDMシステムにおいて,意味的に重要な特徴を優先する意味認識型ハイブリッドビームフォーミングアルゴリズムを開発した。
- 事前学習済みの大規模AIモデルを活用することで,汎用的な特徴表現を強化している。
スティッキーチャネル群の容量 [eess.SY, cs.SY, cs.IT, math.IT]目的:q進スティッキー挿入チャネル群の容量
- 情報伝送において,チャネルの容量は理論的な上限であり重要。
- 反復チャネルの容量を厳密に決定することは困難であった。
- 特定の条件を満たす反復チャネル群の容量を厳密に決定。
- q進スティッキー挿入チャネル群の容量を,$\log_2\lambda$ bits/symbolと決定。
- 容量は,0誤り容量と一致することが証明された。
- Fuss-Catalan数に基づいた明示的な反復則も提示された。
