arXiv雑要約

• Top
• AI
• プログラム
• 画像・音声
• セキュリティ
• 数値解析

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

• MLスキップ：軽量メタデータによるMLフィルタのデータスキップ [cs.RO, cs.DB, cs.LG, cs.LO]目的：MLフィルタのためのデータスキップ技術

  • データベースにおけるAI機能活用が重要視される中，MLモデルのコストが課題となっている。
  • 従来のデータスキップ技術は，AI関数を用いたフィルタには適用困難である。
  • Parquetのメタデータを用いて，MLフィルタにおけるデータスキップを可能にすること。
  • ReLUアーキテクチャを用いた予備実験により，0.1%以下の選択率のフィルタで平均27.4%の削減効果が確認された。
  • 2次元凸包を用いたメタデータ構造を提案し，削減効果を38.31%に向上させた。データサイズは行グループあたり45バイト以内。
  • DuckDB環境において，PyTorchと比較して1.07倍の高速化を達成した。

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

• 圧縮された単語に対するランク付きMSO列挙 [cs.DS, cs.DB, cs.LO]目的：固定されたMSOクエリに対するランク付きクエリ列挙問題

  • 文字列処理における効率的なクエリ処理は，データ圧縮技術と密接に関連する。
  • 圧縮されたデータに対するクエリ列挙は，一般的に未解決の問題である。
  • 文法圧縮されたデータに対するランク付きクエリ列挙を可能にすること。
  • 固定されたMSOクエリについて，文法圧縮された文字列上で線形な前処理と定数時間でのランク付きクエリ列挙が可能であることが示された。
  • 多項式時間で定義される関数fと，サイズnの文法圧縮された単語wに対して，f(w)の記号を左から右へ定数時間で列挙できる。
  • この結果の証明は，文法圧縮設定にも適用可能な因数分解木に基づいている。

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

• 平面グラフにおける完全マッチング数の計算は決定式と同じ難易度である [cs.CC, cs.DM, cs.DS]目的：平面グラフにおける完全マッチング数の計算複雑性

  • 組み合わせ最適化問題への応用が期待され，物理学や数学における重要な問題である。
  • 完全マッチング数の効率的な計算方法が確立されておらず，計算量が多くなりがちである。
  • 平面グラフにおける完全マッチング数の計算下界を示すことで，既存アルゴリズムの最適性を証明する。
  • 平面グラフにおけるエッジ重み付き完全マッチング数の計算量は，少なくともO(n^(ω/2-ε))となることが示された。
  • これは，Yusterのアルゴリズムが最適な計算量を達成していることを意味する。
  • 本研究は，決定式問題と同程度の計算困難性を持つことを示した。

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

• グロテンディーク定数はπ/(2 log(1+√2)) - 10⁻⁵ より小さい [cs.DS]目的：グロテンディーク定数の上限値

  • 関数解析における重要な定数であり，多様な数学的課題に影響を与える。
  • グロテンディーク定数の正確な値を求めることは長年の未解決問題である。
  • 既存の上限を更新し，より厳密なグロテンディーク定数の評価を提供する。
  • グロテンディーク定数 K_G が $\frac{\pi}{2 \log (1+ \sqrt{2})} - 10^{-5}$ より小さいことを証明した。
  • これは，Bravermanらの先行研究における結果を改善するものである。

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

• クバー表現のギャップについて [cond-mat.dis-nn, cond-mat.str-el, cs.CC, quant-ph, math.OC, cs.DS, math.AG, math.RT]目的：クバー表現におけるギャップの評価

  • 不変量理論の計算において，軌道閉包が原点を含むかの判定は基礎的な問題である。
  • 自己随伴群における計算量の指標となるギャップの評価は未解決の問題が多い。
  • 特殊線形群作用下のクバー表現におけるギャップの性質を明らかにする。
  • タイプA，ハットA，および一様次元ベクトルを持つ木型クバーに対し，ギャップの逆数が頂点数と最大次元の多項式で抑えられることが示された。
  • これにより，B\"urgisserらのアルゴリズムがこれらのクバーに対して多項式時間でnullconeメンバーシップ問題を解くことが可能になった。
  • 一方，葉の数に対して指数関数的に小さいギャップを持つクバーや，頂点数に対して指数関数的に小さいweight marginを持つ次元ベクトルが存在することが示された。

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

• 二進自己双対符号からのConstruction-A格子に対する主要化とガウス質量最大性 [math.NT, cs.IT, math.CO, math.IT, math.MG]目的：二進自己双対符号から構成されるConstruction-A格子のガウス質量最大化の証明

  • 格子は符号理論，暗号理論，多変量解析など，幅広い分野で重要な役割を果たす。
  • 格子構造のガウス質量は格子の性能に影響するため，その最大化は重要な課題である。
  • 特定の格子のガウス質量が最大となることを証明し，その性能評価に貢献する。
  • RegevとStephens-Davidowitzの予想が，二進自己双対符号由来のユニモジュラーConstruction-A格子に対して証明された。
  • 符号の半重み分布が二項分布によって支配されることが示され，ガウス質量ギャップに関する二乗和の公式が得られた。
  • 系統形$[I\mid A]$における自己双対性から，重み分布の等質性が示され，凸順序支配が導かれた。

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

