arXiv雑要約
プログラム - 2026/05/14 公開
最小限の形式主義の下での証明を用いたLLMの推論能力のストレステスト [cs.LO, cs.AI]目的：LLMの推論能力の評価
- LLMの性能向上は，様々な分野での応用を可能にする重要な課題である。
- LLMの推論能力評価は，人間による判断やLLM自身による評価に依存し，再現性や客観性に課題があった。
- 機械的に検証可能な証明を用いることで，LLMの推論能力をより正確かつ詳細に評価すること。
- ProofGridというベンチマークスイートを開発し，LLMの推論能力を評価するための新たな枠組みを提示した。
- 最先端モデルは基礎的なタスクでは良好な性能を示すものの，高度な推論や証明合成を要するタスクでは未だ課題が多いことが示された。
- モデルが誤った証明を生成しつつも，個々の推論誤りを認識できるという「認識的不安定性」を特定し，その指標を提案した。
バイプロファイル逸脱論理：報告置換フレームと監査証拠 [cs.LO, cs.GT]目的：戦略的な社会選択状態のモデル化と，その健全性・完全性の証明
- 社会選択理論は，公正な資源配分や集団的意思決定の原理を研究する上で不可欠である。
- 報告された情報と実際の選好との乖離が，社会選択の効率性や公平性を損なう可能性がある。
- 報告情報の操作や改ざんを検出し，適切な監査メカニズムを構築することを目指す。
- バイプロファイル逸脱論理の健全性・完全性が，抽象フレームクラスDev(N)に対して証明された。
- 抽象的なDev(N)コンポーネントと，実際の報告座標積を分離するための座標分離が導入された。
- 表現変化のための監査層として，型付き操作証拠，境界行定理，因子閉包基準が提示された。
ocLTL：{\omega}-カテゴリ構造におけるLTL実現可能性と合成 [cs.LO]目的：{\omega}-カテゴリ理論におけるLTL+Pの実現可能性と合成問題の削減
- モデル検査や合成において，形式的な仕様記述が重要であるため，表現力豊かな論理が必要とされている。
- 既存のLTL+Pでは，無限構造を扱う際に計算量が指数関数的に増加する課題があった。
- {\omega}-カテゴリ構造を用いて，LTL+Pの実現可能性と合成問題を効率的に解決することを目的とする。
- ocLTLの実現可能性と合成問題を，命題LTL+Pの対応する問題に帰着させることに成功した。
- データ部分式を完全型による有限の論理和で置き換える手法を開発した。
- 計算量は2-EXPTIMEのままであり，追加のオーバーヘッドは理論にのみ依存し，式には依存しない。
立方型理論によるナヴァ・ニヤーヤ [cs.LO]目的：ナヴァ・ニヤーヤの技術用語の形式化
- ナヴァ・ニヤーヤは古典インド哲学の論理学であり，形式論理学の基礎研究に重要である。
- 従来の形式化試みでは，重要な構造要素が失われていた。
- 立方型理論を用いて，失われた構造要素を維持した形式化を目指す。
- 立方型理論（CTT）によるナヴァ・ニヤーヤの主要構成要素7つ（関係，区切り，非有，包含，同一性，高次関係，充足）の符号化を提示した。
- padarthaシステムのための階層化された宇宙基盤を開発し，符号化された4つの重要な定理を証明した。
- CCTが，従来の形式化方法の欠点を克服し，ナヴァ・ニヤーヤの構造をより正確に捉えることを示した。
OverrideFuzz：意味を考慮した文法ファジングによるスクリプト実行時脆弱性の検出 [cs.CR, cs.PL]目的：スクリプト言語実行時の脆弱性検出手法
- Python等のスクリプト言語は広く利用され，セキュリティ上重要な場面で用いられる。
- スクリプト言語のテストは構文，型制約，オブジェクトレベルのセマンティクスが複雑なため困難である。
- スクリプトとネイティブコード間の境界における脆弱性を検出するファジング手法の確立。
- OverrideFuzzは，オブジェクトのメソッドを上書きする宣言段階と，それを経由する操作を生成する実行段階の二段階で構成される。
- 動的なリフレクションを利用し，実行時の型を追跡し，エラーメッセージから無効な操作を排除することで，セマンティックな正しさに近づける。
- CPython，Lua，QuickJSでの評価で，一貫したカバレッジ向上を示し，Luaは特にメタメソッド機構によって効果が大きかった。
多様な複数バージョン実行 (DME): 構造的なアドレス空間の非相関による正準命令トレースの誤り検出 [cs.PL, cs.SE]目的：多様な実行の一貫性検証
- システムの信頼性確保は重要であり，誤り検出技術の発展が求められている。
- 従来の冗長化手法では，相関する誤りが全レプリカに影響を及ぼし，検出が困難である。
- アドレス空間の非相関により，相関する誤りの影響を排除し，より強固な誤り検出を実現する。
- 多様なバージョン実行 (DME) により，レプリカ間で異なるコードとデータレイアウトを持つことが可能となった。
- 正準命令トレース比較により，アドレス依存性のない誤りを検出できることが示された。
- DMEは，意図的な改ざん，ソフトウェアバグ，コンパイルバグ，物理的妨害など，様々な誤りの種類に対して有効である。
霧の中での論理的保証：LTL目的を持つ健全なPOMDP合成 [cs.LO, cs.FL]目的：不確実な環境下での複雑な時間的制約を満たす自律エージェントの合成
- ロボット工学やAIにおいて，環境の不確実性に対処しつつ目標を達成する自律システムの実現が重要である。
- 部分観測マルコフ決定過程（POMDP）におけるLTL制約の検証が困難であり，信頼性の高い報酬信号の設計が課題となる。
- LTL制約に基づいた確実な報酬形成メカニズムを開発し，部分観測環境下でのエージェントのナビゲーション能力を向上させる。
- 提案手法は，既存のソルバーが失敗するシナリオでも優れた性能を発揮し，ベンチマークドメイン全体で有効性とスケーラビリティを維持する。
- 認定されたLTL充足度に基づいた，信念依存型の報酬を動的に生成する新たな報酬形成メカニズムを開発した。
- このメカニズムを強化されたモンテカルロプランニングフレームワークに統合することで，検証可能な成功を最大化する探索プロセスを実現した。
自動コードレビューフィードバックのためのモデル微調整 [cs.SE]目的：自動コードレビューフィードバックの質向上
- プログラミング教育における個別最適化された支援の重要性が高まっている。
- 高品質なフィードバック生成には，高コストな商用モデルへの依存が課題となっていた。
- オープンLLMを用いた，費用対効果の高いフィードバックシステムの開発を目指す。
- パラメータ効率的なファインチューニング(PEFT)が，プロンプトエンジニアリングよりもフィードバック品質の大幅な向上に貢献することが示された。
- PEFTモデルのフィードバックは，学習者にとってChatGPTと同程度に有効であると評価された。
- 技術用語の説明追加が，PEFTモデルのフィードバックの更なる改善に繋がる可能性があることが示唆された。
ユーザレビューをユーザビリティ要件のソースとして：大規模言語モデルの利用に関する予備研究 [cs.SE]目的：ユーザレビューからのユーザビリティ要件抽出可能性の評価
- ユーザ中心のアプローチは，エンドユーザに適した製品開発に不可欠である。
- 従来の機械学習は，大量のラベル付きデータが必要で，手間とコストがかかる。
- 大規模言語モデルを活用し，迅速かつ安価に要件を抽出することを目指す。
- 大規模言語モデルは，ユーザレビューにおけるユーザビリティ要件を認識できることが示された。
- ユーザビリティ要件の認識性能は，プロンプトに大きく依存することが明らかになった。
- ユーザレビュー300件からユーザビリティに関する側面を抽出し，アノテーションデータセットを構築した。
ほぼ最小カットに対する疎な木 [cs.DS]目的：ほぼ最小カット集合に対する疎な木構造の存在
- グラフ理論は，ネットワークの構造や効率的な情報伝達を分析する上で不可欠である。
- 疎な木構造の構成は困難であり，既存の結果はグラフのサイズに依存する場合が多い。
- $\eta$-ほぼ最小カット集合において，既存の課題を解決し，より効率的な疎な木構造を構築する。
- 本研究では，カットの数が$(1+1/40)k$以下のほぼ最小カット集合に対し，疎な木構造が存在することを示した。
- このアプローチは，Bencz\'urとGoemansの多角形表現を利用し，問題を既知の疎な木構造問題に帰着させる。
- 提案手法は多項式時間で実行可能であり，実用的な応用が期待される。
エージェント的解釈：LLMベースのプログラム解析のための格子構造化された証拠 [cs.SE, cs.AI, cs.PL]目的：LLMベースのプログラム解析における証拠に基づく判断の構造化
- プログラム解析はソフトウェアの品質と安全性を確保する上で不可欠である。
- 従来の静的解析ツールは，ドキュメントや最新のセキュリティ情報など外部情報にアクセスできない。
- LLMの能力を活用し，証拠に基づいた判断を可視化することで，より堅牢な解析を実現する。
- エージェント的解釈は，分析目標を局所的な主張に分解し，各主張に対するLLMの判断を格子構造で追跡する。
- これにより，LLMの判断根拠を明確化し，証拠に基づいた分析を可能にする。
- 本研究では，エージェント的解釈の形式モデルを提示し，その設計空間を探求した。
Grid-Orch：LLMを活用した配電系統シミュレーションと分析のオーケストレーター [eess.SY, cs.AI, cs.SE, cs.SY]目的：配電系統シミュレーションと分析のためのLLMを活用したフレームワーク
- 配電系統のエンジニア不足が深刻化しており，迅速な分析ツールが求められている。
- 配電系統分析には専門知識と高度なスクリプト作成スキルが必要である。
- 自然言語による指示で，複雑な配電系統分析を容易に実行することを目指す。
- Grid-Orchは，LLMと配電系統シミュレーションをModel Context Protocol (MCP)で接続する。
- 36種類のツール（電力潮流計算，電圧解析，QSTSシミュレーション，最適化など）を搭載し，クラウドとローカル両方のLLMに対応。
- DER連系検討のような従来数時間かかっていた作業が，自然言語で2分以内に完了し，OpenDSSの直接スクリプトと同等の結果が得られる。
C言語におけるカニを見つける：比較記号実行による確実な翻訳 [cs.SE]目的：非メモリ安全なコードとメモリ安全な言語への翻訳コード間の差異の検証
- 現代のソフトウェア開発では安全性が重要であり，メモリ安全な言語が推奨されている。
- 既存のC言語コードの書き換えはコストやリスクが高く，自動翻訳に頼る場合がある。
- 自動翻訳における潜在的な意味的差異を特定し，安全性を保証すること。
- cozyは，非安全なコードと翻訳されたコードのバイナリを比較分析するツールである。
- 差異を開発者に提示し，意図的なものか誤りかを判断させることで，同値性を保証する。
- 本手法は自動翻訳，バグ修正，コードレビューなど多岐にわたる応用が期待される。
オープンソースソフトウェアのプロジェクトライフサイクル [cs.SE, cs.SI]目的：オープンソースプロジェクトにおける開発者の関与と成長のモデル化
- ソフトウェア開発における持続的な成長と価値の最大化は重要である。
- オープンソースプロジェクトの長期的な開発者活動や価値評価が困難である。
- 開発者の関与と成長をモデル化し，プロジェクトのライフタイム価値を推定する。
- 開発者の関与は，プロジェクトライフサイクルを通じて一定のパターンを示すことが確認された。
- 内生成長理論と微分方程式を用いて，オープンソースソフトウェアの成長ダイナミクスをモデル化した。
- モデルは多くのオープンソースプロジェクトの実際のデータと整合性が高く，将来の予測に活用できる。
量子事前符号化された極符号 [cs.IT, math.IT, quant-ph]目的：量子事前符号化極符号の設計
- 量子誤り訂正は，量子情報の信頼性確保に不可欠である。
- 従来の量子誤り訂正符号は，符号長が長く計算コストが高い。
- 短ブロック長で高性能な量子誤り訂正符号を開発すること。
- 本研究では，古典極符号の事前符号化の利点を活用した新しいCSS符号族を提案した。
- 遺伝的アルゴリズムを用いて符号のレートプロファイルと事前符号化器を最適化した。
- 提案符号は，偏光チャネル上で$ [\![1201, 1, 25]\!] $表面符号と同等の論理的誤り率を示した。
生成コミュニケーションにおける曖昧性解消の限界：解像度情報の考察 [cs.MA, cs.CY, cs.MM, cs.IT, math.IT]目的：生成コミュニケーションにおける曖昧性解消の限界
- 情報伝達は不確実性の低減を本質とする。生成コミュニケーションはその概念を拡張した分野である。
- 生成モデルによって誘導される制約が，曖昧性の完全な解消を妨げる場合がある。
- 受信側が曖昧性を解消するために必要な最小限の情報量を定量化する。
- 解像度情報は，受信側の事後確率が低曖昧性領域へ移動するために必要な最小情報更新量として定義された。
- 制約がない理想的な状況下では，解像度情報は各領域の事前確率のみに依存する二項発散に帰着する。
- 生成表現が事後分布を制約する場合，幾何学が重要となり，解消不可能な曖昧性下限が生じることが示された。
k回ビンパッキングを用いた電力分配における時間と公平性 [cs.DS, cs.MA]目的：電力分配における時間的公平性の確保
- 電力需要の増加に伴い，限られた資源を効率的に公平に分配することが重要である。
- 既存手法では，電力分配における時間的な公平性を十分に担保できていない。
- k回ビンパッキング問題を通じて，電力分配の公平性を高める手法を開発する。
- k回ビンパッキング問題に対する近似アルゴリズムを一般化し，性能比を分析した。
- 実データを用いた実験により，提案手法が既存のヒューリスティック手法を公平性指標で上回ることを示した。
- ワット数分配における不可能定理を証明し，公平性向上のためのヒューリスティックアルゴリズムを開発した。
言語に基づくエージェント制御 [cs.PL, cs.AI, cs.CR]目的：エージェント制御のための新しいプログラミングモデル
- 自律型システムの開発が重要視される中，安全性と信頼性の確保が課題となっている。
- 従来の制御方法では，エージェントの振る舞いを厳密に制御することが困難であった。
- 言語ベースの型システムにより，エージェントの安全な振る舞いを事前に保証することを目指す。
- 言語に基づくエージェント制御（LBAC）は，エージェントが生成するプログラムの型チェックを通じて，ポリシーを適用する。
- LBACを用いることで，アクセス制御，情報フロー，データProvenanceといったポリシーを統一的に適用できる。
- ファイルシステム機能，データProvenance，情報フロー制御のケーススタディで有効性が示された。
セルプローブによるサンプリングにおける適応性の利点 [cs.CC, cs.DS]目的：適応的および非適応的セルプローブサンプリング間の分離
- 計算効率化のため，データサンプリング手法の性能向上が求められている。
- 非適応的セルプローブサンプリングは，効率に限界がある場合がある。
- 適応的セルプローブサンプリングの優位性を示すことで，効率的なサンプリング手法の確立を目指す。
- 分布$\mathbf{D}$を構成し，適応的・非適応的セルプローブサンプリング間の分離を実証した。
- 適応的サンプリングでは$2$回のプローブで$\mathbf{D}$を正確にサンプリングできるのに対し，非適応的サンプリングでは$\widetilde{\Omega}(N)$回のプローブが必要となる。
- これにより，適応的対非適応的セルプローブサンプリングの分離を$2$-vs-$\widetilde{\Omega}(N)$に改善し，既存研究を上回る結果が得られた。
LFPL：再検討と機械化 [cs.HC, cs.PL, cs.CC, cs.LO]目的：多項式時間計算可能な関数をアフィン型システムで特徴づけるための関数型言語LFPLの研究
- 関数型言語の型システムは，プログラムの正当性保証や効率的な実行に不可欠である。
- LFPLは影響力があるものの，自立した解説や完全な機械化が存在しなかった。
- LFPLとそのメタ理論を現代的に再検討し，機械化することで理解を深める。
- 本研究では，拡張言語LFPL+を用いて健全性証明を行い，表現のコストを制限する多項式を明示的に構成した。
- LFPLプログラムが多項式時間チューリングマシンをシミュレート可能であることを示す完全性証明を簡略化した。
- 健全性と完全性の証明を完全に機械化し，Istariという新しい証明アシスタントの事例研究とした。
電磁波信号と情報理論：連続開口アレイの視点 [cs.IT, math.IT]目的：連続開口アレイ（CAPA）システムに関する電磁波信号と情報理論の概観
- 無線通信システムの性能向上には，アレイ設計の高度化が不可欠である。
- 従来の離散アレイモデルでは，CAPAの連続的な特性を十分に捉えきれない。
- CAPAシステムの理論的基盤を確立し，その性能限界を明らかにすること。
- 本稿は，CAPAシステムを電磁波信号と情報理論の観点から解説するチュートリアルである。
- CAPAの電磁波的基礎，ハードウェア実装，チャネルモデル，ビームフォーミング，チャネル推定を網羅する。
- 波数領域法や関数解析などのツールを用いて，CAPAの無限次元問題を解決可能な形に変換する手法を示す。
AgentLens：SWE-Agent評価における幸運な合格問題の解明 [cs.SE, cs.AI]目的：SWE-Agentの行動過程の評価
- ソフトウェア開発の自動化は，生産性向上に不可欠であり，その評価手法の確立が重要である。
- 従来のSWE-Agent評価は合格/不合格のみに注目しており，過程の質が無視されている。
- SWE-Agentの合格に至る過程の品質を評価し，より信頼性の高い評価指標を提示すること。
- 「幸運な合格」と呼べる，非効率な過程で合格した事例が全体の約10.7%に存在することを示した。
- AgentLensという評価フレームワークと，そのベンチマークデータセットAgentLens-Benchを公開した。
- 過程の品質スコアによるランキングは，合格率のみのランキングと異なる結果を示すことがわかった。
プロトコル駆動型開発：不変条件と証拠による生成ソフトウェアの統制 [cs.SE, cs.AI, cs.LG]目的：生成ソフトウェアの統制メカニズム
- ソフトウェア開発の自動化が進み，迅速な実装が求められるようになった。
- 生成されたソフトウェアの妥当性検証が困難であり，品質保証が課題となっている。
- プロトコルによる厳格な統制により，信頼性の高いソフトウェア開発を実現する。
- プロトコル駆動型開発（PDD）は，実装コードではなく，機械的に検証可能なプロトコルを主要な成果物とする。
- プロトコルは，構造的不変条件，行動的不変条件，運用的不変条件の3要素で構成され，許容可能な実装空間を定義する。
- 実装はプロトコルに適合し，適合の証拠チェーンを生成することで，自動生成ソフトウェアの信頼性を高める。
グループ化された環状変調送受信機は，空間相関チャネルにおけるRIS支援共生無線でほぼ全自由度を実現する [cs.IT, math.IT]目的：RIS支援共生無線システムにおける通信レート向上
- 無線通信容量増大の必要性。通信環境の複雑化に伴い，効率的な信号処理が重要となる。
- 従来法では，RIS素子ごとの位相変調が限界で，RISがもたらす多重化ゲインを十分に活用できていない。
- RISの潜在能力を最大限に引き出し，全自由度を達成し，スペクトル効率を向上させる。
- 提案手法は，従来のリソース割り当て方式と比較して，大幅に高い通信レートを達成する。
- 独自の行列分解アルゴリズムにより，等価チャネルを構造化し，分解残差を効果的に抑制することで，全自由度を実現する。
- 提案する送受信機は，同等のエラー性能を維持しつつ，スペクトル効率の向上に貢献する。
長さ25の三重最大自己直交符号の分類 [cs.NI, cs.RO, cs.MA, cs.IT, math.CO, math.IT]目的：長さ25の三重最大自己直交符号の分類
- 符号理論は，情報伝送や情報セキュリティにおいて重要な役割を果たす。
- 最大自己直交符号の完全な分類は未解決であり，計算量の問題が存在する。
- 長さ25の三重最大自己直交符号の分類を通して，符号理論の進展を目指す。
- 長さ25の三重最大自己直交符号は，既存の理論と計算に基づいて分類された。
- 分類結果は，以前に分類された長さ24までの符号の理論的枠組みを拡張する。
- この研究は，符号理論における新たな発見と応用の可能性を示唆する。
有限体上の多項式環におけるskew polycyclicコード [cs.IT, math.IT]目的：有限体上の多項式環における左イデアルの構造
- 符号理論において，誤り訂正能力の高い符号の構成は重要な課題である。
- skew polycyclicコードの構造は複雑であり，完全な分類が困難である。
- 特定の多項式に対する左イデアルの構造を明確化し，skew polycyclicコードの分類を深める。
- 中心多項式f(x)がx^{np^s}-λである場合，左イデアルのより詳細な構造を決定した。
- λ_1 ≠ 0の場合，左イデアルの生成子の簡略化された表現と，より詳細な構造的特徴付けを得た。
- n=1, t=3 および n=2, t=2 の場合，左イデアルの完全な記述を与え，既存の研究の欠落を補完した。
グラフ倍増の力：弱スーパーバブルへの帰着による双方向グラフにおけるウルトラバブルの計算 [cs.DS]目的：双方向グラフにおけるウルトラバブルの計算手法
- 生物学的ネットワークなど双方向グラフの応用が広がり，効率的なアルゴリズムが求められている。
- ウルトラバブルの計算は複雑であり，既存手法では効率性に課題があった。
- グラフ倍増を用いてウルトラバブルを効率的に計算し，双方向グラフにおけるアルゴリズム適用を促進すること。
- グラフ倍増によってウルトラバブルと弱スーパーバブルの間に直接的な関係性が確立された。
- 本研究は，任意の双方向グラフ上でウルトラバブルを線形時間で計算する初のアルゴリズムを提案する。
- グラフ倍増は，有向グラフ向けアルゴリズムを双方向グラフに適用するための強力かつシンプルな手法であることが示唆される。
TruncProof：トークン長制約下におけるLLMベースのJSON生成のためのガードレール [cs.CL, cs.FL, cs.SE]目的：LLMによるJSON生成におけるトークン長制約の厳格な適用
- LLMを活用したシステム連携において，機械可読な出力形式であるJSONの重要性が高まっている。
- 既存手法では，生成されるトークン数の上限を厳密に制御できず，無限生成や不完全な出力が発生する可能性がある。
- トークン長制約下でも，文法的に有効なJSONを生成する手法を確立すること。
- TruncProofは，LL(1)パーサーの特性を利用し，各デコードステップで文法的に有効な出力を完了するために必要な最小トークン数を効率的に近似する。
- Text-to-JSONタスクの実験により，TruncProofが厳しいトークン制約下でも構文的に正しい出力を生成できることが示された。
- TruncProofは，高度なデコード戦略と組み合わせることで，文法的に正確かつ意味的に正確な出力を実現できる。
セキュリティインセンティブ：マイクロペイメントがコードセキュリティに与える影響に関する実証研究 [cs.CR, cs.SE]目的：コードセキュリティ改善に対するインセンティブの効果
- ソフトウェア開発において，セキュリティは不可欠であり，その重要性は増している。
- 開発者は直接的な価値が見えにくい場合，セキュリティへの注力が不足しがちである。
- 自動化されたセキュリティ指標と報酬を結びつけることで，コードセキュリティを向上させる。
- セキュリティインセンティブを与えたグループは，セキュリティ問題の密度が有意に低下した。
- 特にバックエンド開発において，セキュリティ改善率が高く，インセンティブの効果が顕著であった。
- この測定パイプラインとツールチェーンは，自動化とスケーラビリティに適していることが示された。
脆弱性修正コミットのコード中心検出：統一ベンチマークと実証研究 [cs.SE, cs.CR, cs.LG]目的：脆弱性修正コミットの検出
- セキュリティパッチの迅速な適用は重要であり，脆弱性情報の遅延は平均25日である。
- 脆弱性修正に関する情報は断片化しており，統一的な評価が困難である。
- コードのみから脆弱性修正コミットを正確に検出する方法を確立すること。
- コード言語モデルを用いた脆弱性修正コミットの検出を評価した結果，モデルはコードの変化からセキュリティに関する理解を獲得していないことが示された。
- コミットメッセージが利用可能な場合，モデルの注意はメッセージに集中し，削除してもコード変化への注意はシフトしない。
- グループ分けされた評価では性能低下が確認され，大規模なデータや生成アプローチも根本的な問題を解決するには至らなかった。
SWE-Cycle：完全な課題解決サイクルにおけるコードエージェントのベンチマーク [cs.SE]目的：コードエージェントの実用的な自律性の評価
- ソフトウェア開発の自動化は，生産性向上と開発コスト削減に不可欠である。
- 既存のベンチマークは，現実の複雑さを反映しておらず，エージェントの真の能力を測れない。
- 完全な課題解決サイクルにおけるコードエージェントのボトルネックを特定し，改善を促す。
- SWE-Cycleは，489の厳選された事例でコードエージェントを評価するベンチマークである。
- 環境構築，コード実装，テスト生成を含む3つの個別タスクと，これらを統合したFullCycleタスクで評価を行う。
- FullCycleタスクでは，エージェントは人間の支援なしにリポジトリ内で自律的に動作する必要がある。個別のタスクからFullCycleへの移行で解決率が低下し，段階間の依存関係の処理とコード品質維持の課題が明らかになった。
UIBenchKit：デザイン-コードモデル評価のための統合ツールキット [cs.SE]目的：デザイン-コードモデル評価のための標準化されたプラットフォーム
- ウェブ開発の自動化は効率化に不可欠であり，研究開発の加速が求められている。
- 既存の研究は評価基準の統一性がなく，客観的な比較が困難であった。
- デザインからコードへの変換モデルの性能を公平に比較できる環境を構築すること。
- UIBenchKitは，環境構築，モデル推論，コードレンダリングの複雑さを抽象化し，プラグアンドプレイ可能なアーキテクチャを提供。
- 既存ツールのベンチマークを実施し，今後の改善に向けた知見を得た。
- UIBenchKitは，ウェブエンジニアリングにおけるベンチマークと革新を加速させることを目指す。
知識蒸留の一般化に関する考察：情報理論的視点 [cs.IT, cs.LG, math.IT]目的：知識蒸留における一般化性能の理論的理解
- 機械学習モデルの汎化性能向上は，実用的な応用において不可欠である。
- 知識蒸留は広く用いられるが，その理論的基盤は未解明な部分が多い。
- 知識蒸留が一般化性能を向上させるメカニズムを情報理論的に解明する。
- 教師モデルと生徒モデルの学習を確率過程としてモデル化し，蒸留ダイバージェンスを導入した。
- 生徒モデルの一般化誤差に対して，サブガウス仮定と中心条件の下でそれぞれ上限と下限を導出した。
- 損失の鋭さ（sharpness）を考慮した一般化境界を開発し，教師の局所的な平坦性が境界を厳しくすることを示した。
反復回数非依存型重み係数によるプロダクトコードおよび階段状コードの復号 [cs.IT, math.IT]目的：プロダクトコードおよび階段状コードの復号性能向上
- 通信システムにおける信頼性向上は重要課題であり，誤り訂正符号は不可欠である。
- 既存の復号方式は，計算量が多く，実装が困難な場合がある。
- 反復回数に依存しない復号方式を開発し，実装の容易性を高める。
- 本研究で提案する復号器は，Chase-Pyndiah復号よりも0.23 dB性能が向上する。
- 反復回数依存型係数を必要とせず，スライディングウィンドウ復号に適している。
構文誘導と意味理解に基づいた選好最適化によるコード翻訳の改善 [cs.AI, cs.SE]目的：コード翻訳の改善
- ソフトウェア開発における生産性向上に不可欠であり，言語間の相互運用性を高める。
- 既存のLLMは，構文の正しさと意味の一貫性を両立させるのが難しい。
- ソースコードから直接導出される，より信頼性の高い意味的報酬を確立する。
- CTOは，クロスリンガルな意味モデルを用いてソースコードと翻訳コードの機能的同等性を直接評価する。
- コード翻訳を多目的最適化問題として定式化し，構文フィードバックと意味的シグナルを統合する。
- C++，Java，Pythonの翻訳実験において，既存手法を大幅に上回る性能を示す。
Linuxカーネルドライバにおける参照カウントバグの自動検出 [cs.CR, cs.SE]目的：Linuxカーネルドライバにおける参照カウントバグの検出
- Linuxカーネルは多くのデバイスを制御し，安定稼働には不可欠である。
- ドライバの参照カウントミスは，システム不安定化やセキュリティリスクに繋がる。
- 既存の検出手法では，誤検出が多く，効率的なバグ特定が課題であった。
- 本研究で開発したDrvHornは，Linuxドライバインタフェースを活用し，参照カウント検証をアサーションチェック問題に還元することで，バグ検出を自動化した。
- Linux v6.6カーネルの全プラットフォームドライバにおいて545件のバグを発見，そのうち424件は未報告のバグであった。
- 誤検出率は29.9%と従来手法よりも低く，発見したバグに対する修正パッチ45件がLinuxカーネルにマージされた。
分散近似最大マッチングと最小頂点被覆の，一般化グラフ分解による実現 [cs.DS]目的：分散近似最大マッチングと最小頂点被覆問題の効率的なアルゴリズム
- 分散アルゴリズムは，大規模ネットワークにおける効率的な問題解決に不可欠である。
- 従来の分散アルゴリズムは，ネットワーク規模やグラフの次数に依存した計算時間が必要となる。
- ネットワーク規模に依存する計算時間短縮を目指し，グラフ分解による次数削減を試みる。
- 本研究では，$2+\varepsilon$-近似最大マッチングと近似最小頂点被覆問題を$O(\frac{\log n}{\log^2 \log n})$ラウンドで解くランダム化アルゴリズムを提案した。
- 提案アルゴリズムは，Miller, Peng, Xuらのグラフ分解法を一般化し，高次数グラフの`有効'次数を削減する。
- この分解法は，他の分散アルゴリズム問題への応用も期待される。
ReproScore：研究ソフトウェアの再現性評価における準備状況と結果の分離 [cs.SE]目的：研究ソフトウェアの再現性評価における準備状況と結果の分離に関するフレームワーク
- 研究ソフトウェアの信頼性は科学的進歩に不可欠であり，再現性は信頼性を担保する重要な要素である。
- 既存の評価ツールは，リポジトリの静的な完全性を実行成功の指標としており，誤った判断を招く可能性がある。
- 準備状況と実行結果を分離し，より正確な再現性評価を行うための基盤を提供することを目的とする。
- ReproScoreは，準備状況（RRS）と実行結果（ROS）を分離する二層構造を持ち，それらを統合した複合スコア（RCS）を提供する。
- 環境カテゴリーが故障モードを強く識別することから，静的なシグナルが構造的な差異を捉えていることが確認された。
- RRSは実行成功との相関がほぼゼロであり，準備状況と結果の乖離を実証的に定量化している。
ノイズ下における量子プログラムの堅牢性変異分析 [cs.SE]目的：量子プログラムにおける変異分析のノイズ環境下での有効性評価
- 量子コンピュータの実用化に向けて，ソフトウェアの信頼性確保が重要課題である。
- 従来の変異分析はノイズのない理想的な環境を前提としており，現実の量子ハードウェアへの適用が困難である。
- 量子ハードウェアのノイズが変異分析に与える影響を評価し，より現実的な変異分析手法を確立すること。
- ノイズはプログラムと変異体の行動距離を変化させ，同等変異体と実際の欠陥の区別を難しくする。
- 密度行列に基づく距離指標が最も高い識別能力を持つが，実ハードウェアでの利用は難しい。
- 出力分布に基づく指標は，最大73.03%の精度と74.89%のF1スコアを達成し，ノイズに特化した閾値を適用することで検出性能が向上する。
読みやすさのスペクトル：LLM生成コードにおけるパターン，課題，およびプロンプトの影響 [cs.SE, cs.AI]目的：LLM生成コードの読みやすさに関する体系的な調査
- ソフトウェア開発において，LLMの利用が拡大する中で，コードの品質が重要視されている。
- LLM生成コードの機能品質は注目される一方，読みやすさという重要な非機能的属性は未解明な点が多い。
- LLM生成コードの読みやすさの現状を把握し，プロンプト設計が読みやすさに及ぼす影響を明らかにする。
- 現在のLLMは，全体的な読みやすさにおいて，人間が書いたコードと同等の水準にあることが示された。
- LLM生成コードには，人間が書いたコードとは異なる，特有の読みやすさに関する課題パターンが存在することが明らかになった。
- 関数シグネチャ，制約，スタイル記述がプロンプト設計の中で最も影響力のある要素であり，長期的な保守性の向上が課題である。
双対被覆を用いた強衝突回避頂点連結：カーネル化と彩色限界 [cs.DM, cs.DS]目的：強衝突回避頂点連結数
- グラフ彩色問題は，計算機科学や応用の幅広い分野で基本的な問題である。
- 強衝突回避頂点連結問題は，NP困難であり，効率的なアルゴリズムが課題である。
- 双対被覆というパラメータを利用して，問題の効率的な解法を開発する。
- 双対被覆と目標彩色数kを与えられたとき，多項式時間で最大{2, t+(t+1)k2^{t+k-1}}個の頂点を持つ等価な注釈付きインスタンスに帰着できる。
- これにより，双対被覆数とkをパラメータとする強衝突回避頂点連結数の固定パラメータ時間アルゴリズムが実現する。
- 連結グラフGにおいて，双対被覆Xのサイズtに対し，χ(G) ≤ svcfc(G) ≤ χ(G)+t が成り立つことが証明された。
逐次キャンセルリストデコーディングを用いた偏極符号のブラインド認識 [cs.CL, cs.IT, math.IT]目的：偏極符号のブラインド認識手法
- 通信セキュリティにおいて，符号化方式の認識は重要であり，誤認識は情報漏洩のリスクを高める。
- 非協調環境下での偏極符号のブラインド認識は難しく，特に情報ビット集合の特定は課題である。
- 受信信号のソフト情報を活用し，より高精度なブラインド認識を実現することを目指す。
- 提案手法では，受信ベクトルのLLRの統計的性質に着目し，凍結ビットと情報ビットの識別を行う。
- 凍結ビットは0への決定を好み，情報ビットはほぼ等確率で0/1の決定を示すという特性を利用する。
- リストサイズを増やすことで認識成功率が向上し，既存手法と比較して2.5dB以上の利得を確認した。
定量線形論理 [cs.LO, math.LO]目的：確率的・定量的システム検証のための定量線形論理
- 機械学習モデルなど，確率的・定量的システムの検証において論理が重要視されている。
- 線形論理やファジィ論理における加法結合子は，微分可能な意味論を与えるのが困難である。
- 実数の性質とシーケント計算の大幅な修正により，加法結合子に「ソフト」な意味論を与えることを目指す。
- 提案する定量シーケント計算は，ファジィ論理や深層推論のハイパーシーケント計算を一般化する。
- 新たな計算pQLLは，hardness degree pによってパラメータ化され，cut-elimination theoremが証明されている。
- pが無限大に近づくとpQLLはMALLに還元され，証明可能性がMALLのそれへ収束する。
AIハーネスエンジニアリング：基盤モデルソフトウェアエージェントのためのランタイム基盤 [eess.SY, cs.SY, cs.SE, cs.AI]目的：基盤モデルソフトウェアエージェントの信頼性を高めるためのランタイム基盤の設計と評価
- 近年の基盤モデルの発展は自動コード生成を飛躍的に向上させたが，現実的な開発環境での自律的なソフトウェアエンジニアリングエージェントの信頼性は課題である。
- 既存研究ではモデル自体の能力不足が問題視されてきたが，ソフトウェアエンジニアリング能力はモデル，ハーネス，環境のシステム全体から生まれる。
- モデルと環境を仲介するハーネスの重要性を認識し，その構成要素と段階的なサポートレベルを定義することで，検証可能な変更を可能にする。
- AIハーネスエンジニアリングを形式化し，タスク仕様，コンテキスト選択，ツールアクセスなど11の要素を特定した。
- ハーネスレベルをH0からH3までの4段階で運用化し，エージェントの実行を監査可能なエピソードパッケージに変換する評価プロトコルを提案した。
- 実験の結果，ハーネスレベルの上昇に伴い，エピソードパッケージの証拠構造が系統的に変化し，より詳細なログや検証レポートが生成された。
NLデータ複雑性を持つDL-LiteのHorn拡張 [cs.LO, cs.AI, cs.DB]目的：オントロジーを介したクエリ応答の効率的な手法
- オントロジーを基盤としたデータ管理は，知識表現と推論を通じて高度なデータ活用を実現する。
- 既存のDL-Lite以外の記述論理では，データ複雑性に関する計算困難性が示されており，実用的なクエリ書き換えが制限されている。
- より表現力豊かな記述論理を維持しつつ，グラフクエリ言語への書き換えを可能にする新たな手法を確立すること。
- ELIの層状化メカニズムを導入し，DL-Liteを厳密に拡張するELbotpreceqという記述論理を提案した。
- ELbotpreceqは到達可能性公理と制限された連言をサポートし，NL時間で推論が可能であることを示した。
- 提案言語をGQLのフラグメントであるネストされた双方向正規パスクエリに書き換えることで，NLの上界を確立した。
シングルトンアーク整合性によるMAP-MRF最適化のより強力な緩和 [cs.DS]目的：MAP-MRF推論における緩和手法の改善
- 組合せ最適化問題であり，画像処理や自然言語処理など幅広い分野に応用される。
- NP困難な問題であり，効率的な近似解法が求められている。
- 既存手法よりも効率的に緩和を強化し，より良い近似解を得る。
- 提案手法は，既存のサイクル探索に基づく手法よりも優れた性能を示す。
- シングルトンアーク整合性アルゴリズムを用いることで，効果的な緩和を特定できる。
- 実装コードは公開されており，再現性と利用可能性が高い。
拡散エンコーダ [cs.AR, cs.DB, cs.DC, cs.LG, cs.IT, math.IT]目的：拡散モデルを活用した新しいエンコーダの構築
- 潜在空間の学習は，画像生成や表現学習において重要な役割を担う。
- 変分オートエンコーダでは，エンコーダの分布の制約が課題となる。
- エンコーダとデコーダの同期を改善し，より表現力豊かな潜在空間を学習する。
- 拡散モデルをエンコーダに適用するため，期待値最大化アルゴリズムに着想を得た交互学習法を開発した。
- この手法により，エンコーダとデコーダの信頼性の高い同期が可能となり，標準的な拡散モデルの効率的な学習目標を維持する。
- 従来の変分オートエンコーダにおけるエンコーダの制約を緩和し，潜在表現の質を向上させることが期待される。
Boykov-Kolmogorovアルゴリズムのための高速かつコンパクトなグラフカット [cs.CV, cs.DS]目的：最小s-tカットの計算効率化
- 画像認識をはじめとする多様な分野で，グラフの最小カット問題は重要な役割を担っている。
- 既存のアルゴリズムでは，大規模グラフに対するメモリ消費量が課題となっていた。
- メモリ効率の高い実装により，より大規模なグラフの最小カット問題を解決することを目指す。
- 本研究で提案するfcBKアルゴリズムは，既存のBKアルゴリズムよりも高速な計算が可能となった。
- 新しいグラフ表現を用いることで，10^9個の頂点と10^10個のエッジを持つグラフの最小カットを計算できることを示した。
- 提案手法の実装は，複数のベンチマークデータセットにおいて，最速のBKアルゴリズム実装であると確認された。
CUR摂動解析の再考：局所接空間展開 [math.NA, cs.IT, cs.NA, math.IT]目的：固定インデックスランク切捨てCUR写像の局所摂動展開
- 行列計算において，低ランク近似はデータ圧縮やノイズ除去に不可欠であり，その理論的基盤の確立が重要である。
- 従来のCUR理論では，ノイズの大きさに依存した摂動の境界が示されているが，局所的な摂動挙動の解析は十分に進んでいない。
- 本研究は，選ばれた行と列によって決定されるサンプリング誘導された斜め接空間射影を用いた，局所的な回復誤差の評価を目指す。
- 固定インデックスランク切捨てCUR写像のフレシェ微分が，サンプリング誘導された斜め接空間射影として表現できることが示された。
- 低ランク行列に対する局所回復誤差は，摂動のノルムだけでなく，この射影による摂動の像によって支配されることが明らかになった。
- CURは選ばれた行と列に不可視な摂動を一次精度で除去するのに対し，SVDは直交正規摂動を一次精度で除去する点で異なる。
液体木オートマトン [cs.PL]目的：コンポーネントベース合成における探索効率の向上
- プログラム合成は，複雑なタスクを自動化する上で重要であり，ソフトウェア開発の生産性向上に貢献する。
- 従来のプログラム合成手法は，制約が厳密になると探索空間が指数関数的に増加し，効率が低下する。
- 本研究は，論理的類似性に着目し，状態空間の冗長な探索を削減することで，合成効率を向上させる。
- 本研究で提案する液体木オートマトン（LTA）は，リファインメント型仕様を活用し，意味的に類似した状態を効率的に統合する。
- LTAを用いることで，探索空間を効果的に削減し，従来のプログラム合成ツールでは合成困難な複雑なクエリに対しても解を見出すことが可能となる。
- 実装したツールHegelの評価により，その有効性が実証された。