arXiv雑要約
プログラム - 2026/04/20 公開
ビジョン言語モデルを用いたクラッシュ図の自動生成：多車線環状交差点におけるケーススタディ [cs.HC, cs.AI, cs.CV, cs.SE]目的：交通安全分析におけるクラッシュ図の自動生成
- 交通安全は社会の根幹であり，事故分析の効率化は重要である。
- クラッシュ図の作成は手作業に頼る部分が多く，時間と労力を要する。
- ビジョン言語モデルを活用し，クラッシュ図作成の自動化を実現すること。
- GPT-4oが最も高い性能（10点満点中6.29点）を示し，Gemini-1.5-Flash (5.28点)，Janus-4o (3.64点)に次ぐ結果となった。
- GPT-4oは空間認識能力が高く，抽出データと視覚化データの整合性が優れていた。
- 生成AIを事故分析ワークフローに統合することで，効率性，一貫性，解釈可能性の向上に貢献できる可能性が示唆された。
確率的言語トライを用いた逐次KVキャッシュ圧縮：ベクトルごとのシャノン限界を超える [eess.SY, cs.SY, physics.ao-ph, physics.app-ph, cs.LG, cs.AI, cs.IT, cs.NE, math.IT]目的：トランスフォーマーのキーバリューキャッシュの逐次圧縮
- 大規模言語モデルの効率的な推論は，メモリ使用量の削減が不可欠である。
- 既存のKVキャッシュ圧縮手法は，ベクトルの独立性を仮定し，言語構造を活かせていない。
- 言語モデルの予測能力を利用し，より高効率なKVキャッシュ圧縮を実現する。
- 提案手法は，確率的プレフィックス重複排除と予測デルタ符号化の二層構造を用いる。
- 理論的には，従来のTurboQuantと比較して約914,000倍の圧縮率を達成可能である。
- 文脈長が長くなるほど圧縮率は向上し，実用的なソースコーダーのオーバーヘッドを考慮してもTurboQuantを上回る。
AutoFlows++：システム・オン・チップ設計における階層的メッセージフローマイニング [cs.AR, cs.LG, cs.SE]目的：システム・オン・チップ設計におけるメッセージフローの抽出
- SoCの複雑化に伴い，検証，性能分析，デバッグにおいて通信動作の理解が不可欠である。
- 既存の手法は，複雑なインターリーブや曖昧な因果関係により，スケーラビリティと精度に課題がある。
- 複雑なSoC設計における正確なメッセージフロー抽出と検証効率の向上を目指す。
- AutoFlows++は，局所的なマイニングとグローバルなマイニングの2段階でメッセージフローを抽出する。
- 局所的なマイニングでは，個々の通信インターフェースから単純なパターンを抽出し，グローバルなマイニングでそれらを合成する。
- GEM5を用いた実験により，AutoFlows++は既存手法と比較してフロー抽出の精度が大幅に向上することが示された。
InfoChess：敵対的推論のゲームと定量的な情報制御の実験場 [cs.MA, cs.AI, cs.IT, cs.LG, math.IT]目的：競争的な情報獲得の主要な目的化
- 情報科学において，情報獲得は意思決定や戦略形成の根幹をなす重要な要素である。
- 既存の研究では，物質的なインセンティブが情報獲得の役割を歪める可能性がある。
- 部分観測下における多エージェント推論の研究のためのテストベッドの提供。
- InfoChessは，駒の奪取がない対称的な敵対的ゲームであり，情報獲得を競争の主要な目的とする。
- 相手のキングの位置に関する確率的推論を，ゲームの期間を通して評価する。
- 強化学習エージェントは，対戦相手のモデリングレベルを徐々に高めたヒューリスティックエージェントよりも優れた性能を発揮した。
LinuxArena：実稼働ソフトウェア環境におけるAIエージェントの制御設定 [cs.CR, cs.AI, cs.SE]目的：実稼働環境におけるAIエージェント制御のためのテストベッド
- ソフトウェア開発におけるAIの活用は進むが，安全性と信頼性の確保が課題である。
- 既存のテスト環境では，実環境の複雑さを再現できず，実用的な検証が困難である。
- 実稼働環境での攻撃と防御を評価できる，大規模かつ多様なテスト環境を構築すること。
- LinuxArenaは，20の環境，1,671の主要タスク，184のサイドタスクを含む，ソフトウェアエンジニアリング分野で最大かつ多様な制御設定である。
- Claude Opus 4.6は，1%の誤検知率のGPT-5-nano監視モデルに対し，約23%の検出されない妨害成功率を示した。
- 人間が作成した攻撃経路データセットLaStrajは，モデル生成の攻撃よりも高い確率で監視を回避することから，LinuxArenaには更なる発展の余地があることが示唆された。
プロンプト駆動型コード要約：体系的文献レビュー [cs.SE, cs.LG]目的：プロンプト駆動型コード要約に関する既存研究の整理と分類
- ソフトウェア開発において，コード理解，開発者の参入，コードレビューは不可欠であり，高品質なドキュメントが重要である。
- 手動によるドキュメント作成は時間がかかり，不完全または矛盾した結果になりやすいという課題がある。
- 大規模言語モデルを用いたコード要約における最適なプロンプト戦略の特定と，評価方法の標準化を目指す。
- 本レビューでは，プロンプト設計がLLMの性能に大きく影響することを確認した。
- Few-shot prompting，Chain-of-Thoughtなどの様々なプロンプト戦略を分類し，その有効性を比較検討した。
- 現在の研究は断片的であり，セマンティックな質を捉えられないオーバーラップベースの評価指標が主流であるという課題を指摘した。
RISアシスト高速鉄道通信カバレッジ向上のためのロバストな伝送設計：不完全なカスケードチャネルを考慮して [cs.FL, cs.DM, math.GR, math.RT, cs.IT, math.IT]目的：RISアシスト高速鉄道通信のカバレッジ向上に関するロバストな伝送設計
- 高速鉄道環境では，電波の届きにくさが課題であり，安定した通信を確保する必要がある。
- 従来のRIS研究では，完全なチャネル状態情報(CSI)を前提としているが，現実にはCSIの取得に限界がある。
- 不完全なCSI環境下においても，高速鉄道通信の安定性を確保できる伝送設計手法を提案する。
- 本研究では，最悪ケースレート制約と統計的CSI誤差モデルの2つのモデルに基づき，RISの最適化問題を検討した。
- 最悪ケースレート制約を線形行列不等式に変換するためにS-procedureを適用し，外れ確率制約を変換するためにBernstein型の不等式を使用した。
- シミュレーション結果から，ベース局-RIS-ユーザ間のカスケードチャネル誤差が，直接的なCSI誤差よりもシステム性能に大きな影響を与えることが示された。
制御フローコード難読化解除における思考の連鎖（CoT）アプローチの分析 [cs.SE, cs.AI]目的：制御フロー難読化解除の品質向上
- ソフトウェアのセキュリティ確保のため，難読化されたコードの解析が不可欠である。
- 従来の難読化解除は手作業に頼ることが多く，時間とコストがかかるという課題がある。
- 大規模言語モデルとCoTを活用し，難読化解除の自動化と効率化を目指す。
- 思考の連鎖（CoT）プロンプトは，単純なプロンプトと比較して，コード難読化解除の品質を大幅に向上させる。
- 特にGPT5は，制御フローグラフの再構成において約16％，意味的保存において約20.5％の平均的な改善が見られた。
- 難読化レベル，難読化ツール，および元の制御フローグラフの複雑さがモデルの性能に影響を与えることが示された。
漸近最適非周期ドップラー耐性補完系列集合の5つの構成法と新たなパラメータ [cs.IT, math.IT]目的：漸近最適非周期ドップラー耐性補完系列集合の新たなパラメータ
- レーダー探知システムや最新のモバイル通信において，良好な曖昧性関数特性を持つ系列は重要である。
- 既存の非周期ドップラー耐性補完系列集合は，パラメータの制約や性能の限界がある。
- 新たなパラメータを持つ系列集合を構成し，既存手法よりも優れた性能を発揮すること。
- 有限体上のトレース関数と列直交複素行列を利用し，5種類の漸近最適非周期ドップラー耐性補完系列集合を構成した。
- 提案手法で得られた非周期ドップラー耐性補完系列集合は，既存手法と比較して，優れたまたは新たなパラメータを提供する。
- 特に3つの系列集合ファミリーでは，適切な列直交複素行列を選択することで，ピーク対平均電力比をpで上限化できる。
基礎最適化埋め込みからの転移学習：教師なしSAT表現への応用 [cs.HC, cs.CY, cs.LG, cs.AI, cs.LO]目的：基礎最適化埋め込みを用いたSATインスタンスの構造的規則性の把握と，教師なしタスクへの応用
- 最適化問題解決において，効率的な表現学習が重要視されており，性能向上に貢献する。
- SAT問題における表現学習は，問題の構造を捉えきれておらず，汎化性能が課題である。
- 最適化問題で学習済みの埋め込みをSAT問題へ転移させ，表現学習の有効性を検証する。
- 基礎最適化埋め込みは，SATインスタンスにおける構造的規則性を捉えることが示された。
- これにより，インスタンスのクラスタリングや分布識別といった教師なしタスクが実現可能となった。
- 最適化問題の埋め込みが，制約充足問題にも転移できる可能性が示唆された。
GraphQLify：自動化されたタイプ安全性を維持するGraphQL API導入 [cs.SE]目的：既存のREST APIからGraphQL APIへの移行
- クライアント・サーバ間の効率的な通信が重要であり，GraphQLはそのための有力な手段である。
- 既存のAPIをGraphQLに移行する際，タイプ安全性の維持とパフォーマンスの向上が課題となる。
- ソースコード解析による正確な型推論を用いて，タイプ安全性を保証するGraphQL APIの自動生成を目指す。
- GraphQLifyは，9つの人気オープンソースプロジェクトに含まれる834個のAPIを100%移行することに成功した。
- 既存のツールOASGraphと比較して，GraphQLifyはタイプミスマッチ率が大幅に低く，エラーが発生しない。
- 5回のAPI連続呼び出しにおいて，GraphQLifyを使用するクライアントは，RESTと比較してデータ取得時間を2倍から4倍短縮した。
準実行スタック：エージェント駆動型ソフトウェアエンジニアリングとSEの範囲拡大 [cs.SE, cs.AI]目的：準実行スタックという診断参照モデルの提示
- AI技術の進化により，ソフトウェアエンジニアリングのあり方が大きく変化しつつある。
- AIによる自動化が進む中で，ソフトウェアエンジニアの専門性が失われるのではないかという懸念がある。
- ソフトウェアエンジニアリングの対象を，コードだけでなく，より広範な要素を含むものとして捉え直す。
- ソフトウェアエンジニアリングは衰退するのではなく，その対象が実行可能なコードから，自然言語やワークフローを含む準実行可能な成果物へと拡大している。
- 準実行スタックモデルは，この拡大を理解し，ボトルネックや移行ポイントを特定するためのフレームワークを提供する。
- 既存のソフトウェアエンジニアリングプロセスを維持すべきか，簡素化・再設計すべきかの判断基準として，保存と浄化のヒューリスティックを提示する。
情報継承を用いた連鎖型軽量ニューラル予測器による可逆圧縮 [eess.SY, cs.SY, eess.SP, cs.IT, cs.LG, math.IT]目的：可逆データ圧縮のための確率推定
- データ圧縮は，情報伝送や保存において不可欠な技術であり，効率化が常に求められている。
- 従来の圧縮手法では，計算量と圧縮率のトレードオフが存在し，特に高効率な可逆圧縮は困難である。
- ニューラルネットワークを活用し，軽量かつ効率的な確率推定器を開発することで，この課題を解決する。
- 提案手法は，連鎖型ニューラル予測器アーキテクチャにより，確率推定に必要なパラメータ数を最小限に抑えることに成功した。
- 情報継承メカニズムの導入により，圧縮効率を向上させ，最先端のPAC圧縮機に匹敵する圧縮率を実現した。
- GPU上でのエンコード・デコード処理において，PAC圧縮機をそれぞれ1.2～6.3倍，2.8～12.3倍上回るスループットを達成した。
LLM4C2Rust：自動メモリ安全コード変換のための大規模言語モデル [cs.IR, cs.SE]目的：C/C++からRustへのコード変換
- ソフトウェアの安全性確保は重要であり，特にC/C++のようなメモリ安全でない言語で書かれたレガシーシステムにおいては不可欠である。
- 手動での変換は時間がかかりエラーが発生しやすく，ルールベースの自動化手法は柔軟性や費用対効果に課題がある。
- 大規模言語モデルを活用し，C/C++コードをメモリ安全なRustコードへ自動変換する手法を開発し，安全性向上を目指す。
- Retrieval-Augmented Generation（RAG）を活用したフレームワークにより，C/C++からRustへの変換精度とセキュリティが向上した。
- 実験の結果，Raw Pointer Dereferences（RPD）やUnsafe Type Casts（UTCs）が完全に解消されたCoreutilsプログラムも存在した。
- 大規模言語モデルベースの変換は，ソフトウェアの近代化，修正，およびメモリ安全なコード生成を促進する可能性を示唆する。
量子コンピューティングツールチェーンとアルゴリズムの実証的調査：Stack Overflowリポジトリのマイニング [cs.SE]目的：量子技術に関する開発者の議論の現状把握
- 量子コンピューティングが実用化段階に入り，開発者の関与状況の理解が重要になっている。
- 量子コンピューティング分野では，開発者のニーズや課題が十分に把握されていない。
- Stack Overflowの投稿分析を通じて，開発者の関心事や困難を明らかにすることを目指す。
- Stack Overflowの投稿分析により，7つの主要な議論トピックが特定された。
- ハイブリッド量子古典コンピューティングと量子回路の実装が最も活発に議論されていることがわかった。
- QiskitとQ#が開発者の議論を主導しており，GroverのアルゴリズムとShorのアルゴリズムが頻繁に参照されている。
検証済みライブラリ契約に基づく検証 [eess.SY, cs.SY, cs.PL, cs.LG, cs.LO, cs.SE]目的：検証済みライブラリ契約によるクライアントプログラムの検証
- 複雑なライブラリを利用するプログラムの検証自動化が求められている。
- ライブラリの振る舞いを正確に表現する契約の生成が困難である。
- クライアントプログラムが正当性を証明できる適切な契約を自動生成する。
- 本研究では，クライアントプログラムの正当性証明に必要なライブラリメソッドのモジュール契約を合成する。
- 文脈依存契約という新しい契約形式を提案し，古典的なモジュール契約よりも簡潔である。
- 制約ソルバーとテストエンジンを活用した，反例誘導学習フレームワークを実現した。
事前登録された信念修正契約 [cs.AI, cs.CL, cs.LO, cs.MA]目的：多主体系における信念修正の際の合意形成による誤った結論への収束を防ぐためのメカニズム
- 多主体系は複雑な問題を解決するために重要だが，合意形成が必ずしも正しい結論に繋がるとは限らない。
- 合意，自信，権威，多数決などが証拠として扱われ，誤った信念への高い確信度での収束を引き起こす可能性がある。
- 事前登録された信念修正契約によって，信念修正を厳格に管理し，誤った合意形成による問題解決を試みる。
- 事前登録された証拠トリガーと修正演算子を用いることで，社会的なラウンドのみでは自信が増加せず，誤ったカスケードが発生しないことが証明された。
- 検証可能なトリガープロトコルは，信念軌跡と監査トレースを保存するPBRC標準形を許容することが示された。
- 健全な強制によって，上位仮説の変化は具体的な検証済みの証拠セットに起因することが保証され，説明責任が確立される。
ドメイン特化型エージェントのための記号的ガードレール：有用性を損なわずに，より強力な安全性とセキュリティの保証 [cs.SE, cs.AI, cs.CR]目的：ドメイン特化型AIエージェントにおける安全性とセキュリティの保証
- AIエージェントは強力な応用を可能にするが，プライバシー侵害や金銭的損失などの重大な損害を引き起こす可能性がある。
- 既存の緩和策は信頼性を向上させるものの，保証を提供できないという課題がある。
- 記号的ガードレールを通じて，AIエージェントの安全性とセキュリティを確実に保証することを目指す。
- 既存の80件のベンチマーク分析の結果，85%は具体的なポリシーを持たず，高レベルな目標や常識に依存していることが判明した。
- 指定されたポリシー要件の74%は，多くの場合，単純かつ低コストなメカニズムを用いて，記号的ガードレールによって強制可能であることが示された。
- 記号的ガードレールは，安全性とセキュリティを向上させながら，エージェントの有用性を損なわないことが確認された。
編集距離を用いたパターンマッチングの通信複雑性に関する再検討 [cs.CL, cs.HC, cs.DS]目的：編集距離を用いたパターンマッチングの通信複雑性
- 文字列処理は，情報検索やバイオインフォマティクスなど，幅広い分野で基盤技術として重要である。
- パターンマッチングにおいて，大規模なテキストデータに対する効率的な検索が課題である。
- 通信量を最小限に抑えつつ，パターンマッチングを効率的に行うための理論的限界を明らかにすること。
- 本研究では，既存の下限との一致する，より改善された符号化サイズを導出した。
- 編集距離を用いたパターンマッチングの符号化サイズがO(n/m ・ k log(m|Σ|/k))であることを示した。
- この結果は，より単純なミスマッチを用いたパターンマッチングの通信複雑性と一致する。
逆誤差境界の合成 [cs.PL]目的：数値プログラムの逆誤差解析
- 数値計算の信頼性評価において，誤差の厳密な評価は不可欠である。
- 従来のツールは前方誤差解析に偏っており，逆誤差解析は未発達である。
- 自動化された逆誤差解析の枠組みを構築し，より広範なプログラムに対応すること。
- 逆誤差安定性の定義を一般化し，合成性と柔軟性を実現した。
- Shelという新しい圏を開発し，安定な数値プログラムの解析を支援する。
- 自動逆誤差解析ツールeggshelを実装し，従来困難だったプログラムへの応用を可能にした。
CodeMMR：自然言語，コード，画像をつなぐ統合検索 [cs.HC, cs.SE, cs.AI]目的：自然言語，コード，画像の統合検索モデルの提案
- 現代のソフトウェア開発において，コード検索は不可欠であり，LLMを活用したコーディング支援にも貢献する。
- 既存のコード検索モデルはテキスト中心であり，プログラムに含まれる視覚的・構造的な要素を考慮していない。
- 自然言語，コード，画像を統合的に扱える検索モデルを開発し，コード検索の精度向上を目指す。
- CodeMMRは，自然言語，コード，画像を共通の潜在空間に埋め込み，高い汎化性能を示す。
- 既存モデル（UniIR，GME，VLM2Vecなど）と比較して，nDCG@10で平均10ポイントの性能向上を達成した。
- CodeMMRをRAGに統合することで，コード生成の精度と視覚的な接地性が向上し，次世代の知的プログラミングシステムの可能性を示唆する。
閉包忠実度における演繹的情報源に対するレート歪み理論 [eess.SY, cs.SY, cs.IT, cs.LO, math.IT]目的：固定された演繹環境で生成される有限ステートメント情報源の可逆圧縮
- 知識表現と推論は，AIやデータベースシステムなど，様々な分野で重要な役割を果たす。
- 従来の圧縮理論は記号単位での等価性を重視するため，演繹的構造を考慮していない。
- 演繹的構造を保存する圧縮方法を理論的に確立し，通信の限界を定量化すること。
- 最小ゼロ歪みレートは，コアのソース質量とコア条件付きソースのエントロピーに等しいことが示された。
- 知識ベースの演繹的閉包に含まれる再構成アルファベットに対し，レート歪み関数はコアのみに依存することが証明された。
- 推論ステップ数に制限がある場合，レート遅延歪み特性評価が正確に得られる。
イザベルに打ち込むだけ！AIエージェントによるヒントからの定式化，機械化，一般化 [cs.LO, cs.AI, cs.PL]目的：ランク1多型ラムダ計算項に対する完全かつ最小な型注釈の生成
- プログラムの正確性を保証するため，型情報は不可欠である。再解析や型推論においても意味を保持する必要がある。
- 型注釈の手動生成は時間と労力がかかる。また，最小性という制約も加わるため，困難な課題である。
- AIエージェントを活用し，人間のヒントから型注釈を自動生成・洗練することで，定式化の効率化を目指す。
- 本研究では，型注釈問題に対する形式的な仕様と証明を提供し，イザベル/HOLで形式化を行った。
- 人間とLLM搭載AIエージェントがそれぞれ筆記による証明を作成し，AIエージェントが両方をイザベルに自動形式化することを実験的に示した。
- 人間のヒントを介したAI介入により，開発の洗練と一般化を促進できることを確認した。
LLMのための代数的invariantに基づく構造化アブダクション・演繹・帰納的推論 [cs.AI, cs.LG, cs.LO]目的：大規模言語モデルにおける構造化論理的推論の枠組み
- AIの信頼性向上には，論理的推論能力の強化が不可欠である。
- LLMは，仮説生成と検証を混同し，推論過程で誤りが累積しやすい。
- 論理的整合性を保証する推論プロトコルをLLMに実装し，推論の信頼性を向上させる。
- 本研究では，パースの三分割推論に基づいた記号的推論フレームワークを提案した。
- Gamma Quintetという5つの代数的invariantを用いて論理的整合性を強制し，特にWeakest Link boundによって推論の信頼性を保証する。
- 10万件以上のケースで検証を行い，今後の推論ベンチマークの基盤となる実装を提供した。
LEO衛星におけるチャネル予測を用いた適応的電力配分とユーザスケジューリング [cs.DC, cs.DC, cs.IT, eess.SP, math.IT]目的：LEO衛星システムにおけるユーザ間の公平性を確保するための適応的電力配分およびスケジューリング方式
- 地方や遠隔地への接続を実現する上で，LEO衛星は重要な技術である。地上や航空システムよりも広いエリアをカバー可能。
- LEO衛星通信では，衛星の高速移動により通信チャネルが急速に変化し，公平なリソース配分が困難である。
- 本研究は，チャネル変化に対応し，ユーザ間の公平性を保ちながら通信効率を向上させることを目指す。
- 提案手法APASSは，チャネル予測に基づき動的に電力配分とスケジューリングを行い，高い性能を発揮する。
- 完全な未来チャネル情報が存在する場合の上限に近く，予測誤差に対しても頑健性を示す。
- 等電力配分と比較して最小ユーザレートを2.98倍改善し，ジェインの公平性指数は0.99を大きく上回る。
発見と証明：Lean 4における難易度高自動定理証明のためのオープンソースエージェントフレームワーク [cs.AI, cs.CL, cs.LO]目的：難易度高自動定理証明のためのエージェントフレームワークの開発と評価
- 形式検証はソフトウェアやハードウェアの信頼性向上に不可欠であり，自動定理証明はその重要なツールである。
- 既存の自動定理証明ベンチマークは答えが埋め込まれており，人間の証明者とは異なる状況で評価されている。
- 本研究は，より現実的な「難易度高モード」ベンチマークとフレームワークを開発し，モデルの能力を正確に評価する。
- 新たに「MiniF2F-Hard」と「FIMO-Hard」という難易度高モードのベンチマークを公開し，専門家による再アノテーションを行った。
- LLMの自然言語推論と自己反省を組み合わせたエージェントフレームワーク「Discover And Prove (DAP)」を開発した。
- DAPはCombiBenchで解決問題を7から10へ，PutnamBenchで36定理の形式証明を初めて達成し，LLMと形式証明器の性能差を明らかにした。
QMutBench：量子回路変異体のデータセット [cs.SE, cs.DB]目的：量子回路変異体を含むデータセット
- 量子ソフトウェアの信頼性向上は重要であり，テスト技術開発が活発である。
- 既存のテスト技術の評価に必要な，故障を含むベンチマークデータセットが不足している。
- 量子ソフトウェアテスト技術の評価や比較，新たなテスト技術開発を支援する。
- QMutBenchは，70万以上の量子回路変異体を含むデータセットである。
- オンラインインターフェースを通じて，変異体の選択基準（元の回路，生存率，変異の種類）を指定できる。
- 本データセットは，量子ソフトウェア開発者やテスターがテストケースの品質評価や技術比較を行う上で有用である。
大規模システムにおける機能トグル動態：普及率，成長，寿命，およびベンチマーキング [cs.SE]目的：機能トグルの動態に関する定量分析
- ソフトウェア開発において，継続的なデリバリーと実験は重要であり，機能トグルはその実現に不可欠である。
- 機能トグルは本来一時的なものであるにも関わらず，技術的負債として残り続けることが多いという課題がある。
- 機能トグルのライフサイクルや管理方法を定量的に分析し，改善のためのベンチマークを提供する。
- KubernetesとGitLabの分析から，機能トグルの削除が追加に遅れ，トグル残高が増加していることが明らかになった。
- Kubernetesの機能トグルの寿命はGitLabのものよりも長く，組織やプロジェクトによって特徴が異なる。
- 機能トグルの管理状況を評価するためのベンチマークフレームワークを提案し，実用的な閾値を提示した。
量化ブール論理式のバックドア [cs.DS]目的：量化ブール論理式問題におけるバックドアサイズの複雑性
- 現代の問題解決にはSATソルバーへの還元が広く用いられており，PSpaceに属する問題への応用が期待される。
- QBFに対するバックドア分析はSATほど進んでおらず，効率的な解法が限られている。
- QBFのバックドアサイズに対する複雑性を解析し，より広範なクラスへの適用を目指す。
- QBFは，定数サイズのバックドアを持つ場合でもPSpace-hardであることが証明された。
- 2-SATとAFFINEクラスにおいては，量化子深度との組み合わせによるFPTアルゴリズムが設計された。
- 強化されたバックドアの概念を導入し，様々なQBFの実行可能クラスにおける検出と評価に対するFPTアルゴリズムが開発された。
小さくても構成可能：ソフトウェアにおけるヌル可変性の解明 [cs.SE]目的：小規模ソフトウェアシステムの構成可能性の程度
- 組み込みシステム等，小規模ソフトウェアは広く利用されている。
- 小規模ソフトウェアの構成可能性は未だ十分に探求されていない。
- 不必要な可変性を削減し，軽量なソフトウェア設計に貢献すること。
- GNU coreutilsの108プログラムの分析から，小規模プログラムでも最大76個のオプションが存在することが示された。
- 実行時の可変性とコードベースサイズの間には0.78という高い相関関係が見られた。
- 小規模プログラムにおける可変性は時間とともに増加する傾向にあり，コンパイル時の可変性の増加が主な要因である。
データ分析スクリプトの理解支援 [cs.HC, cs.CY, cs.SE]目的：データ分析スクリプトの理解と保守の改善
- データ分析は科学研究の根幹であり，その信頼性が重要である。
- データ分析スクリプトは複雑になりがちで，理解と再利用が困難である。
- スクリプト理解を支援するツールが不足しており，その解決が求められている。
- flowRは，R言語のデータ分析スクリプトを理解するためのIDE拡張である。
- 静的逆向きプログラムスライサーに加え，データフローグラフ，Lint機能，値注釈を提供する。
- リアルタイムに近いフィードバックを実現し，スクリプトの保守性と再現性を向上させる。
jMT: Javaメモリモデルの正当性検証 (拡張版) [cs.PL]目的：Javaメモリモデルの正当性検証ツール
- 並行処理プログラムの安全性確保は重要であり，メモリモデルはその基盤となる。
- Javaメモリモデルは複雑であり，修正のたびに予期せぬ振る舞いが生じる。
- 既存のJavaメモリモデルの妥当性評価と新しいモデルの提案を支援する。
- jMTは，単一実行モデルに基づいて多実行意味論を構築する新しいツールである。
- jMTを用いることで，Javaメモリモデルの提案をプログラムごとに評価できる。
- 169の litmus テストを用いた評価により，既存のJavaメモリモデルに関する洞察が得られた。
ファジー充足可能性問題の混合整数非線形計画法による解決 [cs.LO]目的：ファジー論理における充足可能性問題の解決
- ファジー論理は，不確実性や曖昧さを扱う上で重要であり，様々な応用分野が存在する。
- ファジー論理の充足可能性問題は，ブール論理と比較して研究が遅れており，効率的なソルバーが不足している。
- ファジー論理の様々な形式に対応できる，新しい充足可能性問題ソルバーを開発し，その性能を評価すること。
- 本研究では，混合整数非線形計画法（MINLP）ソルバーを用いた新しいファジーSATソルバーSATFuLを提案した。
- 実験の結果，SATFuLはルカシェヴィッチ論理において最先端のソルバーと同等の性能を示し，積論理においては既存ソルバーを上回る性能を示した。
- 本手法は健全性と完全性を有し，新たなファジー演算子への拡張も容易である。
ニューロシンボリックなリポジトリレベルのコード局所化 [cs.SE, cs.AI]目的：キーワードに依存しない論理的なコード局所化の課題とその解決策
- ソフトウェアの自動化において，コード局所化は不可欠な要素であり，その重要性は高まっている。
- 既存のコード局所化手法は，キーワードに過度に依存する傾向があり，構造的な推論が不十分である。
- 構造的な推論能力を必要とする新しいベンチマークを提示し，その上でより正確なコード局所化を実現する。
- 既存の最先端手法は，キーワードに依存しないベンチマークにおいて性能が大幅に低下することが示された。
- 提案手法LogicLocは，Datalogと大規模言語モデルを組み合わせ，正確かつ検証可能なコード局所化を可能にする。
- LogicLocは，新しいベンチマークで優れた性能を示し，トークン消費量と実行時間を大幅に削減した。
有限ピンホイールスケジューリング変種の困難度，計算可能性，および密度閾値 [cs.DS]目的：有限ピンホイールスケジューリングの変種における困難度，計算可能性，および密度閾値の決定
- タスクスケジューリングは，計算資源の効率的な利用において重要であり，様々な応用分野で不可欠である。
- ピンホイールスケジューリング問題はNP困難であり，実用的な規模の問題を効率的に解くことが難しい。
- 本研究は，有限ピンホイールスケジューリング変種の計算困難度を明らかにし，密度閾値の評価を行うことで，問題解決に貢献する。
- 2-Visits問題は，最大マルチプリシティが2であっても強NP困難であることが証明された。
- 異なる期限数が定数であれば，2-Visits問題はRPに属することが示された。
- k-Visits問題の密度閾値の下限が$\sqrt{2}-1/2\approx 0.9142$であることが示され，kが大きくなるにつれて5/6に近づくことが証明された。
異種システム向け統一プログラミングモデルとしてのSYCLの評価 [cs.DC, cs.PL]目的：異種システムにおけるSYCLの有効性に関する評価
- 高性能計算の分野では，多様なアーキテクチャを効率的に活用することが重要であり，そのためのプログラミングモデルの進化が求められている。
- 異種環境向けのプログラミングは複雑であり，コードの移植性や開発効率が課題となっている。
- SYCLのクロスプラットフォーム性，開発生産性，実行効率を評価し，その課題と改善点を示す。
- SYCLは，コードの移植性，開発生産性，実行効率において，必ずしも期待される結果が得られていないことが示された。
- SYCLの実装間には一貫性のない部分があり，信頼性やクロスプラットフォームの可用性の向上には改善が必要である。
- Unified Shared Memory (USM)とbuffer-accessor，NDRangeと階層型カーネルモデルの比較から，SYCLのメモリ管理と並列処理に関する課題が明らかになった。
鞍点法による短パケット伝送のための疎VLSF符号の最適化 [cs.IT, math.IT]目的：疎可変長停止フィードバック（VLSF）符号の最適化
- 無線通信において，信頼性と効率を両立する符号化技術が不可欠である。
- VLSF符号の性能は，復号構成パラメータに大きく依存するが，その最適化は困難である。
- 鞍点近似を用いて，VLSF符号の復号構成パラメータを効率的に最適化すること。
- 鞍点近似に基づく最適化フレームワークにより，低コストでほぼ最適な復号構成が得られる。
- 提案する改良された復号規則は，従来の固定閾値規則よりもタイトな到達可能性限界を示す。
- 本研究により，固定閾値復号規則の制限性が明らかになり，到達可能性限界の更なるタイト化が可能となる。
LLMSniffer：GraphCodeBERTと教師あり対照学習によるLLM生成コードの検出 [cs.SE, cs.CL]目的：LLM生成コードと人間が書いたコードの識別
- ソフトウェア開発におけるLLMの活用が拡大しており，コードの出所を特定することは重要である。
- LLM生成コードと人間が書いたコードを区別することが困難であり，品質保証やセキュリティ上の懸念がある。
- GraphCodeBERTと対照学習を用いた，より高精度なLLM生成コード検出手法を開発する。
- LLMSnifferは，GPTSnifferデータセットで精度を70%から78%に，F1スコアを68%から78%に向上させた。
- Whodunitデータセットにおいても，精度を91%から94.65%に，F1スコアを91%から94.64%に向上させた。
- 対照学習により，特徴表現が分離され，よりコンパクトに表現されることがt-SNEによる可視化で確認された。
二重制約付き公平k-中心点，k-中央値，k-平均クラスタリングに対する定数因子近似 [cs.DS, cs.CY, cs.LG]目的：二重制約付き公平クラスタリング問題における近似アルゴリズムの開発
- 機械学習における公平性の重要性が増しており，特にセンシティブな属性に基づく不公平の解消が求められている。
- 既存手法では，公平性の制約を満たすために近似率が低下する，あるいは制約違反が生じる問題があった。
- グループ公平性と多様な中心選択という二つの制約を同時に満たす，より効率的な近似アルゴリズムを提案する。
- k-中心点問題において，既存の8-近似を改善し，4-近似を達成した。少量の加法的なグループ公平性制約違反を伴う。
- k-中央値およびk-平均問題に対し，初の定数因子近似アルゴリズムを提案した。
- 提案手法は，マトロイドk-クラスタリングやナップサック制約など，他の中心選択制約にも一般化可能である。
相関のある非コヒーレントフェージングチャネルにおける信頼性保証付きVLSF復号 [cs.IT, math.IT]目的：相関のある非コヒーレントフェージングチャネルにおける可変長ストップフィードバック(VLSF)符号の信頼性保証付き復号
- 無線通信において，信頼性の高い情報伝送は不可欠であり，フェージングチャネルにおける性能向上が重要である。
- 従来の復号手法では，チャネルの相関やフェージングの影響を正確に考慮することが難しく，信頼性の評価が困難である。
- 本研究は，フェージングチャネルにおけるVLSF復号の信頼性を保証するための，厳密な上限・下限を導出することを目指す。
- VLSF復号のための情報密度進化に基づく復号規則を提案し，チャネルメモリを考慮した情報密度の厳密な評価を困難にしている問題を解決する。
- 時間軸に沿って一様に成立する情報密度の有限ブロック長の下限と上限を導出し，ストップタイム分析を可能にするとともに，緩和ギャップを特徴付けた。
- ガウス・マルコフフェージングチャネルの数値評価により，ストップタイム分布とフェージング相関が復号性能に及ぼす影響を明らかにした。
線形システムソルバーにおける後方誤差の普遍的収束に向けて [cs.CG, cs.SI, math.NA, cs.DS, cs.LG, cs.NA, math.OC]目的：線形システムソルバーの後方誤差の普遍的収束
- 数値線形代数において，効率的な線形システムの解法は重要であり，計算コスト削減に繋がる。
- 既存手法は条件数に依存し，安定した収束が保証されない場合がある。
- 条件数に依存しない，普遍的な収束性を持つ解法の確立を目指す。
- リチャードソン反復法が正定値線形システムに対し，反復回数$k$で最大$1/k$の後方誤差に収束することを示した。
- この結果から，正定値線形システムを$\epsilon$の後方誤差で解くアルゴリズムが$O(n^2/\epsilon)$の計算量で実現できる。
- MINBERRというアルゴリズムを開発し，$O(n^2/\sqrt\epsilon)$の計算量でより高速な収束を実現した。
テンソル符号の復号アルゴリズム [cs.IT, math.IT]目的：テンソル符号の特性および様々な距離空間における復号手法
- テンソル符号は行列符号の一般化であり，近年，情報理論や符号理論における応用が期待されている。
- 既存の復号アルゴリズムは，復号半径に対して指数的な複雑度を持つ場合があり，効率的な復号が課題となっている。
- テンソル構造を利用した新たな復号手法を開発し，より効率的な復号を実現することを目指す。
- テンソル符号の各ファイバーをガブドゥーリン符号とみなし，ファイバーごとの復号アプローチを検討した。
- ロイドロー・オーバーベックの復号法を一般化し，スライス空間とファイバー空間の次元によって制限されるエラーを訂正可能とした。
- 提案手法は，テンソルランク重みエラーに対する復号も可能であり，幅広いエラーモデルに対応できる。
遅延を考慮した高速かつメモリ効率の良いマルチモーダル経路計画 [cs.DS]目的：遅延を考慮したマルチモーダル経路計画の高速化とメモリ効率の向上
- 都市交通の円滑化に不可欠であり，効率的な経路計画が求められている。
- 既存手法では，計算量が多く，メモリ消費量が課題となっている。
- 計算速度とメモリ使用量を改善し，より正確な経路計画を実現する。
- 単一条件検索において，既存アルゴリズムと比較して1.9～4.2倍の高速化を達成した。
- 複数条件設定においては，競争力のある高速化と高い精度を実現した。
- 遅延の増加に伴い，本手法の拡張性が高いことが確認された。
QBFギャラリー2023 [cs.LO]目的：量化ブール論理式(QBF)ソルバーの性能評価
- 組合せ最適化など，様々な分野で重要な役割を果たす論理問題解決の基盤技術である。
- QBFソルバーの性能向上は進んでいるものの，大規模問題や複雑な構造を持つ問題への対応が課題である。
- 最新のQBFソルバーの性能を比較し，ベンチマーク問題の現状を把握することで，今後の研究方向性を示す。
- QBFギャラリー2023に参加したソルバーと，新たに開発されたベンチマーク問題をまとめた。
- これらを統合したベンチマークセットを用いて，ソルバーの性能比較分析を実施した。
- QBFギャラリーの現状と将来の展望について議論し，コミュニティへの貢献を目指す。
ユーザ意図とLLMの乖離を埋める：コード生成のための要件整合アプローチ [cs.SE]目的：コード生成における要件の整合性向上
- コード生成は，ソフトウェア開発の効率化に不可欠であり，自動化の重要な要素である。
- LLMは能力が高いものの，与えられた要件を正確に理解できない場合がある。
- LLMが要件を正しく理解できない場合の性能低下を改善すること。
- REA-Coderは，LLMと要件のずれを特定し，要件を整合させることで，コード生成性能を向上させる。
- 4つのLLMと5つのプログラミングベンチマークにおいて，既存手法を上回る性能を示した。
- 5つのベンチマークデータセットで，平均7.93%～30.25%の性能改善を達成した。
論文から進歩へ：ソフトウェア工学における知識の蓄積の再考 [cs.SE]目的：ソフトウェア工学における知識の蓄積，統合，再利用に関する課題の理解
- ソフトウェア工学は急速に発展しており，その進歩は社会に不可欠である。
- 研究成果の増加に反し，知識の体系的な蓄積が十分でないという課題がある。
- 研究成果の知識構造とインセンティブ構造の改善を目指す。
- 調査の結果，研究生産性の向上と結果の統合・追跡メカニズムの不足との間に緊張関係が認められた。
- 論文が独立した知識単位として機能し，文脈や起源が失われることが構造的な問題として指摘された。
- 主張と証拠の構造化，方法論的決定の文書化，長期的な基盤の確立，インセンティブの再設計が提案された。
CSP学習を支援する対話型エージェントの調査 [eess.SY, cs.SY, cs.HC, cs.SE]目的：高校におけるCSP学習支援のための対話型エージェントの可能性
- 情報科学教育において，生徒の自律学習を促すことは重要である。
- 適切な学習リソースの探索が困難であり，生徒の学習効率を阻害する。
- 対話型エージェントを活用し，生徒の学習課題に応じた情報提供を目指す。
- 一般的な生成型対話エージェントと，CSP専用の応答型対話エージェントの効果を比較した。
- 45名の高校生を対象とした教室での実験により，両者の学習支援効果とエンゲージメントを評価した。
- 対話型エージェントがCSP学習における情報探索を支援する可能性が示唆された。
直交配列の分類のための同型性枝刈り法による分枝限定法の並列化 [cs.DS, math.CO]目的：直交配列の分類
- 組合せ最適化問題の分野において，効率的な探索アルゴリズムは不可欠である。
- 大規模な組合せ問題では，計算量が指数的に増加し，現実的な時間で解くのが困難である。
- 分枝限定法を並列化することで，計算時間の短縮とより大規模な問題への適用を目指す。
- マルゴットの同型性枝刈り法による分枝限定法を並列化する手法を提案した。
- OA(128, 9, 2, 4)とOA(144, 9, 2, 4)の分類において，線形的な高速化が確認された。
- OA(192, k, 2, 4) (k = 9, 10, 11)のすべての非OD同値な直交配列を初めて分類できた。
グローバル拡散を伴わない量子探索 [quant-ph, cs.DS]目的：量子探索における効率的な探索手法の確立
- 量子計算は，古典計算では困難な問題を解決する可能性を秘めており，その基盤技術として重要である。
- 従来の量子探索アルゴリズムは，グローバルな拡散演算子に依存しており，大規模な量子コンピュータでの実装が課題となっていた。
- グローバル拡散演算子を必要としない，より効率的な量子探索アルゴリズムを開発し，量子計算の応用範囲を広げる。
- 本研究では，グローバルな演算子がオラクルのみである場合でも，量子探索の二次加速を維持できることを示した。
- 特に，初期状態とターゲット状態がテンソル積として分解できる場合に，アルゴリズムのダイナミクスを正確に解析できる再帰的構築を提案した。
- 非構造化探索においては，パーティションごとに少なくともlog₂(log₂N) qubitsを含む場合，Grover探索と同等のオラクル複雑度を維持しつつ，回路深度を大幅に削減できる。
複雑性制約下におけるアクセス可能な量子相関 [quant-ph, cs.CC, cs.IT, math.IT]目的：計算資源に制約のある観測者にとってアクセス不可能な量子系の相関
- 量子情報科学は，古典情報科学の限界を超えた情報処理の可能性を追求する分野である。
- 量子相関の全てが，現実的な計算能力で利用可能とは限らない点が課題である。
- 計算資源の制約下でアクセス可能な量子相関を定量的に評価すること。
- 効率的に実装可能な量子チャネルを用いることで，複雑性制約下での最大ダイバージェンスと計算最小エントロピーを定義した。
- 計算最小エントロピーは，効率的な操作で得られる最大エンタングルメントと，推測確率を定量化する。
- 情報理論的な最小エントロピーと複雑性制約下での最小エントロピーの間には明確な分離が存在し，計算制約が観測可能な量子相関を制限する。
- 1
- 2