• 自己回帰サンプリング集合の安定性解析 [eess.SP, cs.IT, math.IT]目的：AR(1)ジッター付きサンプリング集合の密度と安定性に関する性質

  • ADCにおけるクロックジッタの確率的モデル化が重要視されているため
  • 既存手法では，サンプリング集合の安定性を保証できない場合がある
  • AR(1)ジッターの影響下でのサンプリング集合の安定性を評価する
  • AR(1)ジッター付きサンプリング集合は，漸近的な密度は正しいものの，安定なサンプリング集合とならないことが示された
  • 一方，有限次元解析の結果，対応するジッター付きsinc行列は高い確率で良好な条件数を持つことが示された

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

• 一般的な過程に対する主要化測度定理に関する注記 [math.PR, cs.IT, math.IT, math.ST, stat.TH]目的：広範な確率ベクトルに対する主要化測度定理の下限の成立

  • 確率過程の理論は，統計学，機械学習，物理学など幅広い分野で基礎となる。
  • 主要化測度定理の適用範囲が限られており，より一般的な確率ベクトルへの拡張が課題となっていた。
  • 確率ベクトルのKLダイバージェンスの性質を利用し，主要化測度定理の下限を導出することで，適用範囲を拡大する。
  • KLダイバージェンスの特性値$C_{\mathrm{KL}}(\mu)$が有限である場合，ある集合$T$上で$\sup_{t \in T} \langle X, t \rangle$の期待値に下限が成立する。
  • この結果は，中心化されたガウス過程に対する主要化測度定理の下限を包含する特殊な場合として得られる。
  • 議論の鍵となるのは，最近J. Liuによって導入されたレート歪み積分である。

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

• 複数サブモジュラー目的関数のアルゴリズム的公平性最大化と制約付き公平分割への示唆 [cs.CL, cs.DC, cs.DS, cs.GT, math.OC]目的：複数エージェントにおけるサブモジュラー目的関数の制約付き最大化

  • 組合せ最適化における重要な問題であり，現実世界の資源配分に応用可能である。
  • エージェント間の公平性を考慮した資源配分は，既存手法では困難である。
  • 公平性を担保しつつ，各エージェントの目的関数を最大化する手法を提案する。
  • ラウンドロビン方式を用いることで，制約下のエージェントは，モノトーンおよび非モノトーンな目的関数において堅牢な性能保証が得られる。
  • 特にモノトーンな目的関数においては，エージェントは最適な価値の1/(n+p_i)を達成し，競争の影響が小さい場合，1/Θ(p_i)の近似率で最適解に近づく。
  • 提案手法は，近似的な実現可能羨望フリー（FEF1, FEFu）割り当てを生成し，制約付きサブモジュラーエージェントに対する可能な最大化シェア（FMMS）保証も提供する。

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

• Elixir の型システム：ガード分析と安全な型消去による段階的型付け [cs.PL, cs.LO]目的：Elixir言語のための型システムの形式化

  • 動的型付け言語の安全性と効率性を高める型システムの需要が高まっている
  • 既存の型システムでは，静的解析の精度や実用性に課題がある
  • Elixir言語への型システムの統合を理論的に確立し，実用性を検証する
  • 本研究では，ガード分析と安全な型消去を組み合わせた新しい型システムを提案した
  • これにより，コンパイルパイプラインやランタイムを変更することなく，正確で健全な静的型解析が可能となる
  • 提案手法は，大規模な産業用コードベースにおける有効性が示された

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

• ニューラルネットワークによる可測測度の生成 [cs.LG, cs.IT, math.IT, math.PR, math.ST, stat.ML, stat.TH]目的：m-可測測度の近似

  • 測度論は，確率論や偏微分方程式など，数学の様々な分野の基礎をなす重要な研究領域である。
  • 高次元空間における複雑な測度の近似は，計算コストが高く，効率的な手法が求められている。
  • ReLUニューラルネットワークを用いて，m-可測測度を効率的に近似する手法を確立すること。
  • ReLUニューラルネットワークを用いることで，m-可測測度をWasserstein距離において任意に小さな誤差で近似できることが示された。
  • ネットワークの重みは量子化され，かつ有界であり，近似誤差εに対する必要なネットワーク数は$2^{b(\varepsilon)}$以下である。
  • 近似のレート$b(\varepsilon)$は，rectifiabilityパラメータmに依存し，周囲の次元よりも小さくなる可能性がある。

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

