arXiv雑要約
プログラム - 2026/03/24 公開
エージェント型プログラム検証における補題発見 [cs.SE]目的：エージェント型プログラム検証における補題発見の改善
- プログラムの正当性確保には形式検証が有効であり，信頼性の高いソフトウェア開発に不可欠である。
- 既存の検証エージェントは補題を自動発見できず，大規模かつ複雑なプログラムの検証が困難である。
- プログラム理解に基づいた補題発見により，複雑な検証条件の充足を可能にすることを目指す。
- 提案手法LemmaNetは，ソースコードと仕様を分析し，オフラインで補題を合成する。
- LemmaNetは，検証過程で補題を適応させ，動的に複雑な検証条件を充足する。
- SV-COMPやLinuxカーネル等の実世界の問題に対し，既存手法を大幅に上回る性能を示す。
RLBWTからの最適時間移動構造のバランス調整とLCP配列の計算 [cs.CY, cs.CL, cs.DB, eess.SY, cs.RO, cs.SY, cs.DS]目的：移動構造のバランス調整とLCP配列の計算の効率化
- 反復的なテキスト集合において，BWTは少ない実行数で圧縮可能であり，効率的なデータ構造構築に有用である。
- 移動構造のバランス調整にO(r log r)時間が必要であり，計算のボトルネックとなっている。
- O(r)時間での移動構造のバランス調整アルゴリズムを開発し，LCP配列計算を高速化すること。
- 提案手法により，移動構造のバランス調整を最適時間O(r)で実現した。
- LCP配列の計算も最適時間O(n)で，圧縮空間O(r)で実行可能となった。
- これにより，圧縮空間におけるLCP配列列挙の最適時間アルゴリズムが実現した。
確率分布の比較のための構造を考慮した相違度 [cs.IT, math.IT, physics.soc-ph]目的：確率分布間の相違度の評価手法
- 自然科学や社会科学において，要素間の関係性を持つ確率分布は一般的である。
- 従来の汎用的な情報理論的指標は，要素間の構造的類似性を考慮していない。
- 要素間の関係性を考慮した相違度を導入し，構造を捉えた比較を可能にすること。
- 提案手法は，従来の相違度では検出できないクラスタリング構造を捉えることが示された。
- 計算速度は最適輸送距離よりも大幅に向上し，経済地理学や生態学への応用が期待される。
- 職業間の関連性の定義を変えることで，地域区分に異なる結果が得られることが確認された。
パス幅有界グラフへの距離によるコンポーネント順序連結の構造的カーネル化の境界線 [cs.DS, cs.CC]目的：コンポーネント順序連結問題に対する構造的パラメータに基づいた多項式カーネル化の可能性
- グラフ理論における重要な問題であり，その効率的な解法は計算資源の節約に繋がる。
- 既存の研究では，特定の構造パラメータに対する多項式カーネル化の限界が示されている。
- パス幅に関する距離パラメータを用いたカーネル化の境界線を明確にすることを目指す。
- 本研究では，コンポーネント順序連結問題がパス幅1グラフへの距離と$d$によってパラメータ化された場合に，多項式カーネルを持つことを示した。
- この結果は，頂点被覆問題における同様の境界線と整合性があり，構造的パラメータ化の理論的基盤を強化する。
- パス幅2グラフへの距離をパラメータとする場合，多項式カーネルは存在しないことが示唆され，カーネル化の限界が明確になった。
拡散言語モデルにおける確信度に基づくデコーディングは証明的に効率的である [cs.CL, cs.LG, cs.AI, cs.IT, math.IT, stat.ML]目的：拡散言語モデルにおける確信度に基づくデコーディングの効率性
- 自然言語処理の分野において，効率的なテキスト生成は重要な課題である。
- 拡散言語モデルは柔軟な生成が可能だが，デコーディング戦略が効率に大きく影響する。
- 本研究は，確信度に基づくデコーディング戦略の理論的根拠を確立し，効率向上を目指す。
- 提案手法は，ターゲットデータ分布のエントロピーを用いて，ε-精度のサンプリングを実現する。
- 特に，データ分布のエントロピーが低い場合に，サンプリングの高速化が期待できる。
- この結果は，確信度に基づくデコーディングの理論的基盤を提供し，より効率的なデコーディング戦略の設計に貢献する。
クリティカルセクションはスレッド毎に限定されない：ロックベースの並行処理に対するトレース意味論 [cs.PL, cs.LO]目的：ロックベースの並行処理におけるクリティカルセクションのトレースに基づく特徴付け
- 並行処理は現代のソフトウェアにおいて不可欠であり，その正確性を保証する事が重要である。
- 従来のクリティカルセクションの概念は，単一スレッドに限定されているという誤った前提に基づいている。
- この研究は，より正確なクリティカルセクションの定義を提示し，スレッドを跨ぐクリティカルセクションを扱う事を目的とする。
- 従来のロックセット構築におけるセマンティックギャップを特定し，その問題を解決する。
- C/Pthreadプログラムの本質を捉えるトレースモデルを用いて，スレッド毎の制約のないクリティカルセクションを特徴付けた。
- 実際の実装において発生しうる，複数のスレッドにまたがるクリティカルセクションの存在を示した。
因果的CSITを持つ古典チャネルにおける量子エンタングルメント支援が容量を改善し，ゼロ誤り容量を活性化する [quant-ph, cs.IT, math.IT]目的：因果的CSITを持つ古典チャネルにおける量子エンタングルメント支援の効果
- 通信システムの信頼性向上には，チャネル容量の最大化が不可欠である。
- 従来の古典チャネルでは，量子エンタングルメント支援は容量改善に寄与しないと考えられていた。
- 因果的CSITを持つチャネルにおいて，量子エンタングルメント支援による容量改善とゼロ誤り容量の活性化を検証する。
- 因果的CSITを持つ古典チャネルにおいて，量子エンタングルメント支援は場合によっては容量を改善する。
- 同様に，量子エンタングルメント支援は，ゼロ誤り容量をゼロから非ゼロに活性化することがある。
- これは，従来の古典チャネルに対する量子エンタングルメント支援の効果に関する理解を覆すものである。
予測の限界：時系列における予測可能性プロファイルと情報減衰 [stat.AP, cs.IT, math.IT]目的：時系列データの予測可能性の評価
- 予測は意思決定や計画において不可欠であり，その精度向上は様々な分野で重要である。
- 予測可能な情報の範囲が明確でなく，どの程度の予測が可能なのか判断が難しい。
- 予測可能性の限界を情報理論的に明らかにし，効果的な予測戦略を支援する。
- 予測誤差は利用可能な情報量によって制限され，予測可能性プロファイルによってその変動が可視化される。
- 予測可能性プロファイルは，予測情報の時間的変化を捉え，有用な予測が可能な期間（informative horizon set）を特定する。
- このフレームワークは，モデリング前に予測可能性を診断し，モデリング努力の適切な配分を可能にする。
二重トプリッツ符号とその平均重み列挙子 [math.CO, cs.IT, math.IT]目的：二重トプリッツ符号の平均重み列挙子
- 誤り訂正符号は，情報伝送やデータ記憶において信頼性を確保する上で不可欠である。
- 既存の符号では，効率的な符号化・復号や所望の特性を持つ符号の設計が課題となる場合がある。
- 二重トプリッツ符号の特性を明らかにすることで，より高性能な誤り訂正符号の設計に貢献する。
- 二重トプリッツ符号の平均重み列挙子について研究を行った。
- 有限体 $\mathbb{F}_q$ ($q \in \{2,3,4\}$) における特定の最小重みを持つ二重トプリッツ符号の存在条件を考察した。
- 短い符号長に対して，最大最小重みを持つ二重トプリッツ符号の分類を行った。
コミュニケーションとアクセシビリティに焦点を当てた形式数学への別の手法 [math.LO, cs.LO]目的：形式数学におけるコミュニケーションとアクセシビリティの向上
- 数学は科学技術の基盤であり，厳密な証明が不可欠である。
- 既存の形式数学はツールが複雑で学習コストが高く，実用性に課題がある。
- 数学の実践者にとって使いやすく，コミュニケーションを重視した手法を提案する。
- 本研究では，証明の完全性よりもコミュニケーションとアクセシビリティを優先する「自由形式数学」を提唱する。
- Alonzoという論理に基づいた実装を提示し，その有効性を示す。
- 数学コミュニティに対し，自由形式数学を支援するためのロジック，ソフトウェア，ライブラリの開発を呼びかける。
ソフト工学的シフトの被覆半径の有理性と計算可能性 [stat.ME, cs.SY, eess.SY, math.DS, cs.IT, math.IT]目的：ソフト工学的シフトの被覆半径の有理性とその計算手法
- 情報理論において，ノイズのあるチャネルを通じたデータ伝送に被覆半径が重要である。
- 被覆半径の計算は複雑であり，効率的なアルゴリズムが求められている。
- 原始ソフト工学的シフトの被覆半径を有理数として証明し，計算アルゴリズムを開発する。
- 原始ソフト工学的シフトの被覆半径が有理数であることが証明された。
- ラベル付きグラフによる表現から被覆半径を計算するアルゴリズムが提案された。
非局所フィッシャー情報：持ち上げ，局所極限，ブラクマン-スタム不等式 [quant-ph, cs.CC, math.AP, cs.IT, math.IT, math.PR]目的：非局所フィッシャー情報の性質と極限
- 情報理論は，物理学，生物学，工学など広範な分野で重要である。
- 非局所的な現象を扱うためのフィッシャー情報の理論的枠組みが不足している。
- 非局所フィッシャー情報の数学的な構造を明らかにし，局所的なフィッシャー情報との関係を解明すること。
- 非局所フィッシャー情報は，GuillenとSilvestreの意味で自然な持ち上げを持つことが示された。
- 分数フィッシャー情報に対するブラクマン-スタム不等式が確立された。
- 分数フィッシャー情報は，$s\to 1$ で古典的なフィッシャー情報に収束することが証明された。
推定問題における安定アルゴリズムの下限 [stat.AP, cs.CY, math.PR, math.ST, cs.CC, cs.DS, stat.TH]目的：統計的推定問題に対する安定アルゴリズムの限界
- 推定問題は，機械学習や統計学の根幹であり，現実世界の様々な現象のモデリングに不可欠である。
- 多くの推定問題において，効率的なアルゴリズムの存在が保証されておらず，計算量の壁が存在する。
- MMSE不安定性という条件を用いて，安定アルゴリズムと効率的なアルゴリズムの限界を明確化することを目指す。
- 統計的推定問題において，MMSE不安定性が安定アルゴリズムの失敗を意味することが示された。
- 植えられた最短経路問題，ランダムパリティコード，ガウス部分和問題において，安定アルゴリズムと多項式時間アルゴリズムの分離が確立された。
- MMSE不安定性が，最短経路問題やパリティコード，ガウス部分和問題に共通する特徴であることが示唆された。
DeepNP：超高信頼・低遅延通信のための深層学習ベースノイズ予測 [cs.IT, cs.NI, math.IT]目的：リアルタイムストリーミングにおける高データレートと低遅延の両立のための適応型ネットワークコーディング性能向上
- 無線通信における信頼性と遅延は重要であり，特にリアルタイムアプリケーションにおいてはそのトレードオフが課題。
- 従来のチャネル予測は遅延のあるフィードバックに依存し，チャネルモデルが不明な場合，精度が低下する。
- 深層学習を用いてモデルに依存しないノイズ予測を行い，適応型ネットワークコーディングの性能を改善する。
- DeepNPは統計的なノイズレートを予測することで，予測タスクを簡略化し，従来の推定器よりも高いコーディング性能を実現。
- ER-DeepNPは，スループットをわずか0.1%損なう程度で，平均遅延および最大遅延を最大2倍削減。
- CL-DeepNPは，固定閾値アプローチと比較して，スループットを25%向上させる。
多種型と妥当な空間 [cs.PL, cs.LO]目的：ラムダ計算の空間計算量評価
- 計算機科学において，プログラムの計算資源（時間や空間）の評価は重要である。
- ラムダ計算の空間計算量を正確に評価するモデルは，長年未解決問題であった。
- Space KAMの空間コストモデルを型システムで捉え，空間計算量の評価を目指す。
- 多種型（交差型の変種）を導入し，型推論からSpace KAMが使用する空間を抽出した。
- この型システムは，Space KAMの空間計算量を捉えることができることが示された。
- 型システムのわずかな変更により，Space KAMの実行時間を捉えることも可能であることが示された。
高階数学的演算意味論に向けて [cs.LO, cs.PL, math.CT]目的：高階言語に対する抽象GSOS仕様の理論
- 高階言語の構成性証明は複雑であり，構成性を保証する一般的な意味論的枠組みは少ない。
- TuriとPlotkinの双代数的抽象GSOSフレームワークは，一階言語に対しては有効だが，高階言語には適用できない。
- この研究は，TuriとPlotkinのフレームワークを拡張し，高階言語における構成性を確立することを目指す。
- 本研究では，高階言語の演算意味論を「点付き高階GSOS法則」と呼ばれる特定の双自然変換で表現する理論を開発した。
- この理論に基づき，当該仕様で定義されたすべてのシステムに対して適用可能な一般的な構成性結果が得られた。
- SKI計算とラムダ計算に対する構成性も，アブラムスキーの適用双相似像性に関する強い変形を用いて導き出せる。
ガード付きTGDによるクエリ応答に関するよりタイトな上限 [cs.LO]目的：ガード付きTGDによるクエリ応答の複雑性
- 不完全なデータに対するクエリ応答は，データ統合や知識表現において重要である。
- 既存手法では，問題の決定可能性は保証されるものの，計算量が指数関数的に増加する。
- ガードと追加アトムのarityを分離することで，複雑性の上限を改善すること。
- ガードアトムのarityを任意とし，side signatureのarityを制限することで，EXPTIMEで解決可能となる。
- side signatureを固定し，依存関係の幅を制限することで，計算量をNPまで削減できる。
- 線形化されたガード付きTGDを用いることで，より効率的なクエリ応答が可能となる。
棄権を伴う多腕バンディット問題に対する漸近的・ミニマックス最適後悔限界 [cs.LG, cs.IT, math.IT, stat.ML]目的：棄権を伴う多腕バンディット問題におけるアルゴリズム開発
- 機械学習におけるオンライン意思決定問題の重要性が高まっており，特に探索と活用のバランスが重要である。
- 従来の多腕バンディット問題では，必ず腕を選択する必要があり，最適な腕が不明な場合に不利益を被る可能性がある。
- 本研究では，棄権という戦略を導入することで，より効率的な意思決定を可能にし，後悔を最小限に抑えることを目指す。
- 提案アルゴリズムは，情報理論的な下限と同等の後悔限界を達成し，漸近最適性を示すことができた。
- 棄権オプションの導入が，アルゴリズムの性能向上に貢献することが定量的に明らかになった。
- 数値実験の結果は，理論的な知見を裏付けるとともに，実用的な利点の可能性を示唆している。
エッジラベル付けの良さの計算に関するパラメータ化された複雑性 [cs.FL, cs.DS, cs.CC]目的：グラフのエッジラベル付けの良さの判定問題に関するパラメータ化された複雑性の解析
- ネットワークにおけるルーティングや波長割当問題など，実用的な応用がある重要な分野である。
- エッジラベル付けの良さの判定問題に対する効率的なアルゴリズムが不足しているという課題がある。
- パラメータ化された複雑性という観点から，この判定問題の解決を目指す。
- グラフのエッジラベル付けの良さ問題（GEL）に関して，近傍多様度や頂点被覆をパラメータとした多項式カーネルが存在することが示された。
- 森状の星へのモジュレータのサイズをパラメータとしたGELに対するFPTアルゴリズムが，2-SATによる新しいアプローチを用いて開発された。
- 木幅と最大次数をパラメータとしたGELおよび，$c$-GELに対するFPTアルゴリズムが，動的計画法を用いて提案された。
分割または分解：最大合意森林のための改善されたFPT分岐アルゴリズム [cs.CL, cs.DS, q-bio.PE]目的：最大合意森林の計算におけるFPT分岐アルゴリズムの効率向上
- 系統樹は生物の進化をモデル化する上で重要であり，種間の関係性を明らかにする。
- 異なる系統樹が得られる場合があり，その類似度を定量化する距離尺度の必要性が生じる。
- 既存のアルゴリズムの計算効率を向上させ，より大規模なデータセットへの適用を可能にする。
- 本研究では，無根樹と根付き樹の両方において，既存のアルゴリズムよりも実行時間が改善された。
- 無根樹では$O^*(2.846^k)$，根付き樹では$O^*(2.3391^k)$という計算時間になった。
- この改善の鍵は，分岐ルールを用いた新しい分岐戦略と，問題を部分問題に分解する手法にある。
方策勾配法の強多項式時間性と検証分析 [cs.LG, cs.AI, cs.DS, math.OC]目的：有限状態・行動マルコフ決定過程および強化学習における方策勾配法の収束性
- 強化学習は，複雑な意思決定問題を解決する強力な手法であり，その応用範囲は広い。
- 方策勾配法は実装が容易だが，収束速度が遅く，理論的な保証が不足している。
- 本研究では，方策勾配法の収束性を理論的に保証し，最適解の検証手法を提供する。
- 本研究で提案するアドバンテージギャップ関数を用いることで，方策勾配法が強多項式時間でマルコフ決定過程を解けることを示した。
- 確率的環境下では，アドバンテージギャップ関数が各状態の最適性ギャップを近似し，準線形収束性を示すことが確認された。
- 提案手法は，強化学習における最適性の証明を可能にし，アルゴリズム間比較に依存する現状の課題を克服する。
ロボティクスとソフトウェア工学：Stack Overflowにおけるロボティクスの議論に関する初期調査 [cs.SE]目的：ロボット開発者がStack Overflowに投稿する質問の分析を通じた課題の特定
- ロボットは人間の能力を拡張する可能性を秘めているため，その開発は重要である。
- ロボティクス分野のコミュニティ規模が小さく，質問の可視性が低いという問題がある。
- ロボティクスの実務者が直面する課題を明らかにし，教育資料開発に貢献すること。
- ロボティクス関連の質問は，プラットフォーム全体の平均的な質問と比較して回答数が少ない傾向にある。
- 質問のテーマ分析の結果，ロボットの動作に関する質問が最も多いことがわかった。
- 多くの質問が「どのように」という形式で質問されており，リソース不足を示唆している。
現実世界におけるソフトウェアの誤設定の再検討：実証研究と文献分析 [cs.SE]目的：ソフトウェアの誤設定における根本原因の分類
- ソフトウェアの信頼性確保において，設定の誤りは重大な障害となり得るため，その理解と対策は不可欠である。
- 既存の研究と現実世界の誤設定との間に乖離があり，実際のシステムへの適用が困難な場合がある。
- 現実世界の誤設定事例を分析し，新たな分類を提案することで，より実用的な対策に繋げる。
- 772件の現実世界の誤設定事例を分析し，制約違反，リソース不足，コンポーネント依存エラー，設定の意味解釈誤りという新たな分類を提案した。
- 誤設定トラブルシューティングの研究動向を分析した結果，対象がシステムソフトウェアから高度なアプリケーションへと変化していることが明らかになった。
- 公開されているツールや評価データセットが不足しており，研究の再現性が低いことが課題として指摘された。誤設定事例のデータセットを公開する。
テスト戦略の創出：社会技術的グラウンデッド・セオリー [cs.SE]目的：テスト戦略の創出に関する理論
- ソフトウェア品質確保において，テストは不可欠な要素である。
- 開発者のテストへの関与度にばらつきがあり，その要因が不明である。
- 開発者のテスト行動とその変化の理由を明らかにすることを目指す。
- 本研究は，開発者のテストに対する考え方と行動がどのように変化するかを解明した。
- テストの実施状況やその理由に関する11の状況カテゴリーと3つの概念を特定した。
- テスト成果物と実践者の集合的省察との関連性を示す新たな視点を提示した。
グラフアソシアヘドラ上の距離計算はFPT，ハイパーグラフ多角体上ではW[2]-困難 [eess.SY, cs.RO, cs.SY, cs.DS, cs.CG, cs.DM, math.CO]目的：グラフアソシアヘドラとハイパーグラフ多角体における距離計算の複雑性
- グラフ理論と組み合わせ最適化において，多角体は様々な問題をモデル化する上で重要である。
- グラフアソシアヘドラやハイパーグラフ多角体における距離計算は，計算困難であることが知られていた。
- 距離パラメータに関する固定パラメータアルゴリズムの存在可能性と限界を明らかにすること。
- グラフアソシアヘドラ上の距離計算は，距離をパラメータとして固定パラメータ扱い可能(FPT)である。
- 一方，ハイパーグラフ多角体上の距離計算は，距離をパラメータとするW[2]-困難である。
- ハイパーグラフ多角体上の距離計算は，多項式時間近似アルゴリズムの存在がP=NPを仮定しない限り不可能である。
ガウス混合モデルのKLダイバージェンス最小化による差分プライバシー保護分布公開 [cs.IT, cs.CR, cs.LG, eess.SP, math.IT, stat.ME]目的：ガウス混合モデルのパラメータ公開における差分プライバシー保護
- データマイニングや機械学習等，多様な分野でガウス混合モデルが利用されているため，その安全性が重要である。
- ガウス混合モデルのパラメータ公開は，プライバシー侵害のリスクを伴うことが近年指摘されている。
- 公開とプライバシー保護の両立を目指し，KLダイバージェンスを最小化するメカニズムを提案する。
- 提案手法は，KLダイバージェンスを精度指標として，ノイズの加え方を最適化することで，プライバシー保護と精度維持を両立している。
- 理論解析により，プライバシー予算の配分とノイズ統計が差分プライバシー保証に与える影響を定量的に評価した。
- 合成データと実データを用いた実験により，提案手法が強いプライバシー保護と高い実用性を実現することを示した。
構成制御駆動ブール回路 [cs.NI, cs.MA, eess.SP, cs.LO]目的：ブール回路の構成的制御
- デジタル回路の論理構造と計算能力を抽象化する研究分野であり，現代の情報技術の基盤である。
- 回路を組み合わせる際の構成性が無視されてきた，あるいは非形式的に扱われてきた。
- 構成性を重視し，モジュール性と形式的推論を可能にするブール回路の構築方法を確立すること。
- 本研究では，極限を用いた演算子を提案することで，構成的な回路構築を可能とした。
- これにより，順次，並列，分岐，反復回路を形成する演算子を定義し，制御フローを明示化した新たな計算モデルを提示した。
- このモデルは，従来のブール回路と同等以上の計算能力を持つことが示された。
LLMアシスタントがソフトウェア開発者の生産性に与える影響：システマティックレビューとマッピング研究 [cs.DC, cs.SY, eess.SY, cs.SE, cs.AI, cs.HC]目的：ソフトウェア開発者の生産性に対するLLMアシスタントの影響
- ソフトウェア開発は社会の基盤であり，その効率化は経済成長に不可欠である。
- LLMアシスタントの導入は急速に進んでいるが，その効果は十分に検証されていない。
- LLMアシスタントが開発者の生産性に与える影響を包括的に把握し，課題を明確化すること。
- 多くの研究でLLMアシスタントの利用により開発速度の向上，コード検索時間の短縮，単純作業の自動化といった利点が報告されている。
- 一方で，認知負荷のオフロードやチームコラボレーションの低下といったリスクも指摘されている。
- LLMアシスタントがコード品質を向上させるか否かは，研究によって結果が異なり，コンテキストや評価基準に依存することが示唆されている。
枯渇させず，無駄にしない [cs.PL]目的：リソースを意識したラムダ計算のセマンティクスと型システムの拡張
- 計算資源の効率的な利用は，現代のソフトウェア開発において不可欠である。
- 既存の型システムでは，リソースの枯渇や無駄を十分に検知できない場合がある。
- 型システムの健全性に加え，リソースの枯渇や無駄がない計算を保証すること。
- ラムダ計算に，リソースの使用状況を追跡する機能を組み込む拡張を提案した。
- 拡張は任意の「グレード代数」に依存するため，基盤言語への変更は不要である。
- 大規模なステップ形式のセマンティクスを用いて健全性を証明し，共帰的推論の最新技術を活用した。
ソフトウェアエンジニアによるAI活用：実用的なワークフロー [cs.SE]目的：ソフトウェアエンジニアにおけるAIツールの活用ワークフロー
- ソフトウェア開発の効率化と品質向上において，AIの活用は不可欠となっている。
- AI生成物の信頼性や修正判断が難しく，効果的な活用方法が課題となっている。
- AI生成物の利用における判断基準とワークフローを提示し，質の高い開発を支援する。
- 提案されたワークフローは，AI生成物を反復的にプロンプト，検証，修正することで，エンジニアの判断を支援する。
- 四象限の意思決定モデルを用いて，AI活用における判断ポイントを明確化し，より意識的な利用を促す。
- トルコとアゼルバイジャンの産業現場での観察と事例研究から，ワークフローの実用性が示された。
情報理論的分散型安全集約：受動的共謀耐性 [cs.IT, cs.CR, cs.DC, cs.LG, math.IT]目的：分散型安全集約における情報理論的限界の特性評価
- 分散型機械学習の普及に伴い，プライバシー保護されたデータ集約の重要性が増している。
- 既存研究では，プロトコル設計と計算保証に重点が置かれ，情報理論的限界の理解が不足している。
- 分散型環境における通信効率とセキュリティのトレードオフを明らかにし，プロトコル設計に指針を与える。
- 本研究では，K個のユーザーからなるネットワークにおいて，各ユーザーが秘密鍵を保持し，少なくとも1シンボルを送信する必要があることを示した。
- 安全に1シンボルの入力合計を計算するためには，ユーザー全体でK-1個以上の独立した秘密鍵シンボルが必要となる。
- これらの結果は，分散型学習における安全で通信効率の高いプロトコル設計のための基礎となる。
アグノスティクス：汎用学習環境を用いた強化学習による，あらゆるプログラミング言語の学習 [cs.LG, cs.PL]目的：あらゆるプログラミング言語におけるコード学習手法
- 科学技術分野では，PythonやJavaScriptだけでなく，マイナーな言語も依然として不可欠である。
- 既存の手法では，新しい言語ごとにデータセットやテスト環境，強化学習基盤を構築する必要がある。
- 言語に依存しない学習パイプラインを構築し，言語ごとのエンジニアリングを不要にすること。
- アグノスティクスは，Lua，Julia，R，OCaml，Fortranなどの低リソース言語において，Qwen-3 4Bの性能を他の大規模モデルに匹敵するものに向上させた。
- モデルファミリー（Qwen-3 8B，DeepSeek Coder 6.7B Instruct，Phi 4 Mini）への拡張性も確認された。
- MultiPL-EとLiveCodeBench（多言語版）において，160億パラメータ以下のモデルで最先端のpass@1スコアを達成した。
知識から推測へ：仮説推論のための様相的枠組み [cs.LO, cs.AI]目的：仮説推論を形式化するための認知様相論理
- 人間の思考過程のモデル化は，認知科学や人工知能の発展に不可欠である。
- 従来の様相論理では，事実と推測の区別が曖昧になる場合がある。
- 事実と推測を明確に区別し，推測推論を形式化する。
- 本研究では，Axiom Cを導入し，事実が推測層を通過しても維持されることを示した。
- Axiom Cのみでは様相的崩壊は起こらず，Axiom Tの存在や二値論理が必要であることが判明した。
- 非二値様相論理に基づき，KCおよびKDCという様相システムを定義し，健全性と完全性を証明した。
第5のビジービーバー値の決定 [cs.LO, cs.FL, math.LO]目的：5状態2記号チューリングマシンの停止までの最大ステップ数
- 計算可能性理論において，停止問題など，未解決問題の難解さを示す指標となる。
- ビジービーバー関数の値の算出は計算量が指数関数的に増加し，手計算での決定が困難である。
- Coqを用いて，第5のビジービーバー値の厳密な計算と検証を目指した。
- 5状態2記号チューリングマシンの全1億8138万5789個を検証し，停止判定を行った。
- その結果，$S(5) = 47,176,870$ であることを証明した。
- 40年以上ぶりの新たなビジービーバー値の決定であり，形式検証された初の値である。
$(k+2, k, 2)$ MDS配列符号の最適修復 [cs.IT, math.IT]目的：MDS配列符号における単一障害時の最小修復帯域幅の決定
- 分散ストレージシステムにおいて，耐障害性を最適化するため，MDS符号は不可欠である。
- MSR符号はサブパケット化レベルが指数関数的に増加し，ディスクI/Oのオーバーヘッドが課題となる。
- 固定されたサブパケット化レベルでの最小修復帯域幅を明らかにし，効率的な符号設計を目指す。
- 2つのパリティノード，サブパケット化レベル2の場合において，修復方式と射影線上の点集合の対応関係を確立した。
- $\text{PGL}_2(\Fq)$の鋭意3移入作用を利用し，修復帯域幅の下限を導出した。
- この下限を修復I/Oに拡張し，下限を達成するMDS配列符号のクラスを構築した。
LLM コードエージェントの自動ベンチマーク：エージェント駆動アノテーションと評価による [eess.SY, cs.SY, cs.SE, cs.CL]目的：LLM コードエージェントのベンチマーク評価手法
- ソフトウェア開発における自動化の重要性が増しており，コードエージェントの性能評価が不可欠である。
- 既存のベンチマークは専門知識を要し，コストが高く，多様性に欠けるという課題がある。
- 人間による監督下で多様なタスクを生成し，高精度な評価を実現する。
- エージェント駆動のベンチマーク構築パイプラインを提案し，PRDBenchを開発した。
- PRDBenchは，20ドメインにわたる50のPythonプロジェクトと，詳細なPRDを含む。
- Qwen3-Coder-30Bを基盤とした専用評価モデルPRDJudgeは，90%以上の人間との合致率を達成した。
半空間の相対誤差テストは困難である [cs.CC, cs.DS]目的：ブール関数の相対誤差基準下におけるプロパティテスト
- 疎なブール関数をテストする自然な枠組みを提供し，疎なグラフのプロパティテストのモデルと類似している
- 相対誤差テストにおいて，半空間のような関数クラスのテスト難易度に関する情報が不足していた
- 標準モデルよりも相対誤差テストが困難である関数クラスの最初の例を示す
- 本研究では，ブール超立方体上での半空間の相対誤差テストアルゴリズムには，$\tilde{\Omega}(\log n)$ のオラクル呼び出しが必要であることを示した。
- この結果は，標準モデルにおける半空間の定数クエリテスト可能性とは対照的である。
- 相対誤差モデル下での半空間テストは，標準モデルよりも明らかに難しいことが証明された。
BTCにおけるインセンティブ攻撃：短期的な収益変化と長期的な効率性 [cs.CR, cs.IT, math.IT, math.PR]目的：BTCにおけるインセンティブ攻撃の短期的な収益変化と長期的な効率性
- 暗号資産の安全性確保は，金融システムにおける信頼維持に不可欠であるため，重要性が高い。
- BitcoinのDifficulty Adjustment Algorithm(DAA)には脆弱性があり，悪意のある攻撃の標的となりやすい。
- BitcoinのDAAにおけるインセンティブ攻撃のリスク評価と，効率的な対策の特定を目指す。
- 短期的な収益変化は，既存のselfish mining攻撃と比較して，断続的なマイニング戦略では無視できる程度である。
- 長期的に見ると，selfish miningがより高い効率性を示すことが明らかになった。
- BTCとBitcoin Cash間のコインホッピング戦略は，短期的に見て，BTCの誠実なマイナーと攻撃者に対して同程度の利益をもたらす。
エントロピーベクトルの構造的性質とインガルトン不等式の安定性 [cs.IT, math.IT]目的：エントロピー設定におけるインガルトン不等式の制約付きバージョン
- 情報理論は，情報伝達やデータ圧縮の限界を明らかにする重要な分野である。
- 従来のインガルトン不等式は，一般的なエントロピープロファイルでは成り立たない場合がある。
- 条件付き独立性のわずかな違反に対する不等式の安定性を定量的に評価すること。
- 選択された条件付き相互情報項が小さい場合，不等式は制御された誤差項まで成立することが示された。
- 本研究は，無限個の非シャノンの不等式の影響を暗黙的に捉える構造的補題を導入した。
- 得られた境界は，Matu\v{s} (2007) や Dougherty-Freiling-Zeger (2011) の結果を統一的に回復し，新たな結果も示している。
対立を意識した融合：構造化された認知事前知識による大規模言語モデルの論理慣性の緩和 [cs.AI, cs.CL, cs.LG, cs.LO]目的：大規模言語モデルにおける論理慣性緩和
- 自然言語処理の高度化に伴い，大規模言語モデルの信頼性確保が重要課題となっている。
- 既存の大規模言語モデルは，規則ベースのシステムに対する構造化された摂動に対して脆弱である。
- 矛盾する情報に対するロバスト性を高め，信頼性の高い推論を可能にすることを目指す。
- 本研究では，対立を意識した融合（Fusion-Conflict）というフレームワークを提案し，論理慣性を効果的に緩和できることを示した。
- 提案手法は，前提の検証と論理的推論を分離する二重プロセスアーキテクチャを採用することで，矛盾下でも高い精度を達成した。
- 構造的な検証規律が，学習データの規模と並んで，信頼性の高い多段階推論に不可欠であることを示した。
科学者における生成AIの利用状況とプログラミング生産性に関する調査 [cs.SE, cs.HC]目的：科学者における生成AIの利用状況，ツール選好，および生産性との関連性の解明
- 現代科学研究においてプログラミングは不可欠であり，研究効率を向上させる上で重要である。
- 多くの科学者は十分なソフトウェア開発の訓練を受けておらず，スキル不足が課題となっている。
- 生成AIが科学者のプログラミングを支援し，経験不足を補う可能性を探る。
- 生成AIの利用は学生や経験の浅いプログラマーに多く見られ，分野によって利用状況に差がある。
- 科学者たちは，開発者向けツールよりもChatGPTのような汎用的な会話型インターフェースを好む傾向にある。
- 経験不足や開発プラクティスの不足は，生産性向上と関連するが，両者は相互に影響し合うことが示唆された。
ハイブリッド・コード v2：神経記号的検証と自動知識ベース拡張による幻覚ゼロの臨床ICD-10コーディング [cs.SE, cs.AI]目的：臨床ICD-10コーディングにおける幻覚の排除と，高い網羅率・精度
- 医療分野における正確な診断と効率的な医療管理のために，ICD-10コーディングの自動化が不可欠である。
- ニューラルネットワークによるコーディングは高性能だが，誤ったコードを生成する「幻覚」の問題を抱えている。
- 本研究は，神経記号的アプローチにより幻覚を排除し，知識ベースの拡張を自動化することで，実用的なコーディングシステムを実現する。
- Hybrid-Code v2は，多層検証を通じて幻覚を完全に排除し，高い精度（92%）を達成した。
- MIMIC-IIIデータセットにおいて，従来のルールベースシステムよりも網羅率（85%）を40%向上させた。
- ニューラルベースライン（6-18%）で観測された幻覚を解消し，安全性の高い医療AIシステム構築の可能性を示した。
ソフトウェア工学研究におけるオープンサイエンスの現状：ICSE成果物に関する事例研究 [cs.CL, cs.SE]目的：ソフトウェア工学研究におけるオープンサイエンスの実践状況の評価
- 研究の透明性，検証可能性，再利用性を高める上で，オープンサイエンスは不可欠である。
- ソフトウェア工学分野では，成果物の共有は一般的だが，その実用性は十分に検証されていない。
- ICSEで発表された成果物を評価し，実行可能性と再現性の課題を明らかにすること。
- 評価された100件の成果物中，完全に実行可能であったのは40件のみであった。
- 実行可能な成果物でも，32.5%は修正なしで実行できたが，82.5%は中程度の労力が必要であった。
- 実行可能な成果物全体の35% (14/40) しか元の結果を再現できなかった。本研究は，成果物の準備，ドキュメント作成，レビューに関する3つの具体的な指針を提案する。
ソフトウェアエンジニアリングにおけるAI生産性指標APEX-SWE [cs.SE, cs.AI, cs.CL]目的：ソフトウェアエンジニアリングにおける最先端AIモデルの経済的価値評価
- ソフトウェア開発の効率化は，経済成長と技術革新の鍵となる。
- 既存の評価は限定的なタスクに偏り，現実世界の複雑な課題に対応できない。
- 現実的なソフトウェアエンジニアリングタスクの実行能力を総合的に評価する。
- APEX-SWEは，統合タスクとオブザーバビリティタスクという2つの新しいタスクタイプを用いて評価を行う。
- Claude Opus 4.6がPass@1で40.5%とAPEX-SWEリーダーボードで首位となり，Claude Opus 4.5が38.7%で続いた。
- 高い性能は，仮定と検証済みの事実を区別する「認識的厳密性」に起因し，行動前の体系的な検証と組み合わされることが示された。
分散型ネットワークにおける情報理論的安全な集約 [cs.IT, math.IT]目的：分散型ネットワークにおける情報理論的安全な集約のレート領域の最適化
- 分散型機械学習の普及に伴い，データの安全性確保は重要課題となっている。
- 参加者間の連携において，情報漏洩のリスクが依然として存在する。
- 安全性を保証しつつ，通信効率を最大化する集約手法を確立することを目指す。
- 安全な集約を実現するためには，各ユーザが他の全ユーザに少なくとも1ビットの情報を送信する必要がある。
- また，各ユーザは少なくとも1ビットの秘密鍵を保持する必要があることが示された。
- さらに，全ユーザで合計$K-1$ビット以上の独立した秘密鍵を共有する必要がある。
エージェント評価におけるランダム性について [cs.LG, cs.AI, cs.SE]目的：エージェント評価の信頼性向上
- エージェントシステムの性能評価は，その発展に不可欠である。
- 単一の実行に基づく評価では，結果にばらつきが生じ，正確な性能判断が困難である。
- 評価におけるランダム性の影響を検証し，信頼性の高い評価方法を提案すること。
- SWE-Bench-Verifiedを用いた実験で，単一実行のpass@1スコアには2.2～6.0%程度の変動が確認された。
- 初期トークン段階のわずかな違いが，その後の戦略に大きな影響を与えることが示された。
- 複数回の実行による評価，統計的検出力の分析，pass@k等の指標の使用が推奨される。
要求段階における複雑度の測定：開発努力の予測におけるスペクトル指標 [cs.SE, cs.CL]目的：要求段階における複雑度の評価
- システム開発において，複雑さはコスト超過や遅延，プロジェクト失敗の主要因となる。
- 要求仕様に内在する構造的複雑さは十分に理解・定量化されていない。
- 要求段階での複雑度を定量化し，開発努力を予測する手法を確立すること。
- スペクトル指標は統合努力を0.95以上の相関で予測可能であることが示された。
- 構造的指標は0.89以上の相関を示したが，密度に基づく指標は予測性能に乏しかった。
- 固有値由来の指標は，単純な接続性指標では捉えきれない認知的な側面や努力の度合いを反映している。
ソフトウェア空間分析：内部ソフトウェア実行の可視化と統計に向けて [cs.SE]目的：内部ソフトウェア実行データの評価
- ソフトウェア保守において，変更・削除が必要なモジュール特定は重要である。
- ユーザ要望やバグ報告だけでは，モジュールの実行状況を的確に評価できない。
- 空間統計を用いて，ソフトウェア内部の実行状況を可視化し，評価する手法を提案する。
- ソフトウェアの内部構造をモジュール間の呼び出し関係に基づく空間として定義した。
- 空間統計を用いて，空間的なクラスタの可視化と空間統計量の算出を行った。
- ソフトウェア工学分野における空間統計の有用性と今後の課題について考察した。
普遍的シャッフル漸近論：ガウス領域における厳密なプライバシー解析 [cs.IT, math.IT]目的：ガウス領域におけるシャッフルによるプライバシー増強の実験レベルの厳密なプライバシー理論
- データプライバシー保護は，個人情報保護の観点から極めて重要であり，技術的進歩が求められている。
- 既存のプライバシー解析は近似的なものであり，厳密なプライバシー損失の評価が困難であった。
- シャッフルを用いたプライバシー増強メカニズムに対し，厳密なプライバシー損失を評価し，理論的限界を明らかにする。
- シャッフルされたヒストグラムに対する正確な尤度比恒等式と，明示的な典型集合残差を持つ完全な条件期待値線形化定理を証明した。
- 比例構成における普遍的な主要定数 I_pi/(8n) を特定し，適切な固定構成共分散 Sigma_pi=(1-pi)Sigma_0+pi*Sigma_1 を強調した。
- ガウス微分プライバシーとの等価性，ベリー・エッセン限界，および完全な限界 (epsilon,delta) プライバシー曲線を得た。
ARC：多数の要件シナリオを動作するWebシステムにコンパイル [cs.SE]目的：多数のシナリオを含むマルチモーダル文書からの動作するWebシステムの生成
- 大規模言語モデルの活用が進む中で，その能力を最大限に引き出すことが重要である。
- 要件の規模が大きくなると，大規模言語モデルの性能が著しく低下する問題がある。
- 多数の要件シナリオから，正しく保守可能なWebシステムを自動生成することを目指す。
- ARCは，UI，API，データベース層のモジュール設計，テストスイート，トレーサビリティを生成する。
- GUIテストの通過率が，最先端のベースラインと比較して平均50.6%向上した。
- 初心者ユーザーでも，複雑なシステムのDSL文書を平均5.6時間で作成可能であることが示された。