arXiv雑要約
プログラム - 2026/06/16 公開
低ランク構造を用いたデータ選択における能動学習 [cs.LG, cs.DS]目的：データ選択のための低ランク構造に基づく能動学習手法
- 機械学習モデルの効率的な学習には，適切なデータ部分集合の選択が不可欠である。
- 既存手法はデータの幾何学的構造に依存するため，代数的構造を持つデータセットへの適用が難しい。
- 低ランク近似と残差に基づくサンプリングにより，より広範なデータセットに対応するデータ選択を実現する。
- 提案手法は，平均損失を$(1+\varepsilon)$の相対誤差で近似する$\tilde{O}\left(k + \frac{1}{\varepsilon^2}\right)$個のデータ点を選択可能である。
- 理論的保証に加え，実データ実験により，提案手法が既存のサンプリングやクラスタリングに基づく手法を上回る性能を示すことが確認された。
- この手法は，埋め込み行列の最適ランク-$k$近似コスト$\Phi_k$に依存する誤差項を持つ。
双曲空間における連続$k$-中心問題のためのコアセット [cs.CG, cs.DS]目的：双曲空間における連続$k$-中心問題に対するコアセットの構築
- 機械学習やデータ解析において，大規模データセットの効率的な処理が重要な課題となっている
- 双曲空間における距離の計算やデータ構造の設計は，空間の性質上困難を伴う
- 双曲空間における$k$-中心問題に対し，入力サイズに依存しないサイズのコアセットを構築し，効率的な近似解を求める
- 双曲空間における連続$k$-中心問題に対するコアセットを，入力半径に依存しないサイズで構築した。
- 構築されたコアセットのサイズは$(1/\varepsilon)^{O(kD)}$であり，構築時間は$O(nk(1/\varepsilon)^{O(kD)})$である。
- 固定された$D$, $k$, $\varepsilon$に対して，線形時間で定数サイズのコアセットを構築可能である。
競合クラスタ選択子：局所的な曖昧性，正規形，およびバックトラッキングコスト [cs.DS]目的：ランダム制約充足問題におけるバックトラッキングコストの構造的分析
- 制約充足問題は，AI，オペレーションズリサーチ等，幅広い分野で重要な役割を担う。
- 大規模問題に対する効率的な解法は未だ確立されておらず，計算コストが課題となっている。
- バックトラッキングコストの構造を解明し，効率的な探索手法を開発することを目指す。
- 実験結果から，少数の競合クラスタ選択子がバックトラッキングコストの大部分を占めることが示された。
- 高競合性の変数値を固定することで，バックトラッキングを大幅に削減できることが確認された。
- 競合クラスタ選択子は，バックドア，解空間の幾何学，低次数障壁を結びつける構造的プログラムとして位置づけられる。
強連結性と強双連結性に関する問題 [cs.DS]目的：強双連結グラフにおける最小限のエッジ部分集合
- ネットワークの信頼性向上は重要であり，グラフ構造の解析が不可欠である。
- グラフの連結性を維持しつつ，エッジ数を最小化する問題は難しい。
- 特定の頂点を除いても強連結性を保つ最小エッジ集合の算出を目指す。
- 強双連結グラフに対し，与えられた条件を満たすエッジ部分集合の近似アルゴリズムを提案した。
- 提案アルゴリズムは，多項式時間で7近似解を得られることを証明した。
C^2：適応的二進圧縮を用いたキャッシュ効率を考慮した簡潔トライ [cs.DB, cs.DS]目的：簡潔トライのキャッシュ効率と空間効率の改善
- 文字列検索において，メモリ使用量と検索速度は重要な要素である。
- 既存の簡潔トライは，キャッシュミスや冗長なパスにより性能が制限される。
- キャッシュ効率と二進圧縮により，簡潔トライの性能を向上させる。
- C_1最適化により，FST，CoCo-trie，Marisaの検索性能がそれぞれ1.58倍，1.12倍，1.42倍に向上した。
- C_2最適化により，平均してメモリ使用量を1.3倍削減することに成功した。
- C^2を適用した簡潔トライは，既存の簡潔トライや非簡潔トライと比較して，空間と時間のトレードオフを改善した。
限界を知る：法的推論におけるLLMのソルバーおよび自動形式化としての忠実性について [eess.SY, cs.MA, cs.RO, cs.SY, math.DS, eess.SY, cs.SY, cs.AI, cs.CL, cs.LO]目的：法的推論におけるLLMのソルバーとしての忠実性と自動形式化の評価
- 法的判断は高度な推論能力を必要とし，その自動化は効率化と公平性の向上に繋がる。
- LLMの推論能力は高いものの，論理的な推論に基づいているか，単なる近似に過ぎないか不明である。
- LLMによる形式化推論の忠実性を検証し，論理的な誤りを特定・改善すること。
- LLMを用いた分類，形式化推論，Z3ソルバーを用いた形式化推論を比較した結果，形式化推論は精度を向上させるものの，必ずしも忠実な推論を保証するものではないことが示された。
- LLMには，スコープの誤用，制約の無視，Z3コードの生成エラーといった共通の失敗パターンが認められ，形式化推論の信頼性に疑問を投げかけている。
- ベンチマークの精度と論理的な忠実性には根本的なギャップが存在し，LLMの能力には限界があることを明らかにした。
多水準三段論理の平均計算量の再検討：1995年のコーラント技術レポートからLean 4への形式化 [cs.LO, cs.CC]目的：多水準三段論理の平均計算量に関する形式化
- 論理学や人工知能において，推論の計算量は重要な研究課題である。
- 多水準三段論理の平均計算量の分析は複雑で，形式的な検証が困難であった。
- 平均計算量のクラスを形式的に定義し，決定手続きの健全性と部分完全性を証明すること。
- 本研究では，Lean 4を用いて1995年のコーラント技術レポートを再検討し，多水準三段論理の平均計算量を形式的にモデル化した。
- Reischuk-Schindelhauerの平均計算量クラスや，EMLSセマンティクス層，部分的な決定手続きなどをLean 4で実装した。
- 構造的公理を明示的に示すことで，条件付きNP平均完全性や非AvP困難性に関する帰結を導出した。
フィードバック駆動型マルチターン改善によるバイナリ逆コンパイルLLM [cs.SE]目的：バイナリ逆コンパイルの機能的正確性の向上
- 脆弱性発見やマルウェア解析など，セキュリティ分野においてバイナリの理解は不可欠である。
- 既存のLLMベースの逆コンパイラは一度の生成で完結し，元のバイナリとの動作差異が生じやすい。
- コンパイル，実行，入出力テストによるフィードバックを基に，段階的にコードを改善することで正確性を高める。
- AutoDecompilerは，報酬設計と学習戦略により，逆コンパイルを反復的な改善プロセスとして実現した。
- 実験の結果，AutoDecompilerは既存の一回生成型モデルを凌駕し，動作再現率の向上を示した。
- プログラムからのフィードバックを活用する強化学習が，LLMベースのバイナリ逆コンパイルの有効な方向性である。
obliv-clang：C++における現実的な秘匿プログラミング [cs.PL, cs.CR]目的：C++で記述されたプログラムの秘匿性の検証
- 機密データ処理において，タイミング攻撃などのサイドチャネル脆弱性が重要な課題となっている。
- 既存の秘匿プログラミング手法は，C++の複雑な機能を十分にサポートできていない場合がある。
- C++の機能を考慮した秘匿性検証ツールを開発し，実用的な秘匿プログラミングを支援すること。
- obliv-clangは，C++プログラムの秘匿性を網羅的にチェックするコンパイル時検証ツールである。
- 複雑なポインタ構造を含むC++の豊富な機能をサポートし，既存のコードベースとの連携を容易にすることを目指している。
- obliv-clangでコンパイルされたプログラムは，既存の手法と比較して性能が向上することが示された。
Q-READY：ハイブリッド量子古典アプリケーションの実現可能性予測評価 [cs.DC, cs.SE, cs.CE]目的：ハイブリッド量子古典アプリケーションの実現可能性評価手法
- 量子計算は発展途上であり，化学，材料科学，金融など多様な分野での応用が期待されている。
- 既存の量子ハードウェアの制約下では，ハイブリッドアプリケーションの開発が経験則に頼りがちである。
- ハイブリッド量子古典アプリケーションの開発における実現可能性を，実装前に系統的に評価することを目指す。
- Q-READYは，要件モデル化，問題定式化，ワークフロー設計，ハードウェアを考慮した実現可能性評価を含む構造化されたパイプラインを確立する。
- シミュレーションに基づく評価により，現実的な制約下での候補ソリューションの比較を可能にする。
- クレジットポートフォリオの資本評価事例を通じて，Q-READYの有効性を示す。
並列ビットベクトル最適化による最良の抽象変換器の合成 [cs.PL]目的：最適な抽象変換器の合成
- 静的解析の信頼性を高めるためには，適切な抽象変換器が必要不可欠である。
- 既存手法は計算量が多く，大規模な問題への適用が困難である。
- 並列化により，抽象変換器の合成処理を高速化することを目的とする。
- 提案手法Spearは，既存のOMTソルバーよりも多くのインスタンスを解くことができた。
- Spearは，大幅に改善された実行時間を実現した。
- 抽象変換器の合成に並列性を適用した初の試みである。
UXBench：LLM生成UX批評の実行可能性の測定 [cs.SE, cs.AI]目的：LLM生成UX批評の信頼性と実行可能性の評価
- UX評価は製品の品質向上に不可欠であり，ユーザー体験の改善に直結する。
- 既存のUX評価手法はコストや時間がかかる場合があり，自動化が求められている。
- LLMを活用したUX評価の自動化における課題を明らかにし，その有効性を検証する。
- UXBenchは，多様な製品インターフェースに対応したLLMのUX評価能力を測定するためのベンチマークである。
- 評価の結果，LLMのUX批評は一様ではなく，実行可能性に有意な差が見られた。
- モデルは評価項目ごとに異なる改善パターンを示し，インターフェースの種類によって優位性が変動することが明らかになった。
AIサプライチェーン銀河：ライセンス遵守のための3Dビジュアル分析 [cs.CE, cs.SE, cs.AI]目的：機械学習モデルの再利用に伴うサプライチェーンにおけるライセンス遵守状況の可視化と分析
- AI技術の急速な発展により，モデルの再利用が活発化し，複雑なサプライチェーンが形成されている。
- 従来の遵守ツールは，このような大規模で多段階の依存関係ネットワークに対応できていない。
- AIサプライチェーンにおけるライセンスリスクを特定し，遵守状況の監査を効率化すること。
- AIサプライチェーン銀河(AISCG)は，モデルの依存関係を3D空間にマッピングし，ライセンス遵守状況を可視化する。
- Hugging Faceの908,449モデルを分析した結果，55.46%のモデルにライセンスリスクまたはメタデータの問題が確認された。
- アダプター派生モデルではライセンスの省略が56.67%，ファインチューニングではライセンスドリフトが8.05%で発生していることが明らかになった。
視認は選択ではない：LLMエージェントにおけるツール選択失敗に対する注意セグメントの説明 [cs.AI, cs.CR, cs.SE]目的：LLMエージェントにおけるツール選択失敗の原因の解明
- 大規模言語モデル(LLM)エージェントの活用は，複雑なタスクの自動化に不可欠である。
- LLMエージェントは，利用可能なツールの中から適切なものを選択する際に誤りを犯すことがある。
- 本研究は，ツール定義セグメントへの注意メカニズムに着目し，その失敗原因を特定し，改善策を提案する。
- 実際のBFCL失敗例において，モデルは正解のツールに注意を向けることが約80%のケースで確認された。
- プロンプトの修正や読み出し側の介入により，ツールの選択失敗をそれぞれ最大91%まで回復させることができた。
- セグメントごとの注意に基づいた選択器は，BFCLとSeal-Toolsにおいて高い性能向上を示し，各モデルで有意な結果が得られた。
予算制約下のリードタイム不確実性を伴う単一品目ロットサイズ問題 [cs.DS]目的：予算制約とリードタイムの不確実性を考慮した単一品目ロットサイズ問題における生産計画
- 需要変動やサプライチェーンの複雑化により，リードタイムの不確実性は生産計画の精度を低下させる重要な要因である。
- 従来のロットサイズ問題では，リードタイムが確定値として扱われることが多く，現実の不確実性に対応できない場合がある。
- リードタイムの不確実性を予算制約内で管理し，堅牢な生産計画を立案することで，リスクを最小化することを目指す。
- R*基準を適用することで，楽観的なシナリオから悲観的なシナリオまで，多様な生産計画を生成することが可能である。
- 提案されたアルゴリズムと混合整数計画法により，問題の複雑さを軽減し，効率的な解法を提供することを示した。
- 計算実験の結果から，R*基準を用いることで，より多くの候補となる生産計画を検討できることが示された。
大規模MIMOシステムにおける位相雑音の影響と情報老化 [cs.IT, eess.SP, math.IT]目的：大規模MIMOシステムにおける位相雑音による性能劣化の定量化と，それに対する反復受信機の提案
- 次世代移動通信システム実現には，多数のアンテナを用いる大規模MIMO技術が不可欠である。
- 大規模MIMOシステムでは，位相雑音が受信性能を著しく低下させる可能性がある。
- パイロット信号に基づく位相雑音情報の老化が性能劣化の原因となるため，その影響軽減が課題である。
- 本研究では，5G上りリンクの現実的なシナリオにおいて，情報老化が及ぼす影響を定量的に評価した。
- 提案するEMに基づく反復受信機は，位相雑音に関連する情報老化に対して頑健であることがシミュレーションで確認された。
- これにより，大規模MIMOシステムの信頼性と効率性を向上させることが期待される。
オンラインマッチングにおけるKIIDエッジ到着モデル [cs.DS]目的：オンライン確率的マッチングにおけるエッジ到着モデルの研究
- マッチング問題は，資源配分など幅広い分野に応用され，効率的な解決が求められる
- 従来の頂点到着モデルでは，エッジ到着の確率分布が不明な場合，最適なマッチングが困難である
- 既知のタイプグラフから独立同分布にエッジが到着する状況下でのマッチングアルゴリズム性能評価
- 貪欲法は競争比0.5未満にしかならず，提案マッチング法は積分到着率下で1-1/eの競争比を達成する
- 貪欲法と提案マッチング法を組み合わせた二段階アルゴリズムは，積分到着率下で1-1/eより高い競争比を示す
- エッジ到着モデルにおいても，分布が既知であれば1-1/eを超える競争比が達成可能であることが示された
閉包保存忠実度における可逆因果ネットのレート歪み [cs.CL, cs.IT, math.IT]目的：閉包保存忠実度基準下での可逆ロギングに関する意味的レート歪み理論
- データ管理やシステム復旧において，実行履歴の正確な記録と効率的な復元は不可欠である。
- 従来のレート歪み理論は，意味的な情報を考慮せず，データの冗長性や依存関係を十分に捉えられていない。
- 意味的閉包に基づき，可逆ロギングにおける最小限のレートと歪みを理論的に決定することを試みる。
- 意味的レート歪み理論を構築し，実行履歴をログされた事実の有限集合としてモデル化する。
- 特定の削除スキャンによりログは冗長性のないコアと冗長な残差に分解され，残差は情報理論的に不可視となる。
- 可逆因果ネットや素因果構造に対してフレームワークを適用し，数値的に予測を検証する。
UAV通信における符号語再構成による秘密鍵生成の強化 [cs.IT, cs.SY, eess.SY, math.IT]目的：UAV通信のための秘密鍵生成手法
- UAVの急速な発展に伴い，UAV間の通信セキュリティ確保が重要になっている。
- UAVの高い移動度とノイズにより，チャネル推定誤差が生じ，既存の鍵生成性能が低下する。
- チャネル情報の利用効率を最大化し，信頼性の高い鍵生成を目指す。
- 提案手法は，符号語再構成アルゴリズムにより，信頼性の高い鍵と低い鍵を分離する。
- シミュレーション結果から，合法ユーザー間での鍵不一致率が減少し，一貫した鍵生成数が増加することが示された。
- 傍受者に対する鍵一致率を低下させ，システムセキュリティを担保する。
自動Web GUIテストの理解：探索戦略と状態抽象化に関する実証研究 [cs.SE]目的：自動Web GUIテストの有効性に対する探索戦略と状態抽象化の複合的な影響
- Webアプリケーションの品質保証において，自動テストは不可欠であり，その効率化が求められている。
- 探索戦略と状態抽象化がテスト効率に与える影響は明らかではない点が課題である。
- 多様なテスト戦略と状態抽象化手法の効果を比較し，最適な組み合わせの指針を示す。
- 探索戦略はそれぞれ強みが異なり，コードカバレッジ，状態カバレッジ，欠陥検出において補完的な関係にあることが示された。
- 厳密な状態抽象化はモデルベース戦略に有利であり，コンパクトな抽象化は強化学習ベース戦略に適していることが明らかになった。
- LLMベース戦略では，簡潔で機能レベルの履歴表現が最も効果的である。コードカバレッジと欠陥検出能力の相関は弱い。
設計による信頼 ― モジュール化を称賛して：事例研究 [cs.SE]目的：集合適応システムの安全性，信頼性，および信頼性を確保すること
- 複雑化するシステムにおいて，安全性と信頼性は社会基盤を支える上で不可欠である。
- 従来の形式手法では，システムの信頼性を十分に保証することが困難である。
- モジュール化によって設計段階から信頼性を高める方法を提案し，実証すること。
- 本研究では，局所的な原因と結果の関係を持つイベント実行，それらを尊重する時間論理に基づく検証，コンポーネント特性からのシステム特性構成という3つの対策を提案した。
- 事例研究を通じて，信頼性の高いシステム設計におけるモジュール化の利点を示した。
- 今後の課題として，提案されたアイデアの完全な理論的基盤の構築が挙げられる。
Leanによる$K_8(4, 2) = 23$ の証明 [cs.IT, math.IT]目的：オクトナリ覆い符号値$K_8(4, 2) = 23$ の証明
- 符号理論は，情報伝送や誤り訂正において重要な役割を果たす研究分野である。
- 有限体上の符号の具体的な値の決定は，計算コストが高く困難な場合がある。
- Leanを用いて$K_8(4, 2)$ の値を厳密に証明し，計算の信頼性を高める。
- Lean 4を用いて$K_8(4, 2) = 23$ であることを証明した。
- 23個の符号語からなる半径2の符号が$(Fin\:8)^4$ 上に存在することを示した。
- 証明は，Lean内部で完結しており，外部のSATソルバーを使用していない。
メタデータ駆動型サービスのための参照アーキテクチャ：ソフトウェアシステムにおける再利用性の促進 [cs.SE]目的：ソフトウェアシステムにおけるサービス再利用性の促進
- サービス指向アーキテクチャは再利用性を重視するが，クライアント間の構造的異質性が問題となる。
- 類似機能を持つサービスの重複開発は，システムの進化と保守性を阻害する。
- メタデータを用いた参照アーキテクチャにより，サービス再利用を促進し，重複を削減すること。
- 提案アーキテクチャは，メタデータを中核メカニズムとして活用し，異種データへの対応も考慮されている。
- シナリオベース評価と実システムでのケーススタディを通じて，アーキテクチャの有効性が検証された。
- システムの進化において，参照アーキテクチャの変更は少ない，または設定変更程度の軽微なものが多いことが示された。
ランダムグラフにおける隠れた幾何構造の検定 [cs.MS, cs.MA, cs.CL, cs.IT, math.IT, math.PR, math.ST, stat.TH]目的：ランダムグラフに埋め込まれた微弱な幾何学的信号の検出
- グラフ構造は，ソーシャルネットワークや生物学的ネットワークなど，様々な現象のモデリングに不可欠である。
- ランダムグラフ中に隠された構造を検出することは，計算量的に困難である場合が多い。
- 本研究では，ランダムグラフから幾何学的構造を統計的・計算的に検出する限界を明らかにする。
- 検出可能性に関する鋭い情報理論的下界を導き出し，検出が可能な範囲でその限界を達成するアルゴリズムを提示した。
- このモデルは，容易・困難・不可能という相転移を示し，効率的な検出，計算困難な検出，および検出不可能な領域が存在する。
- 低次多項式アルゴリズムは，推測される困難な領域全体で失敗することを示し，統計的実現可能性と計算的実現可能性の間にギャップがあることを示した。
マイクロサービスアーキテクチャにおける組織的結束：複数プロジェクトの実証研究 [cs.SE]目的：マイクロサービスエコシステムにおける組織的結束の概念と，それを定量的に測定するためのアプローチ
- マイクロサービスアーキテクチャの普及に伴い，ソフトウェアのモジュール性と開発組織構造の整合性が重要になっている。
- 既存研究は技術的な特性に焦点を当てており，開発者の活動がサービス境界とどのように関連しているかの検討が不足している。
- 開発者の活動パターンから組織構造を定量的に評価し，マイクロサービス開発の社会技術的構造の理解を深める。
- ペアワイズチーム結束（PTC）という指標を定義し，マイクロサービス内での開発者貢献のバランスと集中度を測定した。
- Spinnakerプラットフォームと6つのオープンソースシステムを分析した結果，コアサービスと周辺サービスの間で組織的結束に体系的な違いが見られた。
- PTCと平均組織的結合（AOC）はプロジェクト間で弱い相関を示し，チーム結束とクロスサービス開発者活動は異なる組織的ダイナミクスを示唆していることがわかった。
タイミング付きビスミレーションに対する証拠と反例 [cs.RO, cs.LO, cs.FL]目的：タイミング付きビスミレーションの検証における証拠と反例の生成
- タイミング付きオートマトンは，離散状態と連続時間の挙動を持つリアクティブシステムの時間的特性をモデル化する上で重要である。
- タイミング付きオートマトンの無限状態空間の扱いにくさ，およびビスミレーションの検証結果の説明不足が課題となっていた。
- タイミング付きオートマトン間の行動の違いを明確に示す証拠および反例の提供を目指している。
- 仮想クロック拡張されたゾーングラフを用いることで，タイミング付きビスミレーションの効率的な検証が可能となった。
- ビスミレーションが成立する場合，両モデルから得られる証拠は両モデルに対して有効であることが示された。
- ビスミレーションが成立しない場合，具体的な行動の違いを示す反例を生成することができる。
ファイニタリー図における双同値性とモデル検査の複雑性 [cs.LO]目的：ファイニタリー図における双同値性判定と図式的パス論理におけるモデル検査の複雑性評価
- 形式手法の分野において，システムの振る舞いを数学的に検証することは，信頼性向上に不可欠である。
- 双同値性判定やモデル検査は計算コストが高く，大規模システムへの適用が課題となっている。
- ファイニタリー図に対する双同値性判定とモデル検査の複雑性をより厳密に決定することを目的とする。
- 既存研究を基盤とし，効率的なETIM（存在的可逆行列の理論）のランダム化アルゴリズムを開発した。
- ファイニタリー図の双同値性判定の複雑性をNEXPまで改善し，図式的パス論理のモデル検査の複雑性をNPと証明した。
- 有限体上の双同値性判定は，より低い複雑度であるPSPACEで判定可能であることが示された。
ユニバーサル符号化への集合形状理論の応用 [cs.IT, math.IT]目的：均一に生成された系列に対するユニバーサル符号化の平均符号長削減
- 情報圧縮は，データ伝送や保存効率を向上させる上で不可欠な技術である。
- 既知の分布に依存しないユニバーサル符号化では，最悪の場合の性能が課題となる。
- 均一系列に対するユニバーサル符号化の性能限界を改善することを目的とする。
- 集合形状理論(SST)変換により，均一に生成された系列の平均符号長をKrichevsky-Trofimovの基準線以下に削減できる。
- SST変換は入力系列を拡張し，その変換インデックスを追加記号として保存することで可逆性を維持する。
- この変換は，適応型算術符号化，LZ78，ハフマン符号化，適応型ANSなど，異なる圧縮アーキテクチャにおいても有効である。
ローカル差分プライバシー下におけるクロスサイロ非匿名化：脅威モデル，相転移，および連携の必要性 [cs.CR, cs.IT, cs.LG, math.IT]目的：クロスサイロ非匿名化における脅威モデルと相転移点の特定
- 個人情報保護は重要であり，特に複数のデータサイロに分散されたデータを取り扱う際には，プライバシー保護が不可欠である。
- 既存の差分プライバシーの合成定理は最悪ケースを想定しており，実際の攻撃成功の閾値を評価するには不十分である。
- 複数のサイロからの情報を組み合わせた攻撃に対する耐性を評価し，非匿名化のリスクを定量化することを目指す。
- クロスサイロ・パーソンレベルDP（XSP-DP）を導入し，基本合成定理がこのモデルでも成り立つことを確認した。
- 非匿名化は，サイロ数kがΘ(log n / epsilon^2)を超えると相転移を起こし，攻撃が成功することが示された。
- サイロ間の連携がない場合，閾値を超えると非匿名化は不可避であり，連携の必要性が確認された。
先行度伝播とハイブリッドAMOエンコーディングによる効率的なMaxSAT-DDD列車再スケジュール手法 [cs.LO]目的：列車再スケジュールの効率化
- 鉄道運行においては，遅延等によるダイヤの乱れが頻発し，安定運用が課題である。
- 従来の列車再スケジュール手法では，計算時間が課題となり，実用性に乏しい場合がある。
- 先行度伝播とエンコーディング最適化により，再スケジュール計算の迅速化を図る。
- 提案手法(MaxSAT-DDD)は，全ての段階的インスタンスを平均23msで解くことができた。
- MaxSAT-Defaultは，コスト削減時間を794msから479msに短縮し，大幅な改善が見られた。
- 難解な連続軌道インスタンスにおいて，最大79.6%の計算時間削減効果が確認された。
リソース，ベンチマーク，問題なし？ 低リソース言語におけるコード生成用LLMの評価と改善 [cs.SE]目的：低リソース言語におけるコード生成用大規模言語モデルの性能評価と改善
- ソフトウェア開発の自動化は，生産性向上に不可欠であり，近年LLMの活用が注目されている。
- 既存研究は高リソース言語に偏っており，データ不足の低リソース言語への対応が課題となっている。
- 実務で生まれるデータが極端に少ない言語（no-resource言語）に対するLLMの適用可能性を探る。
- 新たにno-resource言語のコード生成ベンチマークを３つ構築し，公開した。
- プロンプト設計，事前学習，ファインチューニング等の手法でLLMの性能を検証した結果，事前学習が最も効果的であった。
- 事前学習済みのinstruction-tunedモデルは指示追従性が低下するため，ベースモデルからの再学習と重み差分転移を組み合わせることで性能を向上させた。
混合ブロックマルコフ重ね合わせ伝送符号 [cs.IT, math.IT]目的：ブロックマルコフ重ね合わせ伝送符号の性能向上
- 通信において，信頼性と効率的なデータ伝送は不可欠であるため，高性能な符号化方式が求められる。
- 従来のBMST符号には，エラー伝播の問題やエラーフロアの存在など，性能上の制約が存在する。
- 再帰型と非再帰型BMST符号の長所を組み合わせ，より高性能な符号構造を実現することを目指す。
- 提案手法であるmBMST符号は，従来のrBMST符号と比較して，FERおよびBER性能が向上する。
- mBMST符号は，従来の符号を包含する汎用的なフレームワークであり，新たな符号構造の設計を可能にする。
- mBMST符号は，同等の性能を維持しながら，メモリ要件を低減できる。
LLMを用いたソフトウェアツール探索の迅速レビュー：ログ異常検知の事例 [cs.IR, cs.SE]目的：ソフトウェアツール探索のための迅速レビューパイプラインの確立
- ソフトウェア工学研究の成果はツールであることが多く，その有効性の評価は重要である。
- ツールのメンテナンス状況や動作検証が難しく，実用的なツールを見つけるのが困難である。
- LLMを活用してレビューを効率化し，利用可能なツールを迅速に特定することを試みる。
- LLMによるスクリーニングにより，3233件の論文から569件に絞り込むことに成功した。
- ダウンロード可能な論文470件中，83件のツールを特定し，LLMベースのコーディングエージェントで実行した。
- 24個のツールが正常に動作し，本手法の有効性と効率性（推定4時間の人的労力）が示された。
AI活用システムを設計するプロジェクトベースの授業に関する考察 [cs.SE, cs.AI]目的：AI活用システムの設計と実装における課題と学習成果
- AI技術の進展に伴い，AIを組み込んだシステム構築の重要性が高まっている。
- 機械学習の知識はあるものの，システムアーキテクチャ設計の実践経験が不足している学生が多い。
- AI活用システムのシステムレベルな設計能力とデータ中心的なMLの実践力を育成する。
- 学生の提出物とアンケート調査の結果，アーキテクチャ設計の初期段階における課題が明らかになった。
- 機械学習の統合，要件の変化への対応，データ管理において，学生の知識・経験の不均衡が課題として浮上した。
- 本授業は，システムレベルの思考力とデータ中心型MLの実践に対する意識向上に貢献した。
ニューロシンボリックソフトウェア検証：大規模なシンボリック推論によるローカル言語モデルの能力向上 [cs.SE]目的：ソフトウェアの形式検証におけるループ不変式の自動合成
- ソフトウェアの信頼性確保は重要であり，形式検証はそのための有力な手段である。
- 従来の形式検証手法は，複雑なプログラムに対して不変式の発見が困難であるという課題がある。
- LLMを活用し，不変式合成を効率化することで，大規模プログラムの検証を可能にすることを目指す。
- VerIbmcは，シンボリック推論とローカルで実行可能なオープンウェイト言語モデルを組み合わせたパイプラインである。
- GPT-OSS-120Bを使用した場合，499問題中431問題を解決し，86.4%の成功率を達成した。
- クラウドAPIに依存せず，単一のローカルマシン上でプライバシーを保護しつつ，効率的な検証を実現する。
ガウスネットワークにおけるエッジ非交差ハミルトンサイクル構築のための統一的な定数時間スイッチング規則 [cs.DC, cs.DM, cs.IT, cs.NI, math.IT]目的：ガウスネットワークにおけるエッジ非交差ハミルトンサイクル構築のための統一的な方法
- ガウスネットワークは並列計算機や通信ネットワークのモデルとして重要であり，効率的なネットワーク設計が求められている。
- 既存手法は，パラメータの条件によって証明が複雑化し，ケース分けが必要となる場合があった。
- 本研究は，パラメータ条件に関わらず適用可能な，簡潔かつ効率的なハミルトンサイクル構築法を提供する。
- 本研究では，行数d，列数rの長方形表現において，各列に対して定数時間で実行可能なローカルスイッチング規則を提案した。
- このスイッチング規則により，ガウスネットワーク内のエッジセットが，2つのエッジ非交差ハミルトンサイクルに分割可能となる。
- 提案手法は，パラメータa, bに関してa≦b≦100までの全範囲と，N=3,250,000までの大規模な検証によって有効性が確認された。
記号的非形式化：流暢，生産的，多言語 [cs.AI, cs.CL, cs.LO]目的：形式数学から自然言語への信頼性の高い変換
- 厳密性が求められる数学の概念を，より多くの人が理解できるようにする必要がある
- 形式的な証明の内容を人間が読みやすい形で表現する手段が限られていた
- 人工知能による証明の構造を説明し，多言語対応を可能にすること
- Informathプロジェクトは，DeduktiとGrammatical Frameworkを連携させることで，複数の形式証明システムと自然言語間の変換を実現する
- このアプローチにより，流暢なテキストを比較的少ない労力で生成し，形式性と自然言語の正確性を両立させる
- その結果，機械検証された内容を，精度の低下なく人間が理解できる形式で提示することが可能になる
高密度ガウスネットワークにおける再ルーティングに基づく耐障害ブロードキャスト [cs.RO, cs.DC, cs.IT, cs.NI, math.IT]目的：高密度ガウスネットワークにおける，ノード障害に強いブロードキャスト手法
- 高密度ガウスネットワークは，効率的な全ノードへのブロードキャストに適した構造を持つため，大規模分散システムで重要である。
- ノード障害が発生した場合，特に内部転送位置に障害が発生すると，ブロードキャストが中断されるという課題がある。
- 障害ノードをブロードキャストの葉レベルに追いやる再ルーティングにより，耐障害性を実現することを目的とする。
- 提案手法は，冗長なスパニングツリーやバックアップ経路構造を構築せず，動的に送信元を再選択することで耐障害性を実現する。
- 単一障害の場合，障害ノードからのグラフ距離kの境界から新しい送信元を直接選択する。
- 二重障害の場合，任意の障害ノードペアに対して，両方からグラフ距離kにあるノードが存在することが証明された。シミュレーションにより，提案手法の有効性が確認された。
構成的選好関係：線形時間論理縮小における未決定性の克服 [cs.LO]目的：非古典論理，特に線形時間論理における認識的選好関係の計算的側面
- 信念縮小は合理的推論の基礎であり，情報更新や知識表現において重要である。
- 線形時間論理における選好関係の構成は，通常自明とされているが，実際には困難である。
- 線形時間論理における信念縮小を有効化するため，必要な条件を満たす選好関係を構築する。
- 線形時間論理において，選好関係の主要な条件が決定不能であることが示された。
- 距離測度を一般化したり，選好関係を階層的に構成するなど，新たな選好関係構築手法が提案された。
- これらの手法は，線形時間論理だけでなく，古典論理における選好関係の幅も広げ，完全な合理性を実現する。
エージェントの軌跡をプログラムとして：行動のフィンガープリントとコーディングエージェントのプログラミング [cs.SE, cs.LG]目的：エージェントの行動特性の識別と，その行動パターンを記述する手続き的表現の開発
- AIエージェントの性能評価は重要だが，その達成方法の理解は不可欠である。
- 現在の評価指標は成功/失敗のみに焦点を当てており，エージェントの内部プロセスはブラックボックスのままになっている。
- エージェントの行動特性を定量的に把握し，モデル間の差異を明確にすること。
- エージェントの軌跡から行動のフィンガープリントを抽出し，未知の軌跡を高い精度(85.7%)で識別可能であることが示された。
- エージェントの軌跡を手続き的に表現することで，モデル間の行動の類似性を定量化し，リリース時期や蒸留関係が類似性に影響を与えることが明らかになった。
- ProcGrepというエージェント監査・評価ライブラリを開発し，タスクへのアプローチを手続きレベルで分析可能にした。
シグナルなし選択，表現による回復：フローズン小規模コードモデルに対する事後検証演算子の測定研究 [cs.SE, cs.CL, cs.LG]目的：フローズン小規模コードモデルにおける事後検証演算子の有効性評価
- オフライン環境やプライバシー制約下でのコードモデル利用が重要視されている。
- 小規模コードモデルは，しばしば妥当だが誤ったプログラムを出力する。
- 事後検証演算子によるプログラムの選択，検証，修正，再処理の効果を測定する。
- 26種類の事後検証演算子を評価した結果，どの演算子もBest-of-Nを超える精度改善は見られなかった。
- その原因として，カバレッジの壁，能力のハサミ，コンセンサスの罠の存在が示された。
- 表現層の回復演算子(M1)は，従来の抽出器が見逃す正解プログラムを回復し，DeepSeek-Coder-1.3BのHumanEval+での性能を向上させた。
平面におけるグロモフ・ハウスドルフ距離の定数因子近似 [eess.SY, cs.SY, math.OC, cs.CG, cs.DS, math.MG]目的：有限点集合間のグロモフ・ハウスドルフ距離の定数因子近似
- 幾何学的な形状比較において，グロモフ・ハウスドルフ距離は重要な指標となる。
- 高次元空間におけるグロモフ・ハウスドルフ距離の効率的な近似アルゴリズムは未解決だった。
- 平面におけるグロモフ・ハウスドルフ距離の多項式時間近似アルゴリズムを開発すること。
- 本研究では，平面上の有限点集合間のグロモフ・ハウスドルフ距離を，多項式時間で定数因子近似するアルゴリズムを初めて提案した。
- このアルゴリズムは，双射型グロモフ・ハウスドルフ距離の近似に基づき，加法的な歪みを最小化する。
- 「太い集合」または「ほぼ共線集合」の二分法により，効率的な近似を実現している。
記号実行トレースによるLLMへのプログラム意味論の教授 [cs.SE, cs.LG, cs.LO, cs.PL]目的：LLMに対するプログラム意味論の教授
- 大規模言語モデルの進化は，ソフトウェア検証を含む多様な分野に影響を与えている。
- LLMはプログラムの性質を正確に確認できるものの，違反の検出精度に課題がある。
- 記号実行トレースを用いてLLMを訓練し，違反検出能力の向上を目指す。
- 500件のC言語検証タスクで評価フレームワークを構築し，14種類のモデルを評価した。
- 約3,000件のバグトレースとChain-of-Thought推論を組み合わせることで，違反検出率が17%以上向上した。
- 訓練された8Bモデルは，4倍サイズのQwen3-32Bモデルを凌駕し，全体的な精度も近づいた。
q指数ランダムグラフ：単純な制約からの高次ネットワーク [physics.soc-ph, cond-mat.dis-nn, cond-mat.stat-mech, cs.IT, math.IT, physics.data-an]目的：q指数ランダムグラフの一般化
- ネットワーク構造の解析は，社会科学，生物学，情報科学など多岐にわたる分野で不可欠である。
- 従来のERGMは，シャノンのエントロピーに偏った仮定に基づいている可能性があり，より客観的なモデルが必要とされていた。
- シャノンのエントロピーに囚われない，より広範なエントロピーに基づくネットワークモデルを構築し，その特性を明らかにすること。
- q指数ランダムグラフでは，従来のERGMには見られない疎な状態と密な状態の間の相転移が観察された。
- また，リッチなアソートメントとクラスタリングプロファイルが確認され，リンクの疎さと三方閉包の共存が可能になった。
- これらの結果は，高次ネットワークがより単純な制約から自然に生じうることを示唆している。
AIネイティブ6Gネットワークのための説明可能なタスク指向型トークン通信 [eess.IV, cs.CV, cs.IT, math.IT]目的：タスク指向型トークン通信フレームワークの提案
- 無線通信における画像伝送は，タスク指向型へと進化を遂げている。効率的な通信が求められている。
- 既存手法では，タスク指向型トークン表現の不足，視覚トークンとタスクトークンの連携不足が課題となっている。
- 視覚情報とタスク意図を統合し，タスクに基づいた効率的な画像伝送と解釈可能性の向上を目指す。
- 提案フレームワークET-TokenComは，視覚トークンとタスクトークンを統合的に扱うことで，端から端までの通信リンクを構築する。
- クロスモーダルアテンション機構により，タスクトークンが視覚トークンの選択と伝送を明示的に制御し，タスク目標に応じた重要領域を強調する。
- シミュレーション結果は，提案手法の有効性と堅牢性を示すとともに，タスク目標と出力の関連性を示唆する。
平面アレイと多次元中国剰余定理を用いた移動目標SAR画像化--第I部：汎用フレームワーク [eess.SP, cs.IT, math.IT]目的：平面アレイを用いた移動目標SAR画像化における汎用的なフレームワークの構築
- SAR画像化は，地形や気象条件に左右されず目標を認識できるため，軍事・民生用途で重要である。
- 移動目標のSAR画像化では，目標の移動によるクロスレンジシフトと高度の同時推定が課題となる。
- 本研究は，多次元中国剰余定理を用いて，推定範囲を拡大し，より正確なパラメータベクトルを復元することを目指す。
- 提案手法では，平面アレイと多次元中国剰余定理を組み合わせることで，単一アレイでは困難な範囲外のパラメータ推定を可能にする。
- 2D-DFT行列のモジュラスを最適化することで，ベクトル剰余誤差の伝播を抑制し，復元精度を向上させる。
- 数値シミュレーションにより，提案するマルチサブアレイフレームワークが，単一平面アレイと比較して不明瞭範囲を拡大することが確認された。
平面アレイと多次元中国剰余定理を用いた移動目標SAR画像化--第2部：2つのサブアレイ設計 [eess.SP, cs.IT, math.IT]目的：移動目標SAR画像化のための平面アンテナアレイと多次元中国剰余定理(MD-CRT)を用いた2つのサブアレイ設計
- SAR画像技術は，高分解能なリモートセンシングを実現し，災害監視や資源探査など幅広い分野で不可欠である。
- 移動目標のSAR画像化は，ドップラー効果による像のぼやけや位置ずれが課題となり，高度な信号処理が必要となる。
- 本研究は，MD-CRTを用いた平面アレイ設計により，移動目標の正確なSAR画像化を可能にすることを目的とする。
- 共通スケーリングを用いた2つのサブアレイ設計において，整数周波数ベクトル上で曖昧性解消が可能となり，第1部と同等の範囲解像度を維持する。
- 平面アレイ枠組みは，従来の分離型スキームと比較して，ロバストな復元のための十分条件が緩和され，再構成誤差の上限がより厳密になる。
- アレイ形状が復元性能に影響を与え，非分離型平面アレイ形状は，同程度のアンテナ数で分離型よりもロバスト性を示す。
事前情報なしオンライン資源配分に対する現代的な原始・双対フレームワーク [math.OC, cs.DS]目的：事前情報なしオンライン資源配分におけるアルゴリズム設計と解析
- 資源配分は，経済，情報科学など広範な分野で不可欠であり，効率的な配分が重要である。
- 不確実な状況下では，従来の最適化手法では十分な性能が得られない場合がある。
- 不確実性下での競争比評価を可能にする汎用的な証明システムを提供する。
- 線形計画法に基づく原始・双対フレームワークにより，貪欲性とヘッジングのトレードオフを捉えることが可能となった。
- 標準的な線形計画緩和が弱かったり，確率的な結果に対して扱いにくかったりする場合に対応できるLPフリーのフレームワークが導入された。
- オンライン頂点重み付き二部マッチング，オンラインエッジ重み付きマッチングなど，幅広いモデルに対応可能な汎用的な証明テンプレートが提供された。
幾何学的制約に基づく分散型独立ベクトル分析 [eess.AS, cs.IT, math.IT]目的：分散型マイクロホンアレイにおける音源分離
- 複数マイクロホンからの情報活用が，音源分離の性能向上に不可欠である。
- アレイ間の一貫性の欠如が，分散型独立ベクトル分析の性能を制限している。
- 幾何学的制約と新たな音源モデルにより，アレイ間の一貫性を高め，分離性能を向上させる。
- 提案手法は，音源到来方向情報を用いることで，アレイ間の置換不整合を軽減し，音源の整合性を高める。
- 新たな音源モデルにより，アレイ間の依存性を弱め，ノイズ環境下でのロバスト性を向上させる。
- 実験結果から，提案手法が分離性能とアレイ間の一貫性の両方を改善することが示された。
ウェーブレット局所化とMRW展開における局所的変調固定化 [cond-mat.stat-mech, cs.IT, math.IT, physics.data-an]目的：多重フラクタル確率過程展開のための局所化ウェーブレット定式化
- 確率過程の解析は，自然現象や金融データなど，様々な分野で重要な役割を果たす。
- 従来のMRW展開では，変調場の影響により，局所的な構造解析が困難であった。
- ウェーブレット局所化による変調固定化により，局所的な確率構造の解析を可能にすることを目指す。
- 局所化ウェーブレットを用いることで，変調成分が効果的に固定化されることが示された。
- ウェーブレット振幅の対数値は，局所的なウェーブレット統計と基盤となる変調場の間の加法分解を近似的に示す。
- ウェーブレットのサポート形状，スケール依存的なオーバーラップ，内部変調の混合が，共分散スケーリングからのずれに影響することが確認された。