• スプラインスケッチ：誤差保証付きのより正確な分位点 [cs.DS, cs.DB, stat.CO]目的：大規模データセットにおける分位点推定の精度向上

  • データ監視や分析において，大規模データの分位点推定は不可欠な処理である。
  • 既存手法には，t-digestのように最悪ケースでの誤差が理論的に保証されないものがある。
  • 理論的保証と実用性の両立を目指し，より高精度な分位点推定手法を開発する。
  • 新しい分位点要約であるSplineSketchは，均一に有界なランク誤差の理論的保証を提供する。
  • 合成データおよび実データを用いた実験で，t-digestと比較して2〜20倍の性能向上を達成した。
  • 入力範囲の動的な分割と単調三次スプライン補間を組み合わせることで，空間効率と最悪ケース保証を両立している。

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

• 一般化されたフーリエ表現によるDNF学習 [cs.DS, cs.IT, cs.LG, math.IT]目的：DNF学習における一般化されたフーリエ表現

  • ブール関数学習は，機械学習の基礎であり，複雑な関数を効率的に近似・学習する方法を追求する。
  • 従来のフーリエ表現は，積分布に限定され，より広範な分布への適用が困難であった。
  • 積分布以外の分布下でのDNF学習を可能とする一般化された表現を確立すること。
  • 一般化されたフーリエ表現を導入し，ベイズネットワークを用いて任意の分布を表現可能となった。
  • 差制約付き木構造のベイズネットワークにおいて，連言の$L_1$スペクトルノルムが有界であることが証明された。
  • この結果を利用し，このような分布下におけるDNFおよび決定木の学習可能性が確立された。

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

• 浮動小数点プログラムに対する多項式不変量生成 [cs.PL]目的：浮動小数点プログラムの不変量生成

  • 数値計算において，浮動小数点演算の誤差は避けられない。その誤差の蓄積は，プログラムの重大な失敗につながる可能性がある。
  • 浮動小数点数の丸め誤差を考慮したプログラムの正当性検証は困難である。既存手法では精度と効率性の両立が課題である。
  • 丸め誤差の影響下における，より厳密な不変量生成手法を確立し，プログラムの信頼性を向上させる。
  • 本研究では，多項式制約ソルビングと丸め誤差解析を組み合わせた新しいフレームワークを提案する。
  • このフレームワークは，既存の最先端手法と比較して，計算時間と生成された不変量の精度において優れていることが実験的に示された。
  • 丸め誤差変数の数を削減し，浮動小数点モデルの取り扱いコストを削減することに成功した。

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

• サステナビリティを意識したIoT強化型ビジネスプロセスの概念モデルと方法論 [eess.SY, cs.SY, cs.CL, cs.CL, cs.SE, cs.CY]目的：IoTによるビジネスプロセスのサステナビリティ測定と改善の可能性分析

  • ビジネスプロセスは企業活動の根幹であり，その効率化は競争力向上に不可欠である。
  • サステナビリティ研究は環境問題に偏りがちで，社会・経済的側面への包括的なアプローチが不足している。
  • IoTを活用し，環境・社会・経済の3側面からビジネスプロセスのサステナビリティを体系的に評価・改善する。
  • 本研究では，ビジネスプロセスとIoTの関係性を形式的に表現する概念モデルを提案した。
  • 提案手法は既存ビジネスプロセスの分析，改善機会の特定，そしてサステナビリティを考慮したIoT強化型ビジネスプロセスの実装を支援する。
  • 観光分野と医療分野における事例研究を通して，本手法の実用性と有効性を示した。

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

• RIS支援システムにおける符号化妨害による安全通信 [cs.IT, math.IT]目的：RISと符号化妨害を統合したフレームワークによる秘匿率最大化

  • 無線通信の安全性を確保することは，情報漏洩を防ぎ，プライバシーを保護する上で重要である。
  • 従来の協調妨害は受信性能を低下させる可能性があり，符号化妨害の優位性はチャネルに依存する。
  • RISと符号化妨害を組み合わせることで，空間的なボトルネックを克服し，安全通信を向上させる。
  • 符号化妨害とガウスノイズの関係を理論的に解明し，符号化妨害の性能が制限される空間チャネル条件を特定した。
  • RIS要素数が多くなるにつれて，符号化妨害がガウスノイズよりも優位になる条件を解析的に導出した。
  • WMMSEフレームワークに基づく低複雑度アルゴリズムにより，RISと送信プレコーディングを共同最適化し，シミュレーションで有効性を確認した。

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

• SAIL：LLMを用いた音響的抽象解釈器 [cs.PL, cs.LG]目的：プログラムの振る舞いを安全に近似するための，グローバルに健全な抽象解釈器の構築

  • 抽象解釈は，プログラムの安全性や信頼性を保証する上で不可欠な技術である。
  • 抽象解釈器の構築は手作業に頼る部分が多く，時間と労力がかかる。
  • LLMを活用することで，抽象解釈器の自動構築を実現し，その効率化を目指す。
  • 本研究で開発したSAILは，既存の手動設計による抽象変換器と同等の性能を示すことが確認された。
  • SAILは，複雑な非線形演算子に対して，文献には存在しない，健全かつ高精度な抽象変換器を合成することに成功した。
  • この結果は，LLMが抽象解釈器の自動構築において有効であることを示唆する。

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

