arXiv雑要約
プログラム - 2026/05/14 公開
PoC-Gym：より信頼性の高いLLM支援PoC脆弱性攻撃コード生成に向けて [cs.SE]目的：Javaセキュリティ脆弱性に対するLLMベースのPoC生成パイプラインの開発
- LLMのセキュリティ分野への応用が期待されるが，PoC生成の信頼性が課題となっている。
- 脆弱性記述からのPoC生成は，検証シグナルの信頼性不足により有効性に限界がある。
- 静的・動的情報を活用し，PoC生成の信頼性を向上させることを目指す。
- PoC-Gymは，CVEに特化したプロンプト，静的トレース，カバレッジに基づいたフィードバックを活用する。
- 20件のJava CVEを用いた評価で，116件の候補が実行時検証を，65件が事後検証を通過し，12件のCVEをカバーした。
- FaultLineとの比較では，PoC-Gymは8件のCVEに対して事後検証で成功し，FaultLineは5件だった。誤ったPoCの分析から，今後の改善点を見出した。
ブローワー木による一般化された決定可能性 [cs.LO, math.LO]目的：性質の決定可能性に関する枠組み
- 構成的数学において，決定可能性のより詳細な分類が求められている。
- 従来の決定可能，半決定可能，決定不能という分類では不十分な場合がある。
- ブローワー順序数を用いて決定可能性のレベルを定義し，より細かな分類を目指す。
- 提案された枠組みにおいて，命題がα-決定可能であるという性質が，決定可能性と半決定可能性を一般化することが示された。
- α-決定可能な命題は二項結合の下で閉じていることが示され，二項分離の下での閉包についても議論された。
- 各P(i)が半決定可能ならば，可算なmeet ∀i∈ℕ. P(i) が ω^2-決定可能であることなどが証明された。
interwhen: 推論モデルのテスト時検証のための汎用的なフレームワーク [cs.LO, cs.AI]目的：推論モデルのテスト時検証による正確性確保
- 複雑な推論プロセスを持つモデルの信頼性評価が重要視されている。
- 従来の検証手法では，初期段階のエラーを見逃したり，計算コストが高くなる問題があった。
- 中間推論段階での検証により，効率的かつ正確なエラー検出を目指す。
- 本研究では，推論過程を監視し，必要に応じてモデルの動作を修正するフレームワークinterwhenを提案した。
- 自然言語で記述されたポリシー文書から自動的に検証器を生成する手法を開発し，検証器の不足という課題を克服した。
- 数学的・論理的制約を含むタスクにおいて，既存手法を上回る高い精度を実現し，特にSLMの性能を大幅に向上させた。
グラフニューラルネットワークによる一様施設配置近似学習 [cs.LG, cs.DS, cs.NE, stat.ML]目的：一様施設配置問題における近似解法の開発
- 組合せ最適化問題へのニューラルネットワーク応用は重要である。特に，現実的なデータ分布に適応できる解法が求められている。
- 既存手法は，計算コストが高い，学習が不安定，性能保証がないといった課題を抱えている。
- 近似アルゴリズムの原理を取り入れた微分可能なニューラルネットワークにより，性能と保証の両立を目指す。
- 提案手法は，従来の近似アルゴリズムを改善し，整数計画法との性能差を縮小することを示した。
- このモデルは，ソルバーの教師信号や離散緩和を用いない，証明可能な近似保証を持つ。
- クラスタリング，要約，ロジスティクスなど，幅広い分野への応用が期待される。
事前順序問題における部分最適性 [cs.DM, cs.DS, cs.LG]目的：事前順序問題における部分最適条件の確立
- 生物情報学やソーシャルネットワーク分析などに応用があり，データ間の関係性を構造化する上で重要である。
- NP困難な問題であり，大規模データへの適用には計算コストが課題となっていた。
- 効率的な部分最適条件を新たに提示し，計算時間の短縮を目指す。
- 本研究で提案する部分最適条件は，既存手法と比較して，最適事前順序において「$a \not\lesssim b$」と効率的に判定できるペアの割合を増加させる。
- 実データおよび合成データを用いた実験により，提案手法の有効性が確認された。
LLM駆動アルゴリズムデバッグによる手続き的洗練：ARC-AGI-2への応用 [eess.SY, cs.SY, cs.SE, cs.AI]目的：抽象的推論における潜在的規則の推論と，未知の事例への適用
- 複雑な抽象的推論は，汎用人工知能(AGI)実現への鍵であり，その性能向上が求められている。
- LLMによる規則表現は，結果の誤りしか指摘できず，誤りの根拠となった推論過程の検証が困難である。
- LLMとPrologメタインタプリタを組み合わせ，推論過程を再検証することで，より正確な規則洗練を目指す。
- 提案手法(ABPR)は，ARC-AGI-2において，Gemini-3-Flashで56.67%，GPT-5.5 xHighで98.33%のPass@2を達成した。
- ABPRは，ARC-AGI-2に特化したタスクだけでなく，RAVENスタイルの推論問題にも適用可能であることが示された。
- トレースガイド型探索の並列化により，探索幅と深さが増加しても確率的な変動を抑制できることが確認された。
木構造グラフにおける測地集合問題のアルゴリズムと困難性 [cs.CL, cs.DB, cs.DS, cs.DM]目的：木構造グラフにおける測地集合問題に対する多項式時間アルゴリズムの存在と，その複雑性の解析
- グラフ理論およびアルゴリズム設計において，ネットワークの構造と効率的な問題解決は重要である。
- 測地集合問題はNP困難であり，大規模グラフへの適用が難しいという課題がある。
- 木構造グラフのような制限されたグラフクラスにおいて，効率的なアルゴリズムを開発することを目指す。
- 木構造グラフ（ditree）上では，測地集合問題を多項式時間で解けることを示した。
- 2-サイクルを持たないグラフにおいて，フィードバック辺集合数fenを用いて，$2^{\mathcal{O}(\textsf{fen})} \cdot n^{\mathcal{O}(1)}$時間で解けることを示した。
- DAG上では，フィードバック頂点集合数が定数，パス幅が定数であっても，NP困難であることが示された。
無線通信のためのリドバーグ原子量子受信機：二色励起と三色励起 [cs.IT, math.IT]目的：無線通信におけるリドバーグ原子量子受信機（RAQR）の効率的な三色（3C）レーザー励起に基づくアーキテクチャ
- 次世代通信への応用が期待される量子通信の実現には，高感度かつ低消費電力な受信機の開発が不可欠である。
- 従来のRAQRは，不安定な青色レーザーの使用や，ドップラー広がりによる感度限界，低周波数帯域の検出困難性などの課題があった。
- 本研究は，これらの課題を解決するため，全て赤色/赤外レーザーを用いる3C5L-RAQRアーキテクチャを提案し，その性能を評価する。
- 提案する3C5L-RAQRは，従来の2C4L-RAQRや古典的な受信機と比較して，優れた感度を示すことが数値シミュレーションにより確認された。
- 3C5L-RAQRは，特に電力制限のある広帯域通信環境において，より適した展開が可能であることが示された。
- 感度と容量のトレードオフが明らかになり，3C5L-RAQRがそのバランスに優れていることが示された。
動的LogLog: より高速で小型，かつ正確なカーディナリティ推定 [cs.DS]目的：ストリーム内の異なる要素の数を推定する手法
- ネットワークからバイオインフォマティクスまで，様々な分野でカーディナリティ推定は重要な課題である。
- 既存のHyperLogLog (HLL)は，遷移領域で誤差が大きくなるという問題があった。
- 本研究は，HLLの誤差を改善し，メモリ使用量を削減することを目的とする。
- 動的LogLog (DLL)は，各バケットあたり4ビットを使用し，HLLと比較してメモリ使用量を33%削減する。
- DLLは，高カーディナリティの場合に99.9%以上の要素を早期に棄却し，HLLよりも10倍以上高速に処理できる。
- DLL4は，1,024バイトで平均1.830%，ピーク1.834%の絶対誤差を達成し，HLL (1,536バイト)の平均1.84%，ピーク34.1%を上回る。
AgenticFlict：GitHubにおけるAIコーディングエージェントのプルリクエストにおけるマージコンフリクトの大規模データセット [cs.SE, cs.AI, cs.HC]目的：AIコーディングエージェントによるプルリクエストにおけるマージコンフリクトのデータセット
- ソフトウェア開発におけるAIの活用が拡大しており，その影響を評価する必要がある。
- AIエージェントが生成したコードの統合における課題は未だ十分に解明されていない。
- AIエージェントによるコード統合の課題を理解し，管理するための基礎を提供する。
- 本研究では，14万件以上のAIエージェントによるプルリクエストからなる大規模データセットAgenticFlictを構築した。
- マージコンフリクトの発生率は27.67%であり，AI生成コードにおけるマージコンフリクトの頻度と大きさが示された。
- エージェントによってコンフリクトの発生率にばらつきが見られ，AI支援開発における統合課題への対応が重要であることが示唆された。
再帰的形状言語の共通基盤 [cs.LO, cs.DB]目的：RDFデータに対するスキーマ言語における再帰的意味論の比較と統一的基盤の提示
- RDFデータスキーマ言語は発展を続け，論理プログラミングや記述論理のアイデアを取り入れている。
- ShExとSHACLで再帰的意味論の解釈が異なり，相互運用性や予測可能性に課題が生じている。
- ShExとSHACLの再帰的意味論の設計空間を明確化し，統一的な形式意味論を提案すること。
- ShEx検証器はGFPを実装しているのに対し，SHACL検証器は多様な実装があることが実証された。
- LFP，GFP，SMSを扱う統一的な形式意味論を提示し，LFPとGFPの間の二重性を明らかにした。
- ShExとSHACLは異なる方向に向かっているように見えるが，表現力の点で同一である大きな断片を含むことが示された。
制約充足問題のストリーミング決定可能性の特性化：冗長性のないことによる [cs.DS, cs.CC]目的：制約充足問題(CSP)の充足可能性をストリーミングで決定することの計算量
- 現代社会において，大規模データの効率的な処理が不可欠であり，ストリーミングアルゴリズムはその重要な手法の一つである。
- CSPの決定問題はNP困難であり，大規模インスタンスに対する効率的なアルゴリズムが求められている。
- 制約言語の冗長性のなさを指標とし，ストリーミング決定問題の計算量を正確に特定すること。
- 制約充足問題のストリーミング決定における空間計算量は，制約言語の冗長性のなさによって決定される。
- 特に，冗長性のなさ $\mathsf{NRD}_n(\Gamma)$ が，ストリーミング計算量の限界を対数因子を除いて特徴づける。
- 本研究により，一般的なCSPにおけるストリーミング決定可能性に関する未解決問題を解決した。
バグ報告駆動型故障局所化：ABB Roboticsにおける産業ベンチマークと教訓 [cs.SE, cs.LG]目的：バグ報告を用いた故障局所化の可能性
- 産業環境では大規模かつ長期にわたるシステムに欠陥が蓄積し，品質保証が重要である。
- 故障箇所特定は時間とコストがかかる場合が多く，特にバグ報告のみに頼る保守段階では困難である。
- バグ報告のテキスト情報のみを用いて，AI支援による効率的な故障局所化を実現することを目指す。
- 従来の機械学習モデル（ロジスティック回帰，SVM，ランダムフォレスト）が，ファインチューニングされたTransformerモデルよりも優れた性能を示した。
- データ拡張がランダムフォレストの性能向上に寄与することを確認した。
- Transformerモデルが常に古典的な手法を上回るわけではないという知見を得た。
広告が愛に行ったように，信頼を消費させないでほしい [cs.CY, cs.AR, cs.SE]目的：AIにおける信頼の議論の促進
- AI技術の発展に伴い，人間とAIとの間の信頼関係構築が重要になっている。
- 「信頼」という言葉が，広告のように曖昧に，あるいは安易に使用される可能性がある。
- AIにおける信頼を具体的に議論し，計測可能な指標を確立することを目指す。
- 信頼の基盤となる複数の要素（「信頼の柱」）を提示し，学際的な議論を促す。
- 自律型AIシステムのインターフェースを「信頼ベクトル」として活用する可能性を提案する。
- AIに対する信頼を，広告による愛の消費化のような状況に陥らないようにすることが重要である。
反復構成の代数 [cs.LO]目的：反復固定点演算の推論
- 計算機科学における固定点は重要な概念であり，様々な応用分野で利用されている。
- 既存のアプローチでは，固定点定理の導出に明示的なインデックス計算が必要となる場合がある。
- 等式論理による固定点定理の構成的証明を可能とする代数的枠組みを提供する。
- 反復構成の代数(AIC)を用いることで，Kleene固定点定理を含む固定点定理を代数的に証明できる。
- Tarski-Kantorovichの原理やk-帰納法といった定理の一般化も，AICによって証明された。
- また，AICの公理化の完全性に関する研究から，有限個の有限公理だけでは標準モデルの完全な公理化は不可能であることが示された。
一階述語論理の断片に対する決定可能性結果：記号モデル特性を通じて [cs.LO]目的：一階述語論理の断片の決定可能性
- 一階述語論理は，数学的構造を形式化するための基盤であり，計算機科学や論理学において重要。
- 一階述語論理の完全な断片の決定可能性は一般に困難であり，制限された断片の決定可能性が課題。
- 記号モデル特性を用いて，特定の制限の下で層状化された論理の断片を拡張する決定可能な断片を特定。
- 記号構造は，無限の可能性のある一階述語構造の有限表現として提案され，決定可能性の研究に新たな道を開いた。
- 自己ループ関数を持つソートを許可することで，層状化された論理の断片の制約を緩和し，より表現力豊かな論理に対する決定可能性を示した。
- 記号モデルの構築と正当性の証明は汎用的に行われ，他の同様に制限された断片にも適用可能である。
RepoZero：LLMはゼロからコードリポジトリを生成できるか [cs.SE]目的：ゼロからリポジトリレベルのコード生成能力の評価
- 近年のLLMの進歩は目覚ましいが，ソフトウェア開発への応用には課題が多い。
- 既存の評価指標は偏りを含むか再現性が低く，大規模な検証が困難である。
- API仕様のみからリポジトリを再現するベンチマークを開発し，客観的な評価を実現する。
- 本研究で開発したRepoZeroベンチマークは，完全自動で実行可能な検証を可能にする。
- 最先端のLLMエージェントでも，合格率は30%から55%にとどまり，実用的なソフトウェア開発には課題があることが示された。
- テスト生成による自己検証が，LLMベースのコーディングエージェントの発展に不可欠であることが強調された。
MathlibPR：形式数学ライブラリのプルリクエストマージ準備度ベンチマーク [cs.LO, cs.AI, cs.LG]目的：Mathlibのプルリクエストの評価に関するベンチマーク
- 近年，LLMによる形式検証が注目されており，Mathlibはその基盤として重要な役割を担う。
- Mathlibの成長は，プルリクエストのレビュープロセスがボトルネックとなっており，人的リソースに依存している。
- LLMがMathlibのプルリクエストレビューを支援することで，効率化と貢献の促進を目指す。
- MathlibPRは，実際のMathlib4のプルリクエスト履歴を基にしたベンチマークである。
- LLMおよびLLMエージェントは，マージ可能なプルリクエストと修正が必要なプルリクエストの区別に苦戦していることが判明した。
- MathlibPRは，プルリクエスト評価支援やLLMの学習に向けた報酬モデル開発に貢献する可能性がある。
直交多角形の順序巡回問題 [cs.CG, cs.DS]目的：直交多角形の順序に対する最短巡回経路の計算
- 多角形巡回問題は，ロボットの経路計画や物流最適化など，様々な応用分野で重要である。
- 従来のアルゴリズムは計算量が大きく，大規模な問題への適用が困難であった。
- 直交多角形とマンハッタン距離という制約下で，より高速な巡回経路計算手法を開発すること。
- 連続する多角形が分離している場合，真の亜2乗時間$\widetilde O(n^{2-\frac{1}{48}})$アルゴリズムを達成した。
- 連続する多角形が分離している直交凸多角形に対し，$\widetilde O(n)$アルゴリズムを開発した。
- 軸平行長方形に対しては，$O(n)$アルゴリズムが実現可能であることを示した。
協力者かアシスタントか：AIコーディングエージェントがプルリクエストライフサイクルにおいてどのように作業を分担するか [cs.SE]目的：AIコーディングエージェントのプルリクエストにおける作業分担のあり方
- ソフトウェア開発におけるAIの活用は，生産性向上や開発効率化に不可欠である。
- AIエージェントの役割分担や権限移譲に関する研究は，まだ十分に進んでいない。
- AIエージェントと人間の役割を明確化し，適切な監督体制を構築することを目指す。
- AIコーディングツールは，「協力者」と「アシスタント」のスペクトルに沿って分類できる。
- 「協力者」型ツールは作業の主体をAIに委ね，最終的な承認は人間が行う傾向がある。
- 「アシスタント」型ツールは人間の指示に基づいてAIが支援し，マージの権限はほぼ常に人間に留まる。
BoostAPR：二重報酬モデルを用いた実行に基づいた強化学習による自動プログラム修復の強化 [cs.AI, cs.SE]目的：自動プログラム修復の性能向上
- ソフトウェアの品質向上には，バグの自動修正が不可欠である。効率的な自動修復手法の開発が求められている。
- 従来の強化学習によるプログラム修復は，稀な実行フィードバックと粗い報酬によって効果が制限されていた。
- 実行に基づいた報酬モデルと強化学習を組み合わせ，より効果的なバグ修正を目指す。
- BoostAPRは，実行検証済みのデモンストレーションによる教師ありファインチューニング，二重報酬モデルの学習，PPOによる最適化という三段階構成である。
- SWE-GymやDefects4Jなど複数のベンチマークで，既存モデルと比較して高い性能を示した。特にSWE-bench Verifiedで+22.9ppの改善を実現。
- BoostAPRは，言語を超えた汎化性能も示しており，JavaからPythonへの転移学習においても良好な結果を得ている。
機械的推論とエージェント的推論の組み合わせによるMoveプログラムの仕様推論 [cs.PL, cs.AI, cs.LO, cs.SE]目的：Move Proverにおける仕様推論ツールの開発
- Moveのようなスマートコントラクト言語の安全性確保は重要である。形式検証は有効な手段の一つ。
- Moveプログラムの形式検証には，関数の事前・事後条件を人手で記述する必要があり，手間がかかる。
- 弱最弱前条件解析とAIエージェントを組み合わせることで，仕様記述の負担を軽減することを目指す。
- 本研究では，弱最弱前条件解析とAIエージェント（Claude Code）を組み合わせた仕様推論ツールを開発した。
- AIエージェントは，弱最弱前条件解析が苦手とするループ不変条件や高レベルな仕様（単調性など）の推論を担当する。
- Move Proverが生成された仕様の妥当性を検証し，AIエージェントは検証成功まで仕様を改善し続ける。
Moveにおける命令型第一級関数に対する形式検証 [cs.PL, cs.LO, cs.SE]目的：命令型第一級関数に対する形式検証手法
- スマートコントラクトの安全性確保は重要であり，形式検証はそのための有力な手段である。
- 従来の形式検証ツールでは，命令型第一級関数を効率的に扱えない場合があった。
- Moveプログラミング言語における命令型第一級関数に対する形式検証を可能にすることを目標とする。
- Move Specification LanguageとMove Prover (MVP)における関数値の表現方法を定式化した。
- 関数の振る舞いを記述する述語と，中間メモリ状態を識別するためのラベルを導入した。
- MVPの仕様推論ツールを拡張し，高階Moveコードに対する自動仕様生成を可能にした。
MDPにおける確率的安全性を保証するシールド [cs.LO, cs.AI]目的：MDPにおける確率的安全性保証のためのシールド
- 自律エージェントの安全性確保は重要であり，モデルベースの手法が注目されている。
- 確率的安全性，すなわち許容可能な確率での危険許容が，古典的なシールドよりも困難である。
- 確率的安全性におけるシールドの理論的枠組みを確立し，実用的な構築法を提供する。
- 古典的なシールドの保証を確率的安全性で維持することは不可能であることが示された。
- 安全性と許容性の保証が緩和された，自然なシールドが提案された。
- 強力な安全性保証を持つオフラインおよびオンラインシールド構築法が導入された。
ストリーミング変換器の最小化 [cs.FL, cs.LO]目的：ストリーミング変換器の最小モデルの存在条件
- 形式言語理論において，変換器は入力文字列を出力文字列に変換する重要なモデルである。
- 既存の変換器モデルでは，最小化が困難であったり，適用範囲が限定される場合があった。
- 本研究は，より広範なストリーミング変換器モデルにおける最小化問題の解決を目指す。
- ストリーミング変換器の最小モデルの存在に関する一般的な条件を確立した。
- 特に，葉または根で項を拡張するストリーミング文字列木変換器のバリアントに対して有効な最小化結果が得られた。
- この研究は，古典的な変換器や多項式オートマトンなど，より多くのモデルに適用可能な最小化手法を提供する。
原始生成と二元判断：テスト時スケーリングからの自己学習 [cs.LG, cs.CL, cs.SE]目的：コード生成における自己学習のためのフレームワーク
- コード生成はソフトウェア開発の自動化に不可欠であり，効率的な学習手法が求められている。
- 従来の学習方法は疎な実行フィードバックに依存し，学習効率が低いという課題がある。
- テスト時スケーリングで得られる比較情報を活用し，より効果的な自己学習を目指す。
- DuSTは，モデル自身の生成した候補プログラム群を比較し，実行結果の正確性に基づいてランキング学習を行う。
- これにより，判断能力と生成能力の両方を向上させることが可能となった。
- Qwen3-30B-Thinkingを用いた実験では，判断精度が+6.2 NDCG，pass@1が+3.1，Best-of-4精度が+4.1向上した。
MDPおよびマルコフ連鎖ファミリーにおける条件付き確率の高速計算 [cs.CL, cs.NI, cs.LO]目的：マルコフ決定過程における最適な条件付き到達確率の計算
- 確率的なシステム検証において，状態空間の爆発が重要な課題となるため，効率的な確率計算が不可欠である。
- 既存の手法では，到達確率への還元により循環的なMDPが発生し，解くことが困難となる場合がある。
- 効率的かつ数値的に安定な条件付き到達確率の計算手法を開発し，大規模なマルコフ連鎖の解析を可能にすること。
- 提案手法は，数値的に安定であり，非循環的なMDPにおける閾値問題を線形時間で決定できる。
- 標準的な到達確率クエリと同等の性能が示されており，実用的な効率性を有している。
- ベイズネットワーク解析，確率的プログラム，実行時監視などのベンチマークで，大幅な高速化が確認された。
半位相バリアセントリック代数 [math.FA, cs.LO]目的：半位相および位相バリアセントリック代数の研究
- 凸集合の抽象化であり，関数解析や測度論など，多様な分野に応用可能な代数的構造である。
- 半位相や位相構造を持つバリアセントリック代数の体系的な研究が不足していた。
- バリアセントリック代数における位相構造と代数的構造の相互関係を明らかにすること。
- 半位相バリアセントリック代数上の自由半位相錐の存在が示された。
- 弱局所凸位相バリアセントリック代数は，局所アフィンなバリアセントリック代数のアフィン縮退写像であることが証明された。
- 連続値関数や確率値関数に対するバリアセントリックの一般化と存在定理が導かれた。
定常状態データに基づく重み付きMaxSMTによる定性的モデルの推論 [q-bio.MN, cs.LG, cs.LO]目的：複雑な生物学的システムのモデリングにおける定性的モデルの推論
- 生物学的システムの理解には，複雑な相互作用を表現するモデルが不可欠である。
- 測定誤差や矛盾する観測データが，モデル推論の安定性を損なうことが多い。
- 不確実性を含むデータから，最も適切な定性的モデルを効率的に推論すること。
- 重み付きMaxSMTを用いることで，矛盾する制約を持つデータに対してもロバストなモデル推論が可能になった。
- Boolean変数や多値変数，離散化されたデータ，発現量差に基づく制約を扱える汎用性を持つ。
- 200-1300遺伝子を含む神経細胞分化モデルの推論において，有効性が確認された。
対称性からの量子容量閾値の向上 [quant-ph, cs.IT, math.IT]目的：量子チャネルにおける量子情報の伝送価値の向上
- 量子通信の限界を示すため，量子チャネルの性能評価が重要である。
- 多くのチャネルにおいて量子容量が不明であり，上限と下限の間に大きな隔たりがある。
- 対称性を活用し，従来の限界を超える量子容量閾値の向上を目指す。
- 両方のノイズモデル（脱分極チャネルとパウリチャネル）において，量子容量閾値の有意な向上が確認された。
- 脱分極チャネルにおいては，18年ぶりの改善であり，ハッシュ境界を上回る増加量は過去の全ての改善を合わせたものよりも大きい。
- 対称空間における環境エントロピーの減少が，結果として得られる符号の退化として説明される。