arXiv雑要約
プログラム - 2026/04/22 公開
Maudeの等式および帰納的推論をAthenaで実現 [cs.LO]目的：Maudeの等式理論をAthenaへの変換フレームワーク
- ソフトウェアやシステムの形式検証において，信頼性の高いモデル構築が不可欠である。
- 等式による記述は強力だが，帰納的・演繹的推論を直接サポートしないという課題がある。
- 等式理論を定理証明に活用し，形式検証の能力を向上させる。
- Maudeの等式理論をAthenaに変換するフレームワークmaude2athenaを提案した。
- Athenaは，多種多様な論理仕様に対する自然演繹証明をサポートし，帰納的推論を可能にする。
- 変換は意味を保持しつつ，コンパクトであり，演繹的推論に適している。
知覚を考慮した損失圧縮符号化への構成的アプローチ：情報理論的指針 [cs.IT, math.IT]目的：知覚を考慮した損失圧縮符号化における情報理論的指針
- 知覚的品質は重要であり，従来の歪み基準だけでは十分ではない。
- 多様な定式化と仮定が存在し，理論的指針の不足が課題である。
- 情報理論的原理に基づき，実践的な指針を提供し，符号化方式の設計を支援する。
- 本稿では，知覚を考慮した損失圧縮符号化を構築するための情報理論的原理を概観する。
- レート歪み知覚理論から得られる実践的な指針を示し，実装可能な符号化方式の設計に役立てる。
- 単位円例を用いて，主要な概念，アーキテクチャ原理，トレードオフを直感的に理解する。
大規模言語モデル生成による難読化XSSペイロードの機械学習ベース検出における評価 [cs.CR, cs.LG, cs.SE]目的：難読化されたXSSペイロードの生成と評価
- Webセキュリティにおいて，クロスサイトスクリプティング（XSS）は依然として重要な脆弱性である。
- 従来の検出システムは，難読化によってペイロードの表面的な形が変わるため，攻撃の識別が困難である。
- 本研究は，大規模言語モデルを用いた難読化ペイロードの生成と，その実行時挙動に基づく評価を目指す。
- 大規模言語モデルによるペイロード生成パイプラインを構築し，決定論的変換技術と組み合わせた。
- ベースラインモデルでは実行時挙動の一致率が0.15であったが，ファインチューニングにより0.22に向上した。
- 生成されたペイロードを付加しても検出性能は向上しないものの，挙動フィルタリングされたサンプルは性能劣化を引き起こさないことが示された。
推論中心LLMに基づく自動定理証明 [cs.SE]目的：自動定理証明におけるLLMの推論能力の活用
- 形式手法の基盤であり，ソフトウェアやハードウェアの検証において不可欠な技術である。
- 既存の証明支援システムは，LLMの高度な推論能力を十分に活用できていない点が課題である。
- LLMを用いた戦略的な証明計画と自己評価により，自動定理証明の能力向上を目指す。
- ReCent-Proverは，LLMによる自己検証と失敗事例の分析により，不適切な戦術の早期排除を実現した。
- LLMが生成した証明計画に基づいて過去の事例を検索することで，予測される証明戦略に合致する補題や証明を見つけ出す。
- CoqStoqベンチマークにおいて，既存の最先端システムと比較して証明定理数が22.58%向上し，推論中心設計の有効性が示された。
論理的意思決定のための目標指向型意味通信 [cs.NI, cs.IT, math.IT]目的：論理的意思決定のための目標指向型意味通信の原理的基盤
- 自律エージェントの共同知覚において，帯域幅の制約下での効率的な情報伝達が重要である。
- 安全性が求められる状況下では，情報の選択と意思決定プロセスの透明性と検証可能性が課題である。
- 意思決定に不可欠な情報を効率的に伝達し，論理的な検証可能性を維持することを目的とする。
- 本研究では，一階述語論理に基づく階層的な世界表現を用いた説明可能な意味通信フレームワークを提案する。
- 意味情報，エントロピー，条件付きエントロピー，相互情報などの定義に基づき，意味レート歪み理論と意味情報ボトルネック原理を用いて目標指向型意味通信の目的を定式化した。
- シミュレーション環境における安全な経路追従タスクで，提案手法の有効性を実証した。
バイナリにコンパイルメタデータを付加し，逆アセンブルを決定可能にする [cs.CR, cs.PL]目的：バイナリ実行ファイルの安全性と保守性の向上
- ソフトウェア配布の標準形式であり，その安全性向上は重要である。
- バイナリは不透明な形式であり，解析や操作が困難である。
- コンパイラの意図を反映したメタデータを付加し，解析を容易にする。
- 提案するバイナリ形式は，コンパイラの意図を捉えたメタデータを含み，より高水準な表現への変換を可能にする。
- 評価の結果，メタデータの付加は実行時動作や性能に影響を与えないことが示された。
- 実世界のC/C++バイナリを用いて検証した結果，動作を変更せずにリフト，インストルメント，再コンパイルが可能であることが確認された。
Kubernetes上のNode.js向け予測型自動スケーリング：低遅延，適切なキャパシティ [cs.SE, cs.DC]目的：Node.jsワークロードの予測型スケーリングアルゴリズム
- クラウド環境におけるアプリケーションのスケーラビリティは，安定稼働とコスト最適化に不可欠である。
- 従来のHPAやKEDAは，負荷の増加にリアクティブに対応するため，遅延の悪化を招く場合がある。
- 負荷予測に基づいたプロアクティブなスケーリングにより，遅延を低減し，適切なキャパシティを維持することを目指す。
- 提案手法は，クラスタ全体の集約指標を用いて，スケーリングによる影響を受けにくい安定した予測信号を生成する。
- ベンチマークでは，HPAやKEDAと比較して，安定した負荷状態と大幅な低遅延を実現した。
- 定常的な負荷増加下でのメディアンレイテンシは26msであり，KEDAの154ms，HPAの522msを大きく上回る。
超計量OGP - パラメータ的RDT対称二値パーセプトロン接続 [cs.LG, cond-mat.dis-nn, cs.IT, math.IT, math.PR, stat.ML]目的：統計的計算ギャップ(SCG)の特性評価
- 機械学習の理論において，学習可能性を評価する上で重要な研究分野である。
- 学習問題の難易度を正確に評価する指標が確立されていない。
- OGPとパラメータ的RDTの関係を解明し，学習閾値の理解を深める。
- 超計量OGPの制約密度の上限を厳密に導出し，数値評価を行った結果，既存のパラメータ的RDT推定値と高い一致性が見られた。
- 第1，第2レベルの超計量OGPにおける上限値は，それぞれパラメータ的RDT推定値の第3，第4リフティングレベルとほぼ一致した。
- 超計量OGPとパラメータ的RDTの間には，完全な同型関係が存在する可能性が示唆され，今後の研究への展望が開かれた。
VLA Foundry: ビジョン-言語-行動モデルの訓練を統合する統一フレームワーク [cs.RO, cs.AI, cs.CV, cs.LG, cs.SE]目的：ビジョン-言語-行動モデルの訓練のための統一的なフレームワークの提供
- 近年の大規模言語モデル(LLM)の発展は，様々なマルチモーダルタスクへの応用を促進している。
- 既存のVLA研究は，多くの場合，アクション訓練段階に特化しており，互換性のない事前学習パイプラインを組み合わせている。
- 言語事前学習から行動専門家による微調整まで，エンドツーエンドで制御可能な訓練スタックを提供すること。
- 本フレームワークを用いて，完全にゼロから訓練したモデルと，Qwen3-VLバックボーンを用いたモデルを訓練し，公開した。
- ゼロから訓練したモデルは，既存の非公開モデルと同等の性能を示し，Qwen3-VLバックボーンを用いることで，多様なタスクにおいてベースラインを大幅に上回る性能を達成した。
- フレームワークのコードベースおよびモデルの重みは，公開されており，誰でも利用可能である。
FB-NLL：パーソナライズされた連合学習におけるノイズラベルへの特徴量に基づくアプローチ [cs.LG, cs.IT, eess.SP, math.IT]目的：ノイズラベルを含む連合学習における，特徴量に基づくユーザークラスタリングとラベル修正
- データ分布の偏りが大きい連合学習において，各クライアントに特化したモデル構築が重要である。
- 既存手法では，学習過程におけるモデル更新の変動に影響されやすく，ノイズラベルに弱いという課題がある。
- 特徴量の構造に着目し，学習ダイナミクスに依存しない，ロバストなユーザーグルーピングを実現する。
- 提案手法FB-NLLは，特徴量の共分散行列のスペクトル構造を利用し，ユーザー間のタスクの一貫性を識別する。
- 本手法は，学習前のワンショットでクラスタリングを行うため，通信コストと計算コストを削減できる。
- 実験結果から，FB-NLLが既存手法よりも高い精度と安定性を実現することが示された。
PlayCoder：LLM生成GUIコードを動作可能に [cs.SE]目的：LLM生成GUIコードの動作可能性評価と改善
- GUIアプリケーションは，ユーザーとのインタラクションが重要であり，現代のソフトウェア開発において不可欠である。
- 既存のコード生成評価は，テストケースによる正誤判定に偏っており，GUIのインタラクティブ性や状態遷移を十分に捉えられていない。
- GUIアプリケーションの論理的正確性を評価し，LLMによるGUIコード生成の課題を克服することを目指す。
- PlayEvalと呼ばれるGUIアプリケーションベンチマークを構築し，Python, TypeScript, JavaScriptのコード生成評価を可能にした。
- Play@kという指標を提案し，生成されたコード候補のうち少なくとも1つがエラーなく動作するかどうかを評価できるようにした。
- PlayCoderという多エージェントフレームワークを開発し，コード生成，評価，反復修正を自動化することで，GUIアプリケーションの動作可能性を大幅に向上させた。
エージェント型コーディングにおけるテスト時計算量のスケーリング [math.OC, cs.SY, eess.SY, math.OC, cs.SY, eess.SY, cs.SE, cs.AI, cs.CL, cs.LG]目的：エージェント型コーディングにおけるテスト時計算量スケーリングの枠組み
- 大規模言語モデルの性能向上は重要であり，テスト時スケーリングはその有効な手法の一つである。
- 既存手法は短い出力に最適化されており，長期間にわたるエージェントの行動系列には不向きである。
- 過去の経験を効果的に表現し，選択・再利用することで，エージェント型コーディングの性能を向上させる。
- 提案手法は，ロールアウト軌跡を要約することで，重要な仮説，進捗，失敗モードを効率的に表現する。
- 並列スケーリングには再帰的トーナメント投票（RTV）を導入し，ロールアウト要約の集団を比較・絞り込む。
- シーケンシャルスケーリングにはPDRを適用し，過去の試行から蒸留された要約に基づいて新たなロールアウトを条件付けする。
k進鎖の展開された木サイズの漸近的評価 [math.CO, cs.DM, cs.DS]目的：k進鎖の展開された木サイズの漸近的期待値
- 木圧縮の文脈で重要であり，木と一意に関連付けられる。
- 鎖の展開された木サイズを正確に評価する方法が課題であった。
- 鎖サイズnに対する展開された木サイズの漸近的期待値を求める。
- kが固定された場合，鎖の展開された木サイズはe^(c*√n)の形の伸張指数項を含むことが示された。
- この結果は，固定長のBrauer鎖の極限分布にも影響を与える。
グラフにおける待ち合わせ時間の近立方時間での計算 [q-bio.PE, cs.DS]目的：無向グラフ上の2つのランダムウォーカーの待ち合わせ時間の計算
- ネットワーク科学や複雑系において，ノード間の到達可能性や相互作用の解析は重要である。
- グラフサイズが大きくなると，待ち合わせ時間を正確に計算することは計算量的に困難である。
- 待ち合わせ時間の計算を効率化し，より大規模なグラフへの適用を可能にすること。
- 提案手法は，待ち合わせ時間の計算を$O(N^4)$ の計算量で行うことが可能である。
- この手法は，Sylvester方程式の構造を利用し，対角線吸収制約を効率的に処理する。
- さらに，Poisson方程式も同様のコストで解くことができ，進化ダイナミクスへの応用も可能である。
安全性が保証された疎なCRT-FFT：$\Omega(k^2)$の下界と$O(N \log N)$の最悪ケース [eess.SP, cs.DS, cs.IT, math.IT]目的：k-疎な信号のフーリエ変換の効率的な計算手法
- 圧縮センシング，レーダー，医療画像処理など，幅広い分野における基盤技術である。
- 既存のCRTに基づく疎なFFTアルゴリズムは，モジュラス選択が性能に影響する点が課題であった。
- モジュラス選択における脆弱性を明らかにし，最悪ケースの性能を保証するロバストなフレームワークを提案する。
- 非互いに素なモジュラスを用いるCRT-FFTにおいて，候補の成長に関する$\Omega(k^2)$の下界が証明された。
- 提案手法は，証明書により衝突リスクを検出し，リスクが低い場合は$O(\sqrt{N} \log N + k N)$の計算量で動作する。
- 証明書が衝突リスクを検出した場合，古典的なFFTにフォールバックすることで$O(N \log N)$の最悪ケース性能を保証する。
6Gネットワークにおける複数移動体のネットワーク追跡 [cond-mat.soft, cond-mat.mtrl-sci, cs.CG, eess.SP, cs.NI, quant-ph, cs.CC, eess.SP, cs.IT, math.IT]目的：複数移動体の追跡におけるネットワークアーキテクチャの設計
- 6G通信では，通信とセンシングの統合が進んでおり，高精度な位置追跡が求められている。
- 単一基地局では追跡可能な範囲や精度に限界があり，複数基地局の協調が必要とされている。
- 基地局間での無線リソースの動的配分と，追跡精度の最適化が課題となっている。
- 提案手法であるネットワークカルマンフィルタは，複数基地局による追跡に適していることが示された。
- 追跡精度評価指標である事後クラメル・ラオ下限を導出し，ビームフォーミング設計に活用した。
- シミュレーションにより，提案する動的ビームフォーミング設計が追跡誤差を低減できることを確認した。
逐次成長型一次元ランダムグラフにおける貪欲ルーティング [quant-ph, cs.CC, math.CO, cs.DS, cs.NI, cs.SI]目的：逐次成長型一次元ランダムグラフにおける貪欲ルーティングのルーティング複雑性
- ネットワークにおけるルーティングは，効率的な情報伝達に不可欠であり，その複雑性解析は重要である。
- 逐次成長型グラフのルーティング複雑性に関する理論的な保証が不足していた。
- 逐次成長型一次元ランダムグラフにおける貪欲ルーティングのルーティング複雑性の漸近的挙動を厳密に解明すること。
- 貪欲探索のステップ数S_nは，高確率でS_n = Θ(log n)を満たすことが証明された。
- 期待ステップ数はE[S_n] = 2H_n - 2 ~ 2 log nであり，その分布はベネットレート関数を用いて評価された。
- 任意の開始ノードと終了ノードのペアに対しても，期待ルーティング複雑性はE[S_{s,t}] = 2 log n + O(1)で近似される。
証明からの全Ambプログラムの抽出 [cs.LO]目的：証明可能な全性と正しさを備えた非決定性並行プログラムの抽出
- ソフトウェアの信頼性向上が重要であり，形式的な手法による検証が不可欠である。
- 既存の手法では，並行性や非決定性を扱うプログラムの検証と抽出が困難である。
- プログラムの全性と正しさを保証しながら，非決定性と並行性を扱うプログラムを抽出すること。
- CFP(Concurrent Fixed Point Logic)という論理システムを提案し，プログラムの抽出を可能にした。
- 抽出されたプログラムの正当性は，ドメイン理論に基づく意味論によって証明された。
- 無限Grayコードを有符号桁表現に変換する非決定性プログラムを抽出することに成功した。
DeepFWI：コードと警告の多Modal意味論によるバグ感受性警告の特定 [cs.SE]目的：バグ感受性警告の特定
- ソフトウェアの品質向上には，バグの早期発見が不可欠であるため，静的解析技術の発展が重要である。
- 静的解析ツールは誤検知が多く，開発者の生産性やツールの信頼性を損なうという課題がある。
- 本研究は，誤検知を抑制し，バグ検出精度を向上させることで，開発者の負担軽減を目指す。
- DeepFWIは，ソースコードと警告の多Modal意味論を捉えるLSTMベースのモデルを設計し，警告のバグ感受性を特定する。
- 大規模データセットを用いた実験の結果，DeepFWIはF1スコア67.06%を達成し，既存手法を大幅に上回る性能を示した。
- DeepFWIをオープンソースプロジェクトに適用した結果，大部分の警告をフィルタリングしつつ，25件の真のバグ関連警告を発見した。
分散プロトコルの帰納的証明分解によるインタラクティブな安全性検証 [cs.DC, cs.LO]目的：分散プロトコルの安全性検証手法
- 分散システムは現代のインフラを支える基盤であり，その信頼性確保は極めて重要である。
- 大規模プロトコルの自動検証は計算コストが高く，失敗原因の特定が困難である。
- 人間と機械の協調による，効率的かつ理解しやすい安全性検証を目指す。
- 帰納的証明分解という新しい手法を提案し，インタラクティブな安全性検証を可能とした。
- 帰納的証明グラフを用いて，人間が誘導的に不変条件を開発するプロセスを支援する。
- Raftコンセンサスプロトコルなど，既存の自動検証ツールでは扱いきれない複雑なプロトコルにも適用可能であることを示した。
保守的 Petri ネットの構造的生きた状態 [cs.LO]目的：保守的 Petri ネットの構造的生きた状態に関する複雑性
- Petri ネットは並行システムのモデリングに広く用いられ，その解析は重要な課題である。
- Petri ネットの構造的生きた状態の判定は計算量的に困難であることが知られている。
- 保守的 Petri ネットにおける構造的生きた状態の複雑性を明らかにすること。
- 構造的生きた状態の判定は，保守的 Petri ネットにおいても EXPSPACE 困難であることが示された。
- 構造的に生きた保守的 Petri ネットにおける最小生きた状態の大きさは，ネットのサイズに対して少なくとも二重指数関数的に大きい。
- この結果は構造的に有界な Petri ネットにも適用される。
認識スキル：知識と忘却についての推論 [cs.AI, cs.CC, cs.LO]目的：知識の獲得と忘却のダイナミクスを捉える認識論理
- 知識とその変化は，AIやマルチエージェントシステムにおける意思決定に不可欠である。
- 既存の認識論理では，知識の獲得と忘却を統一的に扱う枠組みが不足している。
- 知識獲得と忘却のプロセスを定量的にモデル化し，認識能力を評価する手法を提供する。
- 本研究では，知識更新に伴う認識能力を「認識スキル」という指標で表現する重み付きモデルを提案する。
- 知識獲得はスキルの向上，忘却はスキルの低下としてモデル化し，「知得可能性」「忘却可能性」の概念を導入した。
- モデル検査や充足可能性問題の計算複雑性を分析し，理論的基盤と実用的な含意を明らかにした。
ギャップを気にせず！ETH下でのSVP困難性 [cs.CC, cs.CR, cs.DS]目的：指数時間仮説(ETH)の下での基礎的な格子問題の困難性
- 暗号理論や計算複雑性において，問題の困難性を保証する仮説は重要である。
- 格子問題の効率的な解法は，多くの暗号システムの安全性を脅かす可能性がある。
- ETHを仮定することで，特定の格子問題に対する効率的なアルゴリズムの存在可能性を否定する。
- 本研究では，$\mathsf{CVP}_{p,\gamma}$が$2^{o(n)}$時間で解けることはETHが誤っている場合にのみ可能であることを示した。
- $\ell_p$ノルムにおける$\mathsf{SVP}_{p,\gamma}$のランダム化ETH困難性を確立し，整数格子$\mathbb{Z}^n$の幾何学的性質を新たに発見した。
- $\mathsf{3SAT}$から$\mathsf{BDD}_{p,\alpha}$への既存の帰着を改善し，$\mathsf{BDD}_{p,\alpha}$のETH困難性に関するより良い結果を得た。
DeFiスマートコントラクトにおける制御フロー完全性の強制 [cs.NI, cs.CR, cs.SE]目的：DeFiスマートコントラクトのセキュリティ確保
- DeFiは金融サービスに変革をもたらすが，セキュリティ脆弱性が存在し，大きな損失につながる可能性がある。
- 既存のセキュリティ対策は，DeFiプロトコルの合成性と攻撃の巧妙化により，十分な保護を提供できない。
- 攻撃トランザクションに現れる新たな制御フローを検知し，制御フロー完全性を強制することでセキュリティを向上させる。
- 過去37のハッキングされたDeFiプロトコルのトランザクション分析から，攻撃トランザクションは常に新しい制御フローを導入することが明らかになった。
- CrossGuardは，事前にハックの知識を必要とせず，一度デプロイメント時に設定するだけで制御フローのホワイトリストポリシーを適用し，攻撃を防御する。
- CrossGuardは37件の攻撃のうち35件をブロックし，誤検知率は0.26%と低く，ガスコストも最小限に抑えることができた。
vMODB：分散非同期アプリケーションのためのイベントとデータ管理の統合 [cs.DB, cs.SE]目的：分散非同期アプリケーションにおけるイベントとデータ管理の統合手法
- スケーラブルなクラウドアプリケーション構築において，イベント駆動型マイクロサービスアーキテクチャが重要視されている。
- 従来のアーキテクチャでは，コンポーネント間の一貫性確保が難しく，データ整合性とスケーラビリティのトレードオフが生じていた。
- vMODBは，データ整合性とスケーラビリティを両立し，開発者の負担を軽減することを目指している。
- vMODBは，イベントログと状態管理を統合することで，ACID特性を透過的に保証し，コンポーネント間の一貫性を保つ。
- 提案するVirtual Micro Service (VMS)プログラミングモデルは，ORMとメタプログラミングにより，アプリケーションのセマンティクスをシステムに提供する。
- 実験の結果，vMODBは，従来のフレームワークと比較して，最大3倍の性能向上を達成した。
CASS：NvidiaからAMDへのトランスパイル：データ，モデル，ベンチマーク [cs.RO, eess.SP, cs.AR, cs.AI, cs.CL, cs.LG, cs.PL]目的：GPUコードのクロスアーキテクチャ変換
- GPUのハードウェア移植性を高めるためには不可欠な研究分野である。
- スケーラブルな変換ソリューションが存在しないという課題がある。
- 学習ベースの翻訳によるGPUコード変換の性能向上を目指す。
- CASSデータセットとモデル群により，CUDA-HIP間，SASS-RDNA3間の変換精度がそれぞれ88.2%，69.1%と高い性能を示した。
- 生成されたコードは，85%のケースでネイティブコードと同等の性能を達成し，実行時間とメモリ使用量を維持した。
- データ，モデル，評価ツールはオープンソースとして公開され，GPUコンパイラツールやバイナリ互換性の進歩を支援する。
汎用ゲームプレイにおける最良エージェントの特定 [cs.CL, cs.LG, cs.AI, cs.DS, cs.IT, math.IT, stat.ML]目的：複数問題領域における各サブタスクの最良（またはそれに近い）性能を示すアルゴリズムの特定
- 汎用ゲームプレイは，多様なゲームに対応可能なAI開発の重要な研究分野である。
- ゲームの種類が多い場合，最適なエージェントを効率的に特定することが課題となる。
- 限られた試行回数で，各ゲームに適した高性能エージェントの選択を目指す。
- 提案手法は，GVGAIやLudiiといった汎用ゲームプレイ環境で，既存手法よりも低い単純後悔と誤り確率を示すことが確認された。
- エージェント評価における精度と効率を向上させ，アルゴリズムの実行時間が長いマルチタスク領域への応用が期待される。
- 各タスクを多腕バンディット問題として捉え，信頼区間に基づく楽観的な選択プロセスを用いることで，高い性能を実現している。
分離論理の最小限の断片におけるペアノ算術の符号化 [cs.LO]目的：分離論理におけるペアノ算術の符号化
- ソフトウェア検証において，ヒープ操作プログラムの検証に分離論理が有効であるため，その拡張が重要である。
- 分離論理に数値を加えた際の有効性，特に決定可能性や計算複雑性に関する研究が十分に進んでいない。
- ペアノ算術の数式を分離論理の最小断片へ翻訳し，有効性の同値性を証明することで，この課題を解決する。
- ペアノ算術のPi-0-1式を，直観的ポイントトゥ述語，0，後者関数のみで構成される分離論理の断片に翻訳できる。
- ペアノ算術の式が標準モデルで有効であることと，翻訳された分離論理の式が標準解釈で有効であることは同値である。
- この断片における有効性の決定不能性に関する証明も提示されており，一貫性や非終端性といった性質の議論を可能にする。
クロス言語バグ検出のためのコード言語モデルのファインチューニング [cs.SE, cs.AI]目的：クロス言語バグの検出
- 多言語プログラミングの普及に伴い，異なる言語間の相互作用から生じるバグの検出が重要になっている。
- 従来の単一言語のバグ検出ツールでは，複数の言語が絡むクロス言語バグの検出が困難である。
- コード言語モデルを活用し，クロス言語バグを効果的に検出する手法を確立することを目指す。
- 13種類のコード言語モデルをファインチューニングした結果，全てモデルにおいて性能向上が見られた。
- 特にUniXcoder-baseがF1スコア0.7407で最も高い性能を示し，小規模モデルの方が大規模モデルよりも優れる傾向があった。
- 単一言語バグデータセットでファインチューニングされたモデルはクロス言語バグ検出性能が低く，データセットサイズの拡大が性能向上に寄与した。
TREBL：状態遷移を含むEvent-B論理 - 理論 (第1部) [cs.LO]目的：状態遷移を含むEvent-B論理の拡張
- 状態遷移を含むEvent-B論理は，システムの厳密な検証において重要な役割を果たす。
- 既存のEvent-B論理では，状態に着目した解釈であり，状態遷移そのものを直接表現することが難しい。
- 状態から始まる全ての状態遷移を決定する特性を利用し，実行可能性の検証を可能にする論理を開発すること。
- TREBLという論理フラグメントを定義し，それによって関心のあるすべての実行可能性の条件を表現できることを示した。
- 定義された推論規則の健全性を証明した。
- 十分に洗練されたマシンであれば，妥当な含意関係に対して推論を見つけることができることを示した。
タスクからチュートリアルへ：Excelチュートリアル文書およびビデオ作成のための自動GUIフレームワーク [cs.SE]目的：Excelチュートリアルの自動生成
- Excelは汎用性が高いが，複雑なため効果的な利用を支援するチュートリアル需要が高い。
- 既存のチュートリアルは手作業で作成され，ソフトウェア更新ごとに頻繁な修正が必要で，労力がかかる。
- 自然言語によるタスク記述からExcelチュートリアルを全自動で生成する。
- 本フレームワークは，最先端の基盤モデルと比較してタスク実行成功率を8.5%向上させた。
- 生成されたチュートリアルは，可読性と教育効果の点で専門家が作成した教材に匹敵またはそれを上回る。
- 自動化パイプラインにより，手作業が不要になり，専門家による作成時間の1/20にコストが削減された。
物理層ディセプションをスタケルバーグゲームとして：戦略領域，均衡，および堅牢な設計 [cs.CR, cs.IT, math.IT]目的：物理層ディセプションにおける送信機と盗聴者の戦略的相互作用の解析
- 無線通信における情報セキュリティは，ますます重要になっており，新たな脅威への対策が求められている。
- 従来の物理層セキュリティは，傍受に対する脆弱性を抱えており，より高度なセキュリティ手法が課題となっている。
- ディセプション技術を導入することで，盗聴者の誤認を誘い，セキュリティ性能を向上させることを目指す。
- 送信機と盗聴者の相互作用をスタケルバーグゲームとしてモデル化し，戦略領域を解析した。
- 最適な動作点はスタケルバーグ均衡であり，時間平均セキュリティが向上することが示された。
- 提案手法は，ナカガミmフェージング環境下で，従来の物理層セキュリティと比較して12-55%高い盗聴者への歪みをもたらすことが確認された。
SpecAgent：コード補完のための投機的検索・予測エージェント [cs.SE, cs.AI]目的：コード補完における投機的検索と予測の改善
- 大規模言語モデルの活用が重要視される一方，実用的なソフトウェア開発環境での課題が存在する。
- 既存手法では，推論時の低遅延性と文脈の質の維持がトレードオフとなる。
- インデックス作成時に非同期処理を行うことで，遅延を隠蔽し，質の高いコード生成を実現する。
- SpecAgentは，既存の最良手法と比較して，9〜11%（相対的には48〜58%）の絶対的な性能向上を常に達成した。
- 推論遅延も大幅に削減された。
- 既存ベンチマークにおける将来の文脈漏洩問題を特定し，漏洩のない合成ベンチマークを構築した。
単一サンプルによるオンライン距離マッチングの滑らかな解析：距離歪みの克服 [cs.NI, cs.PF, cs.DS]目的：オンライン距離マッチングにおける競争的アルゴリズムの性能評価
- 多様な最適化問題に応用可能であり，資源配分や割り当ての効率化に貢献する分野である。
- 配分先のサーバーが敵対的に配置される状況下では，効率的なマッチングアルゴリズムの設計が困難である。
- 分布に関する事前知識を必要とせず，単一のサンプルのみで高い性能を発揮するアルゴリズムを開発する。
- 本研究では，$d \neq 2$ の場合に$O(1)$-競争的なアルゴリズムを提案し，既存の$o(\log n)$競争比を改善した。
- 確率的距離埋め込みによる$\Omega(\log n)$の障壁を回避し，決定論的な埋め込みにおけるアルゴリズムのコストを直接評価するアプローチを採用した。
- ユークリッド距離におけるオフライン最適解の下界を導出し，提案アルゴリズムの性能保証に利用した。
線形効果，例外，そしてリソース安全性：デストラクタのためのCurry-Howard対応 [cs.PL, cs.LO]目的：線形性，副作用，例外の組み合わせ問題
- 現代的なプログラミング言語では，リソース管理と安全性が重要な課題である。
- 副作用と例外処理を線形型システムと整合させることは困難である。
- リソース安全性を確保するための型システムと計算規則を確立すること。
- 線形および順序付けられたtyping規則に基づき，リソース安全性を保証する2つの線形効果付き計算機を開発した。
- C++やRustのデストラクタに着想を得て，型にデフォルトの破棄アクションを付与し，例外処理を線形性と統合した。
- 副作用のある交換規則（move operation）は，LIFO順序とは異なるリソース解放に必要である。
証明からプログラムへ：大規模言語モデルにおけるツール誘発性の推論ハルシネーションの特徴付け [cs.CL, cs.LO, cs.SE]目的：ツール拡張言語モデルにおける推論の信頼性に関する問題点の特定と解決
- 大規模言語モデルの能力向上は目覚ましいが，その推論過程の信頼性が課題となっている。
- 外部ツールを利用することで性能は向上するものの，推論がツール出力に依存し，思考が浅くなる現象が懸念される。
- ツール利用による推論の質の低下を定量的に評価し，改善策を提案することを目的とする。
- ツール拡張言語モデルは，最終的な正答率を19.3%向上させるものの，推論過程は一貫して悪化する。
- ツール利用頻度が高いほど推論の整合性は低下し，誤りの種類も計算ミスから論理的誤りへと変化する。
- ツール利用を補助的な証拠として捉えさせることで，最終的な正答率と推論の深さを両立させるフレームワークを提案した。
コンピュータプログラミングの図式的な基盤 [cs.LO]目的：コンピュータプログラミングの図式的な基盤の確立
- プログラミングの抽象化と可視化は，複雑なシステムの理解と開発に不可欠である。
- 既存のプログラミングモデルでは，命令型プログラムの構造を直感的に表現することが困難である。
- Kleene-Cartesian rig categoryを用いて，命令型プログラムの構造を明確化し，プログラム論理を支援する。
- Kleene-Cartesian rig categoryと関連するテープ図が，命令型プログラムの扱いと様々なプログラム論理を扱うのに便利であることが示された。
- Rig categoryにおける$\oplus$と$\otimes$という2つのモノイダル積を備えたrig categoryのアローに対する便利なグラフィカルな表記法であるテープ図が導入された。
圧縮されたIEEE 802.11 CSIフィードバックにおける人間活動シグネチャの保護 [cs.IT, cs.CR, cs.NI, math.IT]目的：人間活動シグネチャの保護
- 無線通信において，電波環境の把握は通信品質向上の鍵となる。
- CSIフィードバックには，ユーザーの活動や位置情報等のプライバシーに関わる情報が含まれる可能性がある。
- CSIフィードバックにおけるプライバシー保護と通信性能の両立を目指す。
- 本研究では，差分プライバシーに基づく量子化メカニズムを提案し，CSIフィードバックのプライバシーを保護する。
- 提案手法は，既存の802.11規格との互換性を保ちながら，角度表現に対する感度を解析的に評価可能である。
- シミュレーションにより，提案手法がプライバシー保護とビームフォーミング性能の低下を最小限に抑えることを示した。
重み付き多言語探索によるコード翻訳のブートストラップ [cs.SE, cs.AI]目的：複数プログラミング言語間のコード翻訳
- ソフトウェア開発における異言語間連携の需要増加に伴い，コード翻訳の重要性が高まっている。
- 並行データの不足と，実行可能なテストオラクルがないことが，コード翻訳の大きな課題となっている。
- テストスイートの機能不変性とクロスリンガルな移植性を活用し，データ不足と最適化の偏りを解決する。
- 提案手法BootTransは，多言語強化学習のための汎用的な検証オラクルとして，豊富なピボット言語のユニットテストを活用する。
- シードプールと探索プールという二重プールアーキテクチャにより，実行ガイド型経験収集を通じて学習データを徐々に拡張する。
- 言語を意識した重み付けメカニズムにより，相対的な性能に基づいて，より難しい翻訳方向を動的に優先し，最適化の偏りを軽減する。
$2$-準完全リー符号とアーベル型ラマヌジャングラフ：新たな構成と関係 [cs.IT, math.CO, math.IT]目的：2準完全$p$進リー符号の新たな構成と，アーベル型ラマヌジャングラフとの関連性
- 誤り訂正符号は，通信やデータ保存における信頼性を確保する上で不可欠な技術である。
- 既存のリー符号の構成方法は限られており，効率的な符号の設計が課題となっていた。
- 新たな構成法により，より多くの符号パラメータに対応できるリー符号を構築すること。
- 長さ$\frac{q-1}{2}$，次元$\frac{q-1}{2}-2k$の2準完全$p$進リー符号の無限族を明示的に構成した。
- この符号は，有限体$\mathbb{F}_{q^2}$の生成集合$H_q = \{(a, a^3) \mid a \in \mathbb{F}_q^*\}$から導出される。
- Mesnagerらの2準完全リー符号と，Liグラフや有限ユークリッドグラフといったアーベル型ラマヌジャングラフを結びつけた。
SATソルビングを用いたゲート隠蔽化回路における関数復元攻撃 [cs.CR, cs.LO]目的：ゲート隠蔽化回路における隠されたゲート操作の復元
- 秘匿計算の分野において，入力データと関数自体の両方を保護する技術は重要である。
- ゲート隠蔽化回路は，ゲート機能を隠蔽するが，回路トポロジーの漏洩の影響は十分に検討されていない。
- 本研究は，回路トポロジーからゲート機能を復元する攻撃手法を開発し，その実用的な脅威を明らかにする。
- SATソルビングを組み合わせることで，より効率的にゲート操作を復元することが可能となった。
- ISCASベンチマーク等の回路に対して実験を行った結果，従来の攻撃手法よりも復元時間が大幅に短縮された。
- 回路トポロジーの公開が，隠蔽されたゲート機能の復元を支援することを示し，トポロジーがセキュリティ上の重要な漏洩経路となりうることを明らかにした。
RIS-ISACシステムにおけるセキュアなビームフォーミングと反射設計：受動的・能動的な盗聴者の共謀下 [cs.IT, math.IT]目的：RISを用いた統合センシング通信システムにおけるセキュアなデータ通信の最適化
- 無線通信の安全確保は重要であり，盗聴対策は不可欠である。
- 受動的・能動的な盗聴者の共謀による脅威は，既存のセキュリティ対策では十分ではない。
- RISを利用し，ビームフォーミングと反射設計を最適化することで，より強固なセキュリティを実現する。
- 提案手法は，センシング性能を維持しつつ，システム全体の秘匿率を最大化する。
- 問題の非凸性を克服するため，交互最適化と二次ペナルティ法，逐次凸近似を適用した。
- 数値シミュレーションの結果，提案アルゴリズムの有効性と優位性が確認された。
セキュアな多利用者線形分離型分散コンピューティング [cs.IT, cs.CR, math.IT]目的：多利用者線形分離型分散コンピューティングにおけるデータ秘匿性の確保
- 分散コンピューティングは，計算資源を有効活用し，大規模な問題を効率的に解決する上で重要である。
- 従来の分散コンピューティングでは，データ秘匿性の確保が課題であり，情報漏洩のリスクが存在した。
- 本研究は，情報理論に基づいた秘匿性条件を導出し，コストを維持しつつ安全な分散コンピューティングを実現する。
- 各利用者が自身の要求関数以上の情報を学習しないことを保証するための必要条件が示された。
- 行列Dから利用者が観測するサーバーに対応する列を取り除いた時のランクがK-1以上である必要十分条件が導かれた。
- 行列EにNull(D)の基底を追加し，共有乱数を注入することで，有限体上では完全な情報理論的秘匿性を保証する変換が設計された。
従来型および流体アンテナシステムにおける活動検出のクレーマー・ラオ限界 [cs.IT, math.IT]目的：活動検出性能の限界
- 無線通信システムの効率的な利用には，活動検出の精度向上が不可欠である。
- 従来の活動検出手法では，アンテナ構成の柔軟性を十分に活かせていない場合がある。
- 流体アンテナシステムを含む多様なアンテナ構成における活動検出性能の理論的限界を明らかにすること。
- クレーマー・ラオ限界（CRB）の統一的なフレームワークを確立し，活動検出性能の限界を評価可能にした。
- CRB解析を活動指標に適用するため，二値活動状態を連続パラメータに緩和することで，実用的な閾値ベースの検出決定との整合性を高めた。
- 流体アンテナシステムは，複雑さを大幅に削減しながら，空間的多様性の利点を大きく発揮できることが示唆された。
通信・センシング傍受者下におけるISACシステムのセキュアビームフォーミング [cs.IT, math.IT]目的：通信・センシング傍受者下におけるISACシステムの機密レート最大化
- リソース効率向上からISACが注目されており，無線通信とセンシングの統合が重要である。
- 通信とセンシング両方のセキュリティを確保することが課題となっている。
- 通信とセンシング両方の傍受者に対するセキュアビームフォーミング手法を確立する。
- 提案手法は，通信とセンシングのセキュリティ，性能，送信電力制約を考慮したビームフォーミング設計により，システム機密レートを最大化する。
- 逐次凸近似，一階テイラー展開，半定値緩和を組み合わせることで，非凸最適化問題を解決する。
- シミュレーション結果は，提案手法の有効性と優位性を示している。
Debug2Fix：インタラクティブなデバッグはコーディングエージェントのバグ修正能力を向上させるか [cs.SE, cs.AI]目的：コーディングエージェントのバグ修正能力向上
- ソフトウェア開発の自動化が進む中で，バグ修正は依然として開発者の重要な作業であり，効率化が求められる。
- 既存のコーディングエージェントは，静的解析や試行錯誤的なテスト修正に頼ることが多く，実行時の詳細な情報活用が不足している。
- インタラクティブなデバッグ機能をエージェントに組み込み，実行時情報を活用することで，バグ修正の精度向上を目指す。
- Debug2Fixフレームワークを導入した結果，特定のモデルにおいて，ベースラインと比較して20%以上の性能向上が見られた。
- GPT-5やClaude Haiku 4.5といった比較的小規模なモデルでも，Debug2Fixにより，より高性能なClaude Sonnet 4.5に匹敵する性能を達成することができた。
- サブエージェント構造とデバッガ統合の両方が，性能向上に不可欠であることが，系統的なアブレーション実験によって示された。
バッファと無制限乗り換えに対応するためのダイクストラ法の適応 [cs.CL, cs.DS, cs.AI, cs.RO]目的：公共交通機関における無制限乗り換え経路探索
- 経路探索は，都市生活や物流において不可欠な技術であり，効率的な移動手段を提供する。
- 既存のダイクストラ法は，時間依存性やバッファ時間などの現実的な要素を考慮できていない場合がある。
- バッファ時間の影響を正確に考慮した，より効率的な経路探索アルゴリズムを開発する。
- 時間依存ダイクストラ法（TD-Dijkstra）が，既存のMR法よりも優れた性能を示すことが明らかになった。
- バッファ時間を持つ停留所において，既存の接続フィルタリング手法が不正確であることが示された。
- Transfer Aware Dijkstra（TAD）を提案し，バッファ時間を考慮しつつ，MR法よりも2倍以上の高速化を達成した。
公共交通経路探索における早期枝刈り [cs.DS, cs.AI, cs.RO]目的：公共交通経路探索の効率向上
- 都市交通の利便性向上に不可欠な経路探索技術の基盤となる。
- 大規模ネットワークでは，乗り換え候補の膨大な数により計算コストが増大する。
- 乗り換え時の探索範囲を効率的に絞り込み，計算時間を短縮することを目指す。
- 提案手法「Early Pruning」は，既存の経路探索アルゴリズムに容易に組み込める。
- 乗り換え接続を時間順にソートし，最適な解よりも遅い乗り換えは早期に除外する。
- スイスとロンドンの交通ネットワークで最大57%のクエリ時間短縮を達成した。
ガボウの$O(\sqrt{n}m)$ 最大カルディナリティマッチングアルゴリズムの再検討 [cs.DS]目的：最大カルディナリティマッチングアルゴリズムの効率化
- グラフ理論における基本的な問題であり，ネットワークフローや組み合わせ最適化など広範な応用がある。
- 既存のアルゴリズムは，グラフの規模が大きくなると計算コストが増大する課題があった。
- ガボウのアルゴリズムの最初のステップをより直接的な方法で改善し，理解と実装を容易にする。
- ガボウのアルゴリズムの最初のステップの新たなアルゴリズムを提案した。
- 提案アルゴリズムは，エドモンズのプライマル・デュアルアルゴリズムよりも直接的であり，教育的価値が高いと考えられる。
- アルゴリズムの実装を公開し，検証可能な成果を得た。
オントロジー制約によるニューラル推論：エンタープライズエージェントシステムにおけるドメインに根ざしたAIエージェントのためのニューロシンボリックアーキテクチャ [cs.AI, cs.CL, cs.SE]目的：エンタープライズエージェントにおける，オントロジー制約によるニューラル推論アーキテクチャの開発
- LLMの企業への導入が進む一方で，幻覚やドメインシフトといった課題があり，実用上の制約となっている。
- LLMは，推論レベルでの規制遵守を保証することが難しく，企業利用における大きな障壁となっている。
- オントロジーを用いてLLMの入出力に制約を加え，より信頼性の高いエンタープライズエージェントを実現する。
- 提示されたニューロシンボリックアーキテクチャは，金融，保険，医療など5つの業界において，高い精度，規制遵守，役割一貫性を示した。
- 特に，LLMのパラメータ知識が弱いベトナムローカライズドドメインにおいて，効果が顕著であった。
- オントロジーによる制約は，LLMの訓練データ不足を補い，ドメイン知識が限定的な状況下でも高い性能を発揮する。