arXiv雑要約
プログラム - 2026/06/03 公開
Lean-GAP：大学院レベル代数問題の形式化データセット [cs.LO, cs.AI, cs.PL]目的：大学院レベル代数学の形式化問題のデータセット
- 数学の自動検証は，定理証明や数学教育に革新をもたらす可能性を秘めている。
- 教科書レベルの数学問題を形式化するには，時間と労力がかかる。
- 形式化パイプラインを構築し，形式化の課題を分析することで，効率化を目指す。
- DummitとFooteの「抽象代数」の大学院レベルの問題430問を形式化したデータセットLean-GAPを構築した。
- PDFからLaTeXへの前処理，Lean 4への自動形式化，および非公式-公式の対応検証からなるパイプラインを開発した。
- 自動形式化モデルの性能を比較し，非公式な記述を形式言語に翻訳する際のボトルネックを特定した。
Rocqからメタルへ：形式検証されたマイクロコントローラファームウェアのパイプライン [cs.PL, cs.LO, cs.SE]目的：形式検証されたマイクロコントローラファームウェアの実現
- 安全性確保が重要視されるシステムにおいて，AI生成コードの利用が拡大している。
- 高水準の仕様言語をサポートする実行環境は，組み込みターゲットに対して大きすぎる。
- Rocqを用いた形式検証により，今日のマイクロコントローラ上でファームウェアを検証可能にする。
- Encore!という，Rocqで抽出されたSchemeをマイクロコントローラ上で実行する，ベアメタルCPS VMを開発した。
- ファームウェアを純粋な状態遷移関数として構造化することで，コア部分をRocqで完全に検証可能にした。
- LLMを活用した戦術合成は，形式定理の記述に置き換わり，AI生成ファームウェアの自己証明を可能にする。
データストリームにおける近似最近傍探索のためのオンラインK-d木 [cs.CL, cs.DS]目的：データストリームにおける近似最近傍探索の効率化
- 機械学習応用に広く用いられるkNNアルゴリズムの性能向上は重要である。
- 大規模データに対する近傍探索の計算コストが課題となっている。
- データストリーム環境下でのK-d木の動的な更新と効率的な探索を実現する。
- 提案手法であるオンラインK-d木は，データストリーム環境下で高速な処理時間を実現した。
- Canberra距離への適応により，効果的な部分木刈り込みが可能となり，処理性能が向上した。
- わずかな精度低下を伴いながら，処理速度は大幅に改善された。
ビジネス中心LLMシステムに対する受容テスト駆動型評価プロトコル [cs.SE, cs.AI]目的：ビジネス中心のLLMシステムの評価プロトコル
- LLMの社会実装が進む中で，安全性，信頼性，説明責任が重要となる。
- 従来のベンチマークでは，確率的な生成要素を持つLLMの要件を満たすことが困難である。
- 受容テスト駆動開発に基づき，LLMのガバナンスと実用性を高める評価プロトコルを確立する。
- 受容テスト駆動型開発をLLM開発に取り入れ，変化管理のサイクルを「赤-訓練-緑」とした。
- ステークホルダーの目標を，実行可能な行動規範，リリース条件，監視信号，証拠成果物へ変換する。
- 受容テスト駆動型開発，プロンプト優先型，ベンチマーク後評価のワークフローを比較する指標群を提案した。
説明責任のあるソフトウェアシステム設計に関するワークショップ報告 [cs.SE]目的：ソフトウェアシステムにおける説明責任に関する知識の体系化と研究方向性の特定
- ソフトウェアは社会インフラとして不可欠であり，その信頼性と透明性が重要である。
- ソフトウェアの設計・開発における説明責任の概念が曖昧で，実用的な指針が不足している。
- 組織内の責任の明確化や，法規制とソフトウェア設計の連携を深めることが求められている。
- 本ワークショップの結果，説明責任を果たす組織において，定義と責任の明確化が不可欠であることが示された。
- ソフトウェア設計プロセスへの説明責任構造の組み込みと，関係者との連携改善に関するさらなる研究が必要とされた。
- 学際的な研究チームの編成・維持，および研究方法や成果の伝達における課題が明らかになった。
組合的シンプレックス上のリード・ミュラー型符号：代数的記述 [cs.IT, math.IT]目的：組合的シンプレックスとそのCAP符号の解析
- 符号理論は，情報伝送やデータ保存における信頼性を確保する上で不可欠な研究分野である。
- 従来のリード・ミュラー符号では，高い符号レートを達成することが困難であった。
- 組合的シンプレックスに基づくCAP符号の代数的な性質を解明し，効率的な符号設計に貢献する。
- 組合的シンプレックスの消失イデアルに対する普遍的なグロブナー基を提示した。
- CAP符号の一般化ハミング重みを，消失イデアルのフットプリントを用いて記述した。
- 最小距離の場合において，閉じた形の公式を証明し，CAP符号の双対を生成する多項式集合を明らかにした。
Clefプログラミング言語における不動点足場 [cs.PL, cs.LO, math.CT]目的：Clefプログラミング言語のコンパイラにおける不動点コンビネータの利用
- プログラム言語の正当性確保は重要であり，特に構造的性質を持つ言語においては不可欠である。
- 従来のコンパイラでは，プログラムの構造的性質が失われる可能性があり，検証が困難となる場合がある。
- 本研究は，コンパイラを通してプログラムの構造的性質を維持し，検証を容易にすることを目指す。
- Composerコンパイラは，プログラム意味グラフ（PSG）から得られる次元，等級，脱出，数値表現の構造を不動点コンビネータによって保存する。
- MLIRの静的単一代入，属性システム，方言といった特徴が，構造を具現的に保持する役割を担っている。
- 本研究では，Ohoriの機械コード証明論，パラメトリック性，随伴モード論を基盤とし，負と分数の型を導入することで，型機構を構造を維持したまま実現している。
ダイヤモンドは永遠に：Logicaにおける制限なし集約と再帰のための安定意味論 [cs.LO]目的：制限のない集約と再帰を持つLogicaプログラミング言語の安定意味論
- データベースやAIにおける論理プログラミングの重要性が増しており，より表現力豊かな言語が求められている。
- 従来のDatalogでは集約と再帰の自由な組み合わせが難しく，複雑なアルゴリズムを簡潔に表現できない。
- 集約が置換によって更新されるLogicaのような言語における意味論的課題を解決し，厳密な意味を与える。
- 本研究では，非単調論理プログラムのための安定化ベースの枠組みであるDefendant-Opponent (DO) 意味論を提案する。
- DO意味論は，正のDatalogにおける最小固定点意味論，Well-Founded，Stable Model Semanticsと一致する。
- 固定点に達することなく収束するプログラムに対し，ω-limit解釈によってPageRankのような反復計算に厳密な意味を与える。
公開計測データからの情報漏洩量の定量化 [cs.RO, cs.HC, cs.CR, cs.IT, math.IT]目的：公開科学データおよび計測データの情報漏洩リスクの定量評価
- 科学的データの信頼性は重要であり，その安全性確保は科学研究の進展に不可欠である。
- 公開データに含まれる微細な情報から，機密設定が漏洩する可能性が指摘されている。
- 公開データの情報漏洩リスクを定量的に評価し，安全なデータ公開のための指針を示す。
- 公開データから漏洩する情報を統計的側路攻撃として捉え，漏洩量の評価手法を確立した。
- 特定の条件下において，情報漏洩量を正確に定量化する「有限バンド輸送漏洩則」を導出した。
- 極端紫外線（EUV）粗さスペクトルデータを用いて検証を行い，手法の実用性を示唆した。
非凸から強凸へ：オンライン最適化のための曲率適応型FTPL [cs.LG, cs.DS]目的：オンライン最適化における曲率適応型FTPLアルゴリズムの開発
- オンライン最適化は，変化する環境下での意思決定において重要な役割を果たす。
- 従来のFTPLは，非凸損失関数の場合，曲率を考慮していないため，性能が制限される。
- 曲率の情報を活用することで，より効率的なオンライン最適化を実現することを目指す。
- 提案手法は，任意の非凸Lipschitz損失関数に対して$O(\sqrt{T})$のレグレットを達成する。
- 累積曲率の増加に伴い，レグレットが改善され，線形的に増加する場合には$O(\log T)$のレグレットを達成する。
- 提示されたレートは，特定の累積曲率シーケンスに対する下限と一致し，トレードオフが本質的であることを示す。
塵も積もれば山となる：Androidアプリ開発におけるデータ最小化原則のコード中心の実証研究 [cs.SE]目的：Androidアプリ開発におけるデータ最小化原則の実現状況の分析と，プライバシーに配慮した開発を支援するためのコーディングガイドラインの抽出
- モバイルアプリは大量のデータを扱うため，プライバシー保護は重要課題である。規制遵守の必要性も高まっている。
- 従来のプライバシーポリシー分析では，開発者がコードレベルで対応するための具体的な指針が不足していた。
- データ最小化原則に着目し，開発者が実践可能なガイドラインを提供することで，プライバシーコンプライアンスを向上させる。
- 1,114件のオープンソースAndroidアプリを調査し，データ処理の各段階における10種類のデータ最小化シナリオを特定した。
- 9,875件の実アプリを分析し，プライバシーに配慮した開発を支援するための31のコーディングガイドラインを抽出した。
- LLMによるコード生成は，データ最小化のリスクのあるパターンを再現する傾向があるが，本研究のガイドラインを組み込むことで問題は解消された。
マルチモーダルユーザーインターフェースツールキットのベンチマークフレームワーク：モダリティ網羅性，開発ワークフロー，および実験的サポートの比較 [cs.CL, cs.HC, cs.SE]目的：マルチモーダルユーザーインターフェースツールキットの比較と評価のためのフレームワーク
- 多様な入力モダリティを組み合わせたインターフェースが普及し，その開発効率化が求められている。
- 既存のツールキットの機能や使い勝手に関する体系的な比較評価が不足している。
- ツールキットの比較評価を可能にする，再利用可能なベンチマークテンプレートを提案する。
- 本研究では，モダリティ網羅性，開発ワークフロー，実験的サポートの３つの側面からツールキットを評価するフレームワークを提示した。
- Geno, MSP, ReactGenie, WAMI, EmoSyncの５つの代表的なツールキットを用いてフレームワークの適用例を示した。
- このフレームワークは，今後の研究者が実験的測定や開発者調査によって具体化できる再利用可能なテンプレートとして活用できる。
単一誤り訂正アナログ符号の限界 [cs.IT, math.IT]目的：単一誤り訂正アナログ符号における性能パラメータの限界
- アナログ符号は，ノイズの影響を受けやすい現実世界の通信において重要な役割を果たす。
- 誤り訂正符号の性能限界は，効率的な符号設計のために不可欠な情報である。
- 冗長性二つの単一誤り訂正アナログ符号の最適性に関する未解決問題の解決を目指す。
- 実線形$[n, n-2]$符号に対する$\Gamma_2(\mathcal{C})$の下限を$\frac{1}{\sin^2(\pi/2n)}$と証明した。
- これにより，Rothの未解決問題が解決される。
- 固定冗長性$r \ge 2$を持つアナログ符号クラスに対して，$\Gamma_2(\mathcal{C})\le O\left(n^{1+\frac{1}{r-1}}\right)$が成り立つことを示した。
SkillGuard：エージェントスキルに対する許可フレームワーク [cs.CR, cs.SE]目的：エージェントスキルの許可管理
- LLMエージェントの能力拡張に不可欠なスキルエコシステムの安全性が重要である。
- スキルの実行時に意図しない動作やセキュリティリスクが発生する可能性がある。
- スキル実行時の挙動と宣言された意図の乖離を防ぎ，スキルエコシステムの安全性を高める。
- SkillGuardは，スキルを許可を持つ実行可能アーティファクトとして扱い，二重のガバナンスモデルを導入する。
- 315のスキルとSkillInjectを用いた評価で，保護対象の99.76%を網羅する許可タクソノミを確立した。
- 敵対的評価では，文脈注入と明白な注入に対する攻撃成功率をそれぞれ減らし，有用性は維持された。
MCMC混合のための局所的・大域的収縮原理 [cs.CL, cs.IT, math.IT, math.ST, stat.CO, stat.ML, stat.TH]目的：MCMCアルゴリズムの混合時間評価のための収縮に基づく枠組み
- 統計的推論において，マルコフ連鎖モンテカルロ法は複雑な分布からのサンプリングに不可欠である。
- MCMCの収束速度の評価は難しく，特に高次元や重い尾を持つ分布では困難である。
- 提案手法は，MCMCの収束速度をより厳密に評価し，幅広い分布に対応することを目指す。
- $\mathsf E_\gamma$-divergenceを用いた，局所的・大域的収縮係数に基づく新しい枠組みを開発した。
- コンパクト凸領域上の射影ランジェバンモンテカルロに対し，ガウス平滑化が明示的な大域的収縮係数を与えることを示した。
- 独立メトロポリス・ハスティングス法に対しては，局所的収縮係数を用いることで，重い尾を持つ分布においても有効な収束限界を得た。
回転アンテナと多重アクセス：NOMAかOMAか [cs.IT, cs.SY, eess.SY, math.IT]目的：回転アンテナを用いた通信システムにおけるNOMAとOMAの性能比較
- 周波数資源の有効活用が重要視される中，空間的多様性を活用する技術が求められている
- 回転アンテナの指向性制御能力を最大限に活かす多重アクセス方式は明確でない
- 回転アンテナを用いる際の最適な多重アクセス方式を検討し，電力効率を向上させる
- 回転アンテナを用いることで，固定アンテナと比較して送信電力を大幅に削減できることが示された
- 対称的なユーザ配置においては，NOMAがTDMAよりも劣る場合がある
- 非対称的なシナリオでは，NOMAが優れた堅牢性とエネルギー効率を示す
ZX計算：トレース索引依存型と認識意味論 [cs.LO, cs.CL]目的：トレース索引型，プレシェーフ非単調意味論，構成的AGM信念修正を統合した，マルティン・レーフ依存型理論の保守的拡張であるZX計算
- 計算と意味論の基礎研究は，情報科学および論理学の発展に不可欠である。
- 信念修正は，矛盾する情報への対処が困難であり，理論的な枠組みが十分に確立されていない。
- トレース索引型と非単調意味論を組み合わせることで，信念修正のより正確なモデル化を目指す。
- ZX計算におけるトレース型は，イベントラベルを明示的に扱い，イベント駆動型帰納法を容易にする。
- ZX計算では，証明理論的な単調性と意味論的な非単調性の区別が明確にされ，分離定理が示された。
- AGM信念修正の全8つの公理が定理として証明され，経路依存性と函手一貫性の間の緊張が明らかになった。
SPOQ：マルチエージェントソフトウェアエンジニアリングのためのスペシャリストによるオーケストレーションキューイング [cs.SE, cs.MA]目的：マルチエージェントAIシステムによるソフトウェアエンジニアリングタスクの自動化における，効率と品質の向上
- ソフトウェア開発の効率化と品質向上は，経済発展と技術革新に不可欠である。
- 既存のアプローチでは，調整のオーバーヘッド，品質管理のギャップ，そして人的監督の不足が課題となっている。
- SPOQは，タスク依存グラフに基づいた並列実行，二重検証ゲート，そして人間による介入によって，これらの課題を解決する。
- SPOQのウェーブディスパッチは，クリティカルパスの理論限界に近い性能を示し，最大14.3倍の高速化を実現した。
- SPOQは計画カバレッジを93.0%から99.75%に向上させ，計画の循環を排除し，並列性を高めた。
- 二重検証ゲートはタスクあたりの欠陥数を0.34から0.20に削減し，テスト合格率を91.25%から99.75%に向上させた。
並列メトリックスキップリストと最近傍探索 [cs.DS]目的：メトリック空間における効率的な最近傍および$k$最近傍探索のためのデータ構造であるメトリックスキップリストの構築
- 大規模データセットにおける類似検索は重要であり，効率的なデータ構造が求められている。
- 既存のメトリックスキップリストの構築は逐次的な処理であり，並列化が困難であった。
- 本研究は，メトリックスキップリストの並列構築アルゴリズムを開発し，効率性と並列性を両立させる。
- 本研究で提案する並列アルゴリズムは，期待作業量が$O(n \log n)$，スパンが多対数関数で，高い確率で実現される。
- このアルゴリズムは，分割統治法を利用することで並列化を促進しつつ，効率性を維持している。
- 二色最近対問題や密度ベースクラスタリングなど，最近傍探索を基盤とする応用分野においても改善された結果が得られる。
HRNN：高次元ベクトルにおける近似最近傍逆検索のためのハイブリッドグラフインデックス [cs.DB, cs.DS]目的：高次元ベクトルに対する近似最近傍逆検索の効率化
- 高次元データ解析において，類似データ検索は重要な課題である。効率的な検索手法が求められている。
- 従来の最近傍逆検索手法は，高次元空間において候補の膨大化や検証コストの問題を抱えている。
- HRNNは，これらの問題を解決し，高次元ベクトルにおける逆検索の性能向上を目指す。
- HRNNは，ナビゲーショングラフ，ランキングKNNグラフ，逆近傍リストを組み合わせたハイブリッドインデックスを用いる。
- これにより，効率的なプロキシ検索，候補生成，kNN半径へのアクセスを実現している。
- 実験の結果，HRNNは既存手法と比較して，スループットが最大10倍向上することを示した。
ピンチングアンテナがトラフィックオフローディングに与える影響 [cs.IT, math.IT]目的：ピンチングアンテナを用いたトラフィックオフローディングの実現
- 無線通信におけるセル境界の柔軟な再構成が重要視されている。
- 既存のセル構造では，トラフィック集中による通信品質の低下が課題である。
- ピンチングアンテナによるセル再構成で，効率的なトラフィックオフローディングを目指す。
- ピンチングアンテナは，強力な直達接続を可能にし，柔軟な多重アンテナシステムを実現する。
- 提案するトラフィックオフローディング戦略は，エネルギー消費量を削減し，セルリソースの利用バランスを改善する。
- シミュレーション結果から，ピンチングアンテナがトラフィックオフローディングを効率的にサポートすることが示された。
符号付きジョンソングラフにおける独立集合の分類と，密接配置への応用 [cs.CL, cs.RO, cs.RO, cs.IT, math.CO, math.IT]目的：符号付きジョンソングラフにおける最大独立集合の分類
- ジョンソングラフは，定数重み符号，極値組み合わせ論，組み合わせ幾何学において重要な役割を果たす
- 古典的なジョンソングラフの符号付き類似である符号付きジョンソングラフの研究は十分に進んでいない
- 符号付きジョンソングラフにおける最大独立集合の構造を明らかにすることで，密接配置の多様性を探求する
- n≦12, n≠11において，符号付きジョンソングラフJ±(n,4)における全ての最大独立集合を符号付き置換まで計算するアルゴリズムを開発した
- 特にn=12の場合，1579個の非同型な最大独立集合を特定し，それらは全て${\mathbb R}^{12}$におけるサイズ840の非等距な密接配置に対応する
- n≡2,4 (mod 6)の場合，全ての最大独立集合はシュタイナー四重系に由来することを示し，非自明に自己整合的な符号の特性付けを得た
シングルRF MIMO-OFDMシステム向け新規検出手法 [cs.IT, math.IT]目的：シングルRF MIMO-OFDMシステムにおける新規な検出手法
- 無線通信技術は現代社会の基盤であり，高効率化・高信頼化が求められている。
- 再構成可能アンテナを用いる場合，モデリング誤差がBERのボトルネックとなる。
- 再構成可能アンテナ由来のエラーフロアを軽減し，BER性能を向上させる。
- 本研究では，マハラノビス距離に基づく最大尤度検出手法を提案した。
- シミュレーション結果から，提案手法がエラーフロアを効果的に抑制し，高SNR領域でのBERを低減できることを確認した。
- ESPARアンテナを用いた検証により，提案手法の有効性が示された。
AlgoTouch：命令型プログラムの漸進的構築における実行中心のアプローチ [cs.SE]目的：命令型プログラムの漸進的構築
- 命令型言語のプログラム開発は依然として主流であり，その効率化が求められている。
- 従来のテキストコードによる構築は，認知負荷が高く，初期段階でのエラーが起こりやすい。
- プログラムデータの直接操作を通じて，実行に基づいた漸進的な構築を目指す。
- AlgoTouchは，プログラムデータを直接操作することで，命令型プログラムを漸進的に構築するシステムである。
- 実行行動から制御構造を決定的に合成し，部分的なプログラムの実行，改良，完成を可能にする。
- Python，C，C++，Javaを含む複数の言語で，正しく読みやすいプログラムを自動生成する。
BlobShuffle：Kafka Streamsを用いたストリーム処理システムにおける，オブジェクトストレージを介した費用対効果の高い再分割 [cs.DL, cs.CL, cs.DC, cs.DB, cs.PF, cs.SE]目的：ストリーム処理システムにおける費用対効果の高いデータ再分割手法
- 大規模分散環境でのステートフル処理にはデータの再分割が不可欠であり，クラウド利用の拡大に伴い重要性が増している。
- 従来の再分割は，可用性ゾーン間での大量のネットワークトラフィックが発生し，コストと運用負荷が高いという課題があった。
- クラウドオブジェクトストレージを活用し，ネットワークコストを削減しつつ，低遅延な再分割を実現することを目指す。
- BlobShuffleは，バッチ処理と分散キャッシュ機構により，費用対効果と低遅延性を両立している。
- 大規模実験の結果，BlobShuffleは従来のKafka Streamsの再分割と比較して，再分割コストを40倍以上削減できることが示された。
- 2GiB/s以上のデータ処理速度でもスケーラビリティに制限がなく，大規模なシャッフル集約型ワークロードを経済的にサポート可能であることが確認された。
イザベル核における型計算 [cs.IR, cs.LO, math.CT, math.LO]目的：線形論理と実現可能性，そして豊饒イザベル双対性における型生成の構造の同一性
- 型理論は，プログラム言語の基礎や形式的検証において重要な役割を担う。
- 既存の研究では，型システムが静的で固定されている場合が多く，柔軟性に欠ける。
- 実行と直交性に基づいた型生成の統一的な枠組みを提示し，型システムのより自然な構築を目指す。
- 線形論理と実現可能性，豊饒イザベル双対性における型生成の異なるアプローチが，同じ数学的対象を生み出すことが示された。
- 実行と実数値測定という最小限のデータに基づき，非可換ラムベク計算が導出される。
- 型生成の構造の一貫性定理が証明され，有限次元の場合には具体的な計算式が提示された。
ニューラル変化予測：ソフトウェア変更とそれらの影響の関係 [cs.HC, cs.CY, cs.SE]目的：ソフトウェア変更とその影響間の関連性の学習と予測
- ソフトウェア開発において，変更とその影響の理解は不可欠である。
- コードのセマンティクスを非実行で予測することは依然として困難である。
- ソフトウェア変更と動的効果の関連性を自動的に学習・予測する。
- 本研究では，CSS設定ファイルとPythonプログラムを用いたケーススタディにより，ニューラル変化予測の汎用性と幅広い適用可能性を示した。
- ニューラル変化予測は，プログラムのテスト実行回数を必要とするが，コードやセマンティクスに関する事前知識を必要としない。
- 本手法は，望ましい挙動変化に対する変更箇所の予測，およびコード変更が及ぼす影響の予測を可能にする。
人間とAIの協働とソフトウェアエンジニアリングの仕事の変化 [cs.SE]目的：ソフトウェアエンジニアリングにおける人間とAIの協働の現状と将来像
- ソフトウェア開発は社会基盤であり，その効率化と品質向上が不可欠である。
- 生成AIや自律エージェントの導入により，従来のソフトウェア開発手法が変化している。
- 将来のエンジニアに求められる能力を明確化し，教育や組織変革に貢献すること。
- 生成AIと自律エージェントの導入により，ソフトウェアエンジニアリングの仕事の中心が，コードの記述から，AIシステムの指示，検証，統治へと移行しつつある。
- 従来のソフトウェアエンジニアリングを，伝統的，生成AI活用型，自律エージェント活用型という3つのパラダイムに分類し，各パラダイムにおける活動の変化を分析した。
- 将来のエンジニアには，技術力，認知力，社会技術力，ガバナンス，組織力といった5つの能力が求められ，その能力構造を包括的に示したフレームワークを提案した。
LTLにおける非整礎および循環証明：線形ネスト化シークエントとの構文的対応 [cs.CL, cs.LO, math.LO]目的：LTLの非整礎および循環線形ネスト化シークエント計算
- 形式検証やプログラム検証において，論理的推論の自動化は重要な役割を果たす。
- 線形ネスト化シークエントのような表現力豊かな形式体系における循環証明の処理は困難である。
- 循環証明と非整礎証明の間の変換を可能にし，証明の自動化を促進すること。
- 非整礎証明から循環証明を抽出するための「飽和再帰性」という特性を持つ正規形が示された。
- 循環証明から非整礎証明を再構成するための，線形ネスト化シークエントにおける規則適用を前進させる特殊な手順が導入された。
- 本研究は，表現力豊かなマルチシークエント形式における循環認識と展開のための新たな証明理論的技術を提供する。
スマートフォンアプリ，加速度，乗員の評価を用いた道路粗さの多角的評価 [cs.RO, cs.CE, cs.SE]目的：道路粗さの低コスト評価のための多角的かつ人間中心の枠組み
- 道路の維持管理において，道路粗さは交通安全と車両の耐久性に大きく影響する重要な指標である。
- 従来の道路粗さ測定には高価な専門機器が必要であり，広範囲なモニタリングが困難であった。
- スマートフォン等の低コストなセンサーと乗員の主観評価を組み合わせ，道路粗さの評価手法を確立すること。
- 2つのスマートフォンアプリによるIRI推定値は高い相関を示したが，系統的なバイアスにより相互交換可能性は限定的である。
- IRIとPSRの間には有意な負の相関が認められ，粗さに対する知覚的な感度が確認された。
- IRIと垂直加速度の間に正の相関が認められ，路面の凹凸と車両の動的挙動との物理的な関連性が示された。
線形化によるゲーデル・ローブ論理における証明探索の最適化：木型超順列を用いた手法 [cs.LO, math.LO]目的：ゲーデル・ローブ論理における証明探索アルゴリズムの最適化
- 様相論理の自動推論は，計算機科学や数学基礎論において重要な役割を果たす。
- ゲーデル・ローブ論理の証明探索は，計算量が多く，効率的なアルゴリズムが求められていた。
- 木型超順列システムを用いた証明探索アルゴリズムを開発し，その計算量を削減することを目指す。
- 本研究では，ゲーデル・ローブ論理の証明探索アルゴリズムを開発し，その計算量がPSPACEであることを示した。
- 線形化という手法を導入することで，従来の証明探索における指数的な計算量の増加を回避した。
- 証明探索が失敗した場合に正しい反例を抽出するための方法と，線形ネスト順列との関連性を示した。
OIRS支援可視光通信における秘匿和率最大化 [cs.IT, cs.SY, eess.SY, math.IT]目的：秘匿和率の最大化
- 可視光通信は，電波干渉の少ない無線通信手段として注目されている。
- 物理的な遮蔽や内部からの盗聴が，通信の安全性と信頼性を脅かす。
- OIRSを活用し，秘匿和率を向上させることで，安全な通信を実現する。
- 提案手法は，伝送プレコーダとOIRSユニットの割り当てを共同設計することで，秘匿和率を最大化する。
- 凹凸過程（CCCP）と一次テイラー近似を統合した交互最適化（AO）フレームワークにより，効率的な最適化を実現した。
- シミュレーション結果は，提案アルゴリズムの収束性と，OIRSユニット数の増加による秘匿和率の大幅な向上を示した。
STC：BWT系列テキスト圧縮のための可逆的な数字文脈分解 [cs.IT, math.IT]目的：BWT系列テキスト圧縮における数字文脈分解による圧縮率向上
- テキスト圧縮は，データ保存や通信において不可欠であり，効率的な圧縮手法が求められている。
- 既存のBWT圧縮は，数字列のような特殊な文脈の変化に対応できず，圧縮効率が低下する可能性がある。
- 数字列を分離することで，BWT圧縮の効率を高め，全体的な圧縮率を向上させることを目指す。
- STCは，数字列をプレースホルダーに置き換え，その情報をサイドストリームに保存する手法を用いる。
- enwik9データセットにおいて，STCは既存手法と比較して2,629,561バイトの圧縮率向上を実現した。
- 復号化の検証とSHA-256による整合性確認により，STCの有効性が確認された。
ジオ・区別可能性に基づくチャネルチャート位置プライバシー [cs.CR, cs.IT, math.IT]目的：チャネルチャートにおける位置プライバシーの形式的保証
- 位置情報サービスは広く利用されているが，位置情報の漏洩はプライバシー侵害につながる。
- チャネルチャートは位置情報を明示的に必要としないが，プライバシーの保証は不十分である。
- チャネルチャート表現にジオ・区別可能性を拡張し，位置プライバシーを強化すること。
- 提案手法は，チャネルチャートの局所構造に合わせてノイズを注入するMahalanobis norm planar Laplace (MNPL)機構を用いる。
- MNPL機構は，チャネルチャートの多様体構造を維持しつつ，局所適応的な共分散を用いてプライバシーを定義する。
- 数値実験の結果，提案手法は高いプライバシー保護能力と，位置情報サービスの可用性の両立を示す。
具現化AIの信頼性向上：テストから形式検証へのコミュニティ・アジェンダ [cs.RO, cs.SE, cs.RO]目的：具現化AIシステムの信頼性向上策
- 現実世界でのAI利用拡大に伴い，安全性と信頼性の確保が不可欠となっている。
- 不確実性，人間との相互作用，システム要素間の複雑な関係性が信頼性を損なう原因となる。
- テスト，形式検証，実行時保証を統合し，ライフサイクル全体で信頼性を確保すること。
- 信頼性のある具現化AIの実現には，検証済みの仕様に基づいた信頼できるシナリオベースのテストが重要である。
- 構造化された記号表現を用いることで，システム行動と環境の文脈を検証する手法が有効である。
- 不確実性や分布の変化に対応可能な実行時保証メカニズムが，展開における信頼性を高める。
DDOR：説明可能な過剰拒否テストと修正のためのデルタデバッグ [cs.SE, cs.AI]目的：大規模言語モデルにおける過剰拒否のテストと修正
- 言語モデルの安全性確保は重要だが，過剰な拒否がユーザビリティを損なう可能性がある。
- 言語モデルは，本来無害なクエリをリスクと誤認し，不必要に拒否することがある。
- 過剰拒否の原因を特定し，モデルの安全性を維持しつつ，ユーザビリティを改善すること。
- DDORは，過剰拒否を引き起こす最小限の断片を特定し，説明可能な根拠を提供する。
- 特定された断片に基づき，多様なプロンプトを生成し，過剰拒否テストスイートを作成する。
- デルタデバッグを活用したプロンプト修正により，過剰拒否を大幅に削減し，安全性も維持する。
奇数特性有限体上の冪関数から構成される巡回符号の最小距離拡大 [cs.IT, math.IT]目的：奇数特性有限体上の冪関数を用いた巡回符号の構成
- 通信・記録システム等に応用可能な，高い誤り訂正能力を持つ符号の重要性が増している。
- 符号長半分を超える次元と，符号長平方根を超える最小距離を持つ巡回符号の構成が課題であった。
- 有限体上の冪関数を利用し，高い符号効率と誤り訂正能力を両立する巡回符号の構成を目指す。
- 奇数特性有限体上の冪関数を用いて，符号長$q^m-1$の巡回符号の無限族を構成した。
- 構成された巡回符号は，次元が$(q^m-1)/2$を超え，最小距離の下限が符号長の平方根よりも大きいことが示された。
- 一部の符号の最小距離を正確に決定し，Ding氏が提示した未解決問題5.31の一部を解決した。
AIは簡単にできるか？ EZR.pyツールキットから得られた教訓 [cs.SE]目的：表形式ソフトウェアエンジニアリング最適化タスクにおけるAIツールキットの設計と評価
- 表形式データを用いたソフトウェアエンジニアリングの最適化は，計算コストが高く，効率的な手法が求められている。
- 既存のAIツールは複雑で，理解と応用が難しく，学習コストが高いという課題がある。
- AIアルゴリズムを簡潔化し，統一することで，効率的な最適化ツールを開発し，理解を深める。
- EZR.pyは，Naive Bayes，k-means，決定木，焼きなまし法など多様なアルゴリズムを実装しており，わずか400行のコードで構成されている。
- MOOTリポジトリの120以上のタスクにおいて，EZR.pyは最先端のツールと同等以上の性能を示し，SMAC3などの既存手法よりも500倍高速に動作する。
- この結果は，コードの読解とリファクタリングが洞察を生み出し，小型の統合ツールキットが大規模なライブラリに匹敵することが可能であることを示唆する。
命題的敗北可能視点論理における非単調含意に向けて [cs.AI, cs.LO]目的：命題的敗北可能視点論理における非単調合理的含意関係の拡張
- 敗北可能推論は，不確実な情報や相反する証拠を扱う上で重要であり，その形式化が求められている。
- 既存研究は単調含意に偏っており，より推論力の強い非単調含意の扱いは十分ではない。
- 視点論理に非単調含意を導入し，より柔軟な推論を可能にすることを目指す。
- 本研究では，位置づけられた視点条件子を導入することで，従来のKLMスタイルの推論における非単調合理的含意関係をPDSLに適用する手法を提案した。
- PDSLの一部の断片を位置づけられた条件子の集合として表現可能であることを示し，PDSLにおける非単調含意を特徴づける方法を定義した。
- 提案手法では，命題論理のアルゴリズムを活用しつつ，PDSLにおける含意判定の複雑度を維持することが可能である。
エージェントによる知識モデルの生成と進化 [cs.SE]目的：知識モデルの生成と進化に関するビジョン
- 自律走行車やロボットなど複雑なシステムは，変化する環境との相互作用が重要である。
- 既存の知識モデルは，システムの進化に伴い不完全，矛盾，または陳腐化しやすい。
- システムの信頼性を維持するための，継続的な知識モデルの同期と進化を目指す。
- TrustModelは，モデリング，適合性評価，進化の3つのエージェントサブシステムで構成される。
- モデルベーステストへの適用例を示し，他のMDE活動への潜在的な可能性を議論する。
- TrustModelは，継続的に進化するソフトウェアシステムの信頼性確保のための基盤を提供する。
決定論的距離近似によるMPCにおける改善されたヒット集合 [cs.DS, cs.DC]目的：MPCモデルにおけるスパンナーと近似最短経路の決定論的アルゴリズムの開発
- 大規模グラフの処理において，並列計算モデルであるMPCは重要な役割を担う。
- MPCにおけるラウンド数の削減は，計算効率向上において重要な課題である。
- 決定論的アルゴリズムを用いて，ラウンド数を削減し，計算効率を向上させる。
- 線形MPCおよび混雑クリックにおいて，$O(n^{1+1/k})$サイズの重み付きグラフの$O(k)$伸縮スパンナーを$O(1)$ラウンドで実現した。
- 混雑クリックでは，重み付きグラフの$O(1)$-近似APSPを$O(\log \log \log n)$ラウンドで達成した。
- 決定論的なアルゴリズムは，既存のランダム化アルゴリズムと同等の性能を，ラウンド数に過剰な要素を加えることなく実現した。
安全なEKF強化UAV-ISACシステム [cs.IT, math.IT]目的：UAV支援ISACシステムの秘匿率最大化
- 無線ネットワークにおいて，効率的な資源利用が求められており，ISAC技術はその鍵となる。
- 盗聴者への妨害と合法ユーザーへの通信を両立させるセキュリティ確保が課題である。
- UAVの軌跡と送信ビームフォーミングを最適化し，秘匿率を最大化する。
- 提案手法は，ブロック座標降下法，逐次凸近似，EKFを統合することで，高品質な近似解を得る。
- シミュレーション結果は，提案手法がベンチマークと比較して優れた性能を発揮することを示した。
- 送信ビーム幅，送信電力，UAV推進エネルギー消費等の実用的な制約を考慮している。
形式化プロセス記述のためのAutomationMLドメインライブラリ [cs.SE, cs.DB]目的：形式化プロセス記述の標準化
- 工学分野におけるプロセス記述の標準化は，異種システム間の連携を円滑にし，効率的な設計・開発を実現するために重要である。
- VDI/VDE 3682による形式化プロセス記述は標準的な表記法を提供するものの，機械可読なモデル交換のための標準化されたデータ形式が欠如していた。
- 本研究は，機械可読なモデル交換を可能にするためのデータ形式の標準化を目指す。
- 本研究で開発されたAutomationML (AML) ドメインライブラリは，VDI/VDE 3682の形式化プロセス記述の要素をCAEX 3.0メタモデルに基づいて形式化する。
- ライブラリは，セマンティックロール，接続タイプ，情報モデル，図面交換，インスタンス化テンプレートを定義する5つの関連部分で構成される。
- WebベースのFPDモデラーとAML間の双方向マッピングツールにより，ライブラリの適用可能性が実証され，VDI/VDE 3682のPart 3としての標準化が提案されている。
エントロピーゲート：LLMパイプラインにおけるほぼ無損失のトークン圧縮のためのエントロピー冷却 [eess.SY, cs.SY, cs.CL, cs.IT, math.IT]目的：低情報コンテンツのトークン圧縮
- LLMの効率的な運用には，計算資源とコストの削減が不可欠である。
- LLMパイプラインでは，冗長なトークンが多く，トークン予算を無駄にしている。
- トークン圧縮によって，パイプラインの効率化とコスト削減を目指す。
- エントロピーゲートは，統計的，構造的，位置情報を考慮したエネルギーに基づいてトークンを圧縮する。
- 実験の結果，5つのプロンプトカテゴリで40〜60%の圧縮率を達成し，意味類似度は0.80以上を維持した。
- 出力側の圧縮と外部メモリとの組み合わせにより，エージェント型ワークロードで88〜96%の削減が可能となった。
有限温度におけるド・ブリュインの恒等式：Fisher情報とBlahut-Arimotoダイナミクスのスペクトルギャップ [cs.IT, math.IT]目的：有限温度におけるド・ブリュインの恒等式の拡張
- 情報理論は，通信，機械学習，統計物理など広範な分野に応用される重要な研究領域である。
- 従来のド・ブリュインの恒等式は，特定の条件下でのみ成立するため，その適用範囲に限界があった。
- Blahut-Arimotoダイナミクスのスペクトルギャップを用いて，より一般的な有限温度でのド・ブリュインの恒等式を導出すること。
- ガウス性を持つ情報源において，Blahut-Arimoto緩和カーネルのスペクトルギャップがFisher情報と関係することが示された。
- 導出された有限温度ド・ブリュインの恒等式は，従来の恒等式のより一般的な形であり，特定の極限操作を必要としない。
- この研究は，エントロピー電力不等式やBAダイナミクスの$\chi^2$-dissipation構造など，情報理論における様々な不等式や構造の統一的な理解に貢献する。
FLARE：LLMコード改善のための詳細な診断フィードバック [cs.SE, cs.AI]目的：LLMによるコード改善のための詳細な診断フィードバック手法
- ソフトウェア開発において，コードの品質は不可欠であり，バグの早期発見と修正が重要である。
- 既存のLLMはバグを含むコードを生成することがあり，その修正には粗雑なフィードバックしか利用できない場合が多い。
- LLMによるコード修正の精度を高めるため，バグの箇所を特定し，詳細なフィードバックを提供する。
- 提案手法FLAREは，軽量な診断モデルを用いてコードのどの部分にバグの疑いがあるかを特定する。
- 候補探索（k=1）を行わなくても，既存の最良手法を大きく上回り，性能が1.72%～7.42%向上した。
- 10個の候補を探索することで，さらに平均8.50%の性能向上が見られた。
Simulink要件テーブルにおけるサイバー物理システムの要件自動修復 [cs.SE]目的：サイバー物理システムの要件とシステムの実装との整合性回復
- サイバー物理システムは複雑化しており，実装と要件の一貫性維持が重要である。
- 実装変更により要件との整合性が失われる場合がある。要件自体の不備も課題である。
- システム実行データを利用して，サイバー物理システムの誤った要件を修復し，整合性を回復する。
- 提案手法は，MATLAB Simulink Requirements Tablesを用いて定義された時間依存の実数値信号に対する要件の正しさを評価する。
- 6つの実例と12の要件を用いた評価により，提案フレームワークが有効であることが確認された。
- 修復された要件は，正しく有用であると結論付けられた。
エージェント型AIコーディングツール設定がビルド vs 購入決定に与える影響：研究プロトコル [cs.SE, cs.AI, cs.HC]目的：エージェント型AIコーディングツールにおけるビルド vs 購入決定を制御する要因の解明
- ソフトウェア開発において，外部ライブラリの利用か自社開発かの判断は，セキュリティや保守性に大きく関わる。
- エージェント型AIコーディングツールのビルド vs 購入決定の基準は明確でなく，実験的な検証が不足している。
- 設定メカニズムがビルド vs 購入決定に及ぼす影響を定量的に評価し，最適な設定方法を提案する。
- Claude CodeとOpenAI Codexを用いて，様々な設定条件下でのプログラミングタスクを実行し，ライブラリ選択の傾向を分析した。
- 設定の変更が，ツールのライブラリ選択や情報開示の正確性に影響を与えることを確認した。
- 本研究で構築したベンチマークデータセットと分析パイプラインは，今後の評価に活用できる。
持続可能なセルフリーMassive MIMOネットワークのためのスパース活性化：少なきは多なり [cs.IT, eess.SP, math.IT]目的：セルフリーMassive MIMOネットワークにおけるスパースアンテナ/アレイ活性化問題
- 次世代6Gネットワークの持続可能性が求められる中，ネットワーク消費電力の削減が重要課題となっている。
- 従来のLarge-Scale Fading Decoding (LSFD)では，アンテナ要素ごとの最適な重み付けが考慮されていなかった。
- アンテナ要素を意識した重み付けにより，エネルギー効率とスペクトル効率の両立を目指す。
- 提案するアンテナレベル最適二項イコライザ（OBE）重み付け方式は，LSFDと比較してスペクトル効率を向上させる。
- スパース活性化方式は，制御可能なスペクトル効率の低下を伴いながら，大幅なエネルギー効率改善と電力削減を実現する。
- 相関リicianチャネル下での数値結果は，アンテナ数が増加するにつれてOBEの利点が大きくなることを示している。
アンカー付き編集距離に対する$O(n \log \log n)$チェイニングの再検討 [cs.DS]目的：アンカー付き編集距離の効率的な計算手法の開発
- ゲノム比較において，高速な配列アライメントは不可欠であり，大規模ゲノムデータの解析を可能にする。
- 従来のチェイニング法では，長鎖リードマッピングにおいて重要なフラグメントの重複を考慮していなかった。
- 重複コストを考慮したチェイニングによって，長鎖リードマッピングの感度向上と適用範囲の拡大を目指す。
- 本研究では，$O(n \log^3 n)$であったアンカー付き編集距離の計算時間を，$O(n \log \log n)$に改善することに成功した。
- 開発したllchainは，300万個のアンカーを持つデータセットで既存手法と比較して約10倍高速に動作することが示された。
- HiFiリードとヒトゲノム間のMEMsデータにおいても，llchainは3倍以上の高速化を実現した。
- 1
- 2