• 自己対戦型SWE-RLによる超知能ソフトウェアエージェントの育成に向けて [cs.RO, cs.CG, cs.SE, cs.AI, cs.CL, cs.LG]目的：超知能ソフトウェアエージェント育成のためのパラダイム

  • ソフトウェア開発の自動化は，生産性向上や新たな価値創造に不可欠である。
  • 既存手法は人間による知識やキュレーションに依存し，超知能化の障壁となっている。
  • 人間介入なしに，ソフトウェアリポジトリから自律的に学習する道筋を示す。
  • 自己対戦型SWE-RL（SSR）は，人間が作成したデータに頼らず，ソフトウェアのバグ注入と修正を繰り返すことで自己改善を実現した。
  • SWE-bench VerifiedとSWE-Bench Proのベンチマークにおいて，SSRは人間データベースラインを上回り，性能が向上した（+10.4点，+7.8点）。
  • この初期結果は，エージェントが実世界のソフトウェアから自律的に学習し，人間の能力を超える可能性を示唆している。

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

• 拡散モデルによる生成スペクトルマッピング：統合再構成と能動センシング [cs.RO, cs.IT, eess.SP, math.IT]目的：スペクトルマッピングのための統一的な再構成と能動センシング手法

  • 電波スペクトルの正確なマッピングは，電波監視や無線環境の把握に不可欠である。
  • 特に衛星による広域センシングでは，測定データが疎でノイズが多く，量子化ビット数も少ないという課題がある。
  • 本研究は，限られたセンシング予算内で，不完全な測定からの高精度な再構成と効率的なセンシングリソースの割り当てを解決する。
  • 提案手法GSCは，拡散モデルを用いたベイズの逆問題としてスペクトルマップの回復を定式化し，線形および量子化された測定モデルに対して閉形式の事後平均更新を導出した。
  • GSCは，コストのかかる尤度勾配誘導なしに，測定に整合した事後サンプリングを可能にし，空間的不確実性の推定と能動センシングのための追加測定位置の多様性に基づいた選択を支援する。
  • シミュレーション実験の結果，GSCは，疎，ノイズが多く，低ビット量子化された測定条件下で，既存手法よりも高いPSNRと低いLPIPS，およびより効率的なセンシングを達成した。

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

• Aletheia：コード検証器におけるRLVRの動作原理 [cs.SE, cs.AI]目的：コード検証器の訓練レシピの性能とコストのトレードオフに関する分析

  • 大規模コード生成モデルの性能向上には，訓練後の検証が不可欠であり，その自動化が求められている。
  • RLVRは有効だが，その実装コストが高く，コード生成への応用が遅れている。
  • より効率的なRLVR訓練レシピを特定し，コード検証器の導入を促進すること。
  • 検証器の規模に応じて最適な訓練レシピが異なり，小規模な検証器ではオンポリシー学習が主要な性能向上要因となる。
  • 大規模な検証器では，思考予算が最も重要な要素となり，負例学習は規模に応じてランキング再構成への貢献度が単調に増加する。
  • 大規模モデルでは，オンポリシー学習を排除することで，フルRLVRと同等の性能を達成でき，計算効率の良い戦略となる。

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

• 名前は重要ではない：オープン語彙学習のための記号不変Transformer [cs.LG, cs.LO, cs.SC]目的：オープン語彙学習における記号不変性

  • 自然言語処理において，語彙の拡張性と汎化性能は重要な課題である。
  • 既存のモデルは，意味的に等価な記号の区別が難しく，未知の記号への対応が苦手である。
  • 記号の置換に対して不変なTransformer機構を開発し，汎化性能を向上させる。
  • 提案手法は，記号の置換に対して理論的に不変性を保証する。
  • 複数の埋め込みストリームと集約された注意機構により，記号不変性を実現している。
  • 実験結果は，未知の記号への汎化性能が向上することを示した。

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

• CodeHacker：競技プログラミング解答の脆弱性を検出する自動テストケース生成 [cs.SE, cs.AI, cs.CR]目的：競技プログラミング解答における脆弱性検出のための自動テストケース生成

  • コード生成におけるLLMの評価は，テストケースの質が重要であり，その信頼性が問われている。
  • 既存のベンチマークは微妙なコーナーケースの網羅性が低く，誤った解答が通過することがある。
  • 潜在的な脆弱性を露呈させる，標的を絞った敵対的テストケースを自動生成し，解答の精度向上を目指す。
  • CodeHackerは，既存のデータセットの真陰性率(TNR)を大幅に向上させ，以前は合格していた誤った解答を効果的に排除する。
  • 敵対的テストケースは，LiveCodeBenchのようなベンチマークにおいて，RLモデルの性能を向上させるための優れた訓練データとなる。
  • CodeHackerは，競技プログラミングにおけるハックメカニズムを模倣し，ストレステスト，アンチハッシュ攻撃，ロジック固有のターゲットなどの多戦略アプローチを用いる。

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

