arXiv雑要約
プログラム - 2026/05/27 公開
ユーザ理解可能なものから技術的なプロセスモデルへ：CUTA4BPMを用いたモデル駆動型アプローチ [cs.SE]目的：ビジネスプロセスモデリングにおける理解可能性と技術的な柔軟性の両立
- ビジネスプロセスモデリングは業務効率化の基盤であり，その重要性は増している。
- 専門家にとって理解しやすいブロック指向言語と，柔軟性の高いグラフ指向言語の間には隔たりがある。
- CUTA4BPMとBPMNの連携により，両言語の利点を生かした円滑な移行を可能にする。
- 本研究では，ブロック指向言語CUTA4BPMを用いて高レベルなプロセスモデリングを行い，BPMNによる詳細設計へとつなぐ参加型フォワードエンジニアリングアプローチを提案する。
- CUTA4BPMモデルは，モデル駆動型エンジニアリング技術を用いてBPMNモデルへ自動変換され，スムーズな移行を実現する。
- これにより，業務専門家とプロセス設計者の両方にとって使いやすいモデリング環境を提供する。
制約税：小規模言語モデルにおける構造化出力の妥当性と正しさのトレードオフの測定 [eess.SY, cs.SY, stat.CO, eess.SY, astro-ph.EP, astro-ph.IM, cs.SY, cs.LG, cs.SE]目的：小規模言語モデルにおける構造化出力制約が，回答の正確性と実行可能性に及ぼす影響の定量化
- LLMの普及に伴い，機械可読な出力形式の重要性が高まっている。特に，プライバシーや低遅延性が求められる場面で，小規模モデルの活用が期待される。
- 小規模モデルでは，出力スキーマ制約を満たしつつタスクを解決することが困難であり，制約の厳格化が回答の質に与える影響が不明確である。
- 構造化出力制約による回答の正確性と実行可能性の低下を定量的に評価し，より効果的なシステム設計の指針を示す。
- 構造化出力制約を厳格化することで，出力スキーマの妥当性は向上するものの，回答の正確性は低下し，妥当だが誤った出力を生成する割合が増加する。
- Qwen2.5-1.5Bを用いたカレンダーツール呼び出しタスクにおいて，プロンプトのみの場合は実行精度が91.5%であるのに対し，厳格なツール呼び出しスキーマ下では48.0%に低下する。
- 30億パラメータ以上のモデルでも制約による影響が見られるため，推論後に制約を適用する設計が有効である。
VISTA：ビジュアル仕様からWebアプリケーションのコーディングエージェントのためのエンドツーエンドベンチマーク [cs.SE, cs.AI, cs.CV]目的：LLMベースのエージェントのWebアプリケーション生成能力の評価
- ソフトウェア開発の自動化は，開発効率の向上とコスト削減に不可欠である。
- 既存のコード生成ベンチマークはアルゴリズムに偏っており，UI中心の開発には不向きである。
- ビジュアル情報に基づいた，より現実的なWebアプリケーション開発の自動化を可能にする。
- VISTAは，テキストのみ，参照スクリーンショット，Figma構造といった多様な入力条件を提供し，厳密な評価を可能にする。
- 評価には，DOM比較，ブラウザテスト，CLIPによる視覚的類似性評価を組み合わせ，構造，動作，視覚的忠実性を測定する。
- 実験の結果，視覚的忠実性と機能的な正確さは部分的に分離されており，エージェントの編集スタイルはタスク品質とはほとんど関係がないことが示された。
拡張エンジニアリング：専門分野におけるマルチツールAIオーケストレーションのメソッド論 [cs.SE, cs.AI, cs.HC]目的：複数のAIツールを専門分野横断的にオーケストレーションする手法
- AI導入が進む中で，専門知識を持つ人材の確保が課題となっている。
- 各AIツールの効果を最大化するスキルが，専門分野に依存している現状がある。
- プロンプトエンジニアリング等の汎用的なスキルを活用し，AIツールを効率的に連携させる。
- 拡張エンジニアリングの6段階手法と4つの可搬性指標を提示した。
- 単一の実践者による5ヶ月の実証実験で，7分野のAIツールを連携し，専門家による作業を代替した。
- プロンプトの洗練度と初回受容率，成果物作成速度がそれぞれ統計的に有意な相関を示した。
ニューラル受信機はいつ役立つのか？ 5G/6G NRにおけるキャリブレーションドリフトベンチマークと検知・ロールバック [cs.IT, cs.SY, eess.SY, math.IT]目的：5G/6G NRにおけるニューラル受信機の有効性評価
- 無線通信技術の高度化に伴い，受信信号処理の性能向上が不可欠である。
- 従来の受信機は，送信機やチャネルパラメータの変化に弱く，性能が劣化する。
- ニューラル受信機のキャリブレーションドリフト時の挙動を評価し，安定性を高める。
- ニューラル受信機は，訓練データ内のチャネル・波形設定において，従来の受信機よりも優れた性能を示す。
- しかし，送信機やチャネルパラメータが訓練範囲から逸脱すると，キャリブレーションドリフトにより性能が低下する可能性がある。
- 検知・ロールバック技術を用いることで，キャリブレーションドリフトの影響を軽減し，ニューラル受信機の信頼性を向上させることが示唆された。
敵対的ウォーターフィリング：理論，アルゴリズム，そして基礎モデル [cs.IT, cs.LG, math.IT, math.OC]目的：周波数および空間における競合的なリソース配分問題の解法
- 衛星通信の発展において，周波数資源の効率的な利用が不可欠であるため。
- 既存手法では，離散的な星座を用いる場合に非凸な問題となり，最適解の探索が困難である。
- 実環境下でのリソース配分問題を解決するため，敵対的ウォーターフィリング問題とそのアルゴリズムを提案する。
- 敵対的ウォーターフィリング問題の理論とアルゴリズムを構築し，実用的な無線基礎モデルを開発した。
- 提案モデルは，チャネル表現，制約を考慮したGNN，および潜在変数を組み込むことで，AWFの探索ダイナミクスを学習する。
- 実験の結果，問題規模や制約条件の変化に対応でき，従来の反復法と比較して処理時間を大幅に短縮できることを示した。
マルチモーダル意思決定支援システムのためのゲーミフィケーションを活用した要件定義：SYNCHROMODEの事例 [cs.SE]目的：マルチモーダル輸送運用管理のためのデータ駆動型ICTツールボックス，SYNCHROMODEにおけるコアサービスの要件定義
- 交通システムの効率化は社会経済活動の基盤であり，持続可能な社会実現に不可欠である。
- 複雑なシステムの開発において，初期段階である要件定義の曖昧さは，手戻りやコスト増を招く。
- 本研究は，ゲーミフィケーションを導入することで，多様な関係者のニーズを効果的に把握し，要件定義の精度向上を目指す。
- 伝統的な手法とゲーミフィケーションを用いた要件定義プロセスを比較分析することで，それぞれの有効性を明らかにした。
- 2023年10月にテッサロニキで開催されたワークショップでは，交通管理の専門家，自治体など多様なステークホルダーから要件を収集した。
- ゲーミフィケーションは，従来の要件定義手法を補完し，新たな視点からの要件発見に貢献する可能性が示唆された。
ツール・スキーマ圧縮による制約付きコンテキスト予算下でのエージェント型RAGの実現 [cs.SE, cs.AI, cs.CL]目的：ツール・スキーマ圧縮によるエージェント型RAGシステムの実現可能性
- 大規模言語モデルにツールを組み合わせるRAGシステムは，複雑なタスク解決に有効である。
- ツール定義のスキーマはコンテキストウィンドウを圧迫し，RAGの性能低下を招く可能性がある。
- コンテキストウィンドウの制約下でも，ツール・スキーマ圧縮によってRAGを有効に機能させる。
- ツール・スキーマ圧縮(TSCG)により，スキーマのトークン数を44-50%削減できることが示された。
- 8Kトークンという制約下では，圧縮によりRAGの正答率(EM)が平均で20.5pp向上した。
- 32Kトークンでは圧縮による影響は小さく，圧縮は主にコンテキスト予算が限られている場合に有効であることが確認された。
ESBMC：形式ソフトウェア検証におけるその進化，統合，および将来展望 [cs.SE, cs.LO]目的：ESBMCの進化，統合，将来展望に関する調査
- ソフトウェアの信頼性確保が不可欠であり，形式検証はその重要な手法の一つである。
- 既存の形式検証ツールは，適用範囲や自動化レベルに課題が残されている。
- ESBMCの進化を体系的に整理し，今後の発展課題を明確にすること。
- ESBMCは，組み込みANSI-Cソフトウェアの検証から，多様な形式検証プラットフォームへと進化してきた。
- SV-COMPやTest-Compにおいて43の賞を受賞し，LLMを活用した自己修復ソフトウェアやループ不変量の生成にも貢献している。
- NVIDIA-OpenSMAフレームワークを通じたエージェント型モデルチェックの産業展開により，ESBMCは自律的な検証カーネルとしての地位を確立した。
普遍的な断崖とデザインの指紋：LLMオーケストレーション下での断片間欠陥検出 [cs.SE, cs.AI, cs.CL, cs.MA]目的：大規模言語モデルシステムにおける断片間矛盾という，単一のモデルでは検出困難な欠陥の検出メカニズムの解明
- 大規模言語モデルの活用が進む中，複雑な文書の品質保証が重要となる。
- 大規模言語モデルは，複数のエージェントによるオーケストレーションによって機能するため，文書全体の一貫性を保つことが課題となる。
- LLMオーケストレーションが断片間欠陥検出に及ぼす影響を定量的に評価し，モデルの安全性を向上させる。
- LLMオーケストレーション下では，単一エージェントで検出可能な断片間欠陥の検出能力が大幅に低下し，検出率は3分の2以上減少する。
- 特定の開発者のモデル系列において，アライメント強化により欠陥検出率は向上する一方，誤検出率も上昇する傾向が確認された。
- 統合されたレポートの信頼性は，断片間にまたがる欠陥の検出には役立たず，アライメントの高いシステムが必ずしも安全とは限らない。
RepoMirage：コードエージェントにおけるリポジトリコンテキスト推論の探求 - 摂動を用いた検証 [cs.SE, cs.AI]目的：コードエージェントのリポジトリコンテキスト推論能力の評価
- ソフトウェア開発におけるコード理解の自動化は，生産性向上に不可欠である。
- 既存のコードエージェントはタスク遂行能力を示すが，リポジトリ全体の文脈理解が不十分である。
- リポジトリ全体の文脈理解能力の評価方法を確立し，改善策を提案すること。
- RepoMirageは，リポジトリ構造を変化させる摂動により，コンテキスト推論の要求度を高める評価手法である。
- 摂動を加えた環境下では，コードエージェントの性能が大幅に低下し，リポジトリコンテキスト推論の弱点が明らかになった。
- 構造情報に焦点を当てたRepoAnchorというプロトタイプワークフローは，性能向上に貢献することが示された。
非線形算術とSMTLIB除算は判定不能である [cs.LO]目的：非線形実数算術の判定不能性
- 自動検証や定理証明において重要な役割を担う算術理論の基礎研究。
- SMTLIB標準における除算の扱いが，理論の決定可能性を損なう可能性。
- SMTLIBにおける除算の扱いが引き起こす判定不能性の問題を明確化。
- 非線形実数算術(NRA)が，SMTLIB標準で定義される場合に判定不能であることが示された。
- 除算を未解釈関数として扱うことが，この判定不能性の原因となっている。
- 整数算術の問題をNRA数式に符号化することで，この現象が再現された。
SetupX：LLMエージェントは，機能が正しいコードリポジトリ設定における過去の失敗から学習できるか？ [cs.SE, cs.AI, cs.CL, cs.LG]目的：機能が正しいリポジトリ設定の自動化
- ソフトウェア開発における再現性の確保は重要であり，環境構築の自動化が不可欠である。
- リポジトリ固有の依存関係の問題や不完全なインストールなど，環境構築には多様な問題が存在する。
- 既存のLLMエージェントが抱える問題を解決し，環境構築の成功率向上を目指す。
- SetupXは，検証済みの環境修正を未見のリポジトリに動的に転送する自己進化型経験表現（XPU）を構築する。
- LIFO Dockerスナップショットスタックを利用した経験拡張型推測実行により，エージェントは修正を積極的に試行し，安全に既知の状態にロールバックできる。
- 提案手法は，複雑な複数リポジトリ設定において，既存の最良手法を19%以上上回る高い性能（92%のパス率）を達成した。
オート研究システムにおけるワークフローの完結は科学的完結ではない [cs.SE, cs.AI]目的：オート研究システムにおける科学的妥当性の問題点
- 研究の自動化は，効率化や新たな発見の可能性を秘めている。
- 現在のオート研究システムは，科学的な検証プロセスを十分に備えていない。
- 科学的妥当性を確保するための設計指針を提示すること。
- オート研究システムは研究ループを完結できるものの，それだけでは科学的な根拠は得られない。
- 目標の単一化，検証の内部化，受容のベンチマーク偏重といった問題（objective/validation/acceptance collapse）が共通して見られる。
- これらの問題は設計上の選択によって修正可能であり，科学的妥当性を高めるための議論を促す。
時間変動型マルチプライオリティキューにおける情報鮮度 [cs.IT, math.IT]目的：時間変動型マルチプライオリティキューにおける情報の鮮度
- モバイル，航空宇宙システム等における情報伝達において，情報鮮度は重要な課題である。
- 不定期な接続，到着変動，優先度間相互作用が，情報鮮度維持を困難にしている。
- 時間変動条件下での優先度付きキューにおける情報鮮度を定量的に評価する手法を確立する。
- 状態条件付きの一次モーメントが正確に閉じることを示し，各優先度クラスの平均情報鮮度(AoI)とピーク情報鮮度(PAoI)を記述する有限次元線形時間周期常微分方程式(ODE)系を導出した。
- 周期的な到着率とサービス率に対し，1期間状態写像を定義し，周期性条件を用いて周期定常状態をこの写像の固定点として定式化した。
- 固定点反復アルゴリズムを提案し，その一意の周期定常状態への収束を証明した。数値結果から，高優先度トラフィックが低優先度クラスのサービスプロセスを大きく変化させることが示唆された。
グラフパターンマイニングのためのクエリ書き換えフレームワーク Geo [cs.PL, cs.DB]目的：グラフパターンマイニングにおけるクエリ最適化手法
- グラフデータ分析において，パターン抽出は不可欠であり，その性能が重要である。
- 既存手法では，最適化戦略の開発が難しく，改善が停滞しやすい。
- クエリ書き換えによる自動最適化により，開発の容易性と性能向上を目指す。
- Geoは，パターン等価性を自動的に管理し，最適化の正当性を保証する。
- 等価なパターンを効率的に表現するため，カノニカル表現とEmRecを導入した。
- 実験の結果，クエリコストを最大99%削減し，実用的なグラフマイニング問題でも高い効果を発揮した。
Conv-to-Bench：コードタスクにおけるユーザーとアシスタントの対話による言語モデルの評価 [cs.CL, cs.SE]目的：言語モデルの評価
- 大規模言語モデルの急速な発展に伴い，その能力を正確に評価する基準の重要性が増している。
- 従来の評価基準は専門家による手作業での作成に依存しており，拡張性に限界がある。
- ユーザーとアシスタントの対話から自動的に評価基準を作成することで，評価プロセスの拡張性と効率化を目指す。
- Conv-to-Benchは，実際の対話ログから要件チェックリストを自動生成する多段階フレームワークである。
- 生成された評価セットは，BigCodeBenchなどの人間が作成した基準とほぼ完全に一致し，高い相関関係を示した(ρ = 1.000)。
- LLMを評価者として用いた検証でも，人間の評価との高い一致性(κ = 0.705)が確認された。
ハーフスライス上の低健全性線形性テスト [cs.CC, cs.DM, cs.DS, math.CO]目的：ハーフスライス上のブール関数の線形性に関する検証
- 暗号理論や符号理論において，ブール関数やその線形性は重要な研究テーマである。
- ハーフスライス上での線形性テストは，既存の手法では限界があった。
- より効率的かつ正確な線形性テスト手法を確立し，より広い範囲で応用することを目指す。
- 提案手法は，従来のテストよりも少ないクエリ数（k=3）で線形性を検証できる。
- k=4の場合，より厳密な線形性の一致度を結論付けることが可能となった。
- クラウチュック多項式の限界を用いて，より簡潔なテスト手法を導き出し，q進数におけるスライスにも拡張した。
Verus-SpecGym: 仕様の自動形式化を評価するためのエージェント環境 [cs.SE, cs.AI, cs.CL, cs.PL]目的：仕様の自動形式化におけるLLMエージェントの能力評価
- AIコーディングエージェントの利用拡大に伴い，生成コードの正当性保証が重要課題となっている。
- 形式仕様がユーザーの意図と一致するかどうかの検証が困難である。
- LLMエージェントによる非形式的な問題を形式仕様へ変換する能力を評価する環境を構築する。
- Verus-SpecBenchベンチマークとVerus-SpecGym環境を開発し，LLMエージェントの仕様作成能力を評価した。
- Gemini 3.1 Proはタスクの77.8%を解決し，他の最先端モデルは51.1～57.8%であった。
- 生成された仕様は入力前提の欠落，不正な出力の許容，有効な出力の拒否といった課題が認められた。
構造カバレッジ基準によるエージェントワークフローのテスト [cs.SE]目的：マルチエージェントワークフロー仕様に対する構造的テスト手法
- マルチエージェントシステムは複雑化しており，その協調構造の検証が重要である。
- 既存の評価方法は，タスクの成功のみに焦点を当て，協調構造の網羅性を確認できていない。
- 協調グラフに基づき，エージェント，ツール，委譲経路等の構造的カバレッジを評価する。
- ワークフローを協調グラフとして表現し，到達可能なエージェント，ツール，委譲に関するカバレッジ義務を導出した。
- DSPyを用いたシナリオ生成により，カバレッジ義務を満たす実行可能なテストを生成した。
- 制限されたツールアクセス違反を検出し，ワークフローの信頼性を評価できた。
OpenMP並列化を持つC言語の形式意味論 [cs.DC, cs.PL]目的：OpenMP並列化を持つC言語の形式意味論の構築
- 並列処理は現代の計算機システムにおいて不可欠であり，プログラムの高速化に貢献する。
- OpenMPは手軽に並列化できる一方，誤ったpragmaの使用により，論理エラーやデータ競合が発生しやすい。
- OpenMPpragmaが導入された際の潜在的な問題を検出し，データ競合のない安全な並列実行を保証すること。
- 本研究では，検証済みコンパイラCompCertのC言語意味論を拡張し，OpenMP指令を含むCコードの形式意味論を定義した。
- この意味論は，従来のOpenMP意味論では捉えきれなかった，OpenMP指令と変数状態の間の微妙な相互作用を捉えることが可能である。
- 成功する実行は，データ競合がないことが保証されるため，誤った注釈による意図しない動作を検出するための基盤を提供する。
FuzzPilot：プラトー駆動型レシピ検証による構造化テキストファジング [cs.SE, cs.CR]目的：構造化テキストファジングにおけるレシピ検証手法
- ソフトウェアの脆弱性発見において，ファジングは重要な役割を担う。効率的なファジング手法の開発が求められている。
- 従来のファジングでは，探索空間が広大であり，効率的な探索が課題となっている。特に，カバレッジが停滞するプラトー状態が頻発する。
- プラトー状態の早期解決と，ファジング効率の向上を目指す。
- FuzzPilotは，AFL++のコントローラとして，高コストな推論処理をホットパスから分離し，効率的なファジングを実現する。
- cJSONライブラリを用いた評価実験では，FuzzPilotはベースラインAFL++と同程度のスループットを維持しつつ，プラトー期間の短縮を示したが，統計的な有意差は認められなかった。
- 言語モデルによるレシピ提案は，今回の実験範囲ではカバレッジ向上には貢献せず，プラトー短縮はコントローラのスナップショットと再起動機能に起因する可能性が高い。
大規模MIMO-OFDMにおけるトリプルビームフィンガープリントを用いた同時局所化と姿勢推定 [cs.IT, eess.SP, math.IT]目的：トリプルビームフィンガープリントとTransformerベースの局所化・姿勢認識ネットワーク
- 位置情報サービスの普及に伴い，複雑な電波伝搬環境下での高精度な局所化技術が重要となっている。
- 既存のフィンガープリントは位置情報のみであり，移動状態を捉えられていないという課題がある。
- トリプルビームフィンガープリントを用いて，位置と移動方向を同時に推定することを目指す。
- 提案手法は，従来のWKNNやCNNと比較して，有意に高い局所化精度を達成した。
- トリプルビームフィンガープリントが，有効な小規模かつ疎なフィンガープリントであることを示した。
- 移動方向推定においても満足のいく精度を達成した。
TrajAudit：エージェント型コーディングシステムの自動故障診断 [cs.SE]目的：エージェント型コーディングシステムにおける故障診断の自動化
- ソフトウェア開発の自動化が進む中で，システムの信頼性確保は重要課題である。
- 既存の故障診断手法は，複雑なタスクや長い履歴において性能が低下しやすい。
- ノイズの多い長文の履歴から，効率的に故障箇所を特定することを目指す。
- TrajAuditは，パターンマッチングとキーワード検出により不要な情報をフィルタリングする。
- テスト失敗報告書を事前知識として活用し，ノイズの多い状況下でも診断精度を向上させる。
- RootSEベンチマークにおいて，既存手法を24.4%以上上回る局所化精度と，トークン消費量18%削減を達成した。
構造化マスク拡散による同時多ユーザー復号 [cs.IT, eess.SP, math.IT]目的：同時多ユーザー復号における性能向上
- 無線通信において，複数のユーザーからの信号を効率的に復号することは重要である。
- 多ユーザー環境下では，信号間の干渉が大きく，復号が困難になる場合がある。
- 本研究は，干渉下における多ユーザー復号の信頼性と効率を改善することを目指す。
- 提案手法CIDERは，従来の復号方式と比較して同等またはより優れた誤り率を示す。
- CIDERは，FFT加速型Joint Belief Propagationよりも6倍から100倍以上高速に動作する。
- ブロック長が長くなるほど，速度の向上幅は大きくなる。
抽象解釈に対する証明論的アプローチ [cs.LO, math.LO]目的：抽象解釈の論理体系化
- プログラムの静的解析に不可欠であり，安全性や信頼性の向上に貢献する。
- 抽象化の際の情報の喪失と，その厳密性の保証が課題である。
- 論理体系を用いて抽象化の基礎を明確にし，厳密性を検証する。
- 抽象解釈と論理システムの体系的な対応付けにより，抽象格子とリンドバウム-タルスキ代数の同型性が示された。
- 具体化写像によって保持される論理結合子を特定し，対応する証明規則と公理を導出した。
- この枠組みは，Cartesian積や多変数設定にも拡張可能であり，非Cartesian抽象への応用も示唆されている。
ソフトウェアスタックのアップグレードにおけるエネルギー意識的な意思決定 [cs.SE]目的：ソフトウェアスタックアップグレードにおけるエネルギー消費への影響評価
- 持続可能性への関心の高まりから，ソフトウェアのエネルギー消費量は重要な課題となっている。
- ソフトウェアスタックのアップグレードがエネルギー消費に与える影響は十分に理解されていない。
- ソフトウェアのメンテナンス・進化における意思決定を支援するため，エネルギー消費量の測定方法を確立する。
- Spring BootとJVMのバージョンによってエネルギー消費量が大きく異なり，予期せぬ回帰も確認された。
- Java 21/23で導入された仮想スレッドは，アプリケーション変更なしに大幅な省エネ効果をもたらした。
- ソフトウェアのアップグレードはエネルギー使用量に影響を与える可能性があり，測定が意思決定に役立つ。
散乱雑音環境下における信頼性制約下でのバック散乱MIMOターゲット向けブラインドビームアライメント [cs.CG, math.CO, cs.IT, math.IT]目的：散乱雑音環境下でのバック散乱MIMOターゲットに対するブラインドビームアライメントの信頼性向上
- ISACは実用上，静止性クラッタや非直視多重経路の影響を受けやすく，ターゲットからの反射波が隠蔽され，誤ったピークが生じる。
- 既存手法ではターゲットをパッシブな散乱体としてモデル化するため，ターゲットからの反射波と環境との構造的な分離が困難である。
- バック散乱MIMOの特性を活用し，波形領域での分離と受動ビームフォーミングによる誤ピーク抑制を実現し，信頼性の高いビームアライメントを可能とする。
- バック散乱損失と角度情報を考慮した双方向空間ロックプロトコルを提案し，パイロット信号やCSIフィードバック，ターゲット同期を必要としないブラインドアライメントを実現した。
- タイミングオフセットに強いクラッタ対応型変調波形を導出し，二次位相劣化を利用した調整可能なBS/バック散乱MIMOコードブックを構築した。
- 非直視多重経路環境において，ビーム幅を狭めることが必ずしも有効ではなく，最適なビーム幅は検出とアライメント間の位相競合によって決定されることを解析的に示した。
非同期ストリーム方程式に対するペースング型 [cs.PL]目的：非同期ストリームのタイミング不整合を排除するための型システム
- リアルタイムシステムの健全性を評価する上で，センサーデータ等のストリームに基づく監視が不可欠である。
- センサーのデータ生成速度の非同期性により，監視システムの設計は複雑化し，タイミングの不整合が発生しやすい。
- RTLolaのような監視フレームワークにおいて，ペースング型システムを通じてタイミング不整合を防ぐことを目指す。
- 本研究では，非同期ストリームに対する監視システムのタイミング一貫性を保証するペースング型を提案した。
- 提案する型システムは，RTLolaに実装され，ペースング注釈に対する形式的な意味論と健全性証明が与えられた。
- 健全性証明は，Rocq証明アシスタントを用いて機械的に検証され，信頼性が確保された。
証拠の不在は証拠の不十分性ではない：ファクト検証におけるNEI構築アーチファクトの診断 [cs.CL, cs.IR, cs.SE]目的：ファクト検証におけるNEI（情報不足）構築アーチファクトの診断プロトコル
- ファクト検証は，知識獲得や意思決定において重要な役割を担う。
- 現在のファクト検証ベンチマークは，証拠の不在と不十分性を区別できず，評価が歪められる可能性がある。
- NEI構築に起因する問題を特定し，モデルの性能をより正確に評価することを目指す。
- NEI-CAPという，構築を考慮した診断プロトコルを導入し，ショートカットキューを検証した。
- 異なる構築で学習されたモデル間での能力転移が信頼性に欠けることが明らかになった。
- 固定された主張に対する診断により，証拠条件が参照ラベルの信頼性に影響を及ぼすことが示された。
ほぼ公平なシミュレーション [cs.LO, cs.FL]目的：公平性条件を備えた遷移系に対する，ほぼ公平なシミュレーション関係の体系
- システムの検証において，シミュレーションは効率的な手法であり，特に有限状態システムに有効。
- 従来のシミュレーション手法では，活性性特性の検証に限界があり，公平性条件の導入が必要。
- 公平なシミュレーションの複雑さを軽減し，より直感的で扱いやすいシミュレーション関係を確立する。
- 既存の公平シミュレーション技術を基盤とし，ブヒ公平性条件を備えた遷移系に対する「ほぼ公平なシミュレーション」関係を体系的に構築した。
- 提示されたシミュレーション関係は，直感的な推論規則を備え，公平なトレース包含を証明するための簡潔な演繹システムを導き出す。
- これらのシミュレーション関係と演繹システムをRocq証明支援システムに実装し，健全性を検証，およびいくつかの例を通して有用性を示した。
振幅調整可能ピンチングアンテナシステム：単一モードの位相不整合放射と多重ユーザービームフォーミング [cs.IT, eess.SP, math.IT]目的：振幅調整可能ピンチングアンテナシステムにおける放射重みの制御
- 電波伝搬損失を軽減し，通信距離を延伸するため，再構成可能な放射素子へのニーズは高い。
- 既存のピンチングアンテナは構造パラメータに依存し，放射重みの完全な制御が困難である。
- 誘導波の位相不整合操作により，放射重みを制御し，ビームフォーミング性能を向上させる。
- 提案手法は，既存のピンチングアンテナシステムと互換性を保ちつつ，振幅調整可能なビームフォーミングを実現する。
- 多重ユーザーダウンリンクシステムにおけるレート最大化問題において，提案手法が従来の方式よりも優れた性能を示す。
- 特に干渉限度下において，明確な性能向上を実証した。
小セルシステムにおけるRIS支援耐障害バックホール回復 [cs.IT, eess.SP, math.IT]目的：小セルシステムにおけるRIS支援バックホール回復機構
- 小セルネットワークの密度増加に伴い，バックホールインフラの重要性が増している。
- ケーブル障害によるバックホールネットワークの脆弱性が課題となっている。
- RISを活用し，ケーブル障害時の無線バックホールによるトラフィック再配分を実現する。
- 提案するRIS支援フレームワークは，高トラフィック条件下で生存率を58%から72%に向上させる。
- アンテナ制約のあるシステムにおいて，RISはBSの予備容量へのアクセスを拡大し，カバレッジを拡張する。
- 適度なトラフィック強度下では，BSあたり2アンテナのみでも高い生存率を達成可能である。
行動から義務へ：義務的行動モデル論理 [cs.CL, cs.CL, cs.LO]目的：マルチエージェントシステムにおける行動に関する義務の推論
- 社会規範やルールに基づいた行動を形式的に扱うことが重要であるため。
- 戦略的相互作用や不完全情報の状況下での義務の明確な定義が課題である。
- 行動モデル論理を用いて義務を導き出すための枠組みを確立すること。
- 義務的行動モデル論理(DAML)を導入し，エージェントの行動の望ましさと結果の可能性を評価する。
- DAMLは，意思決定時点において期待される義務的価値を最大化する行動を義務として定める。
- 鉱夫のジレンマなどの事例を通して，DAMLの表現力を実証した。
衛星測位：送信型知能表面（TIS）支援屋内システム [cs.IT, math.IT]目的：送信型知能表面（TIS）を用いた衛星屋内測位システムの検討
- 屋内環境における測位は，ロボット工学，資産追跡，人員管理など多岐にわたる分野で不可欠である。
- 従来の衛星測位システム（GNSS）は，屋内環境では信号減衰や多重反射により，測位精度が著しく低下する。
- TISを用いてGNSS信号を屋内へ伝搬させ，信頼性の高い屋内測位を実現することを目的とする。
- 送信型知能表面（TIS）の特性を活用し，GNSS信号の屋内伝搬を可能にする拡張された見通し路を確立した。
- TISアレイの位置と信号到達角を利用する三段階TIS支援衛星屋内測位アルゴリズム（TSIPA）を提案した。
- TISアレイの配置最適化のため，TPDoP（TIS position dilution of precision）を提案し，RMSEを用いて配置のコンパクトさを評価した。
ソフトウェア工学ポッドキャスト：研究資源としての可能性に関する実証的研究 [cs.SE]目的：ソフトウェア工学ポッドキャストの研究資源としての可能性
- ソフトウェア工学分野の進化は速く，最新動向の把握が不可欠である。
- ソフトウェア工学に関するポッドキャストの内容や研究者による活用が不明である。
- ポッドキャストが実証的ソフトウェア工学研究を促進するための資源となりうるか解明する。
- ソフトウェア工学ポッドキャストの現状分析から，多様なトピックが扱われていることが明らかになった。
- 研究者への調査では，ポッドキャストが業界動向の把握に役立つと認識されていることが示された。
- ポッドキャストは，実証的ソフトウェア工学研究における新たなデータソースとなりうる可能性が示唆された。
HTMLCure：ブラウザ体験を状態遷移に基づくHTML修正へと転換する [cs.SE, cs.AI]目的：インタラクティブなHTMLの修正
- 大規模言語モデルの発展によりHTML生成が可能になったが，動的な挙動の検証が課題となっている。
- スクリーンショットによる評価では，スクロールやクリック時の不具合を見逃しがちである。
- ブラウザ上でのインタラクションを記録し，状態遷移に基づいた修正サイクルを構築すること。
- HTMLCureは，ブラウザでのページ実行と状態遷移を記録し，修正に必要なキーフレームを生成する。
- 97Kのプロンプト群に対し，63703の高品質なページを生成し，最終的に40KページをSFTセットとして構築した。
- HTMLCure-27B-RefinedはHTMLBench-400で50.6を達成し，MiniAppBenchでは平均81.2を記録した。
イノベーション：幻覚のほぼ特徴づけ [cs.LG, cs.AI, cs.IT, math.IT]目的：大規模言語モデルにおける幻覚の性質と回避可能性
- 大規模言語モデルの性能向上には，幻覚の抑制が不可欠である。
- 幻覚の発生メカニズムが十分に解明されておらず，効果的な対策が困難である。
- 幻覚の根本的な原因を特定し，発生率を理論的に評価することを目指す。
- 本研究では，モデルの訓練データ外の出力を生成する傾向を示す「イノベーション」という概念を導入した。
- イノベーションは幻覚をほぼ特徴づけるものであり，幻覚はイノベーションを意味し，その逆もまた真である。
- 訓練データの不足度合い（missing mass）に基づく幻覚率の下限値を新たに導出した。
顧客順列に基づく電気自動車経路構築における分割位置と充電タイミングの最適化 [cs.DS]目的：顧客順列に基づく電気自動車経路構築における，最適な分割位置と充電タイミングの決定
- 持続可能な物流を実現するため，電気自動車の効率的なルート構築が不可欠である。
- 既存手法では，ルート分割と充電所訪問の決定が独立しており，最適化が困難である。
- 顧客順列が固定された状態での，最小距離な実行可能ルートを効率的に構築することを目指す。
- 固定順列分割充電問題として本課題を定式化し，動的計画法と支配幅探索を用いた厳密解法を提案した。
- 提案解法は，ルート分割と充電所挿入の簡略化された戦略と比較検証され，実行可能性と解質が確認された。
- 最も制約の強い簡略化戦略は，ヒューリスティック解法と同等の時間で高い成功率と解質を達成した。
GitHub Actions言語：利用状況，進化，ワークフローの信頼性 [cs.RO, cs.CL, cs.SE]目的：GitHub Actions言語の利用状況と進化がワークフローの信頼性と保守性に与える影響の分析
- ソフトウェア開発における自動化は，開発効率と品質向上の鍵であり，継続的インテグレーションと継続的デリバリー(CI/CD)の重要性が増している。
- GitHub Actionsワークフロー設定の維持管理は難しく，実行失敗が頻繁に発生しているという課題が存在する。
- GitHub Actions言語の利用状況を分析し，信頼性と保守性に影響を与える要素を特定することで，ワークフローの改善に貢献する。
- 26万件のワークフロー（4.9万のリポジトリから）を定量的に分析した結果，少数の言語構成要素と機能が頻繁に使用されていることがわかった。
- 大規模で複雑なワークフローは，高い失敗率とより多くの保守作業に関連していることが明らかになった。
- 信頼性と保守性のリスクと関連性の高い特定の機能が特定され，実務者や研究者がGitHub Actions言語の理解と利用を改善するための洞察を提供する。
信号時相論理の効率的なオンライン監視 [cs.NI, cs.LO]目的：信号時相論理のオンライン監視に関する高性能なライブラリ
- 自動運転やロボティクスなど，安全性が重要なシステムにおいて，時相論理に基づく仕様検証が不可欠である。
- 従来の監視手法では，計算コストが高く，リアルタイム性が求められる状況での利用が困難であった。
- 本研究では，大規模な時相論理式に対しても効率的な監視を可能とする新しいアルゴリズムを提案する。
- 提案手法は，RoSIやブーリアン評価など，複数のSTLセマンティクスを統一的に扱えるインターフェースを提供する。
- ボトムアップ動的計画法と演算子ごとのキャッシュ，ストリーミング極値計算により，監視処理を高速化している。
- RustとPythonでSTLドメイン固有言語を実装し，Rustでは静的構文チェックのためのプロシージャマクロを導入している。
LLMベースのモックレス単体テスト生成（Java向け） [cs.SE]目的：JavaにおけるLLMを用いたモックレス単体テストの自動生成
- ソフトウェア品質保証において，単体テストは欠かせないプロセスである。
- 従来の単体テスト生成はモックフレームワークに依存し，実際の低レベルコードの実行が不十分になる場合がある。
- LLMの幻覚や制約違反といった課題を克服し，より高品質なモックレス単体テスト生成を実現すること。
- MocklessTesterは，既存コードの利用パターンに基づいた文脈付与生成と，記号・プロトコル・反復レベルの制約に基づく修正を組み合わせる。
- Defects4JとDeps4Jを用いた評価により，行カバレッジが19.99%～22.69%，ブランチカバレッジが15.78%～24.90%向上した。
- ミューテーションスコアも向上し，被試験クラスだけでなく依存関係クラスのコードもより多く実行することが確認された。
共同コミットメントのための動的義務論的単純複合論理 [cs.LO]目的：共同コミットメントに関する義務論的論理
- 社会における合意形成や協調行動を形式的に分析する上で重要である。
- 義務や責任の概念を多人数間の関係性の中で扱う論理体系が不足している。
- 単純複合論理を用いて，個々のコミットメントと共同コミットメントの関係を明確化する。
- 本研究では，頂点が個々のコミットメント，高次元の単体(シンプレックス)が共同義務を表す義務論的単純複合論理(DSL)を提案した。
- DSLを拡張した動的義務論的単純複合論理(DDSL)は，相互排他的なコミットメント間の選択をモデル化し，個々の行動や共同行動の影響を捉える。
- 静的および動的単純複合論理について健全性と完全性が証明された。
節約型学習増強オンライン距離マッチング [cs.DS, cs.LG]目的：節約型学習増強アルゴリズムの設計と性能限界の確立
- オンライン最適化は，計算資源の制約下でリアルタイムな意思決定を必要とするため重要である。
- 学習増強アルゴリズムは予測回数と性能のトレードオフがあり，予測コストが課題となっている。
- 距離マッチング問題における予測回数を削減し，効率的なアルゴリズムを開発することを目標とする。
- 提案手法は，予測がない場合に仮想予測を補完することで，節約型学習増強を実現している。
- 理論的解析により，提案手法の性能限界が明らかになった。
- 実験結果は，提案手法の有効性を示している。
LLMによるソフトウェアデザインパターンの利用誘導戦略：Singletonの場合 [cs.SE, cs.AI]目的：LLMによるデザインパターンの組み込みを促す戦略の特定
- ソフトウェア開発における品質と保守性の向上がデザインパターン利用の重要性を高めている
- LLMはコード生成能力を持つが，デザインパターンの一貫した適用が課題となっている
- 生成コードにおけるデザインパターンの適用能力向上を目指す
- 最適な戦略はモデルの種類に依存するが，反復的な二値フィードバックがSingletonパターンとの整合性で優れていた
- Llama 3.3は指示による誘導でSingletonクラスを100%生成し，テスト合格率を34.1%向上させた
- Qwen 3 (8B)は二値フィードバックにより，Singletonパターンとの整合性を99.2%，機能性を58.6%に向上させた
ファクタグラフにおける可換因子の検出：必要条件と十分条件 [cs.AI, cs.DS, cs.LG]目的：ファクタグラフにおける可換因子の識別
- 確率グラフィカルモデルの効率的な推論には，対象の識別可能性の利用が不可欠である。
- 既存の可換因子検出アルゴリズムは，誤った十分条件に基づいている可能性がある。
- 可換因子の識別に関する理論的基盤を修正し，より正確なアルゴリズムを提案する。
- 既存のアルゴリズムが誤った結果を導く場合があることを示した。
- 可換因子の識別に関する修正された定理を証明した。
- 効率性と正確性を両立した修正アルゴリズムと，より厳密な限界を持つ補完アルゴリズムを提示した。
データ機密分野におけるLLM出力の神経記号的検証 [cs.CL, cs.IR, cs.MM, cs.AI, cs.LO, cs.SE]目的：LLM出力の信頼性確保
- 高リスク分野でのLLM利用拡大に伴い，その信頼性確保が不可欠である。
- LLMは幻覚，矛盾，プライバシー侵害といった課題を抱え，深刻なリスクをもたらす。
- LLMの出力検証に，形式的検証と神経意味解析を組み合わせた手法を提案する。
- 提案アーキテクチャは，入力検証に論理推論，出力検証に意味的類似性を活用し，互補的な保証を提供する。
- HAIMEDAを用いた評価により，構造化エンティティの幻覚検出率は83％以上，意味的虚偽は72％以上を達成した。
- レポート作成時間の30%削減も確認され，データ機密分野におけるLLMの安全な導入を支援する可能性を示した。
MerLean-Prover: エンドツーエンドのLean 4定理証明のための再帰ループハーネス [cs.LO, cs.CL]目的：エンドツーエンドのLean 4定理証明システム
- 形式的な検証の自動化は，ソフトウェアやハードウェアの信頼性向上に不可欠である。
- 定理証明は計算資源を大量に消費し，複雑な定理に対しては自動化が困難である。
- より効率的で，汎用的な定理証明ハーネスの開発を目指す。
- MerLean-Proverは，23個の博士課程試験レベルの定理からなるFormalQualBenchにおいて，10個の定理を証明することに成功した。
- Putnam2025の全12個の定理を，既存の最高性能システムよりも短い時間で証明した。
- 小型モデル（Sonnet, Haiku）においても有効であり，ハーネス設計の重要性を示唆する。
ReasonOps：信頼性の高い検証済みLLM推論のための統一的な運用パラダイム [cs.LO, cs.AI]目的：信頼性の高い検証済みLLM推論のための統一的な運用パラダイム
- LLMの推論能力向上により，AIは生成だけでなく，論理的思考を行うシステムへと進化している。
- 既存の推論システムは，論理的不整合や誤った推論，根拠のない定理適用，信頼性の低さといった問題を抱えている。
- 形式検証，実行時保証，ニューロシンボリック推論などの分野を統合し，信頼性の高いAIシステムの基盤を構築すること。
- 本研究では，ReasonOpsという統一的な運用パラダイムを提案し，推論プロセスを継続的に監視・検証可能にする。
- ReasonOpsは，意味解釈，自動形式化，記号推論，定理証明，実行時保証などを統合した推論ライフサイクルを提供する。
- 自動ブレーキシステムの分析例を通じて，ReasonOpsアーキテクチャの有効性を示し，安全性が重要な自律型AIシステムへの応用可能性を議論した。
コントラクトとループ不変量の合成によるスケーラブルな形式検証 [cs.SE, cs.AI]目的：大規模Cプログラムの形式検証
- ソフトウェアの信頼性確保は重要であり，形式検証はそのための強力な手法である。
- 状態空間爆発問題により，大規模プログラムの形式検証は困難である。
- 大規模なプログラムも効率的に検証可能な手法を提案する。
- ConVerは，LLMを用いて関数コントラクトを合成し，トップダウン型の検証を行うことで，状態空間爆発問題を軽減する。
- Frama-Cベンチマークにおいて，ConVerは82-96%の検証成功率を達成し，多くの場合，単一のCEGAR-CEGIS反復で収束した。
- LF VerifierベンチマークをCに変換して検証した結果，67%のベンチマークで成功した。
- 1
- 2