arXiv雑要約

プログラム - 2026/06/17 公開

  • ANEForge:Apple Neural Engine の直接計算のためのPython [cs.PL, cs.AI, cs.MS]目的:Apple Neural Engine の直接制御と計算処理
    • モバイルデバイスにおけるAI処理の高速化が重要視されている。
    • CoreML 経由では ANE の潜在能力を最大限に引き出せていない。
    • CoreML を介さずに ANE を直接制御し,パフォーマンスを向上させる。
    • ANEForge は,CoreML を使用せずに ANE を直接プログラムする Python パッケージである。
    • ANEForge は 58 個の融合演算子と 19 個のネイティブブリッジ演算子からなる遅延テンソルグラフを ANE プログラムにコンパイルする。
    • ResNet-18 の推論処理を 0.33ms で実行可能であり,フレームワーク参照と同等の性能を示す。

    Link: https://arxiv.org/abs/2606.17090

  • LogCopilot:大規模言語モデルによるログ集約分析の自動化 [cs.SE]目的:ログ集約分析の自動化
    • システム規模の拡大に伴い,ソフトウェアのデバッグや障害診断におけるログ分析の重要性が増している。
    • 既存のログ分析システムでは,DSLクエリ言語の習熟やログの詳細な理解が必要であり,クエリ作成に手間がかかる。
    • 大規模言語モデルを用いて,自然言語による指示に基づいてログ分析を自動化し,クエリ作成の負担を軽減すること。
    • LogCopilotは,ログの主要情報を階層的な知識ベースとして構築・提供することで,LogQLクエリの自動生成と実行を実現した。
    • 4つのログデータセットを用いた評価の結果,LogCopilotは平均76.8%の精度を達成し,ベースライン手法を上回った。
    • 実験により,LogCopilotがLogQLクエリ生成において有効であることが示された。

    Link: https://arxiv.org/abs/2606.17094

  • ソフトウェア委任契約:AIコーディングエージェントの作業におけるレビュー可能性の測定 [cs.SE, cs.AI]目的:AIコーディングエージェント作業におけるソフトウェア委任契約の効果測定
    • AIによるソフトウェア開発が普及し,コード品質の保証が重要な課題となっている。
    • 委任されたコーディング作業において,レビューの効率性と正確性が課題となっている。
    • ソフトウェア委任契約がレビュー可能性に与える影響を定量的に評価すること。
    • 明示的な委任契約は,客観的なタスクの成果を改善しなかった。全ての実行が非公開の受容テストに合格した。
    • しかし,レビュー可能性は向上した。証拠の十分性が22/30のペア比較で改善し,曖昧さは減少した。
    • 契約によってレビューに必要な情報(変更ファイルリスト等)が明確化され,エージェントのトークン消費量は13%増加,実行時間は38%増加した。

    Link: https://arxiv.org/abs/2606.17099

  • PromptMN:疑似プロンプト言語 [cs.CL, cs.HC, cs.MA, cs.CL, cs.AI, cs.HC, cs.PL, cs.SE]目的:生成AIへの指示方法の明確化
    • 生成AIの利用拡大に伴い,人間とAI間のインターフェースとしてのプロンプトの重要性が増している。
    • 自然言語によるプロンプトは曖昧になりやすく,AIの誤動作の原因となることがある。
    • PromptMNは,プロンプトの曖昧さを解消し,AIとの連携を円滑にすることを目的とする。
    • PromptMNは,役割,目標,制約などを%記号で始まる型付き指示子で自然言語に注釈する疑似プロンプト言語である。
    • 複数の最先端モデル(Claude, Gemini, GPT)において,PromptMNの指示子が正確に解釈され,ファインチューニングなしで複雑な構造も処理可能であることが確認された。
    • PromptMNは,コードベースの変更や保守,再設計など,ソフトウェア開発ライフサイクル全体で再利用可能な成果物となりうる。

    Link: https://arxiv.org/abs/2606.17164

  • マルチエージェント大規模言語モデルシステムにおける並行性異常の検証による検出と防止 [cs.LG, cs.DC, cs.LO, cs.MA, cs.PL]目的:マルチエージェント大規模言語モデルシステムの並行性異常の検出と防止
    • 大規模言語モデルの利用拡大に伴い,複数のエージェントが連携するシステムの構築が重要になっている。
    • 共有メモリやツール登録において,並行実行によるデータ競合などの異常が発生しやすい。
    • 形式手法を用いて並行性異常を厳密に検証し,安全なシステム構築を目指す。
    • マルチエージェントLLMシステムに発生する4つの並行性異常(陳腐化生成,ファントムツール,因果的カスケード,ツール効果の再順序化)をTLA+で形式化し,TLCで反例を作成した。
    • これらの異常に対する検出器の健全性と完全性を,274のVerus義務を用いて機械的に検証した。
    • Rustで実装された3つの実行環境(L0-L1)を検証し,L2-L4については実行モード検証と依存性なしの防止ツインを用いて実証した。

    Link: https://arxiv.org/abs/2606.17182

  • 大規模自動車ソフトウェア要件に対するクラスタ認識型二段階テスト仕様生成 [cs.SE, cs.AI]目的:自動車SPICE SWE.6要件を満たすテスト仕様の生成
    • 自動車ソフトウェア開発において,品質保証は安全性に直結するため重要である。
    • 要件数が増大すると,手動でのテスト仕様作成に膨大な時間と労力がかかる。
    • 大規模要件群におけるテスト効率と網羅性を向上させることを目指す。
    • 提案手法は,要件間の依存関係を考慮しつつ,大規模な要件群に対応可能である。
    • クラスタリングと要約を組み合わせることで,統合テストの網羅性と要約の忠実性を向上させた。
    • ISO 26262やASPICE等の規格に準拠したテスト仕様を生成することが可能となった。

    Link: https://arxiv.org/abs/2606.17197

  • 信頼性に基づいたマルチエージェント追跡可能性:一貫性のあるソフトウェア成果物管理のための信頼度較正ナレッジグラフ [cs.RO, cs.SE, cs.AI]目的:ソフトウェア成果物管理における一貫性確保
    • 安全性確保が重要な分野において,ソフトウェア開発の自動化が不可欠である。
    • エージェント間の連携不足により,誤りや不確実な情報が伝播し,矛盾や欠落が生じやすい。
    • エージェント間の信頼度を考慮し,一貫性のある追跡可能性を確保することで,これらの問題を解決する。
    • 提案手法では,ナレッジグラフを用いてエージェント間の信頼度を評価し,連携を促進することで,より正確な追跡可能性を実現する。
    • 提示された二段階のトレーサビリティリンク予測パイプラインは,埋め込みベースの検索とLLMベースの多基準分析を組み合わせることで,高い精度を示す。
    • 自動車ソフトウェア工学のケーススタディにおいて,信頼度較正の有効性が確認された。

    Link: https://arxiv.org/abs/2606.17203

  • ロバスト半空間学習における重み付きヒンジ法の二乗和次数障壁:クリストフェル関数の特徴づけ [cs.LG, cs.DS, stat.ML]目的:ロバストな半空間学習における外れ値除去の限界とその特徴付け
    • 機械学習におけるロバスト性は,ノイズの多いデータからの信頼性のある学習に不可欠である。
    • 外れ値の存在は,学習アルゴリズムの性能を著しく低下させる主要な課題である。
    • クリストフェル関数を利用し,外れ値除去の限界を明確化し,ロバスト学習の改善を目指す。
    • 外れ値除去証明書は低次のモーメントのみを用いるため,敵対者はその特性を利用して外れ値を隠蔽する。
    • 外れ値が隠蔽可能な領域の大きさは,クリーンドデータのクリストフェル関数によって正確に決定される。
    • 二乗和次数のトレードオフや次数2の外れ値障壁など,証明書法に対する限界が示唆された。

    Link: https://arxiv.org/abs/2606.17215

  • 残留過程挙動に対するストーン・チェフ収集意味論 [cs.LO, cs.PL]目的:非終端計算によって残された残留挙動のコンパクトな収集意味論
    • 並行処理や分散システムの検証において,無限に続く計算の挙動を理解することは重要である。
    • 既存の手法では,無限計算の多様な挙動(反復,脱出など)を統一的に捉えることが困難であった。
    • ストーン・チェフコンパクト化を用いて,残留過程の挙動を精密かつ統一的に捉えるための基盤を提供する。
    • ストーン・チェフコンパクト化を利用した収集意味論が,通常の反復,混合反復,および観測空間の非コンパクト部分への脱出を共通の枠組みで扱えることを示した。
    • 残留過程のストリームを構造同値性でモジュール化したことで,安定的な発散,有限反復発散,混合反復と脱出,および無限残留成長による脱出を区別できるようになった。
    • 前置,ガード付き展開,有限選択,有限接頭辞選択形式に対する残留尾法則が検証され,並列合成と同期化における法則の境界が特定された。

    Link: https://arxiv.org/abs/2606.17228

  • ソフトウェアベンチマークにおける適切な選択:状態を持つ環境における一貫した意思決定 [cs.PF, cs.SE, stat.AP]目的:状態を持つ環境下におけるソフトウェアベンチマークの一貫性確保
    • 近年のコンピューティングシステムは性能向上を目指し,効率化のために状態を持つ機構に依存している。
    • 適応機構は測定間に時間的依存性をもたらし,個々のプログラム性能の推定に偏りを生じさせる。
    • 絶対的な測定値ではなく性能差を重視し,最速プログラムの識別を意思決定問題として捉える。
    • 提案する実験設計は,プログラム固有の偏りを相殺し,一貫した性能差の推定を可能にする。
    • これらの設計は漸近的に正しい意思決定を導き,限られた予算でのベンチマークに頑健な手法を提供する。
    • 性能に敏感なソフトウェア開発に広範な影響をもたらすと考えられる。

    Link: https://arxiv.org/abs/2606.17261

  • 構文システムは意味的不変量を見ることができない [cs.LO, cs.CR]目的:帰納法の二つの理論,開帰納法と節集合サイクル,の比較可能性
    • 計算可能性理論は,計算の限界と可能性を探求する上で不可欠である。
    • 既存の理論では,数論的な事実と記号的な操作の区別が曖昧になっている。
    • この研究は,構文的な操作が意味論的な不変量にアクセスできないことを示す。
    • 開帰納法と節集合サイクルの比較可能性に関する未解決問題を解決した。
    • 加算規則の適用条件により,$a{+}b$と$b{+}a$は区別可能であり,これは数論的な事実である。
    • この研究から導かれる「構文不変性原理」は,P versus NP問題の障壁にも示唆を与える可能性がある。

    Link: https://arxiv.org/abs/2606.17275

  • アイゼンシュタイン・ヤコビネットワークにおける完全リソース配置の局所的復旧 [cs.DC, cs.IT, cs.NI, math.IT]目的:アイゼンシュタイン・ヤコビネットワークにおける完全リソース配置の,リソース故障後の局所的復旧
    • 通信ネットワークの信頼性確保は重要であり,リソース配置の最適化は特に不可欠である。
    • リソース故障時の迅速かつ効率的な復旧手法は確立されておらず,ネットワーク性能低下の原因となる。
    • 本研究は,アイゼンシュタイン・ヤコビネットワークにおけるリソース故障時の局所的復旧戦略を解明し,最適化することを目指す。
    • 単一のリソース故障に対し,1つの代替リソースでは故障した六角形をカバーできないが,2つで常にカバー可能であることが証明された。
    • 二つのリソース故障の場合,独立した復旧では4つの代替リソースが必要だが,特定の配置では3つで済む場合がある。
    • 故障したセルが十分に離れている場合,q個のリソース故障に対しては2q個の代替リソースで復旧が可能であり,密なクラスタ故障に対しては更なる削減が確認された。

    Link: https://arxiv.org/abs/2606.17288

  • 差分プライバシーを用いたスケーラブルなk-クリーク推定 [cs.DS]目的:k-クリーク数の推定
    • グラフ構造はネットワーク分析等に不可欠であり,その統計量の正確な把握が重要である。
    • グラフデータには個人情報が含まれる場合があり,プライバシー保護が課題となる。
    • プライバシー保護と効率的な推定を両立するアルゴリズムが求められている。
    • 提案手法は,ラダー関数を滑らかな上限として利用することで,ノイズ量を削減し,計算時間を大幅に改善した。
    • 実験の結果,提案手法は従来のラダー関数に基づく推定よりも数桁高速であり,精度は同程度であることが示された。
    • 提案手法は,数百万エッジ規模のグラフや,より大きなk値に対して初めてスケーリングに成功した。

    Link: https://arxiv.org/abs/2606.17297

  • 単体複体からの非ユニタル可換環上の符号の構成とその応用 [cs.CL, cs.IT, math.IT]目的:単体複体から構成される非ユニタル可換環上の線形符号
    • 符号理論は,通信やデータ保存における誤り検出・訂正に不可欠な技術である。
    • 従来の符号構成法では,限られた種類の環のみに適用可能であることが課題であった。
    • より広範な環上で効率的な符号を構成し,その特性を明らかにすることを目指す。
    • 本研究では,単体複体を用いて,非ユニタル可換環上の線形符号を構成し,そのパラメータを決定した。
    • 構成された符号のGray像や準フィールド符号が,整除可能な符号族を生み出すことを示した。
    • さらに,これらの符号が最小,最適,自己直交であるための十分条件を確立し,射影少数重み符号や局所回復可能符号への応用を示した。

    Link: https://arxiv.org/abs/2606.17300

  • 空間効率の良いロックフリー線形探査ハッシュテーブル [eess.SY, cs.SY, cs.DC, cs.DS]目的:空間効率の良いロックフリー線形探査ハッシュテーブルの設計
    • ハッシュテーブルはデータ管理の基盤技術であり,高速な検索が求められる場面で広く利用されている。
    • 並行環境下での線形探査ハッシュテーブル実装は難しく,高い空間効率とライブネス保証の両立が課題であった。
    • 少ないメタデータで並行性とライブネスを保証し,効率的な空間利用を実現するハッシュテーブルを提案する。
    • 本研究では,待機不要な探索を持つロックフリー線形探査ハッシュテーブルを提案した。
    • 提案手法は,テーブルエントリあたり定数ビットまたは対数ビット程度のメタデータしか使用しない。
    • 挿入,削除,探索操作は線形化可能でロックフリーであり,削除された要素の領域も安全に再利用できる。

    Link: https://arxiv.org/abs/2606.17315

  • 近似を保持するコアセット [cs.DS]目的:良質な解のコストを保持するコアセットの定義と構築
    • 大規模データに対するクラスタリングは重要であり,コアセットはそのための有効な手法の一つである。
    • 理論的な保証よりも遥かに小さいコアセットサイズでも十分な結果が得られる場合がある。
    • 良質な解のコストのみを保持するコアセットを構築し,その有用性を検証する。
    • 本研究では,近似を保持するコアセットを定義し,従来の強コアセット,弱コアセットの中間的な保証を提供する。
    • このコアセットは,良質な解に対しては高い精度を保ちながら,サイズを大幅に削減できる。
    • 近似率のわずかな歪みであっても,このサイズのコアセットは存在しないことが示された。

    Link: https://arxiv.org/abs/2606.17316

  • Rust標準ライブラリの検証 [cs.LO, cs.PL, cs.SE]目的:Rust標準ライブラリの検証活動
    • メモリ安全性の重要性が増しており,プログラムの信頼性確保が不可欠である。
    • Rust標準ライブラリはunsafeコードに依存しており,静的検証が不足している。
    • 標準ライブラリの安全性を高めるため,形式検証による安全性の証明を目指す。
    • 大規模な検証キャンペーンを実施し,複数の検証ツールを統合した。
    • 機械的に検証された証明が,境界外アクセス等の未定義動作の検出に有効であることが示された。
    • 形式手法コミュニティへの課題として,残された検証の障害が明確にされた。

    Link: https://arxiv.org/abs/2606.17374

  • プライバシー強化技術の採用を要件工学を通して支援する [cs.SE]目的:プライバシー強化技術の採用促進
    • 個人情報を取り扱うシステムにおいて,プライバシー保護は重要性を増しており,技術的対応が求められている。
    • プライバシー強化技術は研究が進んでいるものの,実際のソフトウェア開発への導入は十分ではない。
    • 要件工学の視点から,技術,ビジネス,法律の各側面を考慮し,採用の課題を解決する。
    • 本研究では,プライバシー強化技術の採用における課題を,関係者や専門分野を跨って分析した。
    • 要件工学を通して,それぞれの視点における課題を体系的に扱うことで,プライバシー強化技術の導入を円滑化できると主張する。
    • 各視点を明示的に要件化することで,関係者間の連携を促進し,ソフトウェア工学におけるプライバシー強化技術の利点を最大限に引き出すことができる。

    Link: https://arxiv.org/abs/2606.17387

  • AI 強化バイナリ逆アセンブルに関する知識の体系化 [cs.CR, cs.AI, cs.SE]目的:AI 強化バイナリ逆アセンブルに関する知識の体系化
    • ソフトウェア理解,脆弱性発見,マルウェア解析など,情報セキュリティ分野において基盤技術である。
    • コンパイル過程で意味情報が失われ,解析が困難であるという課題が存在する。
    • AI 技術を用いて,バイナリ逆アセンブルの効率化と精度向上を目指す。
    • 本研究では,2015年以降に発表された144件の論文を分析し,AI強化バイナリ逆アセンブルの分野を体系的に整理した。
    • 従来の解析技術,バイナリから得られる成果物,表現戦略,学習パラダイムなどを統合的に捉える分類体系を提示した。
    • この研究は,多様なアプローチの共通構造を明らかにし,今後の研究の方向性を示唆する基盤となる。

    Link: https://arxiv.org/abs/2606.17398

  • 教育におけるLLM判定:カリキュラムに基づく採点パイプライン [cs.CL, cs.AI, cs.SE]目的:カリキュラムに基づいた採点パイプラインの構築
    • 教育評価におけるAI活用は,学習の質向上や効率化に貢献しうる重要な課題である。
    • LLMを試験採点に利用する場合,公平性や透明性の確保が課題となる。
    • 公式カリキュラムと採点基準に沿った,信頼性の高い自動採点システムの開発。
    • 本パイプラインは,質問の関連トピック,サブトピック,認知レベルを特定し,LLMによる客観的な判断を支援する。
    • 生成された採点基準は,公式カリキュラムに根ざしており,透明性と一貫性を高める。
    • 予備評価の結果,LLMによる採点結果は人間の採点者と同等であり,根拠もより明確であることが示された。

    Link: https://arxiv.org/abs/2606.17507

  • 次のステップが必ずしも1ステップとは限らない:並行Goプログラムの分布を考慮した実行モデリング [cs.LG, cs.DC, cs.PL, cs.SE]目的:並行プログラムの次のステップの予測モデル
    • 並行プログラムのデバッグは困難であり,効率的なツールが求められている。
    • スケジューラ非決定性により,同じ入力でも次のステップが複数存在し,予測が難しい。
    • スケジューラの非決定性を学習信号として活用し,予測精度向上を目指す。
    • 分布を考慮した学習により,798件のGoプログラムのバグ予測において36.2%の精度を達成した。
    • これは,ゼロショットのGemini 3.5 Flash (34.8%) や,ファインチューニングなしのモデル (28.6%) よりも高い。
    • 期待キャリブレーション誤差を0.205から0.169に低減し,モデルの信頼性を向上させた。

    Link: https://arxiv.org/abs/2606.17508

  • OmniDroneX:LLM支援による包括的なドローン・アズ・ア・サービス生態系 [eess.SY, cs.SY, cs.SE, cs.SY, eess.SY]目的:ドローン・アズ・ア・サービス生態系の構築
    • ドローン技術は急速に進歩する一方,その実用展開には制約が存在する。
    • 既存のドローンシステム研究には,機能や連携に関する課題が残されている。
    • ドローンを動的に構成可能な存在とし,多様な機能を提供する生態系を構築する。
    • OmniDroneXは,ドローンの低レベルな物理機能と高レベルなミッション意図を統合する統一インターフェース(libUAV)と物理-サービス抽象モデル(PT-SOA)を導入する。
    • 大規模言語モデル(LLM)をアーキテクチャの各層に活用し,機能の特定,サービス定義の形式化,自動サービス合成,自然言語によるミッション仕様などを支援する。
    • 物理層の機能拡張,時空間的・機能的・協調的・例外対応型・QoSベースのサービス合成といった構成技術により,スケーラブルで強靭なドローン生態系を実現する。

    Link: https://arxiv.org/abs/2606.17510

  • 反復フィードバックループによるLLMコード修正の可能性の解明 [cs.SE, cs.AI]目的:LLMによる自己コード修正能力の評価
    • ソフトウェア開発において,コード修正は不可欠であり,効率的な修正手法が求められている。
    • 既存のLLM評価は単一試行の精度に焦点を当て,実際の開発における反復修正プロセスを考慮していない。
    • LLMが実行フィードバックを通じてコードを修正する能力を評価し,改善点を見出す。
    • 推論能力を持つモデルは反復を通じて一貫して性能が向上し,フィードバックの活用において推論能力を持たないモデルを大きく上回った。
    • 構文エラーや実行時エラーは,論理的またはアルゴリズム的なエラーよりも修正が容易であった。
    • 本研究は,LLMを活用したコード生成システムにおけるフィードバックループの理解と応用に関する洞察を提供する。

    Link: https://arxiv.org/abs/2606.17514

  • 高密度ガウスネットワークにおける完全リソース配置の局所的障害復旧 [cs.DC, cs.IT, cs.NI, math.IT]目的:高密度ガウスネットワークにおける完全リソース配置の障害発生後の復旧
    • ネットワークリソース配置は,通信ネットワークの性能と信頼性に不可欠である。
    • リソース障害発生時の効率的な復旧手法が確立されていない。
    • 高密度ガウス配置における局所的な障害復旧方法を特定し,最適化すること。
    • 1つのリソースが故障した場合,故障セル内での局所的な復旧が可能であり,必要な置換数はt=1で3,t≧2で2となる。
    • 2つのリソースが故障した場合,t≧2では常に4回の局所置換で復旧が可能である。
    • 高次の密集コアにおいても,包含と排除の原理に基づく公式は正確性を保ち,追加的なオーバーラップはP_2-A-C_3で表現できる。

    Link: https://arxiv.org/abs/2606.17527

  • 高密度ガウスネットワークにおける非冗長耐障害ブロードキャストのための多方向エッジ最小修理 [cs.DC, cs.IT, cs.NI, math.IT]目的:高密度ガウスネットワークにおける,非冗長なワンツーオールブロードキャスト修理手法
    • ネットワークの信頼性は重要であり,特に大規模な通信システムにおいて,故障に対する強靭性が求められる。
    • 既存手法では,故障発生時の修理に冗長性が伴う場合があり,ネットワーク効率が低下する可能性がある。
    • 本研究では,故障に強く,かつ修理に必要なエッジ数を最小化する手法を提案し,ネットワーク効率の向上を目指す。
    • 提案手法(MOEM)は,ガウスブロードキャストツリーの様々な方向性を評価し,故障を考慮した最適な方向性を選択する。
    • 故障箇所を除去後,健全な構成要素を連結し,外部エッジを用いて修理を行うことで,非冗長な修理を実現する。
    • 理論的証明と実験結果により,MOEMが少ない外部修理エッジ数で故障に強く,効率的な修理が可能であることが示された。

    Link: https://arxiv.org/abs/2606.17528

  • カクタスグラフへの辺削除に対する厳密アルゴリズムと重み付き変種 [cs.DS]目的:カクタスグラフへの辺削除問題の厳密解法
    • グラフ理論は,ネットワーク分析や最適化問題など,様々な分野に応用されている。
    • カクタスグラフへの辺削除問題はNP困難であり,効率的なアルゴリズム開発が課題である。
    • 最小の辺削除数でカクタスグラフを得るアルゴリズムを開発し,計算量を改善する。
    • 本研究では,未重みの場合の計算量を $O^*(3^n)$ から $O^*(2^n)$ へと改善した。
    • 削除コストが $q$ 種類までの重み付き問題は,$O^*(2^n n^{O(q)})$ で解ける。
    • 総重量が $W$ の非負整数コストの場合,$O^*(2^n(W+1))$ の擬似多項式時間アルゴリズムを得た。

    Link: https://arxiv.org/abs/2606.17578

  • Visored:LLM生成数学に対する制御自然言語証明器 [cs.PL, cs.AI]目的:LLM生成数学の証明可能性検証
    • 数学の自動化は,定理の発見や検証を加速し,研究効率を飛躍的に向上させる。
    • 既存の証明システムは形式的すぎて,LLMや人間の数学記述との乖離が大きい。
    • LLMが記述した数学の証明を形式的に検証可能なLeanコードへと変換すること。
    • Visoredは,自然な数学言語に近い形式と,自動化された推論規則層を備えている。
    • 実験の結果,特定のプロバー訓練データなしでも,LLMはminiF2Fベンチマークで効果的にVisoredを使用できることが示唆された。
    • Visoredは,受け入れられた証明を検証済みのLeanファイルとして再出力できる。

    Link: https://arxiv.org/abs/2606.17581

  • 論文タイトル・抄録スクリーニングにおけるLLMの理解:不一致から提言へ [cs.SE, cs.AI]目的:論文タイトルと抄録のスクリーニングにおける大規模言語モデル(LLM)の不一致とその要因分析
    • システマティックレビューの質と効率を向上させる上で,情報検索の精度が重要である。
    • LLMのスクリーニング精度にはばらつきがあり,信頼性に関する疑問が残されている。
    • LLMと人間の不一致の原因を特定し,LLMの有効活用に向けた提言を行う。
    • LLMと人間のスクリーニング結果のKappa値は0.52から0.77の範囲であった。
    • 不一致の原因として,キーワードの過剰強調,曖昧な用語の解釈,誤ったトピック推論などが明らかになった。
    • LLM導入前の意味理解の検証,複数LLMの実行,境界事例への検証注力などの提言を行った。

    Link: https://arxiv.org/abs/2606.17588

  • モデルの信頼性だけでは不十分:シミュレーションアーキテクチャにおける信頼性の再考 [cs.SE]目的:シミュレーションアーキテクチャにおける信頼性の評価
    • シミュレーションは複雑なシステムを理解する上で不可欠であり,その信頼性は重要である。
    • シミュレーションアーキテクチャ全体の信頼性評価手法が確立されていない。
    • 構成モデルの信頼性からアーキテクチャ全体の信頼性を評価する問題に取り組む。
    • 感度分析,専門家による定性分析,AIの説明可能性,ネットワーク等の既存手法を比較検討した。
    • 各手法の厳密性,一般化可能性,リソース要件に基づき,強みと弱みを明らかにした。
    • シミュレーションアーキテクチャの信頼性評価における課題と今後の方向性を示した。

    Link: https://arxiv.org/abs/2606.17593

  • 植えられた三角形濃密な部分グラフのスペクトル復元 [cs.DS, math.PR, math.ST, stat.TH]目的:三角形濃密な部分グラフの復元
    • グラフ構造の解析は,ネットワーク科学やデータマイニング等の分野で重要である。
    • 大規模グラフにおける密な部分グラフの発見は計算困難であることが知られている。
    • ランダムグラフ中に植えられた密な部分グラフの復元を試みる。
    • 提案アルゴリズムは,局所的な符号付き三角形カウントに基づくグラフ行列を用いる。
    • グラフ行列のスペクトル解析を通じて,アルゴリズムの理論的な保証を確立した。
    • 植えられたクリーク問題と同様の,統計的閾値と計算閾値のギャップが存在する。

    Link: https://arxiv.org/abs/2606.17604

  • PracRepair:人間らしいデバッグ手法に着想を得たLLMを活用した自動プログラム修正 [cs.CL, cs.DL, cs.CY, cs.SE]目的:ソフトウェアの自動修正手法の開発
    • ソフトウェアの規模と複雑性が増し,デバッグと修正には多大なコストと時間がかかるため,自動化が重要である。
    • 既存のLLMベースの自動プログラム修正は,静的または検索されたコンテキストに依存し,動的な情報(実行トレース等)の活用が不十分である。
    • 失敗実行のダイナミクスや修正の検証ダイナミクスといった動的情報を効果的に活用し,より正確な修正を行うことを目指す。
    • PracRepairは,バグのあるプログラムと失敗実行から必要に応じて静的-動的コンテキストを構築する。
    • 質問駆動型の失敗診断により,明示的な修正仮説を生成し,検証診断とトレースレベルの行動変化を用いて候補パッチを反復的に改良する。
    • Defects4J V1.2/V2.0において,GPT-3.5でそれぞれ139/136件,GPT-4oで162/171件のバグを修正し,既存の手法を上回った。

    Link: https://arxiv.org/abs/2606.17612

  • FacProcessTwin:LLMに基づくプロセスツイン開発システム [cs.SE, cs.AI]目的:プロセスツインの迅速な開発
    • 製造プロセスの効率化が求められる中,プロセス全体の可視化が重要である。
    • 従来のデジタルツインは単一機械に焦点を当て,プロセス全体の相互作用を捉えきれない。
    • プロセスツイン開発のコストと時間を削減し,実用化を促進すること。
    • FacProcessTwinは,LLMを活用し,プラントのプロセス文書とオペレーターの自然言語入力を基にプロセスツインを生成する。
    • 生成されたモデルの精度はF1スコアで95.2%と高く,手動開発時間の約6分の1で完了する。
    • 安全に関わるバインドにおいて,オペレーターの介入により誤バインドをゼロに抑えることが可能となった。

    Link: https://arxiv.org/abs/2606.17666

  • LLMによるコード翻訳における機能的正確性と実行効率のギャップを埋める [cs.CL, cs.CL, cs.PL]目的:LLMベースのコード翻訳の機能的正確性と実行効率の向上
    • ムーアの法則の限界により,プログラムの品質において実行効率が機能的正確性同様に重要になっている。
    • LLMで翻訳されたコードは,人間が書いたコードと比較して実行速度が遅くなる傾向があり,プロンプトエンジニアリングだけでは解決できない。
    • 多様な翻訳候補の生成と,それらの差分に基づいた最適な候補の選択により,実行効率と正確性の両立を目指す。
    • 提案手法SwiftTransは,既存のCodeNet,F2SBenchに加え,新たに作成したSwiftBenchの3つのベンチマークにおいて,機能的正確性と実行効率の両面で改善を達成した。
    • SwiftTransは,多角的な探索と差分を意識した選択という2段階構成で,LLMの適応能力を高めるための階層的ガイダンスと順序的ガイダンスを導入している。
    • MpTranslatorは並列インコンテキストラーニングを利用して多様な翻訳候補を生成し,DiffSelectorは翻訳間の差分を明示的に比較することで最適な候補を特定する。

    Link: https://arxiv.org/abs/2606.17683

  • 無限状態システムに対するLTL検証における終止解析の検証 [cs.LO]目的:無限状態システムのLTL検証
    • ソフトウェアやハードウェアの正確性を保証する上で重要であり,安全性や信頼性確保に不可欠である。
    • 状態数が無限であるため,従来のモデル検査手法では適用が困難なケースが多い。
    • 終止解析を活用することで,無限状態システムにおけるLTL検証の実現を目指す。
    • 提案手法MoATは,既存の終止解析ツールを活用し,LTLモデル検査問題を公平な終止性に帰着させる。
    • 実験結果から,MoATは無限状態システムに対するLTLモデル検査において,既存の最先端ツールと同等の性能を示すことがわかった。

    Link: https://arxiv.org/abs/2606.17693

  • 極性符号のブラインド認識に関する仮説検定分析 [cs.SI, cs.IT, math.IT]目的:極性符号伝送のブラインド認識
    • 非協調的ワイヤレスフォレンジックやセキュリティ指向の信号分析において,符号化方式の特定が重要である。
    • 極性符号の符号長が未知の場合,凍結ビット/情報ビット位置のパターン復元が困難である。
    • 逐次キャンセルに基づく合成ビットチャネル表現を用いて,ブラインド認識の理論的限界を解明する。
    • 理想的な逐次キャンセル条件下で,ビット位置認識を二値仮説検定として定式化し,識別可能性の理論的指標を導出した。
    • 採用したソフト認識指標が,シフトされた対数尤度比として解釈できることを示した。等確率の場合はln 2が中立閾値となる。
    • 複数の独立した観測下での位置別およびシーケンスレベルの認識誤り確率の上限と下限を導出し,オーバーラップ係数とバッタチャリヤパラメータの関係を明らかにした。

    Link: https://arxiv.org/abs/2606.17705

  • 2026年アルゴリズム情報理論データ圧縮チャレンジ [cs.IT, cs.DS, math.IT]目的:汎用的な無損失圧縮アルゴリズムの性能評価
    • データ圧縮は,ストレージ,通信,計算資源に不可欠であり,情報科学の根幹をなす。
    • 現実的な制約下での汎用圧縮アルゴリズムの客観的評価が困難である。
    • 圧縮性能と汎化能力を測るベンチマーク環境の確立を目指す。
    • 圧縮比,速度,Weissmanスコア等の指標から,最適化目標による性能差が確認された。
    • モデル化に注力した圧縮器は,高い計算コストを伴いながらも,より高い圧縮率を達成した。
    • 隠れたテストデータと外部データセットを用いた評価により,汎化性能の重要性が再確認された。

    Link: https://arxiv.org/abs/2606.17712

  • 低退化グラフストリームにおける4サイクル数え上げ [cs.DS]目的:グラフストリームにおける4サイクル数の$(1+\varepsilon)$-近似
    • 大規模グラフの分析は,ソーシャルネットワークやウェブグラフなど様々な応用において不可欠である。
    • グラフストリーム環境下での正確な4サイクル数え上げは,メモリ使用量が多く困難である。
    • メモリ効率の良いアルゴリズムを開発し,実用的なグラフストリームにおける4サイクル近似を可能にすること。
    • 2回のパスを用いるアルゴリズムは,既存手法と比較して大幅に少ないメモリ使用量で所望の精度を達成する。
    • 1回のパスを用いるアルゴリズムは,4サイクルが局所的に集中していない場合に高い精度を維持する。
    • 両アルゴリズムは,非二部グラフを含む様々な実グラフストリームにおいて良好な性能を示す。

    Link: https://arxiv.org/abs/2606.17732

  • 部分観測マルコフ決定過程におけるシグナリングと制御のための情報理論的メタ動的計画法 [cs.IT, cs.SY, eess.SY, math.IT, math.OC]目的:部分観測マルコフ決定過程における同時シグナリングと制御の最適化
    • 複雑なシステム制御において,情報理論的アプローチは効率的な意思決定を可能にする重要な役割を果たす。
    • 部分観測環境下での最適な制御戦略設計は,観測情報の不確実性により困難である。
    • 行動から観測への情報量を最大化しつつ,コスト制約を満たす制御戦略を導出すること。
    • 提案手法は,条件付き確率分布空間上の状態を定義するメタ動的計画法を導出し,効率的な最適化を可能にする。
    • システム状態の事後分布と,その事後分布の分布という2つの結合された情報状態がマルコフ再帰を満たすことを示す。
    • シグナリングがない場合,提案手法は標準的なPOMDPの動的計画方程式に帰着し,既存手法との整合性を示す。

    Link: https://arxiv.org/abs/2606.17743

  • コーディングベンチマークはエージェント型ソフトウェアエンジニアリングと整合していない [cs.SE, cs.AI, cs.CL]目的:エージェント型ソフトウェアエンジニアリングにおけるベンチマークの不整合性
    • ソフトウェア開発において,AIエージェントの活用が拡大しており,その性能評価が重要になっている。
    • 既存のベンチマークは,モデル,ハーネス,環境を統合的に評価するため,改善の方向性を示しにくい。
    • ベンチマークをエージェント型ソフトウェアエンジニアリングに適応させ,より詳細な評価指標を提供することを目指す。
    • 現在のベンチマークは,モデル単体の性能とシステム全体の性能を区別できていない。
    • 単一の正解にのみ基づく評価は,有効な代替案を適切に評価できない。
    • 個々のコンポーネントレベルでの信号がないため,システム全体のスコアの改善が困難である。

    Link: https://arxiv.org/abs/2606.17799

  • 確率モデル検査のための統一されたマルコフ二値形式UMB [cs.LO]目的:確率的システムのモデル表現のための統一的なファイル形式
    • 確率モデル検査は,複雑なシステムの信頼性や安全性評価に不可欠である。
    • 既存のモデル形式は,ツール依存性が高く,相互運用性が課題であった。
    • 低レベルなモデル表現の交換を効率化し,ツール間の連携を促進すること。
    • UMB形式は,効率的かつ拡張可能であり,様々な確率システムを表現できる。
    • ツール固有のテキスト形式と比較して,ファイルサイズと読み書きのオーバーヘッドを削減する。
    • Pythonライブラリが提供されており,モデルの読み込み,操作,作成,検証が容易である。

    Link: https://arxiv.org/abs/2606.17811

  • 大規模評価のためのエージェントスキル評価フレームワーク [cs.SE, cs.AI, cs.CL]目的:エージェントスキルの評価方法
    • LLMエージェントの能力向上に不可欠なエージェントスキルの活用が広がっている。
    • エージェントスキルのクロスドメインでの影響や,評価方法論が確立されていない。
    • 個々のエージェントスキルを客観的に評価するフレームワークを構築すること。
    • 提示されたフレームワークにより,スキル作成者は現実的なタスクを作成し,スキルの重要な側面を厳密に評価できる。
    • 500の実際のスキルを大規模に評価した結果,モデルによって指示への適合度に大きな差が見られた。
    • スキルへのアクセスはモデルの振る舞いを大きく変え,LLMエージェントに意見のあるワークフローを組み込む上で重要なメカニズムとなることが示された。

    Link: https://arxiv.org/abs/2606.17819

  • BCHデコーダの高性能・低遅延ハードウェア実装 [cs.IT, math.IT]目的:BCH符号の従来の復号方式と直接復号方式のハードウェアアーキテクチャ
    • 誤り訂正符号は,通信や記憶媒体においてデータの信頼性を確保する上で不可欠である。
    • BCH符号の復号処理は計算量が多く,ハードウェア実装における高性能化が課題である。
    • 本研究は,BCH符号の高速かつ効率的なハードウェア復号器を実現することを目的とする。
    • 従来の復号方式と直接復号方式のハードウェアアーキテクチャを提案し,任意のブロック長に対応可能であることを示した。
    • 直接復号方式において,誤り訂正能力4に対応するハードウェア実装を初めて実現した。
    • FinFET 16nmおよびXilinx Ultrascale+ XCZU48DRでの合成結果から,特定の条件下において直接復号方式が従来の方式よりも面積効率で優位性を示すことが確認された。最大239Gb/sのデータスループットを達成した。

    Link: https://arxiv.org/abs/2606.17837

  • ニューロシンボリック推論のホモトピー型理論による一般化 [cs.AR, cs.AI, cs.LO]目的:ニューロシンボリックシステムの推論における,ホモトピー型理論に基づく一般化
    • ニューロシンボリック推論は,記号推論とニューラルネットワークを組み合わせ,両者の利点を活かす研究分野である。
    • 従来のニューロシンボリックシステムは,理論の対称性や証明の数を考慮していないため,推論の効率や正確性に課題がある。
    • ホモトピー型理論を導入することで,対称性や証明の数を考慮し,より効率的かつ正確な推論を実現することを目指す。
    • ホモトピー型理論を用いることで,信念重み付きホモトピー基数という新しい概念が導出された。
    • この基数は,対象の対称性を考慮してサイズを測るものであり,推論のショートカットを捉えることができる。
    • MNISTのベンチマークテストでは,この手法がアンサンブル学習よりも優れたキャリブレーション性能を示した。

    Link: https://arxiv.org/abs/2606.17851

  • 軸平行長方形に対するウェグナー予想への反例 [cs.CG, cs.DM, cs.DS, math.CO]目的:軸平行長方形の有限族に対するウェグナー予想の反例の提示
    • 長方形の配置問題は,様々な応用分野で重要な役割を果たす。
    • ウェグナー予想は長年未解決であり,既存の上界も十分とは言えなかった。
    • ウェグナー予想の反例を構成し,その限界を示すことを目指す。
    • ウェグナー予想に反する軸平行長方形の族を具体的に構成した。
    • 構成された長方形族の独立数の上限はn/4であり,貫通点数はν(R)の2倍以上となる。
    • この反例は,長方形の最大独立集合問題に対する標準的な緩和法に少なくとも2.21の積分ギャップが存在することを示唆する。

    Link: https://arxiv.org/abs/2606.17854

  • 確率的協調攻撃のエピステミック分析 [cs.DC, cs.LO]目的:確率的協調攻撃における知識の構造と限界
    • 分散システムにおける合意形成は,信頼性の低い通信環境下で極めて重要である。
    • 従来の協調攻撃問題は不解決であることが示され,知識の共有が課題となる。
    • 確率的協調攻撃の知識論的分析を通して,分散計算の理解を深める。
    • 提案されたエピステミック論理フレームワークは,確率的アルゴリズムの知識的考察を可能にする。
    • Varghese-Lynchアルゴリズムの形式的検証により,既存の下限を強化し,その厳密性を証明した。
    • 情報レベルの概念をエピステミックな論理式として形式化し,知識の重要性を示した。

    Link: https://arxiv.org/abs/2606.17860

  • 信頼性の高い自己構成型ビッグデータサービス:LLMオーケストレーションによるマルチエージェントフレームワーク(自動データエンジニアリング,AutoML,MLOpsデプロイメント,ドリフト対応型ライフサイクル最適化) [eess.SY, cs.SY, eess.SY, cs.SY, cs.MA, cs.AI, cs.DB, cs.SE]目的:ビッグデータサービスのライフサイクル全体を通じた信頼性と適応性の向上
    • ビッグデータはビジネス価値創出に不可欠であり,効率的なデータ活用基盤が求められている。
    • 既存システムはワークフローの断片化やライフサイクル全体の管理不足といった課題を抱えている。
    • LLMとマルチエージェントシステムを活用し,ビッグデータサービスを自動化・最適化することを目指す。
    • 提案フレームワークは,データ収集からモニタリングまで,各段階を専門エージェントが担当する。
    • LLMオーケストレーション層がエージェント間の連携を調整し,中間結果の検証やコンテキスト管理を行う。
    • 実験結果から,本フレームワークは既存手法と比較して,予測性能とライフサイクル全体の信頼性の両面で優れていることが示された。

    Link: https://arxiv.org/abs/2606.17915

  • SA-RA-JSCC:SNR適応型および意味レート認識型結合ソースチャネル符号化 [cs.RO, cs.RO, cs.IT, math.IT]目的:意味的通信システムにおける安定した信頼性の高い画像意味伝送
    • 通信において,伝送効率と信頼性を高めることは重要である。
    • 従来のチャネル適応モジュールでは,層間連携が不十分である。
    • SNR変動と意味レート制約に対応可能な適応型符号化手法を開発する。
    • 提案手法SA-RA-JSCCは,SNRを意味ベクトルにマッピングし,特徴量への全体的なリウェイトを行う。
    • これにより,グローバルに整合性のある学習可能なチャネル適応を実現した。
    • 実験結果から,SA-RA-JSCCはPSNRやMS-SSIMなどの評価指標において,既存手法を大幅に上回ることが示された。

    Link: https://arxiv.org/abs/2606.17940

  • 自己相関関数鍵付け [cs.CL, cs.IT, math.IT]目的:ピークサイドローブレベル制約下での相互情報最大化
    • 次世代6Gネットワークにおいて,通信とセンシングを同時に行うISACの重要性が高まっている。
    • 既存研究では平均的なサイドローブ特性しか評価しておらず,個々のペイロードにおける大きなピークが問題となっている。
    • ピークサイドローブレベルを厳格に制御し,微弱ターゲットの検出性能を向上させることを目指す。
    • 自己相関関数領域における均一構成が,高SNR下で漸近最適となることを示した。
    • 自己相関関数鍵付け(ACFK)は,ACFのサイドローブにデータシンボルを直接埋め込む有限星座変調アーキテクチャである。
    • ACFKは,一般的なPASと比較して,ピークサイドローブレベルの制御性能と微弱ターゲット検出性能を向上させる。

    Link: https://arxiv.org/abs/2606.17970

  • ハンマーに計画を立てて: Rocq証明の自動化のための難易度を考慮した分解 [cs.SE]目的:Rocq証明の自動化のための計画ベースの分解フレームワーク
    • AI生成コードの普及に伴い,ソフトウェアの正しさを保証する形式検証の重要性が増している。
    • 既存の証明自動化ツールは,大域的な計画能力や局所的な厳密性に課題があり,長大な証明の効率的な処理が困難である。
    • LLMとCoqHammerの利点を組み合わせ,難易度に基づいた分解により,Rocq証明の自動化率向上を目指す。
    • 計画に基づく分解と解法可能性を考慮したランキングにより,自動化率が大幅に向上し,コストも予測可能である。
    • 10分間の制限時間内で,3つのRocqベンチマークにおいて,既存の最良のベースラインよりも成功率が7〜13%向上した。
    • ニューラルプランニングと記号的実行を連携させることで,信頼性の高い証明自動化が実現可能であることが示された。

    Link: https://arxiv.org/abs/2606.17981

  • Moveにおける実行時安全性の多層防御 [cs.PL]目的:Moveにおける実行時安全性の多層防御機構
    • ブロックチェーン技術は金融や情報管理など,社会基盤を支える重要な役割を担う。
    • スマートコントラクトの検証には限界があり,バグや悪意のあるコードによる資産損失のリスクが存在する。
    • Moveの実行時安全性チェックにより,検証バグや悪意のあるバイトコードから保護することを目指す。
    • Aptosブロックチェーンにおいて,Moveプログラムの実行時安全性を確保するための多層防御機構が実装されている。
    • この機構は,静的検証の不備や悪意のあるバイトコードによる状態破壊を防ぐために,重要な不変条件を独立して検証する。
    • これにより,Moveプログラムの信頼性と安全性を高め,資産の保護に貢献する。

    Link: https://arxiv.org/abs/2606.18064

  • 1
  • 2