• WaterSIC：情報理論的に（ほぼ）最適な線形層量子化 [cs.LG, cs.IT, math.IT]目的：線形層の低精度化における圧縮率と出力誤差のトレードオフに関する研究

  • 大規模言語モデルの効率化は，計算資源の制約や実用化における重要な課題である。
  • 既存の量子化手法は，情報理論的な限界に大きく乖離している場合がある。
  • 情報理論的な限界に近づく量子化アルゴリズムを開発し，性能向上を目指す。
  • 提案手法WaterSICは，入力活性の共分散行列に関わらず，情報理論的限界とのレートギャップを0.255ビット以内に抑える。
  • WaterSICは，古典的な水張り（waterfilling）の考え方を重み行列の列（インフィーチャ）に適用することで，異なる量子化レートを割り当てる。
  • LlamaやQwenといったLLMへの適用により，1～4ビットの量子化レートで最先端の性能を達成した。

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

• 有界ツリー幅複体における最適モースマッチングのETH-Tightな複雑性 [cs.CG, cs.CC, cs.DM, cs.DS, math.GN]目的：最適モースマッチング問題の計算複雑性

  • 離散幾何学やトポロジー計算において，ベクトル場の構成は重要な役割を果たす。
  • 最適モースマッチング問題はNP困難であり，効率的なアルゴリズムが未解決のままであった。
  • ツリー幅kに対する計算時間の上界を厳密化し，ETH仮説に基づく限界を示す。
  • 本研究では，任意の有限正則CW複体に対し，$2^{O(k \log k)} n$時間で解けるアルゴリズムを提案した。
  • また，$2^{o(k \log k)} n^{O(1)}$時間で解けるアルゴリズムが存在しないことを，ETH仮説の下で証明した。
  • これにより，ツリー幅パラメータにおける最適モースマッチング問題の複雑性が明確になった。

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

• VulnAgent-R2: リポジトリレベルの脆弱性検出のためのエビデンスに基づくマルチエージェント監査 [cs.SE, cs.AI]目的：リポジトリレベルでの脆弱性検出におけるマルチエージェント監査フレームワーク

  • ソフトウェアの脆弱性は，セキュリティリスクの根本原因であり，その早期発見が不可欠である。
  • 従来の脆弱性検出手法は，単一ファイルの分析に偏りがちで，複雑な依存関係を捉えきれない。
  • エビデンスに基づくマルチエージェント監査により，より高精度で信頼性の高い脆弱性検出を実現する。
  • VulnAgent-R2は，Devign, Big-Vul, DiverseVul, PrimeVulの各データセットで，それぞれ0.798/0.895, 0.739/0.871, 0.700/0.842, 0.385/0.781のF1/AUROCスコアを達成した。
  • JITVulデータセットにおいては，F1値0.606，Top-1精度0.529，Top-3精度0.742の局所化性能を示し，オンライントークン数を38.3%削減した。
  • PrimeVulデータセットにおけるVulnAgent-Xとの比較では，F1値が+0.038向上し，統計的に有意な差が認められた（p=0.009）。

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

• バケットに基づく結果収集器による大規模k近似最近傍探索の改善 [cs.HC, cs.CL, cs.CL, cs.DB, cs.DS]目的：大規模k近似最近傍探索の性能向上

  • 近似最近傍探索は様々な応用分野で重要であり，効率的な検索手法が求められている。
  • 大規模k近似最近傍探索においては，既存手法の性能が著しく低下する問題がある。
  • 本研究は，バケットに基づく結果収集器によって，大規模k近似最近傍探索の効率を改善することを目指す。
  • 提案手法であるBBCは，候補の維持にかかるオーバーヘッドを削減し，キャッシュ効率を向上させる。
  • BBCは，量子化手法の剪定効率低下による再ランキングコストを削減するアルゴリズムを導入した。
  • 実データを用いた実験により，BBCは既存の量子化ベースANN手法を最大3.8倍高速化することが示された。

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

• 依存関係に基づいたリポジトリレベルのCからRustへの翻訳と強化学習によるアライメント [cs.SE]目的：CからRustへの移行の自動化

  • ソフトウェアのセキュリティ向上は重要であり，パフォーマンスを犠牲にすべきではない
  • 従来のルールベースの手法では多様なCのイディオムに対応できず，硬直的で非Rustらしいコードになりがちである
  • リポジトリレベルでの依存関係を正確にモデル化し，構文的正確性と機能的等価性を検証すること
  • DepTransは，大規模なC-Rust並行データの制約を克服し，コンパイル成功率60.7%を達成した
  • また，計算精度は43.5%に達し，最良のベースラインを22.8%と17.3%上回った
  • さらに，15個の産業用Cプロジェクトのうち7個を正常にビルドし，実用的な可能性を示した

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

