arXiv雑要約
プログラム - 2025/10/14 公開
拡張三角法：矛盾分離に基づく自動推論の汎化アルゴリズム [cs.AI, cs.LO]目的：矛盾分離に基づく自動推論アルゴリズムの汎化
- 人工知能の中核技術であり，定理証明や形式検証などに応用される重要な分野である。
- 従来の推論方法は2つの節の相互作用に制限され，複数の節間の相乗効果が限定的である。
- 矛盾分離の内部メカニズムを形式化し，より柔軟で効率的な推論を可能にすること。
- 拡張三角法（ETM）は，矛盾構築戦略を統合し，動的な節間相互作用を可能にする幾何学的枠組みを提供する。
- ETMは，高性能定理証明器CSE，CSE-E，CSI-E，CSI-Enigの中核アルゴリズムとして実装され，その有効性が実証されている。
- 理論的抽象と運用実装の橋渡しとなり，論理推論と定理証明の新たな方向性を示す。
相関クラスタリングのための学習増強ストリーミングアルゴリズム [cs.DS, cs.LG]目的：相関クラスタリングにおけるストリーミングアルゴリズム
- 大規模グラフの解析は，ソーシャルネットワーク分析等において重要である。
- エッジの順序が不明なストリームデータへの対応が課題であった。
- 予測器を用いた学習により，空間効率と近似率の改善を目指す。
- 完全グラフにおいて，良好な予測精度下で3未満の近似率を達成した。
- 一般グラフにおいて，良好な予測精度下で$O(\log |E^-|)$の近似率を達成し，既存の非学習アルゴリズムよりも空間効率が良い。
- 合成データおよび実データを用いた実験により，提案手法の優位性が示された。
CSPに対するストリーミング近似アルゴリズムに関する9つの下界予想 [cs.HC, cs.CC, cs.DS]目的：CSPに対するストリーミング近似アルゴリズムの下界予想の整理
- 制約充足問題は計算複雑性理論において重要な問題であり，様々な応用がある。
- ストリーミングモデルにおける近似アルゴリズムの下界は未だ解明されていない点が多い。
- 既存の知見をまとめ，未発表の下界予想を提示することで議論を活性化させる。
- 本稿では，CSPに対するストリーミング近似アルゴリズムに関する9つの下界予想を提示する。
- これらの予想は，低空間ストリーミングモデルにおけるCSPの近似可能性を理解するための手がかりとなる。
- 本研究は，この分野における今後の研究の方向性を示す一助となることを期待する。
多目的LLM対話のための確率微分方程式フレームワーク：コード生成応用による力学系解析 [cs.LG, cs.AI, cs.SE]目的：多目的最適化ダイナミクスのモデリング
- LLMの活用が拡大する中で，複数目的を同時に最適化する手法の重要性が増している。
- LLMの応答の確率性や，目的間の干渉といった問題があり，予測や制御が困難である。
- LLM対話における多目的最適化のダイナミクスを解析し，収束性や予測可能性を高めることを目指す。
- 提案フレームワークは，LLM応答の確率性と目的間干渉を捉え，理論的な裏付けを与える。
- コード生成実験により，戦略に依存した収束挙動が確認され，収束率は0.33～1.29の範囲であった。
- バランスの取れたアプローチでは，予測精度R2=0.74を達成し，力学系解析の有効性を示唆する。
生成AIとソフトウェア開発手法の変革 [cs.DC, cs.SE, cs.AI]目的：ソフトウェア開発における生成AIの影響と課題
- ソフトウェア開発は，社会のデジタル化において不可欠であり，その効率化は重要である。
- 従来の開発手法では，高度な専門知識と時間が必要であり，人材不足も課題である。
- 生成AIを活用することで，開発の効率化と人材の裾野拡大を目指す。
- 生成AIは，チャット形式でのプログラミングやエージェントプログラミングなど，新しい開発スタイルを可能にする。
- 生成AIの導入により，開発サイクルが加速し，より多くの人々がコーディングに参加できるようになる可能性がある。
- ただし，モデルの信頼性やコストといった課題も存在し，責任ある利用のためのスキルとベストプラクティスが求められる。
ソフトウェアテストのためのエージェント的RAG：ハイブリッドベクトルグラフとマルチエージェントオーケストレーション [cs.SE, cs.AI]目的：ソフトウェアテスト自動化のための，エージェント的検索拡張生成（RAG）システムによる品質工学（QE）成果物生成
- ソフトウェア品質の確保は，システム開発において不可欠であり，信頼性の高いソフトウェアを提供するために重要である。
- 従来のソフトウェアテストは，時間とコストがかかり，効率性に課題がある。また，網羅的なテストケースの作成も困難である。
- 本研究は，LLMとマルチエージェントを活用し，テストプロセスの効率化と品質向上を目指す。
- 本システムは，GeminiやMistralといったLLMを活用し，テスト計画，ケース，QEメトリクスの生成を自動化することで，品質工学ライフサイクル全体を通して文書のトレーサビリティを確保する。
- 実験結果から，本システムは従来のソフトウェアテストと比較して，テストの精度が65％から94.8％に大幅に向上することが示された。
- また，企業システムエンジニアリングおよびSAP移行プロジェクトにおいて，テスト期間が85％短縮され，テストスイート効率が85％向上し，コストを35％削減できることが確認された。
オートエンコーダTransformerモデルによるソフトウェア欠陥予測 [cs.DC, cs.FL, cs.DM, math.NT, cs.SE, cs.AI]目的：ソフトウェア欠陥の予測
- ソフトウェア品質は重要であり，欠陥予測は品質保証の鍵となる。
- 従来の機械学習モデルは，ノイズデータ，不均衡，特徴抽出の課題を抱える。
- 高精度な欠陥予測を実現し，ソフトウェア品質向上に貢献すること。
- 本研究では，ADE-QVAETモデルを開発し，高次元潜在特徴とシーケンシャル依存性を維持することで，欠陥予測精度を向上させた。
- ADE最適化により，モデルの収束性と予測性能が向上した。
- 90%の学習データを用いた実験で，ADE-QVAETは，従来のDEモデルと比較して，高い精度，適合率，再現率，F1スコアを達成した。
ソフトウェアプロジェクト管理における生成AI：実務家文献のレビューからの考察 [cs.CL, cs.DB, cs.RO, cs.SE, cs.AI]目的：ソフトウェアプロジェクト管理における生成AIの現状と課題
- ソフトウェア開発の効率化と品質向上は，競争力維持に不可欠である。
- 生成AIの急速な発展に伴い，その実用化と影響に関する体系的な理解が不足している。
- 生成AIのプロジェクト管理への応用可能性と，実務家側のニーズの把握。
- 実務家は生成AIを「アシスタント」「コパイロット」「仲間」と捉え，プロジェクトマネージャーの代替とは考えていない。
- 定型タスクの自動化，予測分析，コミュニケーション，アジャイルプラクティスへの支援がプロジェクト成功に繋がると認識されている。
- 幻覚，倫理，プライバシー，感情知性・判断力の欠如といった懸念から，責任ある生成AI利用が強調されている。
学習と汎化のための構造情報原理としての冗長性 [cs.LG, cs.AI, cs.IT, math.IT, stat.ML]目的：冗長性の構造的情報原理
- 実世界の学習には，情報組織の理解が不可欠である。
- 従来の理論では，冗長性を非効率性として捉える傾向があった。
- 有限系における最適な冗長性水準の特定と，それによる学習能力の向上。
- 本研究は，冗長性を情報組織の基本的な特性と再定義し，古典的な情報理論を拡張する理論的枠組みを提示する。
- 様々な依存性指標が共通の冗長性幾何学の投影であることが示され，平衡状態における学習の安定性と汎化能力が明らかになった。
- マスクドオートエンコーダの実験により，この原理が検証され，冗長性がピークに達する安定したレベルが存在することが確認された。
柔軟セクタ6DMAを用いた多重通信のスループット最大化 [cs.MA, cs.CL, cs.IT, math.IT]目的：多重アクセス方式を用いる無線通信における，柔軟セクタ6DMA基地局のスループット最大化
- 無線通信の需要増加に対応するため，基地局の効率的なリソース管理が重要である。
- 従来の固定アンテナ配置では，ユーザー分布の変化への対応が難しく，容量向上が限界がある。
- ユーザー分布に応じてアンテナ配置を柔軟に調整することで，スループットを向上させる。
- 提案する柔軟セクタ6DMA基地局は，アンテナを円軌道上を移動させ，セクタのカバー範囲を調整することで，スループットを向上させる。
- ユーザーが各セクタに均等に分布することが，共通スループットを最大化する上で最適であることが示された。
- シミュレーション結果から，提案手法が既存方式と比較して，ネットワークのスループットを大幅に改善することが確認された。
知識グラフと大規模言語モデルの相乗的統合によるプロジェクトレベルのCからRustへの翻訳 [cs.IR, cs.SE, cs.AI]目的：Cコードを安全なRustコードに翻訳すること
- メモリ安全性を確保するため，CコードをRustに変換する研究が重要である。
- 既存のLLMベースの手法は，プロジェクト全体の依存関係を捉えきれないため，ポインタの翻訳に苦戦している。
- ポインタのグローバルな意味情報をLLMに提供し，より安全で自然なRustコード生成を目指す。
- 提案手法は，ルールベース変換や既存LLMと比較して，翻訳後のRustコードにおけるunsafeな利用を99.9%削減した。
- ファジング強化型LLM手法よりも平均29.3%高い機能的正確性を実現した。
- C-Rustポインタ知識グラフが，LLMに包括的なポインタ情報をグローバルな視点から提供する。
Barlow Twins の最適な表現効率：情報幾何学的解釈 [cs.IR, cs.RO, cs.LG, cs.CV, cs.IT, math.IT, math.ST, stat.ML, stat.TH]目的：表現効率の定量化
- 教師なし学習はラベルなしで有用な表現を獲得するため，近年重要性が増している。
- 様々な教師なし学習手法の効率を統一的に理論的に比較する枠組みが不足している。
- Barlow Twins の有効性を理解するための厳密な理論的基盤を確立すること。
- 本研究では，表現効率を情報幾何学的に定義し，Fisher情報行列のスペクトル特性を用いることで定量化する。
- Barlow Twins は，表現の相互相関行列を単位行列に近づけることで最適な表現効率（η = 1）を達成することを理論的に証明した。
- この成果は，Barlow Twins の有効性に対する新たな幾何学的視点を提供する。
エネルギー節約を考慮したクレーンスケジューリング問題 [cs.DS]目的：エネルギー節約を考慮したクレーンスケジューリングの最適化
- 港湾におけるクレーンは大量のエネルギーを消費し，効率的な運用はコスト削減と環境負荷低減に不可欠である。
- 従来のクレーンスケジューリングは，エネルギーの無駄を考慮しておらず，更なる省エネルギー化の余地が存在する。
- コンテナの降ろし時のエネルギーを再利用し，クレーンスケジューリング全体のエネルギー消費量を削減することを目指す。
- 本研究では，一次元倉庫を想定した基本的なモデルを構築し，問題の計算複雑性を解析した。
- 半オイラー化問題との関連性を考察し，近似アルゴリズムを提案するとともに，エネルギーバッファが制限された場合の動的計画法アルゴリズムを開発した。
- ハミルトニアンの視点を取り入れ，一般的なケースに対する動的計画法アルゴリズムを提示し，問題の変形が非巡回区間有向グラフ上のパス被覆問題に変換可能な場合に多項式時間で解けることを示した。
単語方程式を用いた文字列領域の定義：縮約積による表現 (拡張版) [cs.PL, cs.FL]目的：文字列抽象領域の定義
- プログラム解析において，文字列操作の正確な追跡は重要である。
- 既存の文字列抽象領域では，表現力と計算効率のバランスが課題である。
- 単語方程式と縮約積を利用し，効率的な文字列抽象領域を構築すること。
- 文字列区間を単語方程式と不等式で表現する新しい抽象領域を提案した。
- この領域は縮約積に基づいており，文字列プロパティの半格子の構造を利用する。
- JavaScriptの文字列操作プログラムの解析への応用可能性を示した。
コードリポジトリに対する特徴指向の要約とドキュメント生成 [cs.SE]目的：コードリポジトリの要約とドキュメントの自動生成
- ソフトウェア開発・保守において，リポジトリの把握は重要である。規模が拡大するにつれ，効率的な理解が不可欠となる。
- 既存手法はディレクトリ構造に依存し，高レベルな機能とそれを実装するコード要素の関連性の追跡が困難である。
- 機能に着目し，コードとドキュメントの一貫性を高め，保守性を向上させることを目指す。
- RepoSummaryは，既存手法と比較して，より多くの機能をカバーし，正確なトレーサビリティを実現した。
- 手動ドキュメントにおける完全カバー率を平均61.2%から71.1%に向上させ，ファイルレベルのトレーサビリティ再現率を29.9%から53.0%に改善した。
- 生成されたドキュメントは概念的に一貫性があり，理解しやすく，フォーマットも良好であった。
Defects4C：C/C++バグを用いた大規模言語モデルの修復能力のベンチマーク [cs.SE]目的：C/C++プログラムの修復能力の評価と改善
- ソフトウェアの品質と信頼性向上には，自動プログラム修復技術が不可欠である。
- Javaに比べ，C/C++プログラムの修復に関する研究は遅れており，高品質なベンチマークの不足が課題である。
- C/C++プログラムの修復研究を促進するためのベンチマーク Defects4C を提供し，LLMの能力評価を行う。
- Defects4C は，C/C++プログラムの修復に特化した包括的なベンチマークであり，実世界のコードから900万件のコミット，248個のバグ関数，102個の脆弱関数を含む。
- 24種類の最先端LLMを用いてDefects4Cで実験を行った結果，現在のLLMベースのAPR技術の限界が明らかになった。
- Defects4Cは，C/C++プログラム修復研究の進展に貢献し，より堅牢な手法の開発を促す上で重要な役割を果たす。
DebugTA: プログラミング教育におけるデバッグと指導を簡素化するLLMベースのエージェント [cs.SE]目的：プログラミング教育におけるデバッグと指導タスクの効率化
- プログラミング学習において，エラー修正支援は不可欠であり，学習効果に大きく影響する。
- 既存手法は，複雑な入力情報や標準コードの活用不足により，十分な効果を発揮できていない。
- 標準コードの検索と活用，変数置換，コンパイラによるコード解析を通じて，LLMの推論負担を軽減すること。
- DebugTAは，標準コードの検索，変数置換，外部コンパイラといった専用ツールを備えたLLMベースのエージェントである。
- このエージェントは，複雑なタスクをLLM間の段階的なやり取りに分解することで，各ステップの論理的推論を簡素化し，全体的な推論の複雑さを軽減する。
- 3つの実世界コードデータセットを用いた実験の結果，DebugTAは，指導効果を向上させるとともに，計算コストを大幅に削減することが示された。
非拡張ファジーコアルジェブラ論理 [cs.LO]目的：非拡張ファジーコアルジェブラ論理における決定可能性基準
- ファジー論理は，古典論理の真偽に加え，中間的な真理値を扱うことで，不確実性の表現を可能にする。
- ファジー様相論理は表現力と計算可能性のトレードオフが存在し，特にLukasiewicz基盤は複雑になりやすい。
- 非拡張基盤を用いることで，表現力と計算可能性のバランスを取り，効率的な推論を実現すること。
- 非拡張ファジーALC論理のPSpaceでの決定可能性が再確認された。
- 確率的および計量遷移システムのための様々な定量的様相論理に対する新たなPSpace上限が導出された。
- コアルジェブラ論理の枠組みにより，多様な様相論理を統一的に扱うことが可能となった。
FMware開発の遅延要因：開発者の課題と解決時間の経験的調査 [cs.SE]目的：FMware開発における開発者の課題と解決時間の分析
- ソフトウェア開発は社会の根幹であり，生産性向上は重要課題である。
- FMwareは新たな開発パラダイムだが，従来のツールや手法が適用困難である。
- FMware開発の課題を特定し，ツールやワークフローの改善に貢献すること。
- FMwareの主要な応用分野は，教育，コンテンツ作成，ビジネス戦略であることが判明した。
- GitHub上では，バグレポートや主要機能の問題が頻繁に報告されている。
- コードレビュー，類似性検索，プロンプトテンプレート設計は，解決に最も時間を要する課題である。
OpenTelemetryからKiekerへの相互運用性：Astronomy Shopからのエクスポートによる実証 [cs.SE, astro-ph.IM]目的：OpenTelemetryトレーシングデータのKiekerフレームワークへの変換
- システムの可観測性は，パフォーマンス分析や問題解決に不可欠であり，ソフトウェア開発の品質向上に貢献する。
- Kiekerはサポート言語が限られており，現代的な開発環境で広く利用されるC#やJavaScriptに対応していないという課題がある。
- OpenTelemetryからのデータ変換により，Kiekerの分析機能を幅広い言語と技術に拡張し，可観測性の向上を目指す。
- OpenTelemetryのトレーシングデータをKieker形式に変換する手法を開発し，相互運用性を実現した。
- Astronomy Shopのトレースデータを可視化することで，提案手法の有用性を実証した。
- 本研究により，Kiekerの適用範囲が拡大し，より多くのシステムにおける可観測性の向上が期待できる。
第20回論理的フレームワークとメタ言語国際ワークショップ：理論と実践 [cs.NI, cs.LO, cs.PL]目的：論理的フレームワークとメタ言語に関する研究発表論文集
- プログラム言語の基礎理論を深め，形式的検証の基盤技術として重要である。
- 実用的な応用において，理論と実装のギャップが存在する。
- 本論文集は，2025年のLFMTPにおける研究発表論文をまとめたものである。
- ワークショップは，FSCD会議に併設して英国バーミンガムで開催された。
- プログラム委員会はKaustuv ChaudhuriとDaniele Nantes-Sobrinhoが議長を務めた。
制限付き復号問題に基づくMPCitH署名 [cs.CR, cs.IT, math.IT]目的：デジタル署名スキームの性能向上
- 情報セキュリティにおいて，安全かつ効率的な署名方式は不可欠である。
- 既存のMPCitHベース署名方式は，署名サイズが大きいという課題があった。
- 制限付き復号問題を導入し，署名サイズの縮小を目指す。
- 本研究では，制限付き復号問題をMPCitHフレームワークに組み込むことで，署名サイズを大幅に削減することに成功した。
- CROSSの安全性仮定に基づくインスタンス化により，NIST提出方式と比較して2倍以上のサイズ削減を実現した。
- WAVEの安全性仮定と関連する三進フルウェイト復号を用いることで，NIST競争における最小のMPCitHベース候補と同等の署名サイズが得られた。
凹型かつ限界効用逓減的な目的関数を持つオンライン配分問題 [cs.HC, cs.DS]目的：凹型かつ限界効用逓減的な目的関数を持つオンライン資源配分問題における最適なアルゴリズムの存在
- 経済学と計算機科学における重要な課題であり，リアルタイムな資源配分を扱う上で不可欠である。
- 既存研究は特定の問題に依存する手法を用いているため，汎用的なアルゴリズムの存在が未解決であった。
- 凹型かつ限界効用逓減的な目的関数を持つオンライン資源配分問題に対して，常に$(1-\frac{1}{e})$-競争率のアルゴリズムが存在することを示す。
- 補助目的関数U(x)に対する連続的な貪欲配分を行うアルゴリズムを提案した。
- Uがfに関して「均衡」特性を満たす場合，アルゴリズムの競争率を評価できることを示した。
- 提案アルゴリズムは，様々な凹型かつ限界効用逓減的な目的関数に対して$(1-\frac{1}{e})$-競争率を達成する。
6G O-RAN向けネットワーク最適化スパイクニューラルネットワーク（NOS）スケジューリング：スペクトルマージンと遅延テール制御 [cs.NI, cs.IT, cs.LG, math.IT]目的：6G無線アクセスにおける遅延を考慮したネットワーク最適化スパイク（NOS）スケジューラーの提案
- 次世代6G通信では，効率的な無線リソース管理が不可欠であり，高スループットと低遅延が求められる。
- 既存のスケジューリング手法は，ネットワークトポロジーや遅延変化に頑健ではなく，性能劣化を招く可能性がある。
- 本研究は，ネットワークトポロジーと遅延に依存しない，よりロバストなスケジューリング手法を開発し，性能向上を目指す。
- 提案手法NOSは，スペクトルマージンと遅延の関係を分析し，単一の設計パラメータに集約することで，柔軟な設計を可能にする。
- 理論的解析により，NOSの幾何学的エルゴード性，バックログ，遅延テールの漸近的挙動が明らかになった。
- シミュレーション結果から，NOSはPFや遅延バックプレッシャー（BP）と比較して，より高い利用率と低い99.9パーセンタイル遅延を達成することが示された。
交代フリー様相μ計算におけるカット除去 [cs.LO, math.LO]目的：交代フリー様相μ計算のカット除去手続き
- 形式的検証において，モデル検査の基盤として様相論理が重要な役割を担う。
- 様相論理の計算の複雑さ，特にμ計算におけるカット除去の困難性が課題である。
- 交代フリー様相μ計算におけるカット除去の効率的な手法を確立すること。
- 本研究では，循環型証明系を用いて，カット除去手続きを直接的に行うことに成功した。
- 多カットとwell-quasi-orderの理論を活用することで，カットのない証明への変換を実現した。
- 中間的な正規化機構を経由せず，効率的なカット除去を実現した点が特徴である。
GitHub ActionsにおけるNyrki\"oを用いたMooBench結果の性能変化検出 [cs.RO, cs.SE, cs.OS, cs.PF]目的：MooBench結果における性能変化の検出
- GitHubは多くのプロジェクトが存在し，それらの性能は利用者にとって重要である。
- GitHub CI/CDで性能測定は可能だが，性能変化の検出は課題である。
- MooBenchの結果を用いて性能変化を検出し，回帰を特定すること。
- Nyrki\"oをMooBenchに組み込むことで，性能変化の検出が可能となった。
- 1件の主要な性能回帰を特定し，詳細な分析を行った。
- 回帰はGitHub Actionsで再現可能であり，Linux Kernelのバージョン変更が原因であることが判明した。
効果的な高階プログラムの時間検証のための表示的積構成 [cs.CL, eess.SY, cs.SY, cs.IR, cs.LO]目的：効果的な高階プログラムの時間検証に関する表示的積構成
- プログラムの信頼性確保が重要であるため，プログラム検証技術の確立が求められている。
- 高階プログラムの効果や確率的な振る舞いを考慮した時間検証は未だ困難である。
- 高階プログラムの時間検証を既存の事前条件計算アルゴリズムに還元する手法を確立する。
- 表示的積構成により，高階プログラムの時間検証を高階プログラムの事前条件計算に還元できることを示した。
- 強モノイド準同型とfibrarationに沿った適切なliftingの存在を示すことで，構成の正当性を証明した。
- 確率的およびangelic非決定的高階プログラムに適用可能であり，確率的ケースの自動検証器を実装した。
単一品目容量制約付きロットサイジング問題に対する，$O(n\log n)$アルゴリズム：単一割引点付き全数量割引と単調減少価格 [cs.CE, econ.EM, cs.NI, cs.PF, cs.DS]目的：単一品目容量制約付きロットサイジング問題の解法
- 在庫管理は，サプライチェーンの効率化に不可欠であり，企業の収益性に大きく影響する。
- 従来のロットサイジング問題の解法は計算量が大きく，大規模な問題への適用が困難であった。
- 本研究は，より効率的なアルゴリズムを開発し，実用的な規模の問題を解決することを目指す。
- 本研究では，単一割引点付き全数量割引と単調減少価格を持つ単一品目容量制約付きロットサイジング問題に対して，$O(n\log n)$時間で解けるアルゴリズムを開発した。
- 提案アルゴリズムは，既存の$O(n^2)$アルゴリズムよりも計算効率が良い。
- 最適な解の特性を明らかにし，重要な情報のみを格納するハイブリッド動的計画法を導入することで，計算量を削減した。
エネルギー効率の良い無線通信のための前方前方型オートエンコーダアーキテクチャ [cs.IT, cs.LG, math.IT]目的：エネルギー効率の良い無線通信システムにおける前方前方学習アルゴリズムを用いたオートエンコーダの設計
- 通信システムへの深層学習の応用は近年注目されており，性能向上への期待が高まっている。
- 従来のバックプロパゲーション法は計算コストが高く，チャネル微分可能性に制限を受ける場合がある。
- 本研究は，バックプロパゲーション法に代わる効率的な学習アルゴリズムを提示し，エネルギー効率の向上を目指す。
- 前方前方学習を用いたオートエンコーダは，加法性白色ガウスノイズ及びレイリーブロックフェージングチャネルにおいて良好な性能を示した。
- 結合符号化・変調において，バックプロパゲーション法で学習されたシステムと同等の性能を発揮することが確認された。
- 固定された非微分可能な変調段階においても有効であり，メモリ及び処理時間の削減に貢献する。
表現 [cs.LO]目的：ソフトウェア解析システムの形式モデル
- 自動システム解析は重要であり，成長を続けている分野である。
- 論理の完全性と意味論との整合性を示すことが難しい場合がある。
- ソフトウェア解析システムの開発と完全性証明を容易にすること。
- 本研究では，ソフトウェア解析システムを形式的にモデル化するための「表現」というモデルを提案する。
- このモデルは，モデル化対象のシステムに対する仮定が少なく，広範なシステムを捉えることが可能である。
- 既存の完全性証明の構造を理解し，新たなシステムの構築と完全性証明に活用できることを示す。
HUGR：量子古典中間表現 [cs.PL, quant-ph]目的：量子古典混合プログラムの中間表現
- 量子計算の発展に伴い，その表現方法の標準化が重要である。
- 既存の中間表現では，量子計算特有の機能を十分に捉えられていない。
- 量子古典混合プログラムを効率的に記述・解析するための新たな表現を提案する。
- HUGRは，グラフ構造に基づく新しい中間表現であり，高い表現力と拡張性を備えている。
- 機械処理に適した構造を持ち，パターンマッチングに基づくコンパイル技術を支援する。
- 厳密な型チェックと線形量子型により，安全なコンパイルツール開発を可能にする。
衛星アクセス向けDFT-s-OFDMにおける繰り返しオフセットQPSK [cs.CL, cs.IT, eess.SP, math.IT]目的：衛星および地上系ネットワークの融合に対応するための変調方式
- 衛星通信と地上系セルラーネットワークの統合が進んでおり，両者の特性を組み合わせた技術が求められている。
- 既存の衛星通信方式は地上系に最適化されたOFDMへの移行が課題となっている。
- 地上系OFDMで利用可能な変調方式を衛星通信へ適用し，性能向上を目指す。
- 提案するRO-QPSKは，自然にハニング窓形状のスペクトルを生成し，低PAPR（約2dB）を実現する。
- RO-QPSKは，単タップ等化とシンボル結合により，狭帯域または周波数選択性チャネルにおいて，FDSSを用いたπ/2-BPSKよりもSINRを改善する。
- RO-QPSKと適度なFDSSの組み合わせにより，PAPRをさらに低減しながら，同等の性能を維持できる。
リー，ユークリッドおよびその他の距離におけるリード・ソロモン符号のリスト復号 [cs.IT, cs.DS, math.IT]目的：リード・ソロモン符号のリスト復号アルゴリズム
- リード・ソロモン符号は，暗号，計算複雑性，通信など幅広い分野で利用されており，情報処理において不可欠である。
- 従来の復号アルゴリズムはハミング距離に焦点を当てており，エラーの具体的な値に依存する他の距離指標には対応できていない。
- 任意の0 < p ≤ 2における$\ell_p$ (半)距離におけるリード・ソロモン符号の効率的なリスト復号アルゴリズムを提案する。
- 提案アルゴリズムは，リー距離（$\ell_1$）およびユークリッド距離（$\ell_2$）における既存のアルゴリズムと比較して，任意の距離で復号可能である。
- 特定のGRS符号のサブクラスにおける$\ell_{1}$および$\ell_{2}$の最小距離に関する下界を証明し，提案のリスト復号器が特定のパラメータに対して一意復号器となることを示す。
- ラプラス誤差およびガウス誤差下におけるアルゴリズムの性能を分析し，最悪の場合のエラーと比較して，より高いレートをサポートすることを示す。
CodeWhisperer利用状況の分析：開発者のインタラクションとパターン [cs.DC, eess.SY, cs.SY, cs.SE, cs.AI]目的：開発者のCodeWhispererとの関わり方
- AIコード生成ツールの利用拡大に伴い，開発者の利用状況の理解が重要である。
- 既存研究では，AIツール利用時の詳細な開発者行動パターンが十分に把握されていない。
- CodeWhisperer利用時の開発者の行動パターンを特定し，AIツール利用の理解を深める。
- 開発者は，コードを段階的に改良する行動を示す。
- 自然言語コメントを用いてCodeWhispererに指示を出すことが確認された。
- モデルの提案を基盤としてコード構造を構築し，外部ソースと統合するパターンが特定された。
CodeWatcher: LLMとコード生成ツール間の開発者インタラクションを理解するためのIDEテレメトリデータ抽出ツール [cs.SE, cs.AI]目的：LLMとコード生成ツールを用いた開発者インタラクションの理解を可能にするIDEテレメトリデータの抽出
- AI技術の進化に伴い，開発者の生産性向上とAIの責任ある利用が重要になっている
- 開発者のリアルタイムなプログラミング行動データの収集は，ワークフローを中断する可能性があり困難である
- 開発者の行動を詳細に分析し，コード生成ツール利用状況の把握と改善を目指す
- CodeWatcherは，VS Codeエディタ内で発生するイベント（挿入，削除，コピー＆ペーストなど）を詳細に記録するシステムである
- このシステムは，開発者のワークフローを妨げることなく，継続的な活動モニタリングを可能にする
- 収集されたデータは，コード生成ツールの利用状況分析や，開発者支援AIの研究に役立つ
単一リンケージクラスタリングコスト推定のためのサブ線形アルゴリズム [cs.RO, cs.CL, cs.DS]目的：単一リンケージクラスタリングのコスト推定
- データ分析において，クラスタリングは重要な手法であり，その効率的な計算が求められる。
- 大規模データに対する単一リンケージクラスタリングのコスト計算は，計算量が膨大になるという課題がある。
- グラフ構造におけるコストのサブ線形な推定アルゴリズムを開発し，計算量の削減を目指す。
- 提案手法は，データ点間の距離が与えられたグラフに対し，簡潔な表現でコストを推定する。
- 実行時間は$\tilde O(d\sqrt{W}/\varepsilon^3)$であり，推定誤差は$\varepsilon\cdot \mathrm{cost}(G)$以下であることが保証される。
- 類似度に基づく場合にも適用可能であり，同様の計算時間で推定が可能である。
スペキュレーション通過スタイルによるSpectreセキュリティの(不)証明 [cs.PL]目的：Spectre脆弱性検出のためのスペキュレーション通過スタイル(SPS)というプログラム変換の形式的な基礎
- 暗号ライブラリのサイドチャネル脆弱性は深刻な脅威であり，情報漏洩につながる可能性があるため，その対策が重要である。
- 従来の定数時間検証ツールではSpectreのような投機的実行を悪用した脆弱性の検出が困難であった。
- SPS変換を用いることで，既存の定数時間検証ツールを活用しSpectre脆弱性をより確実に検出することを目指す。
- SPS変換はプログラムに攻撃者制御の予測に対応する新たな入力を付加し，その予測に従うようにプログラムを修正する。
- プログラムがスペキュレーション通過型(SCT)であることと，そのSPS変換が定数時間型(CT)であることは同値である。
- SPS変換をEasyCrypt, BINSEC, ctgrindといった既存のCT検証ツールと組み合わせることでSpectre-v1に対する有効性を確認した。
グラフニューラルネットワークの検証に関する講義ノート [cs.LO, cs.LG]目的：グラフニューラルネットワークの検証タスク
- グラフ構造データ分析の重要性が増しており，その信頼性検証が不可欠である。
- 既存の検証手法では，複雑なグラフニューラルネットワークの挙動を正確に評価することが困難である。
- グラフニューラルネットワークに対するより強力かつ効率的な検証手法を開発すること。
- グラフニューラルネットワークと，Weisfeiler-Lehmanテスト，および論理との関係が再確認された。
- 線形不等式における数え上げモダリティを含むモダール論理が提案され，グラフニューラルネットワークの検証に活用された。
- その論理の充足可能性問題を解決するためのアルゴリズムが，タブロ法を拡張して開発された。
準線形時間における最大独立集合を通じた距離空間 Steiner 森林 [cs.DS]目的：距離空間における Metric Steiner 森林問題の近似解法
- ネットワーク設計や通信網の最適化において，接続性を保ちつつコストを最小化する問題として重要である。
- 既存手法では，距離行列への問い合わせアクセスを用いる sublinear 時間アルゴリズムが確立されていなかった。
- Metric Steiner 森林問題に対する，効率的な sublinear 時間近似解法を確立することを目指す。
- 本研究では，Metric Steiner 森林問題に対して，O(log k) 近似のアルゴリズムを時間計算量 $\widetilde{O}(n^{3/2})$ で実現した。
- その過程で，最大独立集合(MIS)のサイズを sublinear 時間で推定する初のアルゴリズムを提案した。
- 提案アルゴリズムは，隣接行列オラクルモデル下で時間計算量 $\widetilde{O}(n^{3/2}/\varepsilon^2)$ で，(1+ε) 近似を達成する。
稠密部分グラフの継続的公開：プライバシー増幅とサブ線形空間のためのサブサンプリング [cs.CE, cs.IR, cs.DS, cs.CR, cs.LG]目的：エッジ差分プライバシーを考慮したグラフアルゴリズムにおける，稠密部分グラフ問題の継続的公開
- グラフデータのプライバシー保護は重要であり，特に大規模グラフの解析においては不可欠である。
- 従来の差分プライバシーを適用したグラフアルゴリズムは，空間効率や精度に課題があった。
- 空間効率と精度を改善し，継続的なデータ公開に対応した稠密部分グラフアルゴリズムを開発する。
- 本研究により，既存の静的差分プライバシーアルゴリズムと同等の精度を達成しつつ，ストリーミングアルゴリズムと同等の空間複雑性を実現するアルゴリズムが提案された。
- サブサンプリングとプライバシー増幅を組み合わせることで，高いプライバシー保護と効率的なデータ処理を両立している。
- グラフの稠密化という手法を導入することで，誤差と空間複雑性における既存手法の対数項を削減することに成功した。
Scratchプログラムに関する質問の自動生成 [cs.SE]目的：Scratchプログラムに関する質問の自動生成手法
- プログラミング学習において，理解度評価は重要である。コード完成だけでは概念理解は不明確になり得る。
- 生徒のプログラムに合わせた適切な質問作成は手間がかかり，困難であるという課題がある。
- Scratchプログラムに対し，自動的に意味のある質問を生成し，理解度評価を支援すること。
- 30種類の質問テンプレートを定義し，静的解析ツールLitterBoxを拡張することで自動生成を実現した。
- 60万件を超えるScratchプロジェクトに対し，5400万件以上の質問を生成することに成功した。
- 9年生34人への実験で，生成された質問が意味のあるものであり，解答力と学習成績に相関があることが示された。
重み付き最小頂点被覆問題に対する高速収束分散アプローチ [cs.DC, cs.DS]目的：分散ネットワークにおける最小重み付き頂点被覆の計算
- ネットワーク監視やリソース配置など，様々な応用分野における基盤となる問題である。
- 大規模ネットワークでは，中央集権的な計算が困難であり，分散的な解決策が求められる。
- 分散環境下での効率的な最小重み付き頂点被覆計算を実現し，通信コストを削減すること。
- 提案手法は，局所情報のみを用いて分散的に問題を解決し，実環境および合成グラフで性能を評価した。
- 中央集権型および分散型既存手法と比較して，同程度の解質を維持しつつ，通信オーバーヘッドを削減できることを示した。
- 分散環境における最小重み付き頂点被覆計算の実現可能性を実証した。
関数型ドノホー・エラッド・グリボンヴァル・ニールセン・フックス疎性定理 [math.FA, cs.IT, math.IT, math.OC]目的：抽象バナッハ空間における疎性定理の拡張
- 信号処理や画像処理において，データの疎性に着目することで効率的な表現が可能となる。
- NP困難な$\ell_0$最小化問題に対し，多義的な解が存在する場合がある。
- $\ell_1$最小化問題の解の一意性を保証する条件を，より広いバナッハ空間へ拡張する。
- ドノホー，エラッド，グリボンヴァル，ニールセン，フックスによる疎性定理を抽象バナッハ空間へ拡張した。
- ヒルベルト空間に対する「正規化」条件を，より一般的なバナッハ空間にも適用できることを示した。
- 1-近似シャウダーフレームを用いることで，定理の成立を証明した。
ねじれ群環の導分とその応用 [math.RA, cs.IT, math.AC, math.IT]目的：ねじれ群環の導分の分類
- 群論は数学や物理学の様々な分野で基礎的な役割を果たす重要な研究領域である。
- ねじれ群環の導分に関する体系的な研究は未だ十分とは言えず，課題が残されている。
- 群の生成元と定義関係を用いた導分の分類を通して，その問題を解決することを目指す。
- 本研究では，ねじれ群環の導分が，群の生成元と定義関係によってどのように特徴づけられるかを明らかにした。
- 群環に関する既知の結果をねじれ群環に一般化し，導分を決定するための必要十分条件を導出した。
- アーベル群や二面体群の場合に応用することで，その有用性を示し，Hochschildコホモロジー群の計算への応用も示した。
射影ユニタリ群における大域的位相不変計量に関する境界 [quant-ph, cs.IT, math.IT]目的：射影ユニタリ群における大域的位相不変計量に関する境界
- 量子計算の普遍性を実現するための理論的基盤を確立する上で重要である。
- 射影ユニタリ群における適切な距離計量の評価が困難であり，効率的な量子誤り訂正符号の設計を阻害する。
- 射影ユニタリ群における距離計量に基づいた境界を導出し，量子誤り訂正符号の性能評価を可能にする。
- 射影ユニタリ群における小球の体積と測度を求め，Gilbert-VarshamovおよびHammingの境界を導出した。
- 符号帳の接吻半径の上界と下界を導出し，接吻半径の下界からタイトなHamming境界を得た。
- 射影ユニタリ群上の一様分布する情報源の量子化に関する歪み-レート関数に対する境界を確立した。
Vibeコーディングによるオミクスデータ解析アプリケーションの迅速な開発 [q-bio.OT, cs.SE]目的：オミクスデータ解析アプリケーションの迅速開発手法
- オミクス解析は生命科学研究において不可欠だが，高度な計算能力と専門知識が必要である。
- カスタムデータ解析プラットフォームの構築には専門的なソフトウェアエンジニアリングスキルが不可欠で，研究者の参入障壁となっている。
- LLMと自律型コーディングエージェントを活用し，自然言語による記述から自動的にコードを生成することで，その障壁を取り除く。
- LLMと自律型コーディングエージェントを用いた「Vibeコーディング」により，短時間で機能的なプロテオミクスデータ解析ウェブサイトを開発した。
- ユーザーインターフェース，バックエンドロジック，データアップロードパイプラインを含むアプリケーションを，わずか4つの自然言語プロンプトで10分以内に構築した。
- 従来の開発手法と比較して，コストと労力を大幅に削減できる可能性が示された。
任意の量子ビット接続グラフに対する量子フーリエ変換の量子回路 [quant-ph, cs.DS]目的：量子フーリエ変換アルゴリズムの量子回路構築法
- 量子アルゴリズムの基礎をなすため，その効率的な実装は重要である。
- 量子デバイスの量子ビット接続グラフが制限されている場合，回路構築が困難である。
- 任意の接続グラフに対応可能な，CNOTゲート数を最小化する回路構築法を提案する。
- 提案手法は，既存の特定グラフ向け最適回路と同程度の性能を示す。
- 特に，sun型およびtwo joint suns型グラフに対しては良好な結果が得られた。
- 線形近傍結合(LNN)グラフに対してはCNOTゲート数が増加するものの，任意の接続グラフに対応可能である。
グロブナー基底と線形符号の第二種一般化ハミング重み [math.AC, cs.IT, math.IT]目的：線形符号の第二種一般化ハミング重みを決定するためのグロブナー基底の利用条件
- 符号理論は，通信や情報セキュリティにおいて誤り訂正能力の評価・改善に不可欠である。
- 有限体上の符号において，第二種一般化ハミング重みの効率的な計算方法が課題であった。
- 非バイナリ符号におけるグロブナー基底の適用可能性と限界を明らかにすること。
- 二元符号に対するグロブナー基底を用いた手法が，非二元符号においても成立するための条件が確立された。
- グロブナー基底による部分集合が第二種一般化ハミング重みを決定できない符号の例が構成された。
- グロブナー基底で得られた部分集合が第二種一般化ハミング重みを決定する場合，それは自由分解の次数からも計算可能であることが示された。
系列データにおける学習可能性を決定するパターン [stat.ML, cs.IT, cs.LG, math.IT]目的：系列データの学習可能性を決定するパターンの理解
- 金融時系列や自然言語など，系列データは自己回帰モデルの利用を促進している。
- パターン解釈の誤りは，モデルの誤指定や汎化性能の低下を招く可能性がある。
- 予測情報の概念を用いて，系列データの学習限界を明らかにすること。
- 予測情報量に基づく学習曲線が，観測ウィンドウの拡大に伴う予測情報量の変化を定量化する。
- 系列データの潜在的なパターン有無が，学習可能性に根本的な制約を与えることが示された。
- 合成データ実験により，モデルの適切性評価，データセットの複雑性定量化，系列データの構造解明が可能であることが確認された。
拡散モデルを用いたCSI予測 [math.AC, cs.SC, math.AG, math.RA, eess.SP, cs.IT, math.IT]目的：無線通信におけるCSI予測手法
- 信頼性の高い無線通信には正確なCSIが不可欠であり，通信効率向上に寄与する。
- パイロットオーバーヘッドやチャネルの経時変化が，CSIの正確かつ迅速な取得を妨げる。
- 確率的かつ多峰性のある無線チャネル特性を捉え，CSI予測の精度を向上させる。
- 拡散モデルに基づく新しい確率的フレームワークを提案し，多様な予測スキームとの統合を可能にした。
- 時間エンコーダと拡散生成器の組み合わせにより，チャネルのダイナミクスを抽出し，将来のCSIサンプルを生成する。
- シミュレーションの結果，提案手法は最先端のベースラインを大幅に上回る性能を示した。