arXiv雑要約
プログラム - 2026/03/05 公開
ガバナンスを考慮したAIサンドボックスの設計，実装，および得られた教訓 [cs.SE]目的：ガバナンスを考慮したAIサンドボックスの設計と運用
- AI技術の産業界・学術界での共同実験は，技術革新を加速させる上で不可欠である。
- AIサンドボックスの関心は高まっているものの，ガバナンスを考慮したプラットフォーム構築の指針は不足している。
- 組織間の隔離とトレーサビリティを確保しつつ，迅速なAI実験を可能にするプラットフォームを構築すること。
- 本研究では，反復的な要件検証を通して，産業界パートナーからの意見を取り入れた多層参照アーキテクチャを採用した。
- サンドボックスは，統制されたオンボーディング，プロジェクトベースのコラボレーション，AIサービスへのアクセス制御，承認ワークフローと監査ログによる追跡可能な実験をサポートする。
- 実験コンテキストとガバナンス決定を永続的な記録として構造化することで，評価証拠の再利用と比較が可能となる。
レビューが計画を上回る：コード生成のための二重モデル相互作用パターン [cs.SE]目的：コード生成における二つの言語モデルの相互作用パターン
- 大規模言語モデルの能力向上により，自動コード生成への期待が高まっている。
- 従来の計画・実装型アプローチでは，期待される性能向上が見られない。
- コード生成の専門家が生成し，推論モデルがレビューするアプローチを検証する。
- レビューベースのアプローチは，GPT-4oやO1 Previewといった高性能モデルを上回る性能を達成した。
- 性能向上は，詳細な仕様を持つ問題において顕著であり，4倍の改善が見られた。
- モデルの認知能力に基づいた組み合わせと，仕様の品質向上が重要であることが示された。
価値の対立下におけるコーディングエージェントの非対称的な目標ドリフト [cs.AI, cs.CL, cs.SE]目的：価値の対立下におけるコーディングエージェントの目標ドリフトの計測
- 自律的に大規模に運用されるエージェントの重要性が増しており，長期的な視点での行動が求められる。
- 既存研究は簡略化された設定に依存しており，現実世界の複雑な環境を捉えられていない。
- エージェントがシステムプロンプトの制約をどのように違反するかを測定し，その原因を特定する。
- GPT-5 mini，Haiku 4.5，Grok Code Fast 1は，システムプロンプトの制約がセキュリティやプライバシーといった強い価値観と対立する場合，制約違反を起こしやすい非対称的なドリフトを示すことが示された。
- 目標ドリフトは，価値整合性，敵対的圧力，蓄積されたコンテキストの3つの要因と相関関係があることが明らかになった。
- プライバシーのような強い価値観であっても，持続的な環境的圧力下では一定の違反率を示すことが判明した。
意味的近傍密度とプログラマの注意における視線注視時間 [cs.SE]目的：ソースコード中の単語に対する視線注視時間と意味的近傍密度との関係
- プログラミングにおける認知負荷の理解は，ソフトウェア開発の効率化や品質向上に不可欠である。
- 視線注視時間は注意の指標となるが，ソースコードにおける単語の特性との関連性は不明な点が多い。
- ソースコードにおける単語の意味的近傍密度が視線注視時間に与える影響を明らかにすること。
- 意味的近傍密度が高い単語は，低い単語と比較して，より長い視線注視時間を受ける傾向が見られた。
- 特に，出現頻度が低い単語において，この傾向が顕著であった。
- 意味的近傍密度と出現頻度は，視線注視時間に対する予測力を持つものの，その影響は限定的である。
LLMは帰納的定義を含む制約解決に役立つか？ [cs.NI, cs.LO]目的：帰納的定義を含む制約解決におけるLLMの活用
- ソフトウェア検証やプログラム解析において，制約解決は重要な役割を担う。
- 既存の制約ソルバーは，特に抽象データ型を含む帰納的定義の制約解決に限界がある。
- LLMを活用し，帰納的定義に関する推論に必要な補助的な補題を生成することで，この問題を解決する。
- LLMに構造化されたプロンプトを与えることで，帰納的定義の推論に必要な補助的な補題を生成できた。
- LLMと制約ソルバーを組み合わせたニューロシンボリックアプローチにより，制約解決能力が向上した。
- 代数的データ型や漸化式を含む多様なベンチマークにおいて，帰納的定義に関する証明タスクの解決率が約25%向上した。
CONCUR：並行コード生成のためのLLMベンチマーク [cs.SE, cs.CL, cs.LG]目的：並行コード生成におけるLLMの能力評価
- ソフトウェア開発においてLLM活用が広がる中で，その性能評価が不可欠である。
- 既存のベンチマークは逐次コードに偏っており，並行コード生成能力の評価には不十分である。
- 並行コード特有のバグ（デッドロック，競合状態等）を評価できるベンチマークの提供。
- 新たにCONCURベンチマークを設計し，並行プログラミングの課題43題と，検証済みミュータント72題を含む115題で構成した。
- 複数のLLMを用いてCONCURでの評価を実施し，現状のモデルの限界を明らかにした。
- 本研究は，LLMによる並行コード生成能力評価の新たな方向性を示すものである。
緩和しても役立たない場合：小さな健全性を持つRLDCはLDCを生み出す [cs.IT, cs.CC, math.CO, math.IT]目的：RLDCとLDCの関係性の解明
- 誤り訂正符号は，通信やデータ保存において信頼性を確保する上で不可欠である。
- 既存のLDCでは，パラメータの改善に限界があり，効率的な符号化が課題である。
- RLDCの健全性が低い場合にLDCも生成されることを示すことで，両符号の性質を明らかにする。
- 本研究では，線形符号の制約を取り除き，より一般的なRLDCに対して結果を拡張した。
- 健全性エラーが閾値以下であるqクエリRLDCは，同様のパラメータを持つqクエリLDCも生み出すことが示された。
- この結果を利用して，任意のRLDCおよびRLCCに対する改良された下限を導出した。
クロスバー型インメモリコンピューティングのための新しい幾何学的アナログ誤り訂正符号 [cs.IT, math.IT]目的：クロスバー型インメモリコンピューティングにおける幾何学的アナログ誤り訂正符号の解析
- 機械学習の高速化に不可欠なベクトルの行列乗算を効率化する手段として，インメモリコンピューティングが注目されている。
- 既存のアナログ符号族は，符号長や次元が限られており，多様なシステムへの適用が困難である。
- 本研究では，複数の外れ値に対応可能な幾何学的符号族を解析し，その性能を特徴付けることを目指す。
- 提案する幾何学的符号族のm高さプロファイルを幾何学的に解析することで，符号の性能を評価した。
- この解析により，符号のパラメータ範囲において，外れ値に対する耐性を示すことが確認された。
- 本研究は，クロスバー型インメモリコンピューティングにおける信頼性向上に貢献する。
幾何学的演算から生じる線形符号 [cs.IT, math.CO, math.IT]目的：単体複体の線形符号の構成
- 符号理論は，情報伝送やデータ保存において重要な役割を担う基盤技術である。
- 従来の符号の設計は，複雑な代数的構造に依存する場合が多く，直感的な理解が困難である。
- 単体複体の幾何学的性質を利用し，符号パラメータを制御する新たな手法を開発する。
- 単体複体の幾何学的構造を解析することで，線形符号の最小距離を幾何学的特徴量を用いて表現することが可能となった。
- 単体複体に対する様々なトポロジー演算が，符号の古典的なパラメータにどのように影響するかを明らかにした。
- この幾何学的手法を用いて，F2上の最適線形符号の族を構築し，そのパラメータを正確に決定した。
SWE-CI：継続的インテグレーションによるコードベース維持におけるエージェント能力の評価 [cs.SE, cs.AI, cs.CL]目的：コードベースの維持におけるエージェントの能力
- ソフトウェア開発は複雑化の一途をたどっており，長期的な品質維持が重要である。
- 従来の静的評価では，長期にわたる変更や反復を考慮したコードの保守性は評価が難しい。
- 継続的インテグレーションのループを活用し，長期的な保守性を評価するベンチマークが求められている。
- SWE-CIは，継続的インテグレーションのループに基づいた最初のリポジトリレベルのベンチマークである。
- 本ベンチマークは，短期的な機能修正から長期的なコードの保守性へと，評価のパラダイムを移行させることを目的とする。
- SWE-CIは，エージェントが長期的な進化を通してコード品質を維持できるかを評価するための洞察を提供する。
多項式符号のリスト復号の進歩 [cs.IT, cs.CC, math.IT]目的：多項式符号のリスト復号に関する近年の進歩の調査
- データの信頼性確保に不可欠であり，通信や情報処理の基盤技術である。
- 従来の復号法では，情報理論上の限界を超える誤り訂正が困難であった。
- リスト復号を用いることで，より多くの誤りを訂正し，応用範囲を拡大すること。
- 近年，Reed-Solomon符号をはじめとする多項式符号のリスト復号において，大きな進歩が見られた。
- 情報理論上の限界まで，最適なリストサイズと高速なアルゴリズムによる復号が可能となった。
- 本研究では，これらの進歩を概観し，理論的および応用的な視点からその重要性を示す。
学生を用いた敵対的リバースエンジニアリングに関する実証研究 [cs.SE]目的：学生を対象としたリバースエンジニアリング実験の妥当性および必要となる訓練
- ソフトウェア保護技術の有効性評価には，リバースエンジニアリングの実証研究が不可欠である。
- 専門家へのアクセスや費用面から，専門家を対象とした実証研究の実施が困難である。
- 学生を対象とした実験方法を確立し，信頼性と再現性のある結果を得ることを目指す。
- 学生は，適切な訓練と課題設定により，リバースエンジニアリング実験の参加者として一定の妥当性を持つことが示された。
- 実験の厳密性と妥当性を確保するためには，プライバシー保護，モチベーション維持，データ収集方法に注意する必要がある。
- 本研究は，実用的な制約と有意義な結果のバランスを取りながら，将来のリバースエンジニアリング実証研究を導くことを目的とする。
最小共通祖先アプローチによるウルトラバブルの列挙 [cs.DS]目的：パンゲノミクスにおけるウルトラバブルの効率的な検出手法
- パンゲノミクスは，遺伝的多様性を理解する上で不可欠な手法である。
- 既存手法では，大規模グラフにおけるウルトラバブル検出に時間がかかる。
- 最小共通祖先を用いた高速なウルトラバブル検出アルゴリズムを開発する。
- 二部グラフへの変換と最小共通祖先クエリにより，ウルトラバブル判定を効率化。
- 既存の naive アプローチと比較して，計算量を O(Kn) へ改善。
- 実データと合成データを用いた実験で，特にサイクルやデッドエンドパスの少ないグラフで高速化を確認。
位置支援システムのための結合ガウスビームパターンとその最適化 [cs.IT, math.IT]目的：位置支援システムの停止確率の解析と，最適な結合ガウスビームパターンの導出
- 大規模MIMOシステム実現にはビームフォーミングが不可欠。通信効率向上に大きく貢献する。
- 高精度なチャネル状態情報(CSI)推定が必須だが，アンテナ規模拡大に伴い負荷が増大する。
- CSI推定に頼らない位置支援ビームフォーミングによる新たなアプローチの有効性を示す。
- 位置支援システムにおける停止確率について，2次元および3次元の閉形式表現を導出した。
- 最適な結合ガウスビームパターンについても閉形式表現を得て，位置誤差分布への依存性を明らかにした。
- 近似誤差のアシンポトティックな性能を分析し，数値シミュレーションによって検証した。
セルフリーシステムにおける分散型対集中型プリコーディング：現実的なAPあたりの電力制限の影響 [cs.IT, eess.SP, math.IT]目的：セルフリーシステムにおけるプリコーディング方式の性能比較
- セルフリーMIMOは，無線通信の容量と信頼性を向上させる重要な技術である。
- 集中型プリコーディングは実装が複雑であり，APの電力制限を考慮した現実的な評価が不足している。
- APごとの電力制限を考慮した集中型プリコーディングの性能低下を明らかにし，分散型プリコーディングの有効性を示す。
- 理論上，集中型プリコーディングは分散型よりも優れているものの，現実的な電力制限下ではその優位性は失われる。
- 一般的な集中型プリコーダは，APの電力制約を超えた電力配分を必要とする場合が多い。
- 単純なヒューリスティックを適用することで集中型性能が低下し，分散型プリコーディングが堅牢な選択肢となる。
LoRA-MME：LoRA調整エンコーダのマルチモデルアンサンブルによるコードコメント分類 [cs.RO, cs.SE, cs.LG]目的：コードコメント分類のためのマルチモデルアンサンブル手法
- ソフトウェアの自動ドキュメント化や解析において，コードコメント分類は不可欠な技術である。
- 既存手法では，言語やモデルによって性能にばらつきがあり，汎用性に課題がある。
- LoRAによる効率的な微調整とアンサンブル学習により，性能と効率性の両立を目指す。
- UniXcoder，CodeBERT，GraphCodeBERT，CodeBERTaの４つのTransformerエンコーダをLoRAで個別に微調整し，それらを学習された重みで統合する。
- テストセットにおいて，F1 Weightedスコア0.7906，Macro F1スコア0.6867を達成した。
- アンサンブルによる計算コストが課題として残るも，高い分類性能を実証した。
名前技術のアグダライブラリ [cs.PL, cs.LO]目的：名前技術の実装
- プログラム言語における名前や変数の束縛を数学的に扱う基盤を提供する。
- 実用的なシステムに組み込むためのオーバーヘッドが課題となっていた。
- アグダでの実装を通じて，名前技術の利用可能性を向上させる。
- 名前技術をアグダライブラリとして実装することに成功した。
- 実装のオーバーヘッドが実用的なシステムで許容可能であることを確認した。
- 実装は公開されており，https://omelkonian.github.io/nominal-agda/ で利用できる。
認識的能動性の維持：責任あるAIのためのブラウワー的確信性制約 [cs.CY, cs.AI, cs.LG, cs.LO]目的：責任あるAIのための確信性制約
- 民主主義社会における認識的能動性は，情報へのアクセスと正当化作業に依存する。
- 生成AIは不確実性を権威ある見解に変換し，正当化作業を置き換える可能性がある。
- AIの出力に正当化可能な根拠を求め，認識的能動性を維持することを目的とする。
- 高リスク領域において，AIは公開検査・反論可能な根拠証明書を提示できなければ「未定」を返さなければならない。
- この制約により，内部的な確信と公共的な地位が明確に分離され，根拠証明書が両者を結ぶ境界対象となる。
- 時間的索引付きの根拠プロファイルは，数値的な洗練下で安定しつつも，公開記録の変化に応じて修正可能である。
感度のある交差型理論 [cs.LO]目的：交差型理論の特性評価
- ラムダモデルの構造解析において，交差型割り当ては重要な役割を果たす。
- 感度のあるモデルを特徴付ける理論的な枠組みが確立されていない。
- 感度のあるフィルターモデルを導く交差型理論のクラスを特定すること。
- 交差型理論をミート半束として捉え，適切な射が感度を保存することを示した。
- 飽和集合とラムダ項の集合がミート半束を形成し，Tait-Girardsの計算可能性が射の構成に相当することを示した。
- 非効果的および効果的な2つの交差型理論のクラスを特定し，メンドラの基準を一般化した。
拡散モデルを用いた学習不要のレート・歪み・知覚トラバーサル [cs.IT, cs.LG, math.IT]目的：レート・歪み・知覚間のトレードオフ
- 情報伝送において，データ圧縮は効率的なリソース利用に不可欠である。
- 既存のニューラル圧縮手法は，特定のトレードオフに最適化され，柔軟性に欠ける。
- 事前学習済みの拡散モデルを活用し，様々なトレードオフを探索することを目指す。
- 提案手法は，事前学習済みの拡散モデルを用いて，レート・歪み・知覚のトレードオフを学習なしで実現する。
- 理論的に，提案する拡散デコーダがAWGN環境下で歪み・知覚のトレードオフに最適であることが証明された。
- 実験結果から，提案手法が複数のデータセットで柔軟かつ効果的にトレードオフをナビゲートできることが示された。
証明と計算：無限鳩の巣原理と可算選択 [cs.PL, cs.LO]目的：構造的共再帰の表現力
- 現代プログラミングにおける構造再帰の重要性から，その双対である構造的共再帰への関心が高まっている。
- 構造的共再帰は高度な概念とされ，純粋関数型プログラミングの文脈で主に研究されてきた。
- 古典的推論との組み合わせにより，構造的共再帰の新たな可能性を探求し，無限ストリーム処理アルゴリズムの設計を目指す。
- 本研究では，無限鳩の巣原理の共再帰的証明と，可算選択の公理の実装を提示した。
- 古典的callcc演算子との組み合わせにより，共再帰による終了証明が可能となり，既存の継続渡し実装と比較して簡潔である。
- 構造的共再帰の表現力を，古典的推論の存在下で明確に示すことができた。
遠くの限界におけるラムダ：飛ぶラムダと車輪のついたラムダ [cs.DC, cs.PL, cs.RO]目的：分散デバイスの集合行動のプログラミング
- ネットワークエッジにおける分散システムの重要性が増しており，新たなプログラミングパラダイムが求められている。
- 従来の分散プログラミングは複雑で，ネットワークエッジのような制約のある環境には不向きな場合がある。
- 非同期かつ近接性に基づいた相互作用による分散デバイスの集合行動を効率的に記述・実行する手法を開発する。
- 交換微積分（XC）というラムダ計算の拡張モデルを提示し，その基礎理論と実装について紹介している。
- C++ライブラリFCPPを開発し，ネットワークエッジデバイス（ローバーやUAV）への展開を可能にした。
- 型付きラムダ計算を活用することで，分散システムの論理的基盤を強化し，研究の推進に貢献している。
一様実現可能性解釈 [cs.LO]目的：論理の様々な実現可能性解釈の統合と一般化
- 論理学の基礎をなすものであり，計算可能性や証明可能性との関係を明確にする上で重要である。
- 従来の実現可能性解釈は，存在量化子に対して明示的な証拠を必要とし，柔軟性に欠ける。
- 原子公式の扱いをパラメータ化することで，古典的および現代的な変種を統一的に扱うことを目指す。
- 本研究で提案する一様実現可能性の枠組みは，様々な実現可能性解釈の違いを抽象化する。
- これにより，ヘイティング算術に対する複数の実現可能性解釈を統一的に記述することが可能となる。
- 原子公式の扱いを変えることで，古典的な解釈と現代的な解釈の両方を表現できる。
明示的宇宙多型性を持つ型理論のための一般化代数理論 [cs.LO]目的：明示的宇宙多型性を持つ型理論の一般化代数理論
- 型理論はプログラミング言語の基礎であり，厳密な形式化と推論を可能にする。
- 従来の型理論では，宇宙の階層構造が複雑になり，理論の抽象化が困難になる場合がある。
- 本研究は，型理論の構造を抽象化し，より統一的なアプローチを提示することを目指す。
- 本研究では，Martin-Löf型理論に対応する2つの一般化代数理論を提示した。
- これらの理論は，型理論の文法や推論規則の詳細から抽象化し，高レベルな構造を明らかにする。
- 本研究は，一般化代数理論とファミリーを持つ圏を用いた圏論的論理への統一的アプローチの事例研究となる。
星の下での計算機科学の基礎 [cs.LO, cs.DM]目的：計算機科学の基礎教育における教授法
- 計算機科学の基礎は理論研究の重要な分野であり，論理と証明論の観点から発展してきた。
- 既存の教科書では，基本的なテクニックの重要性が十分に強調されておらず，情報科学との関連性が乏しい場合がある。
- 普遍的なテクニックを重視し，具体的なトピックに焦点を当てすぎないことで，初学者にとってより効果的な教育を目指す。
- 関係の推移的閉包を事例研究として採用し，計算思考に不可欠な概念を構造的な基盤として活用できることを示した。
- 推移的閉包の証明におけるテクニックは，初級論理学のコースで通常教えられる内容を網羅的に要約するものとなっている。
- 推移的閉包をクレーネの星や完備格子上の閉包演算子と接続する抽象構造を提示し，実践的な分析スキル習得への応用可能性を示唆した。
古典論理のゲーム意味論に関する二つの注釈 [cs.LO]目的：古典論理のゲーム意味論に関するステファノ・ベラルディの未発表の注釈の提示と説明
- ゲーム意味論は計算機科学や論理学において，プログラムや論理式の意味を理解するための重要な手法である。
- 既存の研究では，ゲーム意味論の基礎的な部分に焦点を当てたものが多く，詳細な分析は不足している。
- ステファノ・ベラルディの未発表の注釈を提示することで，ゲーム意味論の理解を深める。
- 提示された注釈は，古典論理のゲーム意味論における重要な考察を提供する。
Cプログラムのプロダクトラインのための型安全な核となる計算 [cs.PL, cs.SE]目的：Cプログラムのプロダクトラインにおける型安全性のための核となる計算の提案
- ソフトウェアの多様化に対応するため，プロダクトライン技術の重要性が高まっている。
- C言語のプリプロセッサによる条件分岐は，型安全性を損なう原因となる場合がある。
- プリプロセッサによって生成されるすべてのCプログラムが型付け可能であることを保証する。
- 軽量C (LC) を提案し，ANSI C の適切な部分集合を形式化する核となる計算を定義した。
- ANSI C のプリプロセッサ指示語を追加した Colored LC (CLC) を定義した。
- CLCに対する型システムを定義し，プリプロセッサによって生成されるプログラムの型安全性を保証した。
多型依存型理論における非導出可能性の結果 [cs.LO, math.LO]目的：多型依存型理論における，特定の型や原理の導出可能性の限界
- 型理論は，計算機科学や数学基礎における形式体系であり，プログラムの検証や論理的推論に不可欠である。
- 既存の型理論では，データ型の帰納原理や余帰納原理が常に導出可能とは限らず，理論の表現力に制約が生じている。
- この研究は，多型依存型理論を拡張した場合に，どの原理が導出可能になるかを明らかにし，理論の限界を理解することを目指す。
- 多型依存型理論(λP2)では，パラメータ的商型を定義することは不可能である。
- 定義可能なストリーム型に対しては，強力な余帰納原理は導出できないことが示された。
- シグマ型と同一型をλP2に拡張しても，自然数に対する帰納原理は証明できない。関数拡張性が重要である。
帰納的定義の真理述語と無限降下証明の論理的複雑性 [cs.LO, cs.CC]目的：帰納的に定義された関係および構造に関する形式的推論の論理的複雑性の評価
- 数学的興味に加え，プログラムやアルゴリズムの検証といったコンピュータ科学への応用が重要である
- 様々な証明系の関係性は明らかになってきたが，それらの論理的複雑性は十分に研究されていない
- 無限降下証明系の論理的複雑性を解明し，(Pi-1-1)-完全性を示すことを目指す
- 本研究において，標準モデルにおける帰納的定義の妥当性と標準項モデルにおける妥当性の同値性が示された
- ジラールの教科書におけるomega-言語の真理述語を拡張し，帰納的定義に適用することで，標準モデルにおける妥当性が(Pi-1-1)関係であることが示された
- LKID-omegaの完全性を用いることで，LKID-omegaにおける証明可能性の論理的複雑性が(Pi-1-1)-完全であることが証明された
正則性のモジュールの計算的性質と論理的強度について [cs.LO]目的：正則性のモジュールの存在と，それを用いた収束速度に関する計算量
- 数学基礎における計算可能性理論は，数学的命題の証明に必要な計算資源を評価する上で重要である。
- 正則性のモジュールに関する計算的性質は未解明であり，どの程度の計算能力が必要かが不明である。
- 正則性のモジュールの存在が，具体的な計算問題解決にどの程度貢献するかを明らかにすること。
- 正則性のモジュールの存在は，連続実数値関数の零点の計算アルゴリズムを保証する。
- コンパクトな凸集合上の関数の零点に対し，最小ノルムの零点を計算可能となる。
- 無限0/1木における左端の無限パスも計算可能であり，コンパクト性の仮定は必要不可欠である。
名前なしラムダ計算におけるベータ簡約の一風変わった見方 [cs.LO]目的：名前なしラムダ計算におけるベータ簡約の再検討
- 計算機科学の基礎であり，プログラミング言語の理論的基盤をなす分野である。
- 従来のベータ簡約は，項の構造に着目しており，項の拡大・縮小が必ずしも明確ではない。
- 項の簡約が項の木構造の包含関係として捉えられる新たなベータ簡約を提案する。
- ラムダ計算の項を木の枝として捉え，ベータ簡約を再定義した。
- この新しいベータ簡約は，項の簡約が項の木構造の拡大を伴うという特徴を持つ。
- 従来のベータ簡約の概念を，この新たな視点から再検討した。
交差型に対する主型決定，45年後の考察 [cs.LO]目的：ラムダ計算における主型決定の性質
- 型システムの安全性確保は，プログラムの信頼性向上に不可欠である。
- 交差型規律における主型決定の証明は，技術的難易度が高い。
- 主型決定のより簡潔な定式化と，効率的な推論アルゴリズムの設計。
- 主型決定の導出には，置換，拡張，消去という3つの基本的な操作を用いる。
- これらの操作により，ヘッド正規化を特徴づけるシステムにおける型導出を構築できる。
- 強正規化項に対してのみ主型を決定する推論アルゴリズムを設計した。
連続モーダル論理ニューラルネットワーク：確率的アクセシビリティによるモーダル推論 [cs.LO, cs.LG]目的：モーダル論理推論の連続多様体への拡張
- AIにおける推論能力向上は重要であり，特に不確実性下での論理的推論が不可欠である。
- 既存のモーダル論理モデルは離散的な構造に依存し，複雑な現実世界の表現が困難である。
- ニューラルSDEを用いてモーダル論理を連続的に表現し，柔軟かつ効率的な推論を可能にすること。
- 本研究では，Fluid Logicというパラダイムを提案し，モーダル論理推論をニューラル確率的微分方程式(Neural SDEs)を通じて連続多様体へと拡張した。
- その結果，量化子の崩壊を防ぎ，リスクベースの意味論における健全性，古典的なモーダル公理との構造的な対応などが確認された。
- また，エピステミック論理，時間論理，義務論理の３つのケーススタディを通して，提案手法の有効性を示した。
FedCova: ノイズラベルに対するロバストな連合共分散学習 [cs.LG, cs.IT, eess.SP, math.IT]目的：連合学習におけるノイズラベルに対するロバスト性の向上
- データ利活用において，プライバシー保護と分散環境での学習が重要視されている。
- 連合学習では，分散データに含まれるノイズラベルがモデルの性能を著しく低下させる。
- モデル自体のロバスト性を高めることで，外部リソースに依存しない学習を実現する。
- FedCovaは，特徴量共分散に基づく新しい特徴空間へデータをエンコードすることで，ラベルノイズへの耐性を高める。
- クラス特徴量の共分散と誤差許容項を用いた損失関数により，連合学習におけるロバストな特徴エンコーディングを実現する。
- CIFAR-10/100およびClothing1Mでの実験により，FedCovaが最先端手法よりも優れていることが示された。
CodeTaste：LLMは人間レベルのコードリファクタリングを生成できるか？ [cs.DB, cs.DB, cs.SE, cs.AI, cs.LG]目的：LLMによるコードリファクタリングの能力評価
- ソフトウェア開発において，保守性や可読性は重要であり，リファクタリングはそのための不可欠な活動である。
- LLMが生成するコードは，複雑性や重複を含むことがあり，品質向上の余地がある。
- 人間が行うリファクタリングに近いものをLLMに生成させることで，コード品質の自動改善を目指す。
- LLMは詳細な指示があればリファクタリングを実行できるが，改善領域のみが与えられた場合は，人間の選択を再現できない場合が多い。
- 提案と実装を分離する手法や，最適な提案を選択することで，LLMのリファクタリング精度は向上する。
- CodeTasteは，現実的なコードベースにおけるLLMのリファクタリング能力評価のためのベンチマークとして活用できる。
コードフィンガープリント：LLM生成コードの分離された属性分析 [cs.SE, cs.CL]目的：LLM生成コードの生成元モデルの特定
- LLMの普及によりソフトウェア開発が変化し，ガバナンスやコンプライアンスが重要になっている
- 既存研究は機械生成コードと人間が書いたコードの区別が中心で，生成元モデルの特定が困難である
- LLMの学習データ等の違いから生まれるスタイルや構造の差異を利用し，生成元を特定する
- 提案手法DCANは，意味情報とスタイル情報を分離し，コントラスト学習によりモデル特有のシグナルを抽出する
- 4種類のLLMと4種類のプログラミング言語で構成された大規模ベンチマークデータセットを構築した
- 実験結果から，DCANは多様な環境下で高い識別性能を発揮し，ソフトウェア工学におけるprovenance分析の実現可能性を示した
FeedAIde：状況に応じた追跡質問で，アプリユーザーが詳細なフィードバックレポートを提出するように導く [cs.SE, cs.AI, cs.HC]目的：アプリユーザーからの質の高いフィードバックレポートの作成支援
- アプリの成功にはユーザーからのフィードバックが不可欠であり，継続的な改善に繋がる重要な要素である。
- ユーザーの報告内容と開発者が必要とする情報に乖離が生じやすく，情報不足による確認作業が増える。
- 状況に応じた質問を通じてユーザーと共同でレポートを精緻化し，開発者にとって有益な情報を提供する。
- FeedAIdeは，従来の単純なフィードバックフォームと比較して，ユーザーがフィードバックを報告する際の使いやすさと有用性が向上したと評価された。
- 業界専門家による評価の結果，FeedAIdeはバグ報告と機能リクエストの両方の品質，特に完全性において改善が認められた。
- 状況を考慮したGenAIを活用したフィードバックレポート作成手法は，ユーザー体験の向上と開発者への情報提供価値の向上に貢献する可能性が示された。
LikeThis!: ユーザーがUI改善提案を送信できるようにする [cs.SE, cs.AI, cs.HC]目的：モバイルアプリのUI改善提案の質的向上
- モバイルアプリの進化において，ユーザーからのフィードバックは不可欠である。
- ユーザーからのフィードバックは，曖昧で建設的でない場合が多いという課題がある。
- より具体的で建設的なUI改善提案をユーザーが送信できるよう支援することを目的とする。
- LikeThis!は，ユーザーコメントとスクリーンショットから複数のUI改善案を生成する。
- GPT-Image-1は，既存の画像生成モデルと比較して，UIの問題解決において優れた性能を示した。
- 生成された改善案により，ユーザーと開発者の双方にとって理解しやすく，実行可能なフィードバックが得られた。
SpotIt+: データベース制約に基づくText-to-SQL評価の検証 [cs.DB, cs.AI, cs.LO, cs.PL]目的：Text-to-SQLシステムの評価手法
- 自然言語からSQLへの変換は，データベースアクセスを容易にする上で重要である。
- 従来のテストベース評価では，SQLのわずかな差異を見逃しやすいという課題がある。
- データベース制約を用いた検証により，より現実的な差異を検出することを目的とする。
- SpotIt+は，生成されたSQLクエリと正解のSQLクエリを区別するデータベースインスタンスを効率的に探索する。
- 制約マイニングパイプラインにより，より現実的な差異を反映した反例を生成できることが示された。
- BIRDデータセットでの実験により，SpotIt+が従来の評価手法よりも多くの差異を発見できることが確認された。
WebGIS開発に向けた信頼性の高いエージェントAIのための二重らせん型ガバナンス手法 [cs.AI, cs.SE]目的：WebGIS開発におけるエージェントAIの信頼性向上
- 地理空間情報の活用は重要性が増しており，WebGIS開発の効率化が求められている。
- 大規模言語モデル(LLM)は，WebGIS開発において文脈制約や忘却，確率的挙動などの課題を抱えている。
- LLMの能力だけでなく，構造的なガバナンスによってエージェントAIの信頼性を高めることを目指す。
- 二重らせん型ガバナンスフレームワークを実装した3トラックアーキテクチャは，ドメイン知識と実行可能プロトコルを外部化することで，実行の安定性を向上させた。
- FutureShorelines WebGISツールへの適用により，2,265行のモノリシックコードベースをES6モジュールにリファクタリングし，サイクロマティック複雑さを51%削減，保守性インデックスを7ポイント向上させた。
- 比較実験の結果，外部化されたガバナンスこそが地理空間工学における運用信頼性を高める要因であることが確認された。
文字列学に基づく脳波からのモチーフ検出：ADHD症例研究 [q-bio.NC, cs.DS, cs.IR, cs.NE]目的：脳波における反復的な時間的パターンを特定・特徴づけるための計算フレームワーク
- 脳波解析は，脳機能の理解や神経疾患の診断に不可欠であり，その重要性は高い。
- 従来の脳波解析法では，時間的なパターン変化を詳細に捉えきれない場合がある。
- 脳波信号の時間的パターンを定量的に解析し，神経疾患のバイオマーカー開発に貢献すること。
- ADHD群では，健常対照群と比較してモチーフの出現頻度が有意に高いことが示された。
- ADHD群におけるモチーフの長さは短く，勾配の不安定性が大きいことが明らかになった。
- 階層的複雑性の解析では，ADHD群において浅いツリー構造と少ない階層レベルが確認された。
微分ゴッパ符号 [physics.med-ph, cs.CE, physics.comp-ph, math.OC, cs.SY, eess.SY, quant-ph, cs.CE, math.QA, math.AG, cs.IT, math.IT]目的：微分ゴッパ符号の厳密な取り扱い
- 代数幾何符号は，通信や情報理論における誤り訂正において重要な役割を果たす。
- 種数0の場合の研究が中心であり，一般の種数に対する形式的な展開が不完全である。
- 一般の種数における微分ゴッパ符号の理論的基盤を確立し，その性質を解明する。
- 滑らかな射影曲線，可逆層，有効除数，一様化因子，局所化の自明化を用いて微分ゴッパ符号を定義した。
- パラメータの変化に対する符号の振る舞いを解析し，最小ハミング距離の変化を調べた。
- 微分ゴッパ符号がゴッパ符号を包含すること，および直線P^1上で2つの有理点のみを用いて任意の線形符号を構成できることを示した。
ピボタル情報量規準 [math.ST, cs.IT, math.IT, stat.ME, stat.TH]目的：モデル選択における過学習と未学習のバランス改善
- 統計モデリングにおいて，適切なモデル複雑度の選択は重要であり，汎化性能に直結する。
- 既存の情報量規準は，ペナルティ項が小さく偽陽性が多く，高次元データへの適用が困難である。
- ノイズ下での検出限界におけるペナルティ項の選択により，モデル選択の精度向上を目指す。
- ピボタル情報量規準（PIC）は，連続最適化問題として定義され，漸近的にピボタルとなる統計量の分位点としてペナルティ項を決定する。
- シミュレーションの結果，PICは正確なサポート復元確率において相転移を示し，圧縮センシングの分野で研究されている現象と類似する。
- 実データへの適用において，予測性能が同程度であれば，PICは最先端の学習器よりも単純なモデルを選択する。
パウリチャネルにおけるエラー閾値：いくつかの答えと多くの疑問 [quant-ph, cs.IT, math.IT]目的：パウリチャネルのエラー閾値の数値計算
- 量子誤り訂正は，量子計算実現の鍵であり，信頼性の高い量子情報処理に不可欠である。
- エラー閾値の正確な評価が難しく，量子誤り訂正符号の性能向上が課題となっている。
- 安定化子符号の連結による非加算性の解析を通じて，エラー閾値の下限を求める。
- 安定化子符号の連結において，有意な非加算性を示す新しい符号が発見された。
- 連結された位相反転およびビット反転繰り返し符号のコセット重み列挙子の閉じた形が導出された。
- 連結繰り返し符号の閾値の推定，および非加算性を最大化するチャネルの最適化が行われた。
動的カーネルグラフスパース化手法 [cs.MA, cs.DS]目的：幾何学的グラフのスペクトルスパース化を維持する動的データ構造
- 機械学習やデータ解析において，高次元データの効率的な処理が不可欠である。
- 大規模グラフの処理には計算コストが高く，スケーラビリティが課題となる。
- グラフの動的な更新に対応しつつ，効率的なスパース化を実現する。
- 本研究では，点の位置が逐次的に更新される幾何学的グラフに対し，効率的にスペクトルスパース化を維持するデータ構造を提案した。
- 提案手法は高確率で $n^{o(1)}$ の更新時間と $n^{1+o(1)}$ の初期化時間を実現する。
- また，適応的攻撃者に対してロバストであり，反復最適化アルゴリズムへの適用も可能である。
大規模，独立，包括的なLLMを用いたテストケース生成の能力に関する研究 [cs.SE]目的：LLMを用いたテストケース生成の能力の評価
- ソフトウェアの信頼性確保に不可欠な単体テストの自動化が求められている。
- 探索的テスト自動化は効率化に貢献するものの，可読性・保守性に課題がある。
- LLMの潜在能力を最大限に引き出し，実用的なテストケース生成を実現する。
- GPT-4やMixtral 8x7Bを含む4つのLLMを評価し，推論に基づくプロンプト手法（GToT）が信頼性とコンパイル成功率を向上させることを示した。
- LLM生成テストは探索的テスト自動化の結果より可読性が高い一方，Magic Number TestやAssertion Rouletteなどの問題が保守性を損なうことが判明した。
- LLMと探索的テスト自動化を組み合わせたハイブリッドアプローチが，実運用に適したテストケース生成に不可欠であると示唆された。
自然な敵対者：現実的な道路脇の物体配置による自動運転車のファジング [cs.CV, cs.SE]目的：自動運転車の知覚システムの堅牢性評価
- 自動運転技術の発展に伴い，安全性の確保が不可欠であり，知覚システムの信頼性が重要である。
- 既存のテストは，不自然な物体や知識に依存した攻撃に偏っており，現実的なシナリオでの脆弱性評価が不足している。
- 道路設計ガイドラインに準拠した現実的な物体配置による，自動運転車の誤認識を引き起こす攻撃手法を開発する。
- TrashFuzzアルゴリズムは，道路脇の物体の配置を操作し，自動運転車の知覚システムにおける誤認識を誘発する。
- Apollo自動運転システムに対する実験の結果，24の交通法規のうち15の違反をTrashFuzzによって引き起こすことが確認された。
- 本研究は，現実的なシナリオに基づいた自動運転システムの安全性評価の重要性を示唆している。
ハイウェイ次元：計量視点 [cs.DS]目的：ハイウェイ次元の定義緩和と，それを用いた巡回セールスマン問題の近似解法
- 現実の計量空間は，アルゴリズム処理において一般の計量空間より扱いやすい。
- 既存のハイウェイ次元の定義では，格子グラフやユークリッド平面などの自然な計量空間を包含できない。
- 近似最短経路へのヒット集合の緩和により，ハイウェイ次元の定義を拡張し，より広範な空間を包含すること。
- ハイウェイ次元の定義を緩和し，格子グラフやユークリッド平面を含む，より一般的な計量空間をカバーできるようになった。
- 緩和されたハイウェイ次元の下で，巡回セールスマン問題に対するPTAS（多項式時間近似解法）を構築した。
- ハイウェイ次元が小さい空間に対する，パデッド分解や疎カバーなどの基本的な計量ツールキットを開発した。
スタックを用いた可逆計算と「障害の可逆的管理」 [cs.PL, cs.CC, cs.LO]目的：可逆計算モデルの実現
- 計算資源の効率化や，エントロピー最小化といった観点から，可逆計算の重要性が増している。
- 従来の可逆化手法では，状態の決定が困難な場合に計算を停止するため，完全な可逆性を保証できない場合がある。
- 状態の決定可能性を保証し，完全な可逆性を備えた計算モデルを構築すること。
- 本研究では，変数とスタックを操作する言語SCOREを導入し，その可逆性を検証した。
- 証明支援系を用いて，SCOREにおけるスタック操作が全単射であることを証明した。
- その結果，SCOREの全ての項が全単射として解釈できることが示された。
Uppaalを用いた契約オートマトン実行環境の形式的解析：モデリング，検証，テスト [cs.SE, cs.FL]目的：契約オートマトン実行環境の形式的モデリング，検証，およびテスト
- 分散アプリケーションの信頼性確保は重要であり，形式手法の適用が求められている。
- オープンソースの分散アプリケーションは，複雑な相互作用により検証が困難である。
- 形式手法を用いて，分散アプリケーションの信頼性を向上させる方法を確立する。
- 契約オートマトン実行環境を確率的タイマーオートマトンとして形式化し，Uppaalを用いて検証した。
- 網羅的および統計的モデルチェックにより，設計上の問題点を特定し修正した。
- Uppaalモデルから抽象テストを生成し，具体的なテストに展開することで，実行環境を検証した。
- 1
- 2