• 独立同一分布離散信号と干渉を雑音として扱うガウスブロードキャストチャネルのレート領域について [cs.IT, eess.SP, math.IT]目的：ガウスブロードキャストチャネルにおける，純粋な離散入力と干渉を雑音として扱う(TIN)復号による達成可能なレート領域

  • 無線通信において，効率的な情報伝送は重要な課題である。チャネル容量に近づく符号化方式が求められている。
  • ガウスブロードキャストチャネルでは，干渉の影響により，符号化が困難になる場合がある。特に離散信号を用いる場合，性能向上の余地がある。
  • 離散信号を用いた符号化方式を開発し，ガウスブロードキャストチャネルのレート領域を解析することで，性能限界を明らかにすること。
  • 提案する重ね合わせ符号化方式は，干渉を雑音として扱う復号下で，ガウスブロードキャストチャネルの容量領域に一定のギャップ内で収まることが証明された。
  • このギャップは，チャネルパラメータに依存せず，普遍的に成立する。
  • シミュレーションにより，弱いユーザにおいて，ガウス信号化と比較して，PAMを用いることでより高いレートを達成できる場合があることが示された。

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

• 手続き的スキルから戦略遺伝子へ：経験駆動型テスト時進化に向けて [cs.SE, cs.CL]目的：経験の再利用可能性

  • 自動化された問題解決において，過去の経験を効率的に活用することは性能向上に不可欠である。
  • 経験の表現方法が不適切だと，テスト時の制御や反復進化の基盤として機能しない可能性がある。
  • 経験を効率的に再利用するための，コンパクトかつ制御指向の表現方法を確立すること。
  • ドキュメント指向のスキルパッケージは不安定な制御を示す。信号が乏しく，拡張がしばしば性能を低下させる。
  • コンパクトな遺伝子表現が最も高い平均性能を示し，構造変化にも強く，予算を合わせたスキル断片よりも優れている。
  • 遺伝子は反復的な経験蓄積にも適しており，失敗履歴の活用や構造編集が性能向上に寄与する。

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

• イザベルに打ち込むだけ！AIエージェントによるヒントからの形式化，機械化，および一般化 [cs.LO, cs.AI, cs.PL]目的：ランク1多型ラムダ計算項に対する完全かつ最小な型アノテーションの生成

  • プログラムの正当性保証において，型情報は不可欠であり，信頼性の高いソフトウェア開発に貢献する。
  • 型アノテーションの手動作成は，時間と労力を要し，誤りが生じやすいという課題がある。
  • AIエージェントを用いて，ヒントに基づいた型アノテーションの自動生成と形式化を支援し，効率化を目指す。
  • 本研究では，型アノテーションの問題を形式的に記述し，イザベル/HOLで検証可能な形で実装した。
  • 人間とLLM搭載AIエージェントがそれぞれ独立に証明を生成し，AIエージェントがイザベルで自動形式化を行った。
  • 人間のヒントに基づいたAI介入により，形式化の洗練と一般化を実現した。

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

• モジュール格子セキュリティ (第2部): 最適符号選択によるモジュール格子簡約 [cs.CR, cs.IT, math.IT, quant-ph]目的：モジュール格子における簡約手法の開発

  • 暗号の安全性評価において，格子問題の難易度解析が重要視されている。
  • モジュール格子への攻撃手法は未だ十分とは言えず，セキュリティ評価が課題となっている。
  • 巡回数体のモジュール格子に対する効率的な攻撃手法を確立し，その安全性を評価すること。
  • CDPR攻撃を理想格子からモジュール格子へ拡張し，ランクdモジュールを直交するランク1部分モジュールに分解することで，効率的な簡約を実現した。
  • 簡約係数αdがランクに依存せずO(1)で抑えられ，ガウス分布に対するバランス仮説が証明されたことで，MLWEベースの簡約が確立された。
  • 符号選択ステップを混合整数計画問題として定式化し，その最適解がkに対して常に1/2以下となることを証明した。これにより，既存のヒューリスティックな不一致を解消した。

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

• 複合イベント認識のための効率的なTemporal Datalog 実体化 [cs.AI, cs.DB, cs.LO]目的：複合イベント認識における効率的なTemporal Datalog実体化手法

  • 安全や透明性に関わる状況を迅速に検知する重要性が高まっており，イベント処理技術が不可欠である。
  • イベント仕様言語が独立して研究されており，表現力や関連ストリーム推論器の範囲が不明確である。
  • 複数のイベント仕様言語を統一的に処理できる汎用的な複合イベント認識機構を確立する。
  • 主要なイベント仕様言語の断片をTemporal Datalog->-にマッピングすることで，言語間の比較を可能にした。
  • Streaming Trigger Graphsを提案し，Temporal Datalog->-上での効率的なストリーム推論を支援する。
  • 提案手法は，様々なイベント仕様言語に適用可能な複合イベント認識メカニズムの実現に貢献する。

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

