arXiv雑要約
プログラム - 2025/12/18 公開
AuDaLaの表現力:チューリング完全性と可能な拡張 [cs.LO, cs.PL]目的:AuDaLaの表現力の評価
- データ自律パラダイムは,分散処理や並列処理における新しい可能性を示唆している。
- AuDaLaのような新しいパラダイムにおける言語の表現力は,その実用性を評価する上で重要である。
- AuDaLaの表現力を理論的に評価し,拡張可能性を検討することで,実用的な応用範囲を広げる。
- 本研究により,AuDaLaがチューリング完全であることが証明された。
- AuDaLaでチューリングマシンを実装し,その正当性を検証したことが,この証明の根拠である。
- AuDaLaの表現力を向上させるための拡張方法についても提案し,並列処理言語との適合性改善を示唆した。
生成事前分布を用いた効率的な最適化:粗い学習可能性によるアプローチ [cs.LG, cs.DS, stat.ML]目的:生成事前分布を用いた最適化におけるサンプル効率の向上
- 組み合わせ最適化問題等において,目的関数評価のみで解を探索する手法は重要である。
- 深層生成モデルを事前分布として利用する場合,サンプル複雑度に関する理論的保証が不足している。
- 深層生成モデルの粗い学習可能性を仮定することで,サンプル効率の良い最適化手法を開発する。
- 提案手法は,Metropolis-Hastings補正を用いることで,多項式個のサンプルで目的分布を近似的に求めることを保証する。
- 最大最尤推定が粗い学習可能性に必要なカバレッジ特性を自然に誘導することを理論的に示す。
- 大規模言語モデルが,ゼロ次フィードバックに適応し,組み合わせ最適化問題を解決できることを実験的に示す。
特徴重要度を考慮した計算効率と調整可能な画像伝送のための深層結合ソースチャネル符号化 [cs.IT, math.IT]目的:計算効率と調整可能性を両立した画像伝送のための特徴重要度を考慮した深層結合ソースチャネル符号化モデル
- 深層学習の進展により通信性能は向上したが,その高い計算コストが実用化の障壁となっている。
- 特定のアプリケーションでは,計算複雑さを動的に調整する能力が求められる。
- 計算コストを削減しつつ,特徴を効果的に表現し,複雑な特徴相関を効率的に捉えることを目指す。
- FAJSCCは,空間軸とチャネル軸それぞれに対して効率的な演算を行うことで,計算コストを大幅に削減する。
- 選択的な変形可能自己注意機構により,重要な特徴にのみ自己注意を適用し,特徴間の関係性を効率的に捉える。
- FAJSCCは,エンコーダとデコーダでそれぞれ独立して重要領域の数を制御可能であり,計算資源に応じて複雑さを調整できる。
曲線表現ブレグマンダイバージェンスとその応用 [cs.IT, cs.LG, math.IT]目的:曲線表現ブレグマンダイバージェンスの定義と応用
- 機械学習や情報理論において,距離尺度や類似度尺度の重要性は高い。
- 従来のブレグマンダイバージェンスは線形空間に限定され,非線形空間への拡張が課題であった。
- 非線形部分空間におけるブレグマンダイバージェンスを定義し,その応用可能性を示す。
- 曲線表現ブレグマンダイバージェンスは,非線形パラメータ部分空間に制限されたブレグマンダイバージェンスとして定義される。
- 有限重み付きパラメータ集合の重心は,完全なブレグマンダイバージェンスに対する重心の部分空間へのブレグマン投影に相当することが示された。
- α-ダイバージェンスが曲線表現ブレグマンダイバージェンスであることが証明され,効率的な交差計算手法が提案された。
「ご迷惑をおかけして申し訳ありません」:開発者のプライバシー準拠実装行動の探求 [cs.SE]目的:ソフトウェア開発者のプライバシー準拠実装における行動様式
- ユーザーデータの保護は不可欠であり,ソフトウェア開発において重要な課題である。
- 開発者はプライバシー要件を満たすことが難しい場合が多く,その原因が不明である。
- 開発者がプライバシー要件を実装する際の課題を明らかにし,支援策の検討に貢献する。
- 参加者の79%がGDPRに準拠しないソリューションを提出し,プライバシー保護の実装が困難であることが示された。
- プライバシーに関する促しや専門家のサポートは,準拠率の向上に限定的な効果しかなく,課題解決には至らなかった。
- 開発者は既存の実装に依存し,機能やセキュリティを優先する傾向があり,専門家への相談も少ないことが明らかになった。
LLMとファジングの連携:最弱事前条件の自動生成への新たなアプローチ [cs.SE, cs.AI, cs.LO]目的:最弱事前条件の生成
- プログラムの検証や実行時エラーチェックなど,実用的な応用範囲が広い重要な課題である。
- 最弱事前条件の生成は複雑であり,正確かつ効率的な自動化が困難である。
- LLMとファジングを組み合わせることで,最弱事前条件の自動生成の精度向上を目指す。
- LLMは実行可能な最弱事前条件候補を生成できることが示された。
- ファジングガイダンスを用いることで,LLMの性能を実質的に向上させることが確認された。
- Javaの決定性配列プログラムのベンチマークセットで有効性が実証された。
制約表現力のある中間表現に基づく3Dソフトウェア合成 [cs.CV, cs.AI, cs.MM, cs.SE]目的:制約表現力のある中間表現に基づく3Dソフトウェアの合成手法
- UIソフトウェアは2Dから3D環境へと変化しており,自動生成技術の重要性が高まっている。
- 既存の3Dソフトウェア生成手法は,特定要素の変更や制御が難しく,複雑な制約への対応が課題である。
- 本研究は,ユーザーの要求と生成された3Dソフトウェア間の形式的なトレーサビリティを維持し,制約充足を実現する。
- Scenethesisは,ユーザー要求の80%以上を正確に捉え,厳密な制約の90%以上を満たすことが示された。
- 100以上の制約を同時に処理可能であり,複雑な空間制約への対応が可能であることが確認された。
- 最先端手法と比較して,BLIP-2ビジュアル評価スコアが42.8%向上し,生成品質の改善が示された。
Isabelle/HOL 上でのニューラル定理証明のためのミニマルな証明言語 [cs.PL]目的:ニューラル定理証明におけるミニマルな証明言語の設計と評価
- 形式的証明は数学の正確性を保証する上で不可欠であり,自動化が求められている。
- 既存の証明言語は複雑で,大規模言語モデル(LLM)による扱いが困難である。
- LLMによる形式的証明を容易にするため,簡潔で直感的な証明言語を設計する。
- Minilangを設計し,Isabelle/HOLの証明を約85%の精度でMinilangに翻訳した。
- Minilang上でファインチューニングしたLLMは,PISAベンチマークでIsarベースのLLMよりも最大29%のpass@1成功率を向上させた。
- Minilangは,最新のSOTAモデルを上回るPISAベンチマークのpass@1(69.1%)およびpass@8(79.2%)の成功率を達成した。
異種プロンプトと実行フィードバックによるSWE課題に対するテスト生成と選択 [cs.SE]目的:SWE課題のテスト生成と選択
- ソフトウェア品質向上には,テストが不可欠であり,課題解決を効率化する。
- 多くのSWE課題には再現テストがなく,テスト生成が困難である。
- 正しいコードがない状況下でも,実行フィードバックを活用したテスト生成を目指す。
- 提案手法e-Otter++は,テスト生成における最先端技術を大きく前進させた。
- TDD-Bench Verifiedベンチマークにおいて,平均して63%のテストが修正後にパスした。
- 実行フィードバックを活用することで,欠損または誤ったコードが存在する状況でもテスト生成が可能になった。
一意な最小全域木と一意な最短経路の強制 [cs.DS]目的:最短経路問題と最小全域木問題における最小強制集合および反強制集合の複雑性
- 組合せ最適化問題において,一意な解を得るための要素集合の特定は重要である。
- 既存研究では,多くの組合せ問題において最小強制集合の発見が古典問題よりも困難である。
- 本研究では,最短経路問題と最小全域木問題における強制集合と反強制集合の複雑性を解析する。
- 最短経路問題と最小全域木問題における最小強制集合および反強制集合の探索は,NP困難なケースを除き,多項式時間で解ける。
- 最短経路問題における最小反強制集合の決定問題はNP困難である。
- 既存研究とは異なり,これらの問題は扱いやすいことが示された。
トレースから行へ:実世界OSS脆弱性局所化のためのLLMエージェント [cs.SE, cs.CR, cs.LG]目的:実世界のOSS脆弱性の正確な行レベル局所化と,それに対応するパッチ生成
- ソフトウェアの脆弱性は深刻なセキュリティリスクであり,迅速な発見と修正が不可欠である。
- 従来の脆弱性検出手法は,コードを孤立して検査し,長いコンテキストに対応できず,局所化精度が低い。
- 本研究は,実行時情報とコード解析を融合し,反復的な絞り込みにより正確な脆弱性局所化を実現する。
- 提案手法T2L-Agentは,プロジェクト全体を分析し,モジュールから脆弱な行へと段階的にスコープを絞り込む。
- 新ベンチマークT2L-ARVOを用いて評価した結果,T2L-Agentは既存手法を大幅に上回る検出率と行レベル局所化率を達成した。
- 本研究は,LLMを用いた脆弱性検出を,粗い識別から実用的な精密診断へと進化させ,OSSソフトウェア開発の効率化に貢献する。
モジュール式抽象構文木 (MAST): 第二級ソートを持つ置換テンソル [cs.PL]目的:第二級ソートを持つ言語に対する抽象構文の扱い
- プログラム言語の理論的基礎を構築する上で,抽象構文の厳密な定義は不可欠である。
- 従来の抽象構文の定義では,第二級ソートを持つ言語を適切に扱えない場合がある。
- 第二級ソートを持つ言語,特にCBVやCBPVにおける置換規則の正確な記述を目指す。
- Fiore, Plotkin, Turiの抽象構文の枠組みを拡張し,第二級ソートを持つ言語に対応した新しい理論を構築した。
- 変数コンテキストにおける第二級ソートの禁止が,抽象構文の圏論的特徴を変化させることを示した。
- CBVの様々なバリエーションに対する置換補題を,構築した理論を用いて証明した。
4/δの境界:形式手法保証のための予測可能なLLM検証システム設計 [cs.AI, cs.FL, cs.LG, cs.SE]目的:LLMと形式検証ツールの統合によるソフトウェア検証のスケール化
- ソフトウェアの安全性確保が重要であり,そのための形式手法は不可欠である。
- LLMを用いた検証は,理論的根拠がないため,不安定で収束性が保証されない。
- 多段階検証パイプラインの終端を理論的に保証し,予測可能なシステム設計を目指す。
- LLMと検証ツールの相互作用を吸収マルコフ連鎖としてモデル化し,終端の理論的保証を確立した。
- 各段階の成功確率が非ゼロであれば,システムはほぼ確実に「検証済」状態に到達することが証明された。
- 9万件以上の実験により,理論値である4/δと実測値が一致し,システムの予測可能性が確認された。
ボルツマン・シャノン指数:クラスタリングバランスの幾何学的認識指標 [cs.IT, math.IT]目的:クラスタリングバランスの評価
- データ解析において,クラスタのバランスは,データの構造理解や公平性の評価に不可欠である。
- 既存の指標では,幾何学的構造と頻度に基づく分布の関係を十分に捉えきれていない場合がある。
- 幾何学的構造と頻度に基づく分布を統合的に評価し,クラスタリングのバランスをより正確に測る。
- ボルツマン・シャノン指数(BSI)は,クラスタ内の幾何学的構造と頻度に基づいた確率分布の関係を定量化する指標である。
- BSIは,従来の指標では不十分または誤解を招く可能性のあるケースにおいて,一貫性のある評価を提供する。
- 資源配分においては,BSIは不均衡を高い感度で検出し,最適化フレームワークに組み込みやすい滑らかな指標となる。
有向グラフにおける最小カットと有向木packingの近似:有向expander階層による手法 [cs.DS]目的:有向グラフにおける最小カット近似と最大有向木packing
- ネットワークフローやグラフ分割など,様々な応用で重要な問題である。
- 従来の最小カット計算は計算量が多く,大規模グラフへの適用が困難であった。
- 効率的な近似アルゴリズムを開発し,大規模グラフでの実用化を目指す。
- 有向グラフのs-rooted最小カットに対し,$O(k\log^{5} n)$程度の近似解を,ほぼ線形時間で算出するアルゴリズムを提案。
- s-rooted arborescence packingにおいて,$n^{o(1)}$のcongestionでk個のarborescenceをpackingするアルゴリズムを提案。
- 提案手法は,既存のアルゴリズムよりも高速であり,実用的な計算時間で解を求めることが可能である。
アルゴリズム符号理論における代数 [cs.IT, cs.CC, math.IT]目的:誤り訂正符号とその効率的な情報伝送のためのアルゴリズム
- 情報社会において,信頼性の高いデータ伝送は不可欠であり,誤り訂正符号はそれを実現する基盤技術である。
- 符号の設計とアルゴリズム開発の間の理解のギャップが存在し,アルゴリズム設計における代数の役割が十分に認識されていない。
- 符号構築における代数の役割に加え,アルゴリズム設計における代数の重要性を明らかにすること。
- 誤り訂正符号は,情報伝送における信頼性を高めるために広く利用されていることが確認された。
- 符号の構築には,線形代数などの応用代数学の基本的な要素が用いられていることが示された。
- アルゴリズム設計においても代数の役割は重要であり,その理解を深めることが,より効率的な符号化・復号化手法の開発に繋がることが期待される。
孔子コードエージェント:実世界のコードベース向けのスケーラブルなエージェント構築 [cs.DL, cs.IR, cs.CL, cs.AI, cs.LG, cs.SE]目的:実世界のコードベースにおけるスケーラブルなソフトウェアエンジニアリングエージェントの構築
- ソフトウェア開発における自動化ニーズが高まっており,大規模コードベースへの対応が課題。
- 既存のエージェントは,大規模なコードベースや複雑なツールチェーンの扱いに課題がある。
- 研究と実用性のギャップを埋め,大規模なコードベースに対応可能なエージェント基盤を提供する。
- 孔子コードエージェント(CCA)は,大規模コードベース上で動作するスケーラブルなソフトウェアエンジニアリングエージェントである。
- CCAは,長文脈推論,継続学習,モジュール化されたツール利用を実現する孔子SDK上に構築されている。
- SWE-Bench-Proにおいて,Resolve@1で54.3%を達成し,既存研究や商用システムと比較して高い性能を示した。
シグナルからターンへ:モジュール型音声対話パイプラインにおける相互作用的な摩擦 [cs.HC, cs.AI, cs.CL, cs.SE]目的:モジュール型音声対話パイプラインにおける相互作用的な摩擦の分析
- 音声AIは生成能力が向上しているが,自然な対話が困難である。より人間らしいAI対話を実現する必要がある。
- 既存システムは,応答遅延や表現力の低下といった問題があり,円滑な対話の妨げとなっている。
- モジュール設計が対話の摩擦を生む構造的な要因を特定し,自然な対話AIのインフラ設計指針を示す。
- モジュール型音声対話パイプラインにおいて,時間的なずれ,表現力の低下,修正の硬直性という3つの対話の破綻パターンが確認された。
- これらの摩擦は,欠陥ではなく,制御を優先したモジュール設計の構造的な結果であることが示された。
- 自然な音声AIの構築は,各コンポーネントの最適化だけでなく,それらの連携を慎重に設計するインフラ設計の課題である。
公共部門AIにおける説明責任のための神経記号的フレームワーク [cs.CY, cs.AI, cs.LO]目的:公共部門AIにおける説明責任の確立
- 社会保障制度においてAIの利用が増加しており,公平性と透明性が重要視されている。
- AIシステムの説明が法的根拠と乖離しており,利用者の権利保護が課題となっている。
- AIの判断根拠と法的要件との整合性を検証し,説明責任を担保することを目指す。
- 本フレームワークは,カリフォルニア州のSNAP(CalFresh)の法的規定に基づき,AIの説明を検証可能とする。
- 構築されたフレームワークにより,法的整合性のない説明を検出し,違反された資格ルールを特定することが可能となった。
- 自動化された決定の根拠を追跡可能にし,異議申し立てを支援することで,手続き上の説明責任を向上させる。
無限ロゴスの図式のためのホモトピー型理論 [math.CT, cs.LO, math.LO]目的:無限ロゴスの図式
- ホモトピー型理論は,数学と計算機科学の基礎をなす重要な分野である。
- 既存の型理論では,高次元の論理関係を扱うのが困難であった。
- 無限ロゴスの図式をホモトピー型理論で扱う手法を開発すること。
- ホモトピー型理論にlex的アクセス可能な様相を拡張することで,無限ロゴスの図式を再構成できることを示した。
- 単一の無限ロゴスだけでなく,その図式についてもホモトピー型理論で推論が可能になる。
- これは,高次元論理関係のための型理論であるスターリングの合成 Tait 可計算性の高次元版を提供する。
離散エントロピーの単調性:$\mathbb{Z}^d$上の対数凹型確率ベクトルの場合 [math.PR, cs.IT, math.IT]目的:対数凹型確率ベクトルに対する離散エントロピーの単調性
- 情報理論において,エントロピーは不確実性の尺度として重要であり,その性質を理解することは,情報伝達や統計推論の基礎となる。
- 高次元空間における離散エントロピーの評価は困難であり,特に対数凹型分布のような複雑な分布に対しては,その単調性を証明することが課題であった。
- 本研究は,高次元離散空間における対数凹型確率ベクトルのエントロピーの単調性を明らかにし,エントロピー評価の理論的基盤を強化することを目指す。
- 等方性,対数凹性,独立同分布を持つ確率ベクトル$X_1, \dots, X_{n+1}$の和に関して,離散エントロピーの単調性が証明された。
- エントロピーの増加量は,次元$d$と加法数の数$n$に依存し,$H(X_1+\cdots+X_{n+1}) \geq H(X_1+\cdots+X_{n}) + \frac{d}{2}\log{\Bigl(\frac{n+1}{n}\Bigr)} +o(1)$という不等式で表される。
- この結果は,一次元の場合の結果を$\mathbb{Z}^d$に一般化しており,対数凹性よりも一般的な仮定の下でも成立することが示された。
量子コンピュータへの汎用古典データ強靭かつ最適ローディング [quant-ph, cs.CC, cs.DS, physics.comp-ph]目的:汎用古典データを量子コンピュータへ効率的に読み込む手法
- 量子計算は,機械学習やハミルトニアンシミュレーションなど,様々な応用分野で注目されている。
- 既存のデータローディング手法は,デバイスの不完全性に対して脆弱であり,実用化が課題となっている。
- 本研究では,エラー伝搬を抑制する手法により,古典データの量子コンピュータへの強靭なローディングを実現する。
- 提案手法は,既存の深さ最適化法と比較して,指数関数的にロバスト性を向上させる。
- フォールトトレラント回路の深さ,ゲート数,STAにおいても最先端の結果を達成している。
- 幾何学的に局所的なハミルトニアンの量子シミュレーションにおいて,論理キュービットあたりのコード距離を指数関数的に削減できる可能性がある。
非共鳴型開放タヴィス・カミングスモデルのデジタル量子シミュレーション [math.CO, cs.DM, quant-ph, cs.DS, physics.comp-ph, physics.optics]目的:非共鳴型開放タヴィス・カミングスモデルのダイナミクスのシミュレーション
- 量子情報処理や量子デバイス設計において重要なモデルである。
- 大規模な系では古典的なシミュレーションが困難である。
- 量子アルゴリズムを用いた効率的なシミュレーションを提案する。
- 提案する量子アルゴリズムは,ゲート複雑度が多項式オーダー($O(N^2)$, $O(N^3)$)でスケーリングする。
- 使用する量子ビット数は線形オーダー($O(N)$)でスケーリングする。
- 古典的な微分方程式ソルバーとの比較により,提案アルゴリズムの正確性が確認された。
単一LEDと分散型単一素子OIRSを用いた可視光屋内測位:適応ビームステアリングによる反復アプローチ [eess.SP, cs.IT, math.IT]目的:可視光通信を用いた屋内環境における低コストフォトディテクタの局所化
- 既存の照明インフラを活用し,電波技術の代替となる技術として,可視光通信が注目されている。
- 光路遮蔽の影響を受けやすく,測位精度が低下する可能性がある。
- OIRSを活用し,光路を制御することで,より高精度でロバストな測位を実現すること。
- 提案手法は,OIRSの最適な活性化戦略と,ノイズ分散変換に基づく新しいアルゴリズムにより,効率的な局所化を可能にする。
- 反復加重最小二乗法と適応ビームステアリングを組み合わせることで,PDの位置に関する事前知識なしに,OIRSネットワークを動的に整列させる。
- シミュレーション結果は,提案手法が測位精度,OIRSの誤整列に対するロバスト性,および反復回数の点で有効であることを示している。
ファクタライズ近似を用いたマスク拡散モデルにおける誤差境界と最適スケジュール [stat.ML, cs.IT, cs.LG, math.IT, stat.CO]目的:離散データ生成モデルにおける計算コストと精度に関するトレードオフの解析
- 近年,離散データ生成の効率化が求められており,計算資源の制約下での高性能なモデル構築が重要である。
- 自己回帰モデルは高性能だが計算コストが高いため,近似手法を用いることでコスト削減を図る必要がある。
- マスク拡散モデルの誤差を理論的に評価し,スケジュールの最適化を通じて精度向上を目指す。
- 本研究では,マスク拡散モデルの誤差境界を,データ次元に依存しない形で導出した。
- 非定数スケジュールの利点を明らかにし,データ分布の情報プロファイルに基づく最適スケジュールを特定した。
- 時間逆拡散過程の古典的な導出を用いず,サンプリングアルゴリズムとして直接定義することで,簡潔な証明を得た。
量子LDPC符号に対するビームサーチデコーダ [quant-ph, cs.IT, math.IT]目的:量子LDPC符号のデコーディング手法
- 量子コンピュータ実現に向け,誤り訂正は不可欠であり,LDPC符号は有望な候補である。
- 既存のデコーダは,計算コストが高い,または性能が十分でないという課題がある。
- 高速かつ高精度な量子LDPC符号デコーダを開発し,実用化を促進することを目指す。
- 提案手法は,ビームサーチと信念伝播を組み合わせることで,様々な量子LDPC符号に対応可能である。
- シミュレーションの結果,ビーム幅64では論理誤り率が17倍低下し,ビーム幅8ではBP-OSDと同等の性能を26.2倍の高速化で達成した。
- ビーム幅32は,トラップイオンアーキテクチャに適しており,1ms以下のサイクルタイムで論理誤り率を5.6倍低減する見込みがある。
- 1
- 2
