arXiv雑要約
プログラム - 2026/06/19 公開
ルールベースのモデル変換における設計意思決定の支援 [cs.SE]目的：モデル変換における設計意思決定の明示化と管理
- モデル駆動開発は，自動化された成果物生成に不可欠。その品質向上が重要。
- 設計意図が変換コードに埋没し，柔軟性・再利用性・トレーサビリティが低い。
- 設計決定を分離し，モデル変換の柔軟性と管理性を向上させる。
- 設計決定を独立したモデルとして表現することで，再利用性と一貫性を確保。
- 変換ルール中の分岐点を設定選択に従い動的に解決することで，多様なモデル生成が可能。
- 適用されたルールと選択肢を追跡することで，生成された成果物のトレーサビリティを向上。
LLMがハードウェア設計におけるRTLコーディングで失敗し，汎化する様相 [cs.CL, cs.AI, cs.PL]目的：LLMにおけるハードウェア設計のRTLコーディングにおける失敗と汎化のメカニズムの解明
- ハードウェア設計の自動化は，開発効率の向上や複雑化への対応に不可欠である。
- LLMは有望視されるが，並列性と時間的論理を要するハードウェア設計への適用は困難である。
- LLMのハードウェア設計能力の限界を特定し，改善策の方向性を示す。
- LLMはVerilogEvalベンチマークにおいて，約90.8%の初期パス率で頭打ちとなることが示された。
- この頭打ちの原因は，解決不可能な機能的エラーにあり，計算資源の増加では改善しない。
- 最適化によって構文エラーは軽減されるものの，より深刻な機能的エラーが悪化する傾向が確認された。
エージェントアーマー：コーディングエージェントの失敗に関するフレームワーク，評価，および軽減策 [cs.SE, cs.LG]目的：コーディングエージェントの失敗メカニズムの特定と軽減策の提案
- ソフトウェア開発へのAI導入が進む中で，潜在的な危険性の評価が重要になっている。
- AIエージェントの稀な重大な失敗モードが現実のデプロイで顕在化している。
- エージェントの安全性を高め，有害な失敗を防ぐための具体的な対策を確立する。
- コーディングエージェントの失敗は，仕様不足，能力エラー，エージェントハーネスエラーの3つのメカニズムに起因することが示された。
- 提案手法であるAgentArmorは，システムプロンプトの拡張，コマンド分類器，ストライクポリシー，決定論的ガードレールなどを導入することで，エージェントの安全性を統計的に有意に向上させる。
- 現在のコーディングエージェントに対する具体的な軽減策と，将来のハーネス機能の設計指針が示された。
DynAMO：トポロジカルマルチエージェントスケジューリングによる動的アセット管理オーケストレーション [cs.SE, cs.AI]目的：産業用アセットライフサイクルにおける動的アセット管理オーケストレーション
- インダストリー4.0では，アセット管理の自動化が重要であり，効率性と安全性が求められる。
- LLMエージェントの導入において，遅延，同時実行性の不安定性，安全性へのリスクが課題となっている。
- DynAMOは，これらの課題を解決し，スケーラブルで安全かつ低遅延なエージェント展開を目指す。
- DynAMOは，プランニングと実行のアーキテクチャを採用し，検証可能なワークフローグラフを生成することで，効率と安全性を両立している。
- 並列実行により，エンドツーエンドの遅延を最大1.8倍削減し，並列化可能なワークフローにおいて高い効果を発揮する。
- 構造化されたコンテキストプルーニングにより，推論遅延を約30%削減し，安定した実行と機能的動作を維持する。
構築による両状態性：壁時計で較正された状態監視器は，エージェントの動作頻度では瞬間検出モードを持たない [cs.SE, cs.AI, cs.LG]目的：自律エージェントの状態監視における，時間較正方式の重要性の検証
- 自律エージェントの安全性確保には，状態の変化を的確に監視する仕組みが不可欠である。
- 従来の監視器は，エージェントの動作頻度変動により，誤警報や検出遅延が発生しやすい。
- 壁時計時間で較正された監視器の限界を明らかにし，より適切な監視方法を模索する。
- 壁時計時間で較正された監視器は，エージェントの動作頻度によって，常時アラーム状態か沈黙状態の二つの状態に分かれる。
- 実際の運用データにおいて，エージェントの動作頻度が壁時計時間較正のトラップ領域に該当することが確認された。
- サンプル時間で較正された監視器は，エージェントの動作頻度に関わらず安定した性能を示す。
LLM駆動型段階的洗練による解釈可能かつ検証可能なハードウェア生成 [cs.SE, cs.AI]目的：解釈可能性と検証可能性を備えたハードウェア生成手法
- チップ設計の複雑化と高度化に伴い，効率的な設計手法が求められている。
- LLMは幻覚を起こしやすく，誤った設計を生む可能性があるため，ハードウェア設計への適用が限定的である。
- LLMの創造性と形式手法の厳密性を組み合わせ，信頼性の高いハードウェア生成を実現する。
- 提案手法は，LLMと形式手法を組み合わせることで，設計仕様からRTLプログラムを生成する。
- 段階的な変換規則の適用により，生成されたRTLプログラムの正当性を保証する。
- 実験結果は，提案手法の有効性と効率性を示している。
GUIパラダイムを超えて：モバイルエージェントは画面を必要とするか？ [cs.SE, cs.CL, cs.HC]目的：モバイルエージェントにおけるCLI（コマンドラインインターフェース）の有効性検証
- モバイルエージェント技術は，自動化や利便性向上に不可欠であり，その発展が期待されている。
- 従来のモバイルエージェント研究はGUI中心であり，CLIの潜在能力が十分に活用されていない。
- GUIに頼らないCLIを活用することで，モバイルエージェントの能力を拡張し，より高度なタスクの実行を目指す。
- Claude Code (Opus 4.7) がAndroidWorldとMobileWorldの両方で，既存のGUIベースラインを上回る性能を示した。
- CLIのオーラクル解法は高い正答率を達成し，CLIパラダイムの更なる改善の余地を示唆した。
- 新たに開発したCLI-Advantage Task Suiteにおいて，CLIエージェントはGUIベースラインを全てのカテゴリで上回り，効率性も高かった。
エージェント型AI向け実行制約アドバイザリ自動化：再現性のあるAIBOM駆動型CSAF-VEXフレームワーク [cs.SE, cs.AI]目的：エージェント型AIにおける脆弱性対応の自動化
- AIシステムの普及に伴い，セキュリティ確保が不可欠である。
- ソフトウェア部品の脆弱性情報と実行環境の関連性が不明確である。
- SBOM/AIBOMを活用し，実行時の証拠に基づいた脆弱性評価を可能にする。
- SBOMとAIBOMの連携により，決定論的な環境キャプチャと実行時テレメトリを実現した。
- 静的・動的証拠を組み合わせることで，CSAF VEXアドバイザリを生成し，検証できる。
- 合成エージェント型AIワークロードを用いた評価で，効果が確認された。
有限グラフの別の定義方法 [cs.DM, cs.DS, math.CO]目的：有限グラフの新たな定義
- グラフ理論は，ネットワーク構造の解析に不可欠であり，様々な分野に応用されている。
- グラフの対称性への対応や，グラフ同型性の判定は計算量が大きく，課題となっていた。
- グラフの表現方法を工夫し，これらの問題解決を目指す。
- 「グラフ線形表記」というグラフ不変量を紹介し，有限グラフの新たな定義として提案した。
- この表記を用いることで，グラフの図示や同型性判定の効率化が期待できる。
- グラフ彩色や経路といった古典的なグラフ理論概念も，この表記に適用可能であることを示した。
DevOpsと一般開発者：Stack Overflow 2023調査からの洞察 [cs.FL, cs.SE]目的：DevOps専門家と一般ソフトウェア開発者の役割の違い
- ソフトウェア開発はIT業界の中核であり，その効率性と品質が経済成長に不可欠である。
- DevOpsと一般開発者の役割分担が不明確で，最適な人材配置や技術戦略の策定が困難である。
- ソフトウェア開発におけるDevOpsの役割と，その有効性を明確にすること。
- DevOps専門家と一般開発者の間で，使用するツールや技術に有意な差は見られなかった。
- 両者ともDockerやKubernetesといったツールを活用し，効率性と自動化を重視している。
- 一般開発者は多様なツールを使用する一方，DevOpsは経験豊富な中年層が多く，リモートワークへの適応も進んでいる。
VERITAS：ゼロショット形式定理証明のための検証者誘導証明探索 [cs.LG, cs.AI, cs.LO, cs.PL]目的：ゼロショット形式定理証明における証明探索
- 形式定理証明は，数学的推論の自動化に不可欠であり，ソフトウェアやハードウェアの検証に役立つ。
- 従来のLLMベースの形式証明器は，検証者の信号を十分に活用できていない。
- 検証者の信号を効果的に利用し，証明探索の精度を向上させる。
- VERITASは，検証者からの信号を二段階のプロトコルで証明探索に組み込むことで，性能を向上させている。
- miniF2Fベンチマークにおいて，40.6%の正解率を達成し，既存手法を上回った。
- VERITAS-CombiBenchという新しいベンチマークにおいて，不案内なサンプリングの課題を明らかにした。
JustDiag!：説明責任のある根本原因分析のための診断正当化エンジン [cs.SE, cs.AI]目的：説明責任のある根本原因分析のための診断正当化
- 高ステークスの運用においては，単なる結果の正確性だけでは不十分である。
- 既存の根本原因分析は，根拠や検討過程が不明確な場合がある。
- 診断の根拠や代替案の検討状況を明示化し，説明責任を果たすことを目指す。
- JustDiagは，証拠，発見，競合仮説，矛盾，次の確認事項などを明示的に管理する。
- 実世界の66事例における評価で，最終回答の質とプロセス品質の両方において，JustDiagは対照群を上回った。
- JustDiagは，より慎重な不確実性の維持により，最終的な完了率はわずかに低下した。
OpenRath：エージェントシステムのセッション中心実行時状態 [cs.SE, cs.PL]目的：エージェントシステムの実行時状態の統合
- エージェントシステムは複雑化しており，実行時の状態管理が重要である。
- 既存システムでは，実行時状態が分散し，検査や再現が困難である。
- セッションという概念を用いて，実行時状態を統合し，監査可能性を高める。
- OpenRathは，エージェント間およびワークフロー間で受け渡されるセッションを中核抽象化として提供する。
- セッションは分岐，検査，再生が可能であり，実行時の状態を記録する。
- これにより，状態の再構築が不要になり，監査しやすいシステムを構築できる。
カリキュラムの整合性評価：CS2013とCS2023への長期的な適用フレームワーク [cs.CL, cs.AI, cs.SE]目的：コンピュータサイエンスのカリキュラムと国際的なガイドラインの整合性測定
- コンピュータサイエンス教育において，最新の知識とスキルを習得するためには，体系的なカリキュラムが不可欠である。
- カリキュラムが最新のガイドラインにどの程度準拠しているか，客観的に評価する手法が不足している。
- カリキュラムの現状を定量的に把握し，改善点を見出すための信頼性のある評価フレームワークを確立する。
- 本研究では，コンピュータサイエンスのカリキュラムとCS2013/CS2023ガイドラインの知識ユニットのマッチングを，人間による確認を含むパイプラインで評価した。
- 評価の結果，対象プログラムはCS2023の約49.7%，CS2013の約50.9%の知識ユニットをカバーしており，10年間で大きな変化は見られなかった。
- 能力と認知レベルの評価では，CS2023ガイドラインの方が期待されるレベルが高く，カリキュラムの到達率に差が見られた。この差は，プログラムの問題ではなくガイドラインの進化を反映している。
LLM支援による耐量子計算暗号開発におけるセキュアコーディングのドリフト：ゲーミフィケーションによる修正 [cs.CR, cs.AI, cs.SE]目的：耐量子計算暗号開発におけるセキュアコーディングのドリフト現象とその抑制策
- 耐量子計算暗号は，将来のセキュリティを確保する上で不可欠であり，実装の厳格さが求められる。
- LLMによるコード生成は生産性を向上させる一方，セキュリティ上の脆弱性を生む可能性が指摘されている。
- LLM利用に伴うセキュアコーディングの低下を抑制し，安全な耐量子計算暗号の実装を支援することを目的とする。
- 本研究では，LLMに依存した開発環境下で，セキュアコーディングが徐々に低下する「セキュアコーディングのドリフト」という新たな脆弱性モデルを提示した。
- ゲーミフィケーションを活用し，敵対的評価，行動フィードバック，セキュリティスコアリングを組み込んだセキュアコーディングフレームワークを提案した。
- LLMを単なる支援ツールではなく，セキュリティを考慮した共同開発者として位置づけることで，より安全な耐量子計算暗号の実装に貢献する。
Bures-Helstrom qubit計量の Ricci flow [cs.IT, math-ph, math.IT, math.MP, quant-ph]目的：Bures-Helstrom qubit計量に対する Ricci flow の記述
- 量子情報理論において，量子状態間の距離を測る指標として重要である。
- Bures-Helstrom計量の Ricci flow の解析は，一般的に困難である。
- Bures-Helstrom qubit計量に対する Ricci flow を明示的に記述し，その性質を解明する。
- Bures-Helstrom計量は，回転対称なゲージにおいて，動径lapse と warping factor の連立システムとして Ricci flow が記述できる。
- 得られた Ricci flow は，ホモセティック収縮であり，extinction time は 1/4 であることが示された。
- 体積正規化された Ricci flow は Bures-Helstrom計量を固定点とし，その線形化はシフトされた球 Laplacian となる。
機械学習支援Bluetooth方向探査のための軽量な非直達路チャネル検出 [cs.IT, math.IT]目的：Bluetoothの非直達路チャネル検出手法の開発
- 屋内産業用測位において，Bluetooth方向探査は有望な技術である。正確な測位には，電波環境への対応が不可欠である。
- マルチパス環境下では，反射や散乱により角度推定精度が低下する。BLE方向探査における，狭帯域チャネル特徴表現の欠如が課題である。
- BLE環境下における，軽量かつ高精度な直達路/非直達路チャネルの識別手法を確立し，測位精度を向上させる。
- 提案手法では，外れ値の影響を低減するquantileベースの標準化と，PCA・AKDEによる特徴分析を実施した。
- Nyström Kernel Approximation (NKA)を用いた手法は，既存手法と比較して約7-14%の精度向上を示した。
- NKA-SVCアプローチは，学習複雑性，推論コスト，メモリフットプリントのバランスに優れており，リソース制約のあるシステムに適用可能である。
Vancomycert：検証可能なニューロシンボリック薬物送達システム（ケーススタディ） [cs.LO]目的：抗生物質投与量の自動決定のためのニューラルネットワークコントローラの形式検証
- サイバーフィジカルシステムにおけるニューラルネットワーク制御は一般的だが，医療分野での安全性検証は遅れている。
- 安全性と適応性を両立させつつ，時間無限の範囲で安全性を保証する必要がある。
- 自動投与が治療濃度を超えないことを無限の時間枠で形式的に証明する。
- 本研究では，バンコマイシン投与量の形式検証パイプラインを構築し，安全性と治療効果の両立を示した。
- RocqとVehicleを用いて，無限の時間枠における安全性を証明することに成功した。
- この手法は，患者一人ひとりに合わせた治療アプローチを安全に実現する可能性を示す。
LLM-ソルバー連携におけるナレーションギャップの分析 [cs.RO, cs.AI, cs.CR, cs.LO]目的：LLMとソルバーの連携におけるナレーション段階の課題と対策
- 安全性・セキュリティが重要な問いに対し，論理形式化による形式手法の活用が重要視されている。
- LLMとソルバーの連携において，ナレーション段階での堅牢性に課題があり，悪意のある入力に脆弱である。
- LLM-ソルバー連携におけるナレーションギャップを特定し，その対策を検討することで，より安全な推論システムを構築する。
- LLM-ソルバー連携を検証可能な意思決定手続きとしてモデル化し，ナレーション段階の脆弱性を明らかにした。
- プロンプトインジェクション攻撃に対する脆弱性を検証し，証明書ゲートがソルバーの検証結果の信頼性を高めることを確認した。
- 堅牢なプロンプトの使用や適応的な攻撃に対する軽減策を検討したが，完全な防御は困難であることが示された。
FAPO：多段階LLMパイプラインの完全自動プロンプト最適化 [cs.SE, cs.AI]目的：多段階LLMパイプラインの最適化
- LLMの性能向上は，より複雑なタスクへの応用を可能にし，AIの可能性を広げる上で重要である。
- 多段階LLMパイプラインでは，各ステップ間の相互作用が複雑であり，ボトルネックの特定が困難である。
- プロンプトのみの最適化では改善が難しいパイプラインの構造的ボトルネックを，自動的に特定・修正すること。
- FAPOは，6つのベンチマークと3つのタスクモデルにおいて，ベースラインのGEPAを18回の比較のうち15回で上回った。
- FAPOは，プロンプト最適化が不十分な場合に，構造変更を行うことで，特にHoVerとIFBenchで顕著な性能向上を示した。
- セキュリティタスクCTIBench-RCMにおいて，FAPOはGPT-5などのモデルでテスト精度を大幅に向上させた。
StaminaBench: 100回のインタラクションターンにおけるコーディングエージェントのストレステスト [cs.SE, cs.AI]目的：コーディングエージェントの持続力評価
- ソフトウェア開発において，反復的な変更要求は不可避であり，エージェントの長期的な安定性が重要である。
- 従来のタスク解決率では，実際の開発における複数回の修正サイクルを捉えきれない。
- 複数回のインタラクションターンにわたるコーディングエージェントの性能を評価し，課題を特定すること。
- テストの結果，全てのモデルが5～6ターン以内に失敗しており，テストなしの反復開発はバグを生みやすいことが確認された。
- エージェントへのテストフィードバックと再試行の許可により，成功ターン数が最大12倍に向上した。
- エージェントの性能は，使用するフレームワークに大きく依存し，高性能モデルでは最大6倍の差が見られた。
プルリクエスト以前: マルチエージェント協調のマイニング [cs.SE, cs.AI, cs.MA]目的：マルチエージェント協調における課題の特定と改善策の提案
- 自動コーディングエージェントの利用拡大に伴い，その協調動作の最適化が重要になっている。
- プルリクエストの受理率が低いという問題があり，その原因が協調プロセスの不備にあると考えられる。
- エージェント間の作業の重複や競合を減らし，協調効率を向上させることを目指す。
- 共有基盤griteの導入により，チームメイトの作業をやり直す割合が78%から0%に減少し，有用なスループットが3倍以上増加した。
- ログは，競合編集，ロック飢餓，冗長な再発見など，プルリクエスト履歴では見えない具体的な障害モードを自動的に回復可能にする。
- ログの全エージェント間でのコピーは，書き込みが失われることなく同じ状態に収束し，高い信頼性を示した。
学習されたマルチエージェント通信ポリシーの決定木蒸留による形式検証 [cs.RO, cs.AI, cs.LG, cs.LO, cs.MA]目的：学習されたマルチエージェント通信ポリシーの形式検証手法
- ドローン群や自動運転車隊など，安全性が重要なロボット応用にMARLを適用するためには，安全性保証が不可欠である。
- ニューラルポリシーは複雑であり，安全性に関する形式的な保証が不足している。そのため，安全性を検証することが困難である。
- ニューラルポリシーを解釈可能な決定木に蒸留し，形式検証を行うことで，安全性の保証を提供する。
- ニューラルポリシーを決定木に蒸留するパイプラインを構築し，97.9% +/- 1.2%の忠実度を達成した。
- 決定木をPRISMで検証可能な形式に変換し，安全性，生存性，協調性に関する18の時系列論理特性を検証した。
- 検証された安全性特性は元のニューラルポリシーにも転移し，衝突確率は0.3%であり，1%の閾値を下回った。
プロンプトの質とプルリクエストの結果：LLM支援開発の段階的経験的研究 [cs.SE]目的：LLM支援開発におけるプロンプト構造とプルリクエスト成果の関係
- ソフトウェア開発において，LLMの活用が拡大しており，その効果を理解することが重要である。
- プロンプトの構造がプルリクエストの成果に及ぼす影響は不明であり，十分な研究がなされていない。
- プロンプト構造が，コード生成，採用，統合の深さに与える影響を明らかにすること。
- プロンプトの具体性が最も安定して人間の判断と一致し，文脈はLLMによって過小評価される傾向が見られた。
- プロンプトの具体性と文脈は，実行可能なコード生成と強く関連しており，検証はコードの採用を予測する主要因となった。
- プロンプト特性は，文脈による根拠付け，タスクの具体性，評価可能性のヒントを通じて，AI支援ソフトウェアエンジニアリングワークフロー全体に段階依存的な影響を与えることが示された。
PUFFERDOS：正規表現DoS脆弱性に対する効率的かつ効果的な攻撃文字列生成 [cs.CR, cs.SE]目的：正規表現DoS脆弱性の攻撃文字列生成
- Webアプリケーション等のセキュリティにおいて，正規表現の利用は不可欠である。
- 正規表現エンジンの特性により，特定の文字列で処理負荷が指数関数的に増大するReDoS脆弱性が存在する。
- 現実的な入力長でプログラムレベルでの有効性が確認できる攻撃文字列生成手法を確立すること。
- PUFFERDOSは，脆弱なパターンに基づき攻撃文字列を合成し，精緻化する。
- ReDoS特有のコンコリック実行により，現実世界での攻撃可能性を保証する。
- 既存手法では困難だった，現実的な入力長とプログラムレベルでの検証を両立した攻撃文字列生成を実現した。
効果システムを抽象解釈として [cs.PL]目的：効果システムと抽象解釈の関係性
- プログラムの振る舞いを静的に検証する技術は重要であり，信頼性の高いソフトウェア開発に不可欠である。
- 型システムと効果システムの間の形式的な関係性は十分に研究されていない現状がある。
- 効果システムを抽象解釈として捉えることで，その理論的基盤を確立し，応用範囲を広げることを目指す。
- 効果量化子を抽象ドメインに埋め込む関係性を形式的に記述した。
- 効果量化子の一般的な形を，状態や値ではなく，イベントの発生に対する抽象解釈として復元した。
- これにより，効果システムと抽象解釈の間のより深い理解と，両者の統合への道が開かれた。
駆動定常状態における情報と消散のパリティ選択則 [cs.CL, cs.IT, math.IT]目的：駆動定常状態における対称的な情報量とエントロピー生成の関係性
- 非平衡系の熱力学理解において，情報とエントロピー生成の定量的な関係は重要である。
- 駆動定常状態における厳密な情報量とエントロピー生成の関係性は未だ解明されていない。
- 回転駆動される線形非平衡定常状態におけるパリティ選択則を明らかにすること。
- 緩和と拡散行列が可換な場合，駆動反転時のスナップショット相互情報量は常に偶数となる。
- 対称性が崩れると，パリティ違反は交換子のノルムに比例して上昇する。
- 完全な等方性下では，相互情報量は駆動によらず一定値(約0.145 nats)となる。
大規模言語モデル生成単体テストにおけるライブラリ認識型ダブルと反復修正 [cs.SE, cs.AI, cs.MA]目的：OpenSILファームウェアの単体テスト自動生成ワークフロー
- 低レベルCファームウェアの変更検証は，厳格なビルド制約により単体テストが脆弱になりやすい。
- ヘッダーファイルの欠落や依存関係の不一致により，コンパイルやリンクが頻繁に失敗する。
- LLMを活用し，ビルドログとコードカバレッジに基づいた反復修正により，単体テスト作成の効率化を目指す。
- 76個の関数を対象に，73個の関数に対してコンパイル可能な単体テストを自動生成した。
- コードカバレッジガイダンスなしでは平均73.9%，ガイダンスありでは98.8%に達した。
- ベクトルデータベース検索との組み合わせで94.7%となり，単体テスト作成の効率とカバレッジが大幅に向上した。
確実性に基づく生成モデル：決定論的カプセル化の原理 [cs.AI, cs.SE]目的：生成モデルと従来システムを統合するための基礎的枠組み
- AI技術の進展は，既存システムに大きな可能性をもたらす一方で，リスクも伴う。
- AIの導入における危険性が認識されているものの，安全な統合を保証する基盤は不足している。
- 生成モデルを従来システムに安全に統合するための原理と反パターンを提示する。
- 本研究では，AIと従来システムを融合したアーキテクチャを定義する4つの基本要素を確立した。
- さらに，業界で広く見られる2つの反パターンを提示し，エンジニアへの警告を発している。
- 本枠組みは，生成モデルの次世代インターフェース開発の基盤となることが期待される。
ハイブリッド論理$L(\forall)$に対するオルテアンの完全性証明のLean 4による完成 [cs.LO, math.LO]目的：ハイブリッド論理$L(\forall)$の完全性定理の機械検証
- ハイブリッド論理は，様相論理に公理的制約を加え，より表現力豊かな推論を可能にする。
- ハイブリッド論理の完全性証明は複雑であり，機械検証が困難である。
- オルテアンの形式化を完成させ，$L(\forall)$の完全性を証明すること。
- この研究では，2種類の異なる名前生成ツールが必要であることを示した。
- 根拠を伴う最大の整合集合の構築には，言語拡張による構造的な新鮮さが不可欠である。
- 最大整合集合のダイヤモンド後者を得るには，Henkin構成とデータ担持型証拠アキュムレータが必要である。
エージェント駆動型電子設計自動化：ハンドオフの視点 [cs.SE, cs.AI]目的：電子設計自動化におけるハンドオフの有効性
- 電子設計自動化は複雑であり，効率化が不可欠である。
- 従来の設計フローでは，ハンドオフ時の情報伝達に課題がある。
- LLMエージェントを活用し，信頼性の高いハンドオフを実現すること。
- 本調査では，ハンドオフの有効性を軸に82のシステムを分類した。
- システムは，ステージ境界，フロー境界，組織境界の3つのクラスに分類される。
- エージェント間の通信プロトコル（EACP）を提案し，信頼性の高いエージェント駆動型EDAを促進する。
TensorFlowおよびKerasアプリケーションにおける不良コーディング慣行の隠れた環境コスト：リソースリークと炭素排出に関する研究 [cs.SE, cs.LG]目的：TensorFlowおよびKerasにおけるリソースリークがエネルギー消費と二酸化炭素排出量に与える影響の定量化
- 機械学習の普及に伴い，その環境負荷への関心が高まっている。効率性と持続可能性が重要な課題となっている。
- 機械学習コードにおけるリソースリークは，エネルギー消費と二酸化炭素排出量を増加させる隠れた非効率性の原因となるが，その影響を定量的に評価した研究は限られている。
- 機械学習開発におけるリソースライフサイクル管理とエネルギー効率の重要性を強調し，リソースリークによる環境負荷を測定する。
- Improper Model Reuse（IMR）は電力消費量を約32%増加させ，同様の割合で二酸化炭素排出量も増加させた。
- Unreleased Tensor References（UTR）は電力消費量を約46%増加させ，同様の割合で二酸化炭素排出量も増加させた。
- これらの増加は統計的に有意であり，リソースリークが機械学習のエネルギー効率と環境の持続可能性を低下させる可能性があることを示唆している。
CoRaCommit：類似コミット検索によるコミットメッセージ生成のためのVS Code拡張 [cs.RO, cs.SE]目的：コミットメッセージ生成の改善
- バージョン管理において，変更意図を明確にするコミットメッセージは不可欠である。
- 手動での作成は時間がかかり，品質や表現に一貫性が無い場合がある。
- 類似コミットを参考に，より適切なコミットメッセージを提案すること。
- CoRaCommitは，類似コミットを検索し，その情報をプロンプトとして活用することで，コミットメッセージ生成の精度を向上させた。
- 複数のLLMを並行して実行し，ユーザーのフィードバックに基づいて最適なLLMを動的に推奨する。
- ApacheCMデータセットを用いた実験により，既存のVS Code拡張機能と比較して，BLEU，CIDEr，METEOR，ROUGE-Lの指標でCoRaCommitの有効性が示された。
JAMER：プロジェクトレベルのコードフレームワークデータセットとプロフェッショナルゲームエンジンにおけるベンチマーク [cs.SE, cs.CL]目的：プロフェッショナルゲームエンジン上のプロジェクトレベルコードエンジニアリングに関するデータセット及びベンチマーク
- ゲーム開発におけるAI活用は進むも，大規模プロジェクトのコードエンジニアリングは未開拓分野である。
- 大規模データセットと決定論的な評価手法の欠如が，ゲームエンジン上のコード研究の障壁となっている。
- ゲームジャムのプロジェクトを利用し，大規模データセットと評価パイプラインを構築し，課題解決を目指す。
- JamSetとJamBenchという，プロフェッショナルゲームエンジン上のプロジェクトレベルコードフレームワークデータセットとベンチマークを構築した。
- 大規模プロジェクトでは，実行パス率が著しく低下することから，アーキテクチャ設計がボトルネックであることが示唆された。
- JamSetは効果的な学習データとして機能し，コードエージェントはコンパイル率を向上させるも，ランタイム品質は改善されなかった。
アイゼンシュタイン・ヤコビネットワークにおける3つのエッジ非共有ハミルトンサイクルに対する，認定されたユークリッド剰余最小アラインメントスイッチ分解 [cs.DC, cs.IT, cs.NI, math.IT]目的：アイゼンシュタイン・ヤコビネットワークにおける，エッジ非共有ハミルトンサイクルを生成するための最小スイッチ分解手法の開発
- ネットワーク設計において，効率的なサイクル分解は，通信性能や耐障害性に大きく影響する重要な課題である。
- 非互いに素なアイゼンシュタイン・ヤコビネットワークでは，ハミルトンサイクル分解が複雑化し，既存手法では効率性に課題がある。
- ユークリッド剰余族に属するネットワークに対し，最小限のスイッチを用いた，公式に基づいたコンパクトな分解手法を提供すること。
- 本研究では，自然なケイリー幾何学に基づいた局所的なスイッチ計算を開発し，最初の2つのハミルトンサイクルを最小限のスイッチ数で構築した。
- 残りのハミルトンサイクルは，未使用のエッジを補完することで得られ，全体として効率的な分解を実現した。
- 証明は，コンポーネントラベルの崩壊，アンカーのキャンセル，リフトされたスイッチ代表の非衝突，および接続された補完インシデンスの4つの要素に分離された。
巡回結合ネットワークにおけるフォールトトレラントな共有リレー通信 [cs.DC, cs.IT, cs.NI, math.IT]目的：巡回結合ネットワークにおけるフォールトトレラントな2ホップ基本素子の次数冗長性の範囲
- ネットワークの信頼性は重要であり，特に障害発生時の通信維持が不可欠である。
- 従来のネットワーク設計では，障害に対する耐性が十分でない場合がある。
- 本研究は，障害発生時の通信を保証するネットワーク設計手法を確立する。
- 巡回結合ネットワークの生成器の選択が，最悪の場合のリレー生存性に大きく影響することが示された。
- 最適化された閾値設計は，理論的な下限に近いフォールトトレラント性を実現する。
- 標準的な区間生成器は，より高い次数であっても構造的な欠陥により失敗する可能性がある。
高密度アイゼンシュタイン・ヤコビネットワークにおける非冗長フォールトトレラントブロードキャストのための多方向エッジ最小修復 [cs.DC, cs.IT, cs.NI, math.IT]目的：高密度アイゼンシュタイン・ヤコビネットワークにおける非冗長な全ノードへのブロードキャスト修復手法の開発
- ネットワークの信頼性は重要であり，特に大規模なネットワークでは，単一障害点によるシステム全体の停止を避ける必要がある。
- 従来のネットワーク構造では，フォールトトレランスの実現が困難であり，修復コストが高くなる場合がある。
- 高密度アイゼンシュタイン・ヤコビネットワークにおいて，効率的かつ低コストなフォールトトレラントブロードキャストを実現すること。
- 本研究では，EJ-MOEMと呼ばれる多方向エッジ最小修復法を提案し，故障に強いブロードキャストツリーを構築できることを示した。
- 故障に起因するネットワーク成分が連結であれば，正確に$c-1$本の外部修復エッジで十分であると証明された（$c$は健全な成分数）。
- 座標削減ツリーの深さ証明定理を確立し，1つの故障箇所に対して深さ$t+1$以下，2つの故障箇所に対して深さ$t+2$以下で修復可能であることを示した。
ドブリン曲線 [cs.IT, cs.LG, math.IT, math.PR, math.ST, stat.TH]目的：多方向収縮のより詳細なドブリンに基づく特徴付け
- 情報理論において，収縮性の評価はアルゴリズムの性能やプライバシー保護に重要である。
- 従来のドブリン係数は強い条件を必要とし，係数が0の場合には収縮性の保証が得られない。
- ドブリン曲線を用いて，より広い範囲で収縮性の保証を提供し，応用範囲を拡大すること。
- ドブリン曲線は，マルコフ核の収縮性を，入力分布の集まりにおける発散とパワーの特定のレベルで定量化する非線形関数である。
- ドブリン係数の新しい変分的特徴付けを開発し，ドブリン曲線の様々な性質と制約付きバージョンを定義した。
- これらの結果は，ノイズの多い反復最適化，ノイズの多い回路による信頼性の高い計算，オンライン反復アルゴリズムの差分プライバシー保証などの分野に適用される。
Prismriver：Lean 4における音楽理論の形式化とアルゴリズム作曲 [cs.LO, cs.MM]目的：音楽理論の形式化
- 音楽理論は数学的規則と対称性に基づき，その構造を厳密に検証できる。
- 既存の研究では，音楽理論の数学的構造の形式的な検証が不足している。
- Lean 4を用いて音楽理論を形式化し，検証可能な作曲アルゴリズムを開発する。
- 本研究では，Lean 4を用いて音楽理論を形式化したPrismriverを提示した。
- これにより，検証可能なアルゴリズム作曲や伴奏生成への道が開かれる。
- また，音楽構造の単体的解析を可能にする。
大規模言語モデルによるリポジトリレベルのSolidityコード生成：プロンプティングからファインチューニングまで [cs.SE]目的：リポジトリレベルのSolidityスマートコントラクト生成のベンチマークと評価
- ブロックチェーン技術の普及に伴い，スマートコントラクトの安全性と効率性が重要視されている。
- 既存のコード生成ベンチマークは，リポジトリレベルのSolidity生成には不十分である。
- 大規模言語モデルによる信頼性の高いSolidityコード生成戦略を確立すること。
- SolidityBenchと呼ばれる5,470件のリポジトリレベルSolidityスマートコントラクトと自然言語記述のベンチマークを新たに作成した。
- SolidityScoreというSolidity特有のセマンティックメトリックを提案し，セキュリティやコントラクト定義などの重要な要素を重視した。
- ファインチューニングが，Solidity固有の制約をモデルパラメータに組み込むことで，最も大きな改善をもたらすことが示された。
静的エンドポイントを超えて：柔軟なエージェント型ウェブサービスのインターフェースとしてのツールプログラム [cs.SE, cs.AI]目的：エージェント型ウェブサービスにおけるツール利用の効率化
- LLMエージェントの普及に伴い，ウェブサービスとの連携が不可欠となっている。
- 既存のインターフェースは静的エンドポイントが主流で，複雑なワークフローの表現が困難である。
- ツールプログラムを用いることで，多段階のサービス連携を効率的に表現し，性能向上を目指す。
- ToolProは，ツール意図を効果タイプ付きの実行可能なツールプログラムとして表現する。
- 制約に基づくプログラム構築，効果を考慮したリプレイ，そしてプロファイルに基づくポリシーを用いる。
- 実験の結果，エンドツーエンドの待ち時間が最大53.4％，クライアントサイドのトラフィックが最大96.1％削減された。
十分な権限で事足る場合：LLMエージェントにおける過剰な権限を持つツールの選択に関する調査 [cs.SE, cs.AI, cs.CL]目的：LLMエージェントのツール選択における，過剰な権限を持つツールの選択の調査
- LLMエージェントの自律的なツール選択が重要視される中，セキュリティ上の考慮が不可欠となっている。
- 従来のツール選択研究は安全性を考慮せず，権限に基づいた選択は十分に探求されていない。
- より安全なツール選択を促すため，過剰な権限を持つツールの選択とその軽減策を検討する。
- LLMエージェントは，十分な権限を持つ代替手段があるにもかかわらず，過剰な権限を持つツールを選択する傾向があることが示された。
- ツールの一時的な故障は，この過剰な権限を持つツール選択をさらに悪化させる。
- 権限を意識した事後学習防御により，不必要な高権限ツールの使用を大幅に削減しつつ，一般的な機能を維持できることが確認された。
拡散とフローマッチングによるサイト固有のMIMOチャネル生成：忠実度，効率性，および下流タスクへの有用性 [cs.CG, q-bio.NC, cs.CL, cs.IT, eess.SP, math.IT]目的：サイト固有のMIMOチャネルデータの合成
- AIネイティブ無線ネットワークの発展には，現実世界のデータが不可欠である。
- 現実世界のデータを収集するための大規模測定キャンペーンは高コストである。
- データ収集コストを削減し，AI活用を促進する。
- 提案手法は，ユーザー座標に基づき，サイトの空間構造を保持したMIMOチャネル行列を生成する。
- cFMMは，cDDIMと同等の品質を，推論時間の大幅な短縮で実現した。
- 合成チャネルによるデータ拡張は，下流の物理層タスクにおいて性能向上をもたらす。
BARReL：LeanにおけるAtelier Bの現代的なバックエンド [cs.LO]目的：Atelier BとLean間の橋渡し
- 形式手法の産業利用が重要視されており，信頼性の高いソフトウェア開発への貢献が期待される。
- 既存のAtelier Bツールチェーンには，形式的な検証と信頼性のギャップが存在する。
- Leanの強力な型システムを活用し，Atelier B開発の信頼性を高めることを目指す。
- BARReLは，Atelier Bで記述された形式仕様をLean内でインタラクティブに検証可能にする。
- Bのpartial operatorを，Leanの依存型を用いて明確に定義することで，型エラーや未定義のインスタンス化を防ぐ。
- メタプログラミングによって実装されており，Bの構文拡張が容易である。
LLM生成GPUカーネルにおける正しさの錯覚 [eess.SY, cs.SY, cs.SE, cs.DC, cs.LG]目的：LLM生成GPUカーネルの正しさ評価方法の検証
- GPUカーネルは高性能計算に不可欠であり，その自動生成技術が注目されている。
- 既存の評価方法は，限られたテストケースと固定された許容範囲に依存しており，誤った結果を導く可能性がある。
- LLM生成カーネルの信頼性を高めるため，より厳密な正しさ評価手法を確立することを目指す。
- 既存のベンチマークでは，LLM生成GPUカーネルの誤りを検出しきれない場合があることが示された。
- 構築したテストデータを用いて，既存の評価方法では誤ったカーネルを正しく評価してしまう「正しさの錯覚」を再現した。
- 複数のGPU環境で検証した結果，既存の評価方法の限界と，より厳密な評価の必要性が確認された。
パズルを通じた批判的テストリテラシーの学習：経験報告 [cs.SE]目的：批判的テストリテラシー学習におけるパズル活用に関する経験と考察
- ソフトウェアテストは重要だが，教育が困難であるため，効果的な教授法の確立が求められている。
- 既存のテスト教育では，批判的思考力や問題解決能力を育成することが課題となっている。
- パズルを活用した教育フレームワークP4TESTの効果検証と，学習体験の改善を目指す。
- ワークショップ参加者は，パズル解決を通じて実験的な学習体験を得ていると認識していた。
- 学生は一つの解法に収束する傾向があった一方，専門家は探求を続けた。
- パズル解決，振り返り，考察という一連の流れが学習効果の鍵であり，シーケンスの設計が重要である。
ピンチングアンテナを用いた空間ロバストな近距離SWIPT：レート・エネルギートレードオフ限界 [cs.IT, math.IT]目的：空間ロバストな近距離SWIPT設計
- 無線情報と電力の同時伝送は，エネルギーハーベスティング技術を促進し，持続可能なIoT社会の実現に不可欠である。
- 従来の近距離SWIPT設計は点集束型であり，位置ずれや移動に弱く，安定した性能を確保するのが困難である。
- サービスエリア内での品質保証により，ユーザーの移動に対するロバスト性を向上させる設計手法を提案する。
- 提案手法は，サービスエリアにおける情報復号およびエネルギーハーベスティング受信機に対して，品質保証を行うことで空間ロバスト性を実現する。
- レート・エネルギー制約を考慮した非凸二値二次計画問題として定式化し，達成可能なレート・エネルギー領域の上限を決定した。
- 離散アンテナ活性化に基づくエリア網羅型設計は，点集束型アプローチと比較して，安定した性能とロバストなレート・エネルギーのトレードオフを示す。
弱いメモリ検証および堅牢性に関するMSOフレームワーク [cs.LO, cs.PL]目的：弱いメモリモデルのツリー幅とMSO表現可能性に関する研究
- 並行プログラムの検証において，メモリモデルの正確な理解は不可欠である。最適化による影響を考慮する必要がある。
- メモリモデルの数と複雑性の増加により，統一的な検証が困難になっている。
- MSO論理をメタ理論として用いることで，弱いメモリモデルの検証問題を統一的に解決することを目指す。
- シーケンシャルコンシステンシー(SC)モデルは有界ツリー幅を持つことが証明された一方で，TSOモデルは持たない。
- リリース/アキュアイアやRC20といった幅広いモデルはMSOで表現可能だが，Strong Release/AcquireやTSOは，特定の問題が解決されない限り不可能。
- 読み込み依存性の堅牢性という概念を導入し，MSO表現可能なモデルにおいて，プログラムの検証または非堅牢性の報告を行うアルゴリズムの存在を示した。
コーディングエージェントによるN版プログラミング [cs.SE]目的：コーディングエージェントを用いたN版プログラミングの有効性
- ソフトウェアの信頼性確保は重要であり，特に安全性が求められるシステムでは不可欠である。
- 単一の実装に依存するシステムは，その実装の欠陥により全体が影響を受けるリスクがある。
- 多様な実装によるN版プログラミングは，共通の欠陥によるシステム全体の故障を回避する手段となる。
- コーディングエージェントによる実装においても，Knight-Levesonの実験と同様に，共通モード故障が多数確認された。
- 仕様が曖昧な箇所に共通の故障が発生しやすいことが示された。
- 3版による多数決を用いることで，単一実装に比べて故障数が大幅に減少した。11,844個のN版ユニットで故障が全く見られなかった。
ハイパーグラフ推論に基づく暗黙的意味認識通信 [cs.AI, cs.IT, cs.NI, math.IT]目的：意味認識通信における暗黙的意味の解釈精度向上
- 次世代通信システムにおいて，ビット単位の伝送から意味の理解へと重点が移りつつあり，その重要性が高まっている。
- 既存研究では，意味内容をグラフ構造で表現するものの，ペアの関係性のみに着目し，高次の関係性を捉えきれていない。
- 本研究は，ハイパーグラフを用いて複雑な多要素間の関係性を表現し，意味推論の曖昧さを解消し，性能低下を防ぐことを目指す。
- 提案手法HISRは，従来のグラフ埋め込み法の過剰平滑化の影響を軽減し，多様な意味的相互作用を分離する。
- HISRは，伝送中の情報損失が発生した場合でも，堅牢な意味推論を可能にする。
- 数値実験の結果，提案手法HISRは最先端のベンチマークと比較して，暗黙的意味解釈の精度を最大36.6%向上させた。
- 1
- 2