論文の概要: Teaching LLMs Program Semantics via Symbolic Execution Traces

• arxiv url: http://arxiv.org/abs/2605.06184v1
• Date: Thu, 07 May 2026 13:01:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-08 22:27:11.804049
• Title: Teaching LLMs Program Semantics via Symbolic Execution Traces
• Title（参考訳）: 記号的実行トレースによるLLMプログラムセマンティックス指導
• Authors: Jonas Bayer, Stefan Zetzsche, Olivier Bouissou, Remi Delmas, Michael Tautschnig, Soonho Kong,
• Abstract要約: SV-COMP 2025上に構築された500 C 検証タスクの評価フレームワークを提案する。 6家族の14モデルを評価し,総合的精度の高いマスクが致命的な弱点であることを確認した。 わずか$sim$3,000のバグトレースと、推論時の連鎖推論を組み合わせることで、違反検出を17ポイント以上改善する。
• 参考スコア（独自算出の注目度）: 0.7046782561282057
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce an evaluation framework of 500 C verification tasks across five property types (memory safety, overflow, termination, reachability, data races) built on SV-COMP 2025, and evaluate 14 models across six families. We find that high overall accuracy masks a critical weakness: while most models reliably confirm properties hold, violation detection varies widely and degrades sharply with program length. To close this gap, we train on formal verification artifacts: running the Soteria symbolic execution engine on generic open-source C code and using the resulting traces for continued pretraining of Qwen3-8B. Just ${\sim}$3,000 bug traces combined with chain-of-thought reasoning at inference time improve violation detection by over 17 percentage points, producing one of the most balanced accuracy profiles among evaluated models. On violation detection, the trained 8B model outperforms the 4$\times$ larger Qwen3-32B without thinking and approaches it in overall accuracy. The interaction between trace training and chain-of-thought is superadditive: neither alone provides meaningful gains, but their combination does. Improvements transfer across all five property types, including ones the training traces do not target. Our 28 configurations confirm the gains stem from trace semantics, not code volume, and that trace curation and format matter.
• Abstract（参考訳）: SV-COMP 2025上に構築された5つのプロパティタイプ(メモリ安全性,オーバーフロー,終端,到達性,データレース)にまたがる500のC検証タスクの評価フレームワークを導入し,6つのファミリーにまたがる14のモデルを評価する。 ほとんどのモデルでは、プロパティが確実に保持されていることを確実に確認しているが、違反検出は広範囲に渡り、プログラム長とともに大幅に劣化する。 このギャップを埋めるために、我々は正式な検証アーティファクトをトレーニングする: 一般的なオープンソースCコードでSoteriaのシンボル実行エンジンを実行し、結果として得られたトレースを使用してQwen3-8Bの事前トレーニングを継続する。 ちょうど${\sim}$3,000のバグトレースと、推論時の連鎖推論を組み合わせることで、違反検出が17ポイント以上向上し、評価されたモデルの中で最もバランスの取れた精度プロファイルの1つが生み出された。 違反検出では、トレーニングされた8Bモデルは、考えずに4$\times$大きなQwen3-32Bより優れ、全体的な精度でアプローチする。 トレーストレーニングとチェーンオブ思考の相互作用は超加法的であり、どちらも有意義な利得を提供するものではないが、それらの組み合わせは可能である。 トレーニングトレースがターゲットにしていないものを含む、5つのプロパティタイプすべての改善が転送される。 28の構成は、コードボリュームではなくトレースセマンティクスと、トレースキュレーションとフォーマットの問題に由来することを確認しています。

関連論文リスト

• KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code [15.778121969330476]
  我々は、VerusベースのRust検証のための検索拡張システムであるKVerusを紹介する。 KVerusは、コードメタデータ、レムマセマンティクス、ツールチェーン仕様の動的知識ベースを構築する。 複雑なファイル間の依存関係をナビゲートして証明を合成し、共通の進化的変化に直面した時に自動的に証明を修正することができる。
  論文  参考訳（メタデータ） (2026-05-05T14:50:24Z)
• Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
  SPECAは、明示的で分類されたセキュリティプロパティを自然言語仕様から導き出し、実装間で再利用する監査フレームワークである。 RepoAuditのベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化している。 Sherlock Fusaka Audit Contest(10のターゲット、366の応募)では、SPECAが専門家が強化した15の脆弱性をすべて回復し、4つの修正確認バグが浮上した。
  論文  参考訳（メタデータ） (2026-04-29T09:57:07Z)
• Claw-Eval: Toward Trustworthy Evaluation of Autonomous Agents [66.97968363332465]
  エージェントベンチマークの3つのギャップに対処するエンドツーエンド評価スイートであるClaw-Evalを紹介した。 Claw-Evalは3つのグループにまたがる9つのカテゴリにまたがる300の人間検証タスクで構成されている。 すべてのエージェントアクションは、3つの独立したエビデンスチャネルを通じて記録される。
  論文  参考訳（メタデータ） (2026-04-07T17:43:18Z)
• TraPO: A Semi-Supervised Reinforcement Learning Framework for Boosting LLM Reasoning [33.47825979936341]
  検証可能な報酬(RLVR)を用いた強化学習は、大きな推論モデル(LRM)の訓練に有効であることが証明された。 提案アルゴリズムは,学習軌跡とラベル付き標本との類似性を一致させることで,信頼できない標本を同定する。 1Kのラベル付きサンプルと3Kのラベルなしサンプルだけで、TraPOの平均精度は42.6%に達し、45Kのラベルなしサンプル(38.3%)で訓練された最高の教師なしメソッドを上回った。
  論文  参考訳（メタデータ） (2025-12-15T09:03:45Z)
• LYNX: Learning Dynamic Exits for Confidence-Controlled Reasoning [15.597220136913258]
  LYNXはオンラインのアーリーエグジットメカニズムで、モデル自身の隠れ状態の認識を信頼性制御による停止決定に変換する。 一般的な数学的コーパスで一度このプローブをトレーニングして校正し、ベンチマーク、復号化温度、さらには非数学的なタスクで再利用します。
  論文  参考訳（メタデータ） (2025-12-05T00:04:42Z)
• Explainable Vulnerability Detection in C/C++ Using Edge-Aware Graph Attention Networks [0.2499907423888049]
  本稿では,C/C++コードの脆弱性検出のためのグラフベースのフレームワークであるExplainVulDを提案する。 平均精度88.25パーセント、F1スコア48.23パーセントをReVealデータセット上で30の独立ランで達成している。
  論文  参考訳（メタデータ） (2025-07-22T12:49:14Z)
• SEAL: Steerable Reasoning Calibration of Large Language Models for Free [58.931194824519935]
  大規模言語モデル(LLM)は、拡張チェーン・オブ・ソート(CoT)推論機構を通じて複雑な推論タスクに魅力的な機能を示した。 最近の研究では、CoT推論トレースにかなりの冗長性が示されており、これはモデル性能に悪影響を及ぼす。 我々は,CoTプロセスをシームレスに校正し,高い効率性を示しながら精度を向上する,トレーニング不要なアプローチであるSEALを紹介した。
  論文  参考訳（メタデータ） (2025-04-07T02:42:07Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Masked Thought: Simply Masking Partial Reasoning Steps Can Improve Mathematical Reasoning Learning of Language Models [102.72940700598055]
  推論タスクでは、小さなエラーでも不正確な結果にカスケードすることができる。 入力の摂動に頼らず、外部リソースの導入を避ける手法を開発した。 私たちのトレーニングアプローチでは、思考の連鎖の中で特定のトークンをランダムにマスクします。
  論文  参考訳（メタデータ） (2024-03-04T16:21:54Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。