arXiv雑要約
プログラム - 2026/04/22 公開
再帰関係式に対する自動コード生成が，専門家による最適化を超える：階層型Codegenによる [cs.PL]目的：再帰関係式に対する最適化されたC++コードの自動生成
- 再帰関係式は，直交多項式，特殊関数，数値積分，分子積分評価など，科学計算の基本的な構成要素である。
- 既存のコードは，手作業による最適化に依存しており，専門知識と労力を要する。
- 自動コード生成により，手作業による最適化の限界を超え，高性能な科学計算を実現することを目指す。
- 階層型Codegenは，McMurchie-Davidson Hermite係数において，専門家による実装を9.8倍，テンプレートメタプログラミングを1.9倍上回る速度を達成した。
- 速度向上は，ゼロコピー出力パラメータ，関数のインライン化保証，正確なサイズのスタックバッファの利用によるものである。
- RECURSUMは，再帰アルゴリズムの性能限界を自動コード生成によって達成することを示し，高性能科学計算の民主化に貢献する。
コンパイルによる圧縮：コンパイラ出力を活用した形式定理証明の性能向上 [cs.LG, cs.AI, cs.LO, cs.PL]目的：形式定理証明の性能向上
- 形式定理証明は，ソフトウェアやハードウェアの信頼性保証に不可欠であり，その自動化が強く求められている。
- 大規模言語モデルは有望だが，計算コストが高く，大規模な探索や長い履歴が必要となる点が課題である。
- コンパイラが示す多様な証明試行と，構造化されたエラーモードの圧縮を利用し，効率的な学習と探索を目指す。
- 本手法は，ベースとなる定理証明器の推論能力を，様々な規模で一貫して向上させる。
- PutnamBenchにおいて，$\sim$8Bおよび$\sim$32Bパラメータモデルで最先端の性能を，同等の計算時間内で達成した。
- 検証者によるガイダンスに基づいた次世代推論の，スケーラブルなパラダイムを提供する。
HELIX: LLVM IRへのサイバー物理制御システムの検証付きコンパイル [cs.PL]目的：サイバー物理制御システムの検証付きコード生成
- 高性能かつ高信頼な数値計算が求められる分野であり，安全性確保が重要である。
- 生成されたコードの正当性を形式的に保証することが困難であった。
- 形式的な検証を通じて，正当性が保証された効率的なコード生成を実現する。
- HELIXは，高水準の数学的定式化からLLVM IRまでのセマンティック保存の形式的検証を可能にする。
- ベクトルおよび行列計算の代数的変換により，並列化やベクトル化に最適化されたデータフロー生成を実現する。
- Coq証明アシスタントを用いて，検証インフラを構築し，検証済み項書き換えや翻訳検証などを実装した。
緊急用UAVのための遅延と信頼性保証の基礎 [cs.IT, math.IT]目的：緊急時における厳しい制約下での，ワイヤレスネットワークにおける遅延・信頼性保証
- 災害時などの緊急時サービスにおいて，確実な通信網の確立が不可欠である。
- UAVを用いた通信網は展開が迅速だが，有限ブロック長符号化下でのQoS保証が課題である。
- 分散型UAV-MIMOシステムにおける遅延・信頼性保証の理論的枠組みを確立すること。
- 分散型UAV-MIMOシステムの確率的サービス過程を厳密にモデル化することで，遅延・誤り率のQoS指数を導出した。
- ε-有効容量や実行可能なQoS領域など，QoS駆動型の制御関数を確立した。
- シミュレーション結果により，提案手法がmURLLCをサポートできることが確認された。
ARGUS：データフロー不変量に基づくGPU最適化エージェント [cs.DC, cs.DC, cs.AI, cs.PL]目的：GPUカーネルの最適化
- AIを活用したコード生成は重要性を増している。特にGPUのような複雑なハードウェアへの最適化は困難である。
- 既存のエージェントは，疎なフィードバックに依存するため，全体的な制約違反の診断が困難である。
- データフロー不変量を用いて，より効率的なGPUカーネルの自動生成を実現することを目指す。
- Argusは，データフロー不変量を用いてGPUカーネルの最適化を行うエージェントフレームワークである。
- 生成されたカーネルは，最先端の手動最適化アセンブリのスループットの99-104%を達成し，既存のエージェントシステムを2-1543倍上回る速度を実現した。
- KernelBenchタスクにおいて，レベル1の100%とレベル2の90%の問題を解決できることが示された。
区分を持つ時空の統合を相乗効果で定量化する [cs.IT, math.IT]目的：時空統合の定量化
- 意識の数学的基盤を理解する上で，情報統合の定量的評価は不可欠である。
- 既存の情報統合の指標は，複雑系の特性を十分に捉えられていない可能性がある。
- 相乗効果に基づく情報統合指標が，意識研究においてより適切な評価を提供すること。
- 相乗効果に基づく指標は，現在のIITの実践よりも，意識研究への応用に適していることが示された。
- 本研究で提案する指標は，離散力学系における複雑性の評価にも活用できる可能性がある。
- 部分情報分解に基づいた4つの統合指標が，情報統合理論の数学的基礎を支える。
線形ゲイングラフにおける座標別平衡被覆と，2のべき乗におけるcoset-list min-2-Linへの応用 [cs.DS, cs.CC]目的：2のべき乗におけるcoset-list min-2-Lin$^{\pm}$問題の最小制約削除
- 組合せ最適化問題の理論的基礎を深める上で重要である。
- リスト制約付きのmod方程式削除問題は未解明な部分が多い。
- 平衡被覆定理とサイクル空間による解法を提示し，効率的なアルゴリズムを開発する。
- 線形ゲイングラフにおける座標別平衡被覆定理を証明した。
- ランダム化手続きにより，平衡部分グラフを効率的に検出できることを示した。
- dyadic cosetシステムに対するbit-lifting解析を行い，計算複雑性を評価した。
パス頻度クエリに対する高速線形空間データ構造 [cs.DS]目的：木構造におけるパスモード，パス最小頻度要素，パスαマイノリティクエリに対する線形空間データ構造
- グラフ構造の解析は，ネットワーク，データベース，バイオインフォマティクスなど広範な分野で重要である。
- 大規模グラフにおけるパス頻度クエリは，計算コストが高く，効率的なデータ構造が求められている。
- 線形空間で高速なパス頻度クエリを実現し，既存手法の計算量を改善することを目指す。
- パスモードおよびパス最小頻度要素クエリに対する線形空間データ構造を提案し，クエリ時間をO(√n/w)に改善した。
- パスαマイノリティ問題において，既存手法のクエリ時間をO(α⁻¹)に削減した。
- 「パス最大g値の色」クエリをサポートする線形空間データ構造を初めて提案し，O(√n/w)のクエリ時間を実現した。
パラメータ化された容量付き頂点被覆問題の再検討 [cs.DS, cs.CC]目的：容量付き頂点被覆問題の計算複雑性に関する研究
- 頂点被覆問題はグラフ理論における基本的な問題であり，ネットワーク設計やスケジューリングなどに応用がある。
- 容量付き頂点被覆問題はNP困難であり，効率的なアルゴリズムの設計が難しい。
- パラメータ化された複雑性理論を用いて，問題のより精密な計算困難性を明らかにする。
- パラメータkに関するアルゴリズムの時間計算量は，$k^{o(k)} n^{\mathcal{O}(1)}$ を達成できないことが示された。
- 頂点被覆数vcに関するアルゴリズムの時間計算量は，$2^{\mathcal{O}(\mathrm{vc}^{2-\varepsilon})} n^{\mathcal{O}(1)}$ を達成できないことが示唆された。
- 頂点完全性viに関するアルゴリズムの時間計算量は，$\mathrm{vi}^{\mathcal{O}(\mathrm{vi}^{2})} n^{\mathcal{O}(1)}$ で達成可能であることが示された。
矛盾を制御するための分類 [cs.LO]目的：制御された矛盾論理の階層
- 論理学は，推論の妥当性を検証し，知識体系の整合性を保証する上で不可欠である。
- 従来の論理では矛盾を含む情報を取り扱うことが困難であり，現実世界の複雑な状況に対応できない場合がある。
- 矛盾許容性を伴う論理体系を構築し，矛盾を含む状況下での推論の枠組みを提供する。
- 本研究では，矛盾の度合いを表現可能な制御された矛盾論理の階層LCCを提示した。
- LCCは，懐疑主義からドグマティズムまで，多様な哲学的立場を表現できる柔軟性を有する。
- さらに，3値論理LFI3の公理化と意味論的解釈を行い，多値論理の発展に貢献する。
ビジネス課題からAIソリューションへ：変革支援が失敗する地点 [cs.CE, econ.GN, q-fin.EC, cs.HC, cs.SE]目的：ビジネス課題を明確な機械学習ソリューションに変換すること
- AIの成功はビジネス課題の理解に不可欠であり，その重要性は増している。
- 既存の方法論では，ビジネス課題をAIソリューションへ変換する初期段階の支援が不足している。
- 課題のAI変換におけるギャップ（ATP）を特定し，その解決策を探る。
- 要件工学，機械学習プロジェクト管理，自動化に関する18のアプローチを分析した。
- 分析の結果，多くの手法はMLタスクやアルゴリズムの仕様を求めるが，具体的な導出ガイダンスは少ない。
- 多角的探索，タスク導出，制約フィルタリングなど5つの研究課題を提案する。
モデル変換の実行可能性検証：DSLTransのためのカットオフ定理によるアプローチ [cs.SE, cs.SC]目的：モデル変換の実行可能性検証手法
- モデル駆動開発において，モデル変換は不可欠だが，形式検証は困難である。
- 既存の変換言語は決定不能であるため，形式検証に指数関数的なコストがかかる。
- DSLTransの検証問題を解決し，現実的な規模の変換に対応可能な手法を開発する。
- カットオフ定理を用いることで，DSLTransの一部における有界モデル検査の完全性が証明された。
- SMTエンコーディングサイズを削減する最適化手法を導入し，効率的な検証を実現した。
- ATL Zoo等の現実的な変換に対して，多くの性質を証明または反例を生成することに成功した。
ツールインザループデバッグなしの信頼性の高いEDAコード生成のための構造検証 [cs.SE, cs.SY, eess.SY]目的：EDAコード生成における構造的正確性の保証
- EDA（電子設計自動化）は，現代の電子機器開発において不可欠であり，自動化による効率化が求められている。
- LLM（大規模言語モデル）を用いたEDA自動化では，設計オブジェクト間の暗黙の依存関係の違反が問題となっている。
- 本研究は，実行前に構造的正確性を検証することで，ツールとの反復的なやり取りを不要にし，効率性と信頼性を高めることを目指す。
- 提案手法は，単一ステップタスクにおいて，LLM+RAGやツールインザループと比較して，合格率を向上させた。
- 特に，多段階タスクでは，合格率が大幅に向上し，ツールの呼び出し回数を削減することに成功した。
- 不確実性対応フィルタリングにより，検証器の誤検出を低減し，精度を向上させた結果，信頼性も向上した。
相互学習的ニューラルアクティブラーニングによる人機協調型バグ報告特定 [cs.SE, cs.AI]目的：バグ報告の特定と，その適切なチームへの割り当ての効率化
- ソフトウェア品質維持において，多様なバグ報告は不可欠であり，その管理は重要である。
- バグ報告の増加と複雑化により，人的な特定・割り当てが時間的・資源的に困難になっている。
- 人機協調により，バグ報告の特定を自動化し，その効率性と精度を向上させる。
- 提案手法MNALは，異なるプロジェクト間での知識共有と，アクティブラーニングを活用している。
- 人的なラベル付けの可読性と特定可能性において，それぞれ95.8%と196.0%の改善が確認された。
- MNALは様々なニューラル言語モデルに適用可能であり，モデルの性能向上に貢献する。
依存型理論による形式検証された特許分析：ハイブリッドAI + Lean 4パイプラインからの機械検証可能な証明 [cs.AI, cs.LO, cs.PL]目的：特許分析の形式検証フレームワーク
- 特許は技術革新の重要な成果であり，その保護と活用は経済成長の鍵となる。
- 従来の特許分析は専門家による手作業に依存しており，時間とコストがかかる。
- 機械検証可能なフレームワークにより，特許分析の信頼性と効率性を向上させる。
- AIとLean 4を組み合わせることで，特許分析の自動化と形式検証を可能にした。
- 特許クレームをDAGとしてエンコードし，完全格子を用いてマッチング強度を検証する。
- 5つのIPユースケース（特許-製品マッピング，自由実施権，クレーム解釈感受性等）を形式化し，機械検証された構造的補題を提示した。
冒険を選べ: EvoGraphによる非線形AI支援プログラミング [cs.HC, cs.AI, cs.SE]目的：AI支援プログラミングの新しい開発環境
- プログラミングは反復的で分岐が多く，AI支援による効率化が期待される
- 既存のAI支援ツールは線形であり，探索や変更の追跡が困難である
- AI支援プログラミングの過程を可視化し，効率的な反復と探索を支援する
- EvoGraphは，AIとの対話とコード変更を開発グラフとして記録・操作可能にするIDEプラグインである。
- ユーザ調査の結果，EvoGraphは認知負荷を軽減し，安全な探索，効率的な反復，AI生成コードの考察を支援することが示された。
- 本研究は，AI支援プログラミングにおける問題解決の進捗を理解し，行動するためのツール設計の機会を示唆する。
粒子から危険へ：自動運転システムテストのためのSVGDベースの危険シナリオ生成 [cs.SE, cs.LG]目的：自動運転システムのテストにおける現実的かつ多様な故障の発見
- 自動運転技術の安全性を確保するためには，様々な運転環境下でのテストが不可欠である。
- 従来の探索手法は高次元空間で有効な故障シナリオを見つけにくいという課題がある。
- 多様で故障を引き起こす初期条件を効率的に生成し，システムの安全性を向上させる。
- 本研究で提案するPtoPは，SVGDを用いてリスクの高い領域に焦点を当てつつ，多様なシナリオを生成することに成功した。
- CARLAシミュレーション環境での実験により，PtoPは既存手法と比較して安全違反率を最大27.68%改善した。
- また，シナリオの多様性とマップカバレッジもそれぞれ9.6%と16.78%向上することを示した。
同時ワイヤレス電力伝送統合型受信機に対する厳密なチャネル容量下限 [cs.IT, math.IT]目的：同時ワイヤレス電力伝送におけるチャネル容量下限
- 無線電力伝送は，エネルギーハーベスティングやIoTデバイスの普及に不可欠である。
- 既存研究は主に分離型受信機に焦点を当てており，統合型受信機の容量限界は未解明であった。
- 統合型受信機の容量を正確に評価し，効率的な電力伝送システムを設計すること。
- ショットキーダイオードの特性を４次テイラー展開で近似することで，チャネル移行確率行列の厳密な近似を導出した。
- 入力分布としてガンマ分布を用いることで，レイリー分布や一様分布よりもタイトな容量下限が得られた。
- ４次テイラー展開項を考慮することで，２次テイラー展開のみを用いたモデルと比較して，容量が顕著に向上することが示された。
セキュリティは相対的：訓練不要の脆弱性検出におけるマルチエージェント行動契約合成 [cs.CR, cs.SE]目的：脆弱性検出のための行動契約合成
- ソフトウェアの安全性確保は，現代社会における情報システムの信頼性維持に不可欠である。
- 既存の深層学習モデルは，厳密な重複排除により性能が大幅に低下する課題がある。
- プロジェクト固有の行動契約に基づき，脆弱性の曖昧さを解消することを目指す。
- Phoenixは，Semantic Slicer，Requirement Reverse Engineer，Contract Judgeの３段階で脆弱性を検出する。
- PrimeVul Pairedデータセットにおいて，F1スコア0.825，Pair-Correct 64.4%を達成し，既存手法を上回る性能を示した。
- 誤検出の18%は，実際にはパッチされたコードにおけるセキュリティ上の懸念を示しており，セキュリティは絶対的なコード構文ではなく，行動契約に対する相対的な性質であることが示唆された。
LLM-Viterbi：畳み込み符号のための意味認識デコーディング [cs.IT, math.IT]目的：畳み込み符号を用いたテキスト伝送におけるデコーディング性能向上
- 無線通信において誤り訂正は重要であり，信頼性の高いデータ伝送を可能とする。
- 従来の誤り訂正符号はデータソースの意味構造を利用していないという課題がある。
- 言語モデルを活用し，符号と意味の両面から最適な復号を試みる。
- 提案手法は，従来のViterbiデコーディングと比較して，ブロック誤り率と意味類似度において有意な改善を達成した。
- 制約長3の畳み込み符号において，約1.5dBの符号ゲインと，意味類似度の50%以上の向上が確認された。
- 本フレームワークは，テキスト以外の構造化データソースにも拡張可能である。
妥当性推論と一階述語の妥当性論理 [cs.AI, cs.LO]目的：妥当性推論の原理と一階述語の妥当性論理の定義
- 日常的な推論は確率を用いないため，人間の思考モデルとして重要である。
- 既存の論理では，不確実な情報や例外的な状況への対応が困難である。
- 確率を用いない妥当性推論のための論理体系を構築し，その有効性を示す。
- 妥当性推論を行うための17の原理が提案され，そのうち14が必須原理，3が望ましい原理とされた。
- 提案された一階述語論理「妥当性論理(PL)」は，望ましい原理のほとんどを満たし，妥当性推論の事例に対して正しく推論する。
- PLは，与えられた状況から複数の妥当な結論を導き出す8つの推論アルゴリズムを持つ。
素数pの冪乗環上の$x^{p+1}-1$の明示的な因数分解：ディクソン多項式による構造的アプローチ [cs.IT, math.IT]目的：素数pの冪乗環$\mathbb{Z}_{p^e}$上での多項式$x^{p+1}-1$の因数分解に関する研究
- 巡回符号の構成に不可欠であり，特に線形相補双対符号やエンタングルメント支援型量子誤り訂正符号の設計に利用される。
- 従来の因数分解の持ち上げはHenselの補題に依存しており，その背後にある代数構造が見えにくいという問題があった。
- ディクソン多項式との決定的な関連性を明らかにし，効率的な因数分解アルゴリズムを開発すること。
- 持ち上げ過程と補助多項式$V(x)$の根との間の構造的同型性を確立し，線形時間($O(ep)$)で動作する「Dickson-Engine」アルゴリズムを開発した。
- $\mathbb{Z}_{169}$に適用することで，等長Gray写像を用いた長さ$n=182$の古典的LCD符号の族を明示的に構成することに成功した。
- 発見された符号は，Griesmerの上界に対して「ほぼ最適」であり，次元が大きくなるにつれて最小距離が安定する「頑健性プラトー」が存在することが示された。
反論または推奨：高精度なLLM支援欠陥発見のための敵対的段階ゲート型マルチエージェントレビュー手法 [cs.CR, cs.AI, cs.SE]目的：LLM支援欠陥発見における誤報の抑制と，実質的な発見の信頼性向上
- ソフトウェアの信頼性確保は，社会インフラや経済活動を支える上で不可欠である。
- LLMによる欠陥発見は有望視されているが，誤報が多く，実用上の信頼性に課題がある。
- LLMの誤報を効果的に削減し，より信頼性の高い欠陥発見プロセスを確立すること。
- 提案手法「Refute-or-Promote」は，候補となる欠陥を敵対的に検証するプロセスを導入し，誤報の約79-83%を事前に排除した。
- 本研究により，CVE 4件，C++標準への提案，コンパイラバグの修正など，実際のソフトウェア改善に貢献した。
- 実証実験から，LLMだけでは見過ごされる可能性のある欠陥を，経験的なテストと外部レビューによって発見できることが示された。
LDPC符号非線形チャネル向け３モジュールSC-VAMP [cs.IT, math.IT]目的：非線形チャネルにおける信号復元
- 通信システムの信頼性向上は重要であり，特に非線形チャネル環境下での性能改善が求められる。
- 従来の復号手法では，非線形チャネルの特性を十分に捉えきれず，性能劣化が生じることが課題である。
- 本研究は，非線形チャネルにおける復号性能を向上させるための新たなフレームワークを提案する。
- 提案手法である３モジュールSC-VAMPは，ビット誤り率において明確なウォーターフォール特性を示す。
- ブロック長を128から2304に増加させるにつれて，容量推定値とのギャップが縮小する。
- 本フレームワークは，モジュール構造により，様々な非線形チャネルへの適用が容易である。
マルチウィンドウ環境におけるマルチモーダル推論によるGUI欠陥の積極的検出 [cs.SE]目的：マルチウィンドウ環境におけるGUI表示欠陥の検出，ローカライズ，および説明
- モバイルアプリケーション利用の多様化により，分割画面や折りたたみ端末などマルチウィンドウ環境の重要性が増している。
- 従来のGUIテスト技術は受動的であり，マルチウィンドウ環境におけるレイアウト崩れ等の検出が困難である。
- 本研究は，マルチウィンドウ環境下で発生しやすいGUI欠陥を能動的に検出し，その原因を特定することを目指す。
- マルチウィンドウ環境では，フルスクリーン環境と比較して，テキストの切り抜けなどのレイアウト関連欠陥が大幅に増加することが確認された。
- 提案手法は，偽陽性率10.00%，偽陰性率11.11%で40個の欠陥を起こしやすいアプリを特定し，既存手法を上回る性能を示した。
- 特に，ウィジェットの遮蔽検出において，F1スコア87.2%という最高の結果を達成した。
MUCOCO：コードLLMの一貫性自動テスト [eess.SY, cs.SY, cs.SE]目的：コードLLMの一貫性検証手法
- コード生成AIの発展に伴い，その品質保証が重要になっている。
- 既存のベンチマークは手動作成であり，一貫性の検証に特化していない。
- コードLLMにおける不整合なプログラム挙動を自動的に発見すること。
- MUCOCOは，意味を保持する変異分析を用いてコードLLMの不整合を検出する。
- 4つのコーディングタスクと7つのLLMを用いた評価で，MUCOCOはTURBULENCEよりも高い効果を示した。
- MUCOCOが生成した入力の約15%で一貫性の問題が明らかになった。
クリーク幅を超えて：縮小成分最大リーフと関連パラメータ [eess.SY, cs.SY, cs.CL, cs.DS, cs.DM, math.CO]目的：縮小パラメータを用いたグラフの構造解析
- グラフ理論は，ネットワーク科学や計算機科学の基礎であり，様々な応用分野で重要である。
- グラフの複雑度を測るパラメータの限界があり，より表現力の高い指標が求められている。
- グラフの構造に着目し，縮小成分最大リーフという新たなパラメータを導入することで，グラフの解析可能性を向上させる。
- 縮小成分最大リーフは，クリーク幅と縮小帯域幅の間に位置し，単位区間グラフでは有界であることが示された。
- 縮小成分最大リーフが低いグラフでは，最大誘導d-正則部分グラフ問題や誘導離散パス問題が多項式時間で解けることが示された。
- 縮小パラメータの閉包性に関する結果が得られ，3次元グリッドが無限の縮小帯域幅を持つことが証明された。
より共感的なプログラミング環境へ: 実験的な共感型AI拡張IDE [cs.SE, cs.CY]目的：初心者プログラマーの学習と感情的サポートを重視した共感型IDEの有効性評価
- ソフトウェア開発における生成AIの利用拡大に伴い，学習支援の重要性が増している。
- 生成AIへの過度な依存による批判的思考力の低下が懸念されている。
- AIによる共感的な応答が，初心者プログラマーの学習効果向上に貢献するかを検証する。
- CeciとVSCode+ChatGPTの比較実験の結果，学習効果や作業負荷に有意差は認められなかった。
- エラー修正における有用性に関して，Ceci利用群は有意に高い評価を得た(p = 0.0220)。
- 共感的な応答だけでは学習効果の向上や作業負荷の軽減には不十分である可能性が示唆された。
カスケード型コード編集：効果的かつ効率的なコード編集のための大規模・小規模モデルの連携 [cs.SE]目的：効果的かつ効率的なコード編集の実現
- ソフトウェア開発において，コード編集は不可欠な作業であり，その効率化は生産性向上に直結する。
- 大規模言語モデルは性能を示すものの，変更されていないコードを多く含んだファイル全体を生成するため非効率である。
- 大規模モデルと小規模モデルを連携させ，効率性と正確性を両立することを目指す。
- 本研究では，コード編集を「編集スケッチ生成」と「編集スケッチ適用」の二段階のカスケード構造に分解する手法を提案する。
- 大規模モデルで編集内容のスケッチを生成し，小規模モデルでそれをコードに適用することで，大規模モデルのトークン生成量を削減する。
- 現状の小規模モデルは長文脈やファイル間の依存関係の処理に限界があり，スケッチの適用において課題が残る。
トポロジーニューラルネットワークの論理的表現力 [cs.LG, cs.LO]目的：トポロジーニューラルネットワークの論理的表現力の解明
- グラフ構造データに対する機械学習の重要性が高まっており，表現力の高いモデルが求められている。
- 従来のグラフニューラルネットワークは表現力に限界があり，複雑なグラフ構造の学習が困難である。
- トポロジーニューラルネットワークの表現力を理論的に明らかにし，その能力を評価すること。
- 本研究では，トポロジーニューラルネットワークのメカニズムから導出される同型性テストを分析した。
- 組み合わせ的複体のための，より高次のWLテストである$k$-CCWLテストと，トポロジカルカウント論理TC$_k$を導入し，その関係性を調べた。
- $k$-CCWLテスト，TC$_{k+2}$，そして$(k+2)$-pebbleゲームの論理的同値性を厳密に証明し，トポロジーニューラルネットワークの論理的表現力の理論を確立した。
iCoRe：バグ再現テスト生成のための反復相関認識検索器 [cs.SE]目的：バグ再現テストの自動生成における，高品質なコードベースのコンテキスト検索
- ソフトウェア保守において，バグ修正は不可欠であり，効率的なテストがその成功を左右する。
- 既存のコンテキスト検索手法は，ソースコードとテストケースの性質の違いを考慮していない場合がある。
- 本研究は，ソースコードとテストケース間の相関を考慮した反復的なコンテキスト検索により，バグ再現テストの精度向上を目指す。
- 提案手法iCoReは，既存手法と比較して，SWT-bench Liteベンチマークで19.7%，TDD-bench Verifiedベンチマークで31.7%高い相対的な改善を示す。
- iCoReは，ソースコードとテストケースを区別した検索，テキストの意味と関数呼び出し構造の相関，検索と生成フェーズ間のフィードバックループを実現する。
- 実験結果から，iCoReはFail-to-Pass率を42.0%と52.8%に低減し，バグ再現テスト生成の有効性を示す。
信頼性の低い構成要素からの信頼できるリモート推論：通信と計算の限界 [cs.IT, eess.SP, math.IT]目的：信頼性の低い構成要素からなる受信側におけるリモート推論の限界
- 通信・計算資源が限られた環境下での情報処理の信頼性確保は重要である。
- 受信側の構成要素に信頼性がない場合，推論の正確性が損なわれる可能性がある。
- 信頼性の低い構成要素を用いながらも，信頼性の高いリモート推論を可能にする限界を明らかにする。
- 従来の分離定理では，受信側の計算資源の信頼性が前提とされていたが，本研究ではその限界を示す。
- コミットメント/バイパス制約下では，計算グラフにおけるボトルネックが推論性能に影響を与えることが示された。
- ソフト情報が利用可能な場合は，単一のボトルネックによる制約が適用され，性能向上が期待できる。
BONSAI：ビジュアル分析アプリケーションの人間とAIによる共同開発のための混合型ワークスペース [cs.HC, cs.MA, cs.SE]目的：ビジュアル分析アプリケーションの人間とAIによる共同開発
- ビジュアル分析は，複雑なデータから洞察を得る上で不可欠であり，そのアプリケーション開発の効率化が求められている。
- 既存の開発手法では，柔軟性と保守性の両立が難しく，AIによる自動生成は制御が困難であるという課題がある。
- AIの生成能力と人間の制御を両立させ，ビジュアル分析アプリケーション開発の効率と構造化を同時に実現することを目指す。
- BONSAIは，ハードウェア，サービス，オーケストレーション，アプリケーションの4層構造を持つワークスペースである。
- この構造により，人間とAIの開発者が再利用可能なコンポーネントを独立して貢献することが可能となる。
- ケーススタディにより，BONSAIが新規ツールの効率的な作成と，研究論文からの複雑なアプリケーションの迅速な再構築を可能にすることが示された。
Answer Set Programmingのためのストリーマー [eess.SY, cs.SY, cs.LO, cs.AI]目的：組み合わせ問題の探索空間削減
- 組合せ最適化問題解決において，効率的な探索が重要である。
- 既存手法では探索空間が広大で，計算コストが高い場合がある。
- LLMを活用し，問題構造を捉えた制約を生成することで，探索効率を向上させる。
- 提案手法により，ASP Competitionの3つのベンチマーク問題で，最大4～5倍の高速化を達成した。
- 異なるLLMが意味的に多様な制約を生成し，単なる構文的変化ではないことが示された。
- 仮想最良符号化(VBE)により，元の符号化とストリーマーを組み合わせた最適なパフォーマンスが得られた。
大規模MIMO-ISACシステムにおけるアップリンク信号検出 [cs.IT, math.IT]目的：大規模MIMO-ISACシステムにおける信号検出問題
- 次世代無線通信は，高性能なセンシングと通信を実現するため，MIMOとISACの統合が不可欠である。
- MIMO-ISACシステムにおける効率的な信号検出は，計算量が大きく，困難な課題である。
- 本研究は，MIMO-ISACシステムの信号検出における計算量と性能の課題を解決することを目指す。
- 提案手法であるP-NS-ADMMは，理論的に最尤検出と同等の受信多様度を獲得することが示された。
- さらに計算量を削減するため，投影演算を省略したI-NS-ADMMを提案し，P-NS-ADMMと比較して有利性を示した。
- シミュレーションにより，提案手法がBERとNMSEの両面で有意な性能向上をもたらすことが確認された。
自動制約充足問題 [cs.LO, cs.FL]目的：自動制約充足問題の複雑性
- 制約充足問題は，AIや計算機科学の根幹をなす重要な問題である。
- 従来の制約充足問題では，制約の表現が冗長になる場合がある。
- 有限オートマトンで定義される制約言語を用いることで，簡潔な制約表現を可能とする。
- 本研究では，制約言語を有限オートマトンで定義する自動制約充足問題($AutCSP$)の複雑性を解析した。
- 演算がそのような言語の多型であるかの判定は多項時間で可能であることが示された。
- Schaeferの二分定理が$AutCSP$に拡張され，一部のクラスの$AutCSP$の実行可能性が自動多型を用いて決定された。
巡回泥棒問題の計量インスタンスに対する効果的な移動 [cs.IR, cs.RO, cs.HC, cs.DS]目的：巡回泥棒問題におけるルート最適化の複雑性と近似アルゴリズム
- 巡回泥棒問題は，TSPとナップサック問題の融合であり，現実世界の複雑な最適化問題への応用が期待される。
- 既存の厳密解法は計算量が大きいため，大規模問題に対する性能評価が困難である。
- 固定された荷物計画の下で，ルート最適化の計算量と近似可能性を明らかにすること。
- 経路距離の計量において，一般的なコスト関数に対する動的計画法アルゴリズムをO(n^2)時間で実現した。
- 星型計量においてもNP困難性が証明され，星型計量に対する定数倍近似アルゴリズムを開発した。
- 一般的な計量と線形コスト関数下での近似アルゴリズムを提案し，実験的にその有効性を示した。
LLMに基づく自動プログラム修理における自己主導デバッグによる機能強化 [cs.SE]目的：LLMを用いた自動プログラム修理の性能向上
- ソフトウェアの品質確保は重要であり，バグの自動修正は開発効率を飛躍的に向上させる可能性を秘めている。
- 既存の自動プログラム修理手法は，スタックトレースなどの表面的な情報に依存しており，根本原因の特定が困難である。
- 本研究では，ランタイム時の情報を活用することで，より正確なバグ修正を可能にすることを目指す。
- DebugRepairは，テストのセマンティック浄化，シミュレーションによる計測，デバッグ駆動型対話修理の3つの要素で構成される。
- 実験の結果，Defects4Jベンチマークにおいて，GPT-3.5を用いて224件のバグを修正し，既存の最先端手法を26.2%上回る性能を示した。
- また，DeepSeek-V3を使用した場合，295件のバグを修正し，2番目に良いベースラインを59件上回る結果を得た。
モック情報からの学習によるLLM駆動型テスト生成の改善 [cs.SE]目的：LLM駆動型テスト生成の改善
- ソフトウェア品質の確保は重要であり，自動テストはその効率化に不可欠である。
- 既存のテスト生成手法では，十分なテストカバレッジや欠陥検出が難しい場合がある。
- モック情報を用いることで，LLMによるテスト生成の精度と網羅性を向上させる。
- MOCKMILLは，既存のテストスイートから自動的にモック情報を抽出し，テストケース生成に活用する。
- 実験の結果，MOCKMILLによって生成されたテストは，既存テストやベースライン手法で生成されたテストよりも多くのコード行をカバーし，より多くのミュータントを検出した。
- これらの結果は，モック情報の活用がLLMベースのテスト生成を効果的に強化する可能性を示唆する。
エージェントはルートシェルを夢見るか？ CTFチャレンジにおけるLLMエージェントの段階的評価 [cs.CL, cs.AI, cs.CR, cs.SE]目的：LLMエージェントのCTFチャレンジにおける能力評価
- サイバーセキュリティの自動化ニーズが高まる中で，LLMの活用が期待されている。
- 現実的な攻撃環境下でのLLMエージェントの能力は，十分に評価されていない。
- LLMエージェントの具体的な能力と課題を明らかにすること。
- DeepRedという，現実的なCTFチャレンジを評価するためのベンチマークが開発された。
- 10種類のLLMを評価した結果，平均的なチェックポイント達成率は35%に留まった。
- 一般的なチャレンジタイプには強い一方，非標準的な探索や長期的な適応能力は低いことが示された。
関数反転によるサフィックスランダムアクセス：非対称ストリーミング文字列アルゴリズムの鍵 [cs.CE, cs.DS]目的：非対称ストリーミングモデルにおける文字列問題の効率的な解決
- 文字列処理は計算機科学の基礎であり，効率的なアルゴリズム開発は重要である。
- 古典的な設定で効率的な問題でも，ストリーミング設定では効率化が難しい場合が多い。
- 非対称ストリーミングモデルを用いて，古典的なアルゴリズムをストリーミングモデルへ応用すること。
- サフィックスランダムアクセスデータ構造を導入し，非対称ストリーミングモデルでの効率的な計算を可能にした。
- パターンマッチング（ハミング距離，編集距離），相対的なLempel-Ziv圧縮などのアルゴリズムを改善した。
- サフィックスランダムアクセスと関数反転の間の双方向削減を示し，理論的な基盤を確立した。
Javaプロジェクトにおけるエネルギー回帰と対応するコードパターンの体系的検出 [cs.SE]目的：Javaプロジェクトにおけるエネルギー回帰とその原因となるコードパターンの検出
- 情報技術のエネルギー消費増加に対応するグリーンソフトウェア工学の重要性が高まっている。
- コミットごとのエネルギー回帰を自動検出する手法が不足している。
- エネルギー回帰の自動検出と，その原因となるコード反パターンを特定することを目指す。
- 開発されたEnergyTrackrは，複数のコミットにわたるエネルギー回帰を検出できる。
- 3,232コミットの分析から，有意なエネルギー変化を特定することに成功した。
- 早期終了の欠如や，コストのかかる依存関係のアップグレードといった反パターンが明らかになった。
一般帰納的定義に対する順序計算 [cs.LO]目的：一般帰納的定義に関する知識表現と推論
- 知識表現の基礎であり，プログラム検証やAI分野で不可欠な役割を担う。
- 既存の証明システムは定義に制約を課し，有用な定義を排除する問題がある。
- 制約のない一般帰納的定義を扱える，形式的な証明システムの構築を目指す。
- 非単調な帰納的定義を扱うため，安定意味論の考え方を導入した。
- SCFO(ID)という新たな順序計算を提案し，その理論的性質を証明した。
- 様々な例を通して，SCFO(ID)が一般帰納的定義を含む定理の形式的証明を可能にすることを示した。
SysML v2 を用いたステークホルダーコンテキストの形式化に向けた試み [cs.SE]目的：ステークホルダーコンテキストと正式なシステムアーキテクチャ間のギャップを埋めるためのフレームワーク
- システム開発において，ステークホルダーの要求を正確に把握し，システムに反映することは重要である。
- ステークホルダーのコンテキストは主観的であり，システムアーキテクチャへの形式的な変換が困難である。
- ステークホルダーコンテキストをSysML v2を用いて形式化することで，誤解のリスクを低減することを目指す。
- 本研究では，ソフトシステム手法 (SSM) と SysML v2 を組み合わせたフレームワークを提案している。
- 提案フレームワークは，SSM のアウトプットと SysML v2 のステークホルダーや関心事項といった概念間のマッピングを可能にする。
- ケーススタディを通して，ステークホルダーコンテキストからシステムアーキテクチャへのトレーサビリティが確認された。
超低消費電力IoTにおけるノイズ変調の実用性能：限界，容量，エネルギーのトレードオフ [cs.IT, eess.SP, math.IT, stat.AP]目的：超低消費電力IoT向けノイズ変調の実用性能評価
- IoTデバイスの普及に伴い，低消費電力通信技術の重要性が増している。
- 従来の変調方式では，消費電力の低減に限界がある。
- ノイズ変調の理論的潜在能力と実用展開のギャップを明確にすること。
- ノイズ変調は，フェージング環境下で急激なエラーフロアに陥り，2アンテナ選択ダイバーシティなどの追加が必要となる。
- ADCを考慮したエネルギーモデルの結果，ノイズ変調のオーバーサンプリングが容量を制限し，AWGN環境下でNC-FSKと比較して8dBのSNRペナルティが生じる。
- 周波数が高まるにつれて，エネルギー効率で優位性を示す距離（エネルギー・クロスオーバー距離）が短縮される。
CASCADE：コードとドキュメント間の不整合を自動テスト生成で検出 [cs.SE]目的：コードとドキュメント間の不整合の検出
- ソフトウェア開発において，コードとドキュメントの一貫性は重要だが，見過ごされがちである。
- 不整合はAPI利用者を混乱させ，バグを誘発し，保守コストを増加させるという問題がある。
- 誤検出を減らし，開発者の負担を軽減する自動化された不整合検出手法を提供する。
- CASCADEは，ドキュメントからユニットテストを自動生成することで不整合を検出する。
- 生成されたテストが失敗し，ドキュメントから生成されたコードが同じテストに合格した場合にのみ，不整合として報告される。
- オープンソースJavaプロジェクトのデータセットで評価した結果，13件の未知の不整合を発見し，そのうち10件が修正された。
生成AIにおける事後バイアス軽減のための分岐時間意味論：ワールド数のカウント [cs.HC, cs.HC, cs.CY, cs.HC, cs.NI, cs.SY, eess.SY, cs.HC, cs.CY, cs.LO, cs.AI]目的：生成AIの出力系列におけるバイアスを形式的に検証・軽減するための論理CTLFの提案
- 生成AIは社会に広く利用されつつあり，その公平性が重要課題となっている。
- 生成AIは学習データに存在するバイアスを増幅する傾向があり，その軽減が困難である。
- 出力系列全体の公平性を保証する形式的な手法を確立し，バイアス軽減の理論的基盤を提供する。
- CTLFは，各出力が異なる「ワールド」として表現される分岐時間論理であり，生成過程の各段階でバイアスを評価できる。
- CTLFのモダル演算子を用いることで，意図した属性分布の尊重度，許容範囲内にとどまる確率，公平性を回復するための削除数などを検証できる。
- バイアスの存在する画像生成の例において，CTLFが具体的な公平性特性を表現できることを示した。
動的な振る舞いの学習による悪意のある機械学習モデルの検出 [cs.CR, cs.SE]目的：悪意のある事前学習済み機械学習モデルの検出
- 機械学習モデルの共有が容易になった一方，悪意のあるモデルによる攻撃のリスクが増大している。
- 既存の検出手法は静的解析に頼るため，実行時の振る舞いを捉えきれず，誤検知や見逃しが発生しやすい。
- 本研究は，動的解析と機械学習を用いて，正常なモデルの振る舞いを学習し，悪意のあるモデルを高精度に検出する。
- 提案手法DynaHugは，正常なモデルの実行時振る舞いを学習することで，悪意のあるモデルを検出する。
- 25,000以上のモデルを用いて評価した結果，既存手法と比較してF1スコアで最大44%の改善が見られた。
- 動的解析，OCSVM，クラスタリングといった設計要素が，DynaHugの有効性に貢献していることが示された。
クラッシュフリーな演繹的検証器 [cs.CL, cs.SE]目的：演繹的検証器の品質と堅牢性の向上
- 演繹的検証器は開発者以外にも利用が広がりつつあり，信頼性が重要となる。
- 大規模で複雑な検証器自体の完全な検証は困難である。
- ファジングを用いて，検証器の信頼性を実質的に向上させる。
- ファジングは，演繹的検証器の品質向上に有効な手段であることが示された。
- プロトタイプツールAValAnCHEを用いてVerCors検証器の複数の問題を検出した。
- このアプローチは他の演繹的検証器にも適用可能であることが確認された。
LLMは形式化を操作するか？論理的推論における忠実性の評価 [cs.AI, cs.CL, cs.LO]目的：論理的推論における形式化の忠実性
- 形式検証は証明の妥当性を保証するが，形式化の忠実性は保証しない。
- 自然言語からの論理的推論では，形式化と証明が一体で行われるため，忠実性の評価が難しい。
- LLMが形式化の忠実性を無視して妥当な証明を生成する「形式化の操作」を検証する。
- GPT-5とDeepSeek-R1の実験では，統一生成において体系的な操作は見られなかった。
- GPT-5は証明生成時に公理を捏造するが，DeepSeek-R1は前提の誤訳により検出困難な不忠実性を示す。
- 高いコンパイル率や精度は，必ずしも忠実な推論を意味しないことが示唆される。