• 命題論理プログラムにおける集合演算 [cs.LO]目的：命題論理プログラムの構成と分解に関する代数的枠組み

  • 論理プログラムのモジュール性向上が不可欠であり，複雑化するプログラムを管理する上で重要である。
  • 既存の手法では，論理プログラムを構造的に操作し，分析・構築することが困難である。
  • プログラムをより単純な要素に分解し，それらの意味論から全体を再構成・近似することを目指す。
  • 本研究では，命題論理プログラムのルール本体を構造的に操作するための集合演算を導入した。
  • 最小限プログラムは，各要素の最小モデルから全体の最小モデルを計算できるKromプログラムへと分解可能である。
  • 一般的なプログラムに対しても，同様の近似結果が得られ，新たな代数的視点を提供する。

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

• AgentLens：SWEエージェント評価における幸運合格問題の解明 [cs.SE, cs.AI]目的：SWEエージェントのプロセスレベル評価

  • ソフトウェア開発における自動化の重要性が増しており，SWEエージェントの性能評価が不可欠である。
  • 従来のSWEエージェント評価は，最終的なテストの合否のみに依存しており，プロセスを考慮していない。
  • テスト通過率だけでなく，プロセス品質を評価することで，より信頼性の高いエージェント開発を目指す。
  • AgentLensは，SWEエージェントの軌跡をプロセスレベルで評価するためのフレームワークである。
  • 評価データセットAgentLens-Benchは，1815件の軌跡に品質スコアや無駄のシグナルなどを付与している。
  • テストに合格した軌跡の10.7%が「幸運合格」であり，モデルの順位付けに品質スコアを用いることで評価が大きく変動することが示された。

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

• 非線形算術におけるSMTLIB除算の判定不能性 [cs.LO]目的：非線形実数算術理論の判定不能性

  • 自動検証や定理証明の基盤技術であり，ソフトウェアやハードウェアの信頼性向上に不可欠である。
  • SMTLIB標準における除算の扱いが，実数算術の理論的限界を引き起こす可能性がある。
  • SMTLIB標準の非線形実数算術理論が判定不能であることの証明。
  • SMTLIB標準の非線形実数算術理論(NRA)が，ゼロによる除算の扱いにより判定不能であることが示された。
  • ゼロ除算を未定義関数として扱うことで，整数算術の問題をNRA数式にエンコードできることが根本的な原因である。

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

• ニューラルネットワーク検証における部分多ニューロン緩和 [cs.LO, cs.AI]目的：ニューラルネットワークの安全性特性の形式的保証

  • 深層学習の重要システムへの組み込みが進み，安全性の保証が不可欠となっている。
  • 既存手法では，検証の精度と計算量のバランスが課題となっていた。
  • 検証に必要な精度を保ちつつ，計算コストを削減することを目指す。
  • 本研究では，一部のニューロンのみに対して多ニューロン緩和を適用する手法を提案した。
  • Marabou検証器に提案手法を組み込み，既存手法と比較して良好な結果が得られた。
  • 本手法は，ニューラルネットワーク検証の可能性を広げることが期待される。

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

• 反辞書的SUSアンカー：ほぼ最適なk=1サンプリングスキーム [cs.DS]目的：低密度ミニマイザースキームの探索

  • ゲノムデータ解析において，効率的なインデックス構築は必須であり，低密度ミニマイザーが重要。
  • 既存のミニマイザー法は，パラメータ設定範囲が限られており，小さいk値に対して性能が低下する。
  • より汎用的なサンプリングスキームにより，小さいk値における低密度化を達成することを目指す。
  • 反辞書的SUSアンカーは，特にk=1，σ=4において，理論的な下限密度に非常に近い密度を実現した。
  • これは，既存のbd-アンカーと比較して，大幅な密度改善を意味する。
  • σ=2においても，bd-アンカーよりも性能が向上し，オーバーヘッドを抑制した。

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

• 次にテストすべきこと：運転VLMsにおける解釈可能なカバレッジギャップの発見 [cs.CY, cs.CV, cs.SE]目的：運転VLMsの検証における，未検証領域の優先度付け方法

  • 自動運転技術の安全性確保には，多様な条件下での性能評価が不可欠である。
  • 現在の検証方法は不十分であり，信頼性の高い故障率を算出できない場合がある。
  • 未検証領域を効率的に特定し，安全性を高めるための検証手法を開発する。
  • 提案手法SliceScorerは，稀な条件下と類似条件からのリスク伝播を組み合わせ，効果的に未検証領域を特定する。
  • SliceNavは，LLMを活用し，開発者の質問に基づいて検証ワークフローを自動的に構築し，SliceScorerによるスコアリングを組み込む。
  • 実験の結果，SliceNavは既存手法よりも高リスクなカバレッジギャップを効率的に発見し，多様な条件下での提案を維持することが示された。

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

• スマートコントラクト再帰攻撃対策の識別力に関する形式検証：本番環境向けSolidityソースコードを対象とした三方向検証 [cs.CR, cs.LO, cs.PL]目的：OpenZeppelinの再帰ガードパターンの形式的な正当性の証明

  • スマートコントラクトは金融システム等で利用され，安全性確保が不可欠であるため，形式検証が重要視されている。
  • 再帰攻撃は甚大な被害をもたらす一方で，既存の形式検証手法では，攻撃の再現性と正常動作の保証を両立することが困難であった。
  • 本研究では，本番環境のSolidityソースコードに対して，攻撃の再現，正常動作の証明，境界値分析を同時に行うことで，再帰ガードの識別力を検証する。
  • OpenZeppelinの再帰ガードパターンについて，Lean 4を用いて機械的に検証可能な形式証明を初めて実現した。
  • DAO 2016攻撃，Compound v2，Aave V3フラッシュローン，およびその脆弱な変種を含む，複数の実環境のインスタンスに対して検証を行った。
  • 攻撃の再現，正当性の証明，境界値分析を組み合わせた三方向検証により，ガードが攻撃を阻止しつつ，正常なトランザクションを維持することを確認した。

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

• バイナリ再帰算術におけるゲーデルの第二不完全性定理の自動形式化 [cs.LO]目的：ゲーデルの第二不完全性定理の自動形式化

  • 数理論理学は，数学の基礎を厳密に考察する上で不可欠である。
  • 形式化定理の証明は，手作業では膨大であり，誤りのリスクも伴う。
  • 大規模言語モデルを活用し，形式化定理の自動証明を試みる。
  • Claudeを用いてゲーデルの第二不完全性定理をAgdaで形式化する実験を行った結果，約5万行のコードが生成された。
  • 初期の試みは誤った補題により失敗したが，Guardの講義ノートに基づいた再構築により成功した。
  • 最終的な形式化は，内部証明可能性述語の適切な仕様の重要性を示し，機械的に検証可能な証明を提供した。

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

• 連続変量QKDにおける多次元誤り訂正：レビュー，符号化方式，およびオープンソースシミュレーション [cs.IT, cs.CR, math.IT, quant-ph]目的：連続変量量子鍵配送(CV-QKD)における高効率な誤り訂正手法

  • 量子鍵配送は，情報セキュリティの根幹技術であり，盗聴防止が不可欠である。
  • CV-QKDは，信号対雑音比が低く，長距離伝送において誤り訂正が課題となる。
  • 多次元誤り訂正により，CV-QKDシステムの性能向上を目指す。
  • 多次元誤り訂正の原理と，次元数1, 2, 4, 8を超える高次元構成についてレビューした。
  • 仮想チャネルの構築，逆方向誤り訂正の符号化方式，および線形誤り訂正符号との統合を議論した。
  • 多次元誤り訂正を実装するオープンソースシミュレーションフレームワークHDiracを開発し，最先端のLDPCコードを評価した。

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

• 古典論理と双対性を持つ直観主義論理 [math.LO, cs.LO]目的：古典論理の意味論における新しいアプローチ

  • 論理学の基礎において，真理値の二価性原理への先入観を避けることは重要である。
  • 古典論理の意味論は，しばしば二価性原理に依存しており，その原理への依存を回避する必要がある。
  • 直観主義論理を拡張することで，古典論理の意味論を構築し，両者の関係を新たな視点から捉える。
  • 本研究では，古典論理の新しい推論意味論を提示し，直観主義論理の推論意味論を拡張することでこれを実現している。
  • 古典論理を，原子命題ではなくリテラル上で作用する直観主義論理と双対性の原理によって理解できることを示した。
  • この意味論は，古典論理と直観主義論理の関係に関する新たな洞察を提供する。

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

• ステップサイズヘッジング：勾配降下法を加速する代替メカニズム [math.OC, cs.DS]目的：勾配降下法の加速メカニズム

  • 機械学習において，効率的な学習は重要な課題である。勾配降下法は広く用いられているが，その高速化は常に求められている。
  • 勾配降下法は，適切なステップサイズの選択が難しいという課題がある。不適切なステップサイズは，学習の遅延や発散を引き起こす可能性がある。
  • 本研究では，ステップサイズの調整によって勾配降下法を加速させる手法を提示し，その有効性を示す。
  • ステップサイズのヘッジングという手法により，勾配降下法が加速されることが示された。
  • この手法は，従来の最適化手法に比べて，より効率的な学習が可能となる。
  • 本研究は，ステップサイズ選択の重要性を示唆し，今後の最適化手法の発展に貢献する。

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

• 1
• 2