arXiv雑要約

• Top
• AI
• プログラム
• 画像・音声
• セキュリティ
• 数値解析

プログラム - 2026/03/02 公開

• 量子制御とユニタリーケースを超えた一般再帰 [cs.LO]目的：量子操作のコヒーレント制御を可能にする再帰を持つ量子プログラミング言語の設計

  • 量子計算の基礎概念であり，量子ソフトウェア開発にも不可欠な技術である。
  • 再帰や測定を含む状況下でのコヒーレント制御の定義が困難であった。
  • 再帰，測定，コヒーレント制御を組み合わせた量子プログラミング言語を開発し，その理論的基盤を確立する。
  • 再帰を持つ量子プログラミング言語を設計し，操作的および表現的意味論を定義した。
  • この言語は，任意の量子操作のコヒーレント制御を可能にする。
  • 定義された意味論は，観測的同値性に対して完全抽象性を持つことが示された。

  Link: https://arxiv.org/abs/2507.10466

• 離散領域を超えた近似SMTカウント [cs.LO, cs.AI]目的：ハイブリッドSMT数式のモデルカウント手法

  • 自動推論の分野で重要な役割を担うSMTソルバの発展
  • 離散変数に限定される既存のアプローチによる制約
  • ハイブリッド数式における離散領域への投影解のカウント問題の解決
  • pactは，理論的な保証付きで解を推定するためのハッシュベースの近似モデルカウントを用いる。
  • 投影変数に関して，SMTソルバを対数的に呼び出す回数に抑えることができる。
  • 大規模なベンチマークスイートにおいて，既存手法と比較して大幅な性能向上を達成した。

  Link: https://arxiv.org/abs/2507.18612

• 異方性メッシュ細分化の美しさ：効率的なダイアディック離散化のためのオムニツリー [cs.DS, cs.CG, cs.GR, cs.IT, cs.NA, math.IT, math.NA]目的：異方性問題に対する効率的な離散化手法の開発

  • 様々な分野で適応メッシュ細分化が活用されている。計算効率と精度の向上が求められている。
  • オクトリーは等方的に細分化するため，異方性問題に対して非効率な場合がある。
  • オムニツリーを用いて，必要な方向にのみ細分化することで効率化を図る。
  • オムニツリーは，従来のオクトリーよりも高い収束率を示すことが，3次元形状データの検証で確認された。
  • オムニツリーは，同等の誤差範囲を達成するために必要なストレージ量を削減できることが示された。
  • 高次元問題におけるオムニツリーの利点が，4次元回転を用いた検証により示唆された。

  Link: https://arxiv.org/abs/2508.06316

• SATへの入出力論理の帰着 [cs.LO, cs.AI]目的：入出力論理の自動化手法

  • 規範，義務，許可などを扱う様相論理は，倫理学や法学などに応用が期待される。
  • 従来の様相論理では，規範を対象の論理言語外で扱うことが難しかった。
  • 入出力論理の自動推論を可能にする手法を提示し，その有効性を検証する。
  • 入出力論理を命題充足可能性問題(SAT)への帰着により自動化する手法を提案した。
  • 提案手法の実装であるrioを開発し，具体的な例題への適用を示した。
  • 本手法により，入出力論理における規範の推論を効率的に行うことが期待される。

  Link: https://arxiv.org/abs/2508.16242

• 一度だけで全て：LLMによる生成器を用いたスケルトンガイド型SMTソルバーファジング [cs.SE, cs.AI, cs.PL]目的：SMTソルバーのバグ検出

  • 現代のシステムやプログラミング言語研究の基盤であり，その信頼性は不可欠である。
  • 従来のテスト手法では，ソルバーの進化に追いつけず，十分なバグ検出が困難である。
  • LLMを活用し，構文的に有効で多様なテストケースを効率的に生成することで，問題を解決する。
  • Once4Allは，LLMを用いてSMT理論の文法を自動抽出し，再利用可能な項の生成器を合成する。
  • 既存の数式から構造的スケルトンを作成し，LLM生成器で生成された項を反復的に埋め込むことで，構文の有効性と意味的多様性を確保する。
  • Z3とcvc5の2つの主要なSMTソルバーで評価した結果，43件のバグが確認され，そのうち40件は既に修正されている。

  Link: https://arxiv.org/abs/2508.20340

• RSAの量子耐性強化に向けた制約付きRényiエントロピー最適化：後方互換性のある暗号のための数学的フレームワーク [cs.CR, cs.IT, math.IT, quant-ph]目的：RSA暗号の量子耐性向上

  • RSA暗号は広く利用されており，現代のインターネットセキュリティの基盤を支えている。
  • 量子コンピュータの出現により，RSA暗号はShorのアルゴリズムによって解読される危険に晒されている。
  • 既存のRSAインフラを置き換えることなく，量子コンピュータに対する耐性を高める方法を模索する。
  • 制約付きRényiエントロピー最適化(CREO)フレームワークによって，RSA素数の近接性を制約することで，Shorのアルゴリズムにおける量子状態の識別性を低減できる。
  • CREOを適用した場合，信頼性の高い周期抽出に必要な量子測定回数は，標準的なRSAと比較して増加する。
  • 素数間隔の定理を用いた構成的な存在証明により，CREOフレームワークの実現可能性が示されている。

  Link: https://arxiv.org/abs/2509.00104

• GitHubにおける浮動小数点数の利用状況：静的型付け言語の大規模調査 [cs.PL, cs.SE]目的：GitHub上の静的型付け言語における浮動小数点数の利用状況

  • 浮動小数点演算は複雑であり，その正確な理解はソフトウェア開発において重要である。
  • 既存の浮動小数点数に関する研究は，実際のコードベースでの利用状況を十分に反映していない場合がある。
  • 実際のコードベースにおける浮動小数点数の利用状況を把握し，より実用的な分析手法を開発すること。
  • 本研究では，GitHub上の数百万のリポジトリを対象に，浮動小数点数の利用状況を大規模に調査した。
  • その結果，浮動小数点演算は広く利用されていることが確認された。また，既存のベンチマークと実際のコードベースの間には相違点が見られた。
  • 本研究で収集した1000万件の浮動小数点数関数からなるデータセットを公開し，今後の研究に役立てることを目指す。

  Link: https://arxiv.org/abs/2509.04936

• 機能情報分解：機能的関係の分析に対する原理第一主義的アプローチ [cs.CY, cs.RO, cs.SY, eess.SY, cs.CY, cs.HC, cs.CY, cs.RO, cs.SY, eess.SY, cs.IT, math.IT]目的：多変量系の相互作用における，複数の入力がどのように出力に共同で影響を与えるかの分解

  • 複雑な系の理解には，要素間の機能的関係を明確化することが不可欠である。
  • 既存の手法では，観測データに依存し，真の相互作用を見落とす可能性がある。
  • システムの完全な入力-出力マッピングに基づいて，情報成分を明確に定義すること。
  • FIDは，独立および相乗的な寄与への一意な分解を提供する。
  • 部分的な観測しかない場合でも，FIDは整合性のある分解の空間を特徴づける。
  • 論理関数，ライフゲーム，癌薬物応答予測への応用を通じて，FIDの有用性が示された。

  Link: https://arxiv.org/abs/2509.18522

• プラットフォームによるエージェントワークフローにおける障害のライフサイクル解明 [cs.AI, cs.SE]目的：プラットフォームによるエージェントワークフローの障害の現れ方，根本原因，および対応策の特定

  • ローコードプラットフォームによるエージェントワークフローは開発を加速するが，信頼性・保守性の課題がある
  • 自然言語やツール連携を介して障害が伝播しやすく，原因特定と修復が困難である
  • エージェントワークフローにおける障害メカニズムを明らかにし，信頼性の高い設計・修復を支援する
  • 307件の実際の障害事例を含むデータセットAgentFailを構築し，分析を行った。
  • 障害パターン，根本原因，修復の難易度には，ワークフローのノードや原因によって差異が見られた。
  • エージェントワークフローの主要な障害メカニズムを特定し，実用的な設計・修復ガイドラインを提示した。

  Link: https://arxiv.org/abs/2509.23735

• スペキュレーション通過スタイルによるSpectreセキュリティの(不)証明 [cs.PL]目的：Spectre脆弱性検出のための定数時間検証の形式的な基盤

  • 暗号ライブラリにおけるサイドチャネル攻撃の検出は，情報セキュリティにおいて重要な課題である。
  • 既存の定数時間検証ツールからSpectre脆弱性を検出する手法は，形式的な定義と分析が不足している。
  • スペキュレーション通過スタイル(SPS)変換を用いて，Spectre脆弱性検証を定数時間検証に帰着させ，実用的な利点を示す。
  • SPS変換は，プログラムを攻撃者の予測に従うように変更し，定数時間検証に変換する。
  • SPS変換は，プログラムがスペキュレーション安全であることと，その変換結果が定数時間安全であることの同値性を示す。
  • 既存の定数時間検証ツール(EasyCrypt, BINSEC, ctgrind)とSPS変換を組み合わせ，Spectre-v1のベンチマークで評価を行った。

  Link: https://arxiv.org/abs/2510.11573

• 連続アパーチャアレイにおける相互結合：物理モデルとビームフォーミング設計 [cs.IT, math.IT]目的：連続アパーチャアレイにおける相互結合現象の解析と最適ビームフォーミング設計

  • 電波利用技術の高度化に伴い，高効率なアレイアンテナの設計が重要視されている。
  • アレイアンテナにおいて，相互結合の影響を無視した設計は，性能劣化を引き起こす可能性がある。
  • 偏波特性と損失を考慮した物理モデルに基づき，相互結合を考慮した最適ビームフォーミングを確立する。
  • 偏波が異方的な結合を引き起こし，従来の半波長間隔規則が無効になることが示された。
  • 相互結合を考慮したビームフォーミング設計問題は，変分法を用いて最適化された。
  • 数値シミュレーションにより，結合モデルの物理的な妥当性と偏波の影響が確認された。

  Link: https://arxiv.org/abs/2511.11225

• 繰り返し欠陥発生源の特定と予測：極めて欠陥しやすいソースメソッドの特徴付け [cs.SE]目的：極めて欠陥しやすいソースメソッドの存在頻度，コード品質指標，および導入時点での予測可能性

  • ソフトウェア品質向上には，欠陥の早期発見と予防が不可欠である。そのため，経験的ソフトウェア工学における欠陥予測研究は重要視されている。
  • 従来の欠陥予測はクラスやファイル単位で行われることが多く，実践的な価値が低いという課題があった。メソッドレベルでの予測への注目が高まっている。
  • 複数回欠陥を引き起こす「極めて欠陥しやすい」メソッドに焦点を当て，その特性を分析し，早期予測の可能性を探る。
  • オープンソースJavaプロジェクトから抽出した125万件以上のメソッドを分析した結果，極めて欠陥しやすいメソッドは少数だが，プロジェクト全体の欠陥の大きな割合を占めていることが判明した。
  • 極めて欠陥しやすいメソッドと他のメソッドの間には統計的に有意な差が見られたものの，その予測は依然として困難である。
  • 手動分析の結果，これらのメソッドには共通する特徴が複数存在することが明らかになり，今後の研究や実践への示唆が得られた。

  Link: https://arxiv.org/abs/2511.22726

• 長距離LLM強化学習のためのトラストリージョンマスキング [cs.LG, cs.AI, cs.IT, math.IT, stat.ML]目的：大規模言語モデル強化学習における，長距離タスクに対する改善保証

  • 大規模言語モデルの強化学習は，複雑なタスクの自動化に不可欠であり，その性能向上は重要な課題である。
  • 従来の強化学習手法は，大規模言語モデル特有のオフポリシー不一致や近似誤差の影響を受けやすく，長距離タスクでは性能が低下する。
  • 本研究は，トラストリージョンマスキングを提案し，長距離タスクにおける大規模言語モデル強化学習の安定性と改善を保証することを目的とする。
  • 本研究では，KL divergenceおよびTotal Variation distanceに基づいた新しい信頼領域の境界を導出し，従来の境界よりもタイトな保証を提供することを示した。
  • 提案手法であるトラストリージョンマスキングは，信頼領域に違反する系列をマスクすることで，長距離タスクにおいて初めて意味のある単調増加の保証を実現する。
  • 特に，系列レベルでのKL divergenceの最大値を制御することで，トークン独立な手法では困難だった安定的な学習を可能にした。

  Link: https://arxiv.org/abs/2512.23075

• 直接衛星通信におけるセマンティック伝送フレームワーク [cs.RO, cs.IT, eess.SP, math.IT]目的：直接衛星通信におけるセマンティック伝送の最適化

  • 衛星通信は，広範囲な通信を可能にする重要な技術であり，災害時のインフラとして不可欠である。
  • 現在の衛星通信では，リンク予算の不足が直接アクセスを妨げる大きな課題となっている。
  • 本研究は，限られたリソース下でのセマンティック伝送効率を最大化し，通信品質の向上を目指す。
  • 提案手法では，伝送モード選択，衛星-ユーザー割り当て，ISLタスク移行などを同時に最適化することで，セマンティック効率を向上させている。
  • 実現可能性を考慮した行動空間と安定化されたポリシー更新を用いるREINFORCE++アルゴリズムを提案し，複雑な非線形整数計画問題を解決している。
  • 数値実験の結果，提案アルゴリズムは既存手法と比較して，より高いセマンティック効率を実現することが示された。

  Link: https://arxiv.org/abs/2601.00381

• LIA：課題自動割り当てのための大規模言語モデルの教師ありファインチューニング [cs.AR, cs.OS, cs.PF, cs.SE, cs.AI]目的：課題の自動割り当てに関する研究

  • ソフトウェア保守において，課題の適切な割り当ては，効率的な開発と品質維持に不可欠である。
  • 大規模なオープンソースプロジェクトでは，手動割り当ては非効率で，人的ミスが発生しやすい。
  • 既存手法は，十分な学習データや信頼性の高い関係情報がない場合，効果が限定される問題を解決する。
  • 提案手法LIAは，大規模言語モデルをファインチューニングすることで，課題のタイトルと説明文から開発者をランク付けして推奨する。
  • 実験結果から，LIAはベースモデルと比較してHit@1で最大187.8%の改善を示し，最先端手法をも凌駕することが示された。
  • この結果は，ドメイン適応された大規模言語モデルがソフトウェア保守タスクに有効であることを示唆し，LIAの実用性を裏付けている。

  Link: https://arxiv.org/abs/2601.01780

• ラムダ計算における群と逆半群 [cs.LO]目的：ラムダ項の可逆性に関する研究

  • ラムダ計算は計算理論の基礎であり，プログラミング言語や形式システムに影響を与えている。
  • ラムダ項の可逆性に関する既存の研究は，特定の理論に限定される場合が多い。
  • より広範な理論において，ラムダ項の可逆性を特徴づけることを目指す。
  • 有限遺伝的置換(FHP)は，最小拡張ラムダ理論において可逆な要素を構成する。
  • 無限遺伝的置換(HP)は，最大の妥当なラムダ理論において可逆な要素を構成する。
  • FHPおよびHPは，ラムダ理論Tを法とした逆半群を形成し，その自然順序はη-展開に対応する。

  Link: https://arxiv.org/abs/2602.05654

• GitHubの世界への没入：コーディングエージェントを熟練度へ [cs.SE]目的：大規模な高品質なソフトウェアエンジニアリング学習データ

  • 現実世界のソフトウェア開発では，質の高い学習データの不足が課題である。
  • 環境構築，ユニットテスト生成，問題文作成の複雑さから，データ拡充が困難である。
  • 大規模データ自動生成による学習データ不足の解消を目指す。
  • ScaleSWEにより，5200リポジトリの600万件のプルリクエストを処理し，10万件の検証済みSWEインスタンスを生成した。
  • このデータセットは，既存のデータセットと比較してリポジトリの多様性とタスクの複雑さにおいて優れている。
  • ScaleSWE AgentはSWE Bench Verifiedで64%の解決率を達成し，ベースモデルを大幅に上回った。

  Link: https://arxiv.org/abs/2602.09892

• エージェント型自動化キャンバス：エージェントAIプロジェクト設計のための構造化フレームワーク [cs.SE]目的：エージェントAIプロジェクトの構造的な設計，ガバナンス，将来的な評価のためのフレームワーク

  • エージェントAIの活用は急速に進んでいるが，その設計と運用には体系的な方法論が不可欠である。
  • 既存のAIドキュメントは，事後的なものであったり，機械可読性や相互運用性が不足している。
  • エージェントAIプロジェクトの設計段階から，関係者間のコミュニケーションを円滑にし，品質を向上させる。
  • 本研究では，エージェント型自動化キャンバス（AAC）という構造化フレームワークを提案した。
  • AACは，プロジェクトの定義，ユーザーの期待，開発者の評価，ガバナンス，データアクセス，結果の6つの側面を捉える。
  • 完成したキャンバスはFAIR原則に準拠したRO-Crateとしてエクスポートされ，ユーザーと開発者の間の機械可読な契約を可能にする。

  Link: https://arxiv.org/abs/2602.15090

• DSLean：Lean 4と外部DSL間の型安全な相互運用フレームワーク [cs.HC, cs.CY, cs.LO]目的：Lean 4と外部DSL間の双方向変換

  • 対話的証明支援システムと外部自動化の連携において，DSLが重要な役割を果たす。
  • 証明支援システムの内部表現とDSL間の変換は，手間のかかるエンジニアリング作業である。
  • DSL間の変換作業を簡素化し，外部ソルバーの活用を容易にすること。
  • DSLeanフレームワークは，外部言語の仕様とLean相当性のみを必要とし，メタレベルの実装詳細は抽象化される。
  • 区間演算，常微分方程式，環イデアルメンバーシップ向けの3つの新しい自動化タクティクスを実装することで，DSLeanの能力が示された。
  • 本フレームワークは，DSL間の相互運用性を高め，外部自動化の導入を促進する。

  Link: https://arxiv.org/abs/2602.18657

• 現代LLMエージェントフレームワークにおけるバグの実証的調査 [cs.SE]目的：LLMエージェントフレームワークにおけるバグの分類と原因分析

  • LLMエージェントは実用化が進んでおり，その信頼性確保が重要である。
  • 既存研究はエージェント自体の問題に偏り，フレームワークレベルのバグ調査が不足している。
  • エージェントフレームワークのバグの根本原因と可視的な症状を特定し，改善に資することを目的とする。
  • CrewAIとLangChainの998件のバグレポートを分析した結果，15種類の根本原因と7種類の症状が特定された。
  • バグの主な原因は「APIの誤用」「APIの非互換性」「ドキュメントとの不一致」であり，「Self-Action」段階に集中している。
  • 症状としては，「機能エラー」「クラッシュ」「ビルド失敗」が頻繁に発生し，タスクの進行と制御フローの妨げとなっている。

  Link: https://arxiv.org/abs/2602.21806

• 大規模言語モデルを活用した深層学習ライブラリにおける無音バグファジング：多様かつ制御されたバグ転移によるアプローチ [cs.SE]目的：深層学習ライブラリにおける無音バグの検出

  • 深層学習ライブラリは重要システムで広く利用されており，信頼性が不可欠である。
  • 既存のファジング技術は，テストプログラムやオラクルの不足から無音バグの検出が困難である。
  • 過去のバグレポートに含まれる情報を活用し，リスクの高いバグを転移することで無音バグを検出する。
  • 提案手法TransFuzzは，PyTorch，TensorFlow，MindSporeの3つの主要な深層学習ライブラリで評価された。
  • その結果，79個の未知のバグ（12個はCVEとして確認）が10種類のバグタイプで発見された。
  • この成果は，深層学習ライブラリのバグ検出能力を向上させる本手法の有効性と汎用性を示すものである。

  Link: https://arxiv.org/abs/2602.23065

• 関数契約生成のための配列伝播シンボリック実行 [cs.PL, cs.LO, cs.SE]目的：関数契約の生成

  • プログラム全体の解析には，関数ごとの特性把握が不可欠であり，関数契約はその基盤となる。
  • 配列操作を含むプログラムでは，配列領域に対する不変条件の推論が困難である。
  • 配列領域の情報を伝播することで，既存手法では扱えなかった関数の解析を目指す。
  • 提案手法は，LLVMにプロトタイプを実装し，ACSLやFrama-Cとの連携を実現した。
  • 様々なベンチマークと実用的なライブラリ関数に対して実験を行い，有効性を検証した。
  • 配列操作を含む関数において，既存手法を上回る契約生成能力が確認された。

  Link: https://arxiv.org/abs/2602.23216

• ヘイティング・ルイス含意に対するゲーデル-マッキンゼイ-タルスキおよび(完全ではない)ブロック-エサキア [math.LO, cs.LO]目的：ヘイティング・ルイス論理の記述的フレームと代数的解釈の間の圏論的双対性

  • ヘイティング・ルイス論理は様々な分野で現れ，理論的な重要性が高い。
  • ヘイティング・ルイス論理のモデル理論的な性質は完全には解明されていない。
  • ヘイティング・ルイス論理の有限モデル性および決定可能性を示す。
  • ヘイティング・ルイス論理を古典様相論理に変換する変換を適用することで，古典的な結果を活用できる。
  • 記述的フレーム（エサキア空間の一般化）を定義し，代数的解釈とフレーム意味論の間の圏論的双対性を確立した。
  • ヘイティング・ルイス論理の広い範囲に対し，有限モデル性と決定可能性が示された。

  Link: https://arxiv.org/abs/2105.01873

• 自己教師あり刺激符号化のためのスペクトル-刺激情報 [q-bio.NC, cs.IT, cs.LG, cs.NE, math.IT]目的：空間における効率的な場所細胞の符号化原理の解明

  • 哺乳類の空間ナビゲーションは，場所細胞やグリッド細胞など特殊なニューロンに依存する。
  • 既存の空間情報レート指標は単一ニューロンの符号化しか評価できず，集団レベルでの表現に関する知見が限られている。
  • ニューロン集団の符号化効率を評価し，人工ナビゲーションシステムの最適化を目指す。
  • スペクトル-刺激情報は，局所的で重ならない発火場を持つニューロンで最大化され，場所細胞や頭方向細胞の活動を反映する。
  • マウスとサルからの神経データへの適用により，ニューロンペアと集団間の符号化効率の違いが明らかになった。
  • これらの指標を用いてRNNを自己教師あり学習させると，場所細胞や頭方向細胞が出現することが示された。

  Link: https://arxiv.org/abs/2407.06195

• 環とブール代数：代数的理論として [math.LO, cs.LO]目的：環とブール代数の表現

  • 代数学の基礎をなす重要な概念であり，多様な分野に応用がある。
  • 環やブール代数の構造を統一的に捉える枠組みが不足していた。
  • 代数的理論を用いて環とブール代数を表現し，関係性を明らかにする。
  • 可換環とブール環は，それぞれアフィン代数的理論とハイパーアフィン代数的理論を通して表現できる。
  • ブール環上のアフィン理論のモデルは，ブールベクトル空間として特徴づけられる。
  • ハイパーアフィン理論は，多次元ブール代数と密接な関係があることが示された。

  Link: https://arxiv.org/abs/2503.04430

• 量子妨害に対するチャネル符号化：ミニマックスアプローチ [quant-ph, cs.CC, quant-ph, cs.IT, math.IT]目的：完全量子変動チャネルの容量特性

  • 量子情報理論の発展は，安全な通信や量子コンピュータ実現に不可欠である。
  • 量子妨害に対する通信容量の評価は，従来の古典的な手法では困難であった。
  • ミニマックスアプローチを用いて，量子妨害下での通信容量を厳密に評価すること。
  • ミニマックスアプローチにより，次元に依存しない簡潔な容量評価が可能になった。
  • エンタングルメント支援および共有乱数支援型の完全量子変動チャネル容量が，対応する複合チャネルと一致することが示された。
  • この結果は，一般的な量子妨害下における安全な通信設計に貢献する。

  Link: https://arxiv.org/abs/2505.11362

• 1
• 2