論文の概要: Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought

• arxiv url: http://arxiv.org/abs/2603.18334v1
• Date: Wed, 18 Mar 2026 22:42:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-20 17:19:05.874191
• Title: Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought
• Title（参考訳）: LLMは、Rust検証のための自動定理プローバーのように見えるか?VCoT-Bench: 思考の検証チェーンによる評価
• Authors: Zichen Xie, Wenxi Wang,
• Abstract要約: VCoT-Liftは低レベルの解法推論を高レベルで可読性のある検証ステップに引き上げる。 VCoT-Benchは、欠落した証明の様々な程度に対する堅牢性、異なる証明タイプに対する能力、証明位置に対する感度の3つの次元で性能を測定する。
• 参考スコア（独自算出の注目度）: 1.167370706056905
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: As Large Language Models (LLMs) increasingly assist secure software development, their ability to meet the rigorous demands of Rust program verification remains unclear. Existing evaluations treat Rust verification as a black box, assessing models only by binary pass or fail outcomes for proof hints. This obscures whether models truly understand the logical deductions required for verifying nontrivial Rust code. To bridge this gap, we introduce VCoT-Lift, a framework that lifts low-level solver reasoning into high-level, human-readable verification steps. By exposing solver-level reasoning as an explicit Verification Chain-of-Thought, VCoT-Lift provides a concrete ground truth for fine-grained evaluation. Leveraging VCoT-Lift, we introduce VCoT-Bench, a comprehensive benchmark of 1,988 VCoT completion tasks for rigorously evaluating LLMs' understanding of the entire verification process. VCoT-Bench measures performance along three orthogonal dimensions: robustness to varying degrees of missing proofs, competence across different proof types, and sensitivity to the proof locations. Evaluation of ten state-of-the-art models reveals severe fragility, indicating that current LLMs fall well short of the reasoning capabilities exhibited by automated theorem provers.
• Abstract（参考訳）: 大きな言語モデル(LLM)は、セキュアなソフトウェア開発をますます支援しているため、Rustプログラム検証の厳格な要求を満たす能力は、まだ不明である。 既存の評価では、Rust検証をブラックボックスとして扱い、証明ヒントのバイナリパスやフェール結果のみによってモデルを評価する。 これは、モデルは非自明なRustコードの検証に必要な論理的推論を真に理解しているかどうかを曖昧にしている。 このギャップを埋めるために、我々はVCoT-Liftという低レベルソルバ推論を高レベルかつ人間可読な検証ステップに引き上げるフレームワークを紹介します。 VCoT-Liftは、ソルバレベルの推論を明示的な検証チェーンとして公開することにより、きめ細かい評価のための具体的な基礎的真実を提供する。 VCoT-Liftを活用することで、検証プロセス全体に対するLLMの理解を厳格に評価するための1,988のVCoT完了タスクの包括的なベンチマークであるVCoT-Benchを導入する。 VCoT-Benchは、3つの直交次元に沿って性能を測定する。 10種類の最先端モデルの評価では、重大な脆弱さが示され、現在のLLMは自動定理プローバーによって示される推論能力にかなり劣っていることが示されている。

関連論文リスト

• Grounding the Score: Explicit Visual Premise Verification for Reliable Vision-Language Process Reward Models [8.630726904040781]
  EVPV(Explicit Visual Premise Verification)は,ステップが依存する視覚的前提の信頼性を段階的に評価する,軽量な検証インターフェースである。 EVPVはステップレベルの検証を改善し、強いベースラインよりも常にBest-of-Nの精度を向上する。
  論文  参考訳（メタデータ） (2026-03-17T08:40:26Z)
• Execution-State-Aware LLM Reasoning for Automated Proof-of-Vulnerability Generation [36.950993500170014]
  本稿では,PoV生成を反復的仮説検証法として再構成するエージェントフレームワークであるDrillAgentを提案する。 我々は、実世界のC/C++脆弱性の大規模なベンチマークであるSEC-bench上でDrillAgentを評価する。
  論文  参考訳（メタデータ） (2026-02-14T03:17:27Z)
• VIRO: Robust and Efficient Neuro-Symbolic Reasoning with Verification for Referring Expression Comprehension [51.76841625486355]
  Referring Expression (REC) は、自然言語クエリに対応する画像領域をローカライズすることを目的としている。 最近のニューロシンボリックRECアプローチは、大規模言語モデル(LLM)と視覚言語モデル(VLM)を利用して構成推論を行う。 推論ステップ内に軽量な演算子レベルの検証器を組み込む,ニューロシンボリックなフレームワークであるVIROを紹介する。
  論文  参考訳（メタデータ） (2026-01-19T07:21:19Z)
• Towards Comprehensive Stage-wise Benchmarking of Large Language Models in Fact-Checking [64.97768177044355]
  大規模言語モデル(LLM)は、現実のファクトチェックシステムにますます多くデプロイされている。 FactArenaは、完全に自動化されたアリーナスタイルの評価フレームワークである。 本研究では,静的クレーム検証精度とエンドツーエンドのファクトチェック能力の相違点を明らかにした。
  論文  参考訳（メタデータ） (2026-01-06T02:51:56Z)
• Look As You Think: Unifying Reasoning and Visual Evidence Attribution for Verifiable Document RAG via Reinforcement Learning [55.232400251303794]
  Look As You Think (LAT)は、モデルをトレーニングし、一貫した帰属性を持った検証可能な推論パスを生成するための強化学習フレームワークである。 LATはシングルイメージとマルチイメージの両方でバニラモデルを一貫して改善し、平均ゲインは8.23%、IoU@0.5では47.0%となる。
  論文  参考訳（メタデータ） (2025-11-15T02:50:23Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。 評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
  論文  参考訳（メタデータ） (2025-05-25T19:00:52Z)
• 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)
• A Chain-of-Thought Is as Strong as Its Weakest Link: A Benchmark for Verifiers of Reasoning Chains [33.46649770312231]
  ステップバイステップの回答を提供するために言語モデルを実証することは、複雑な推論タスクにおいて顕著なアプローチである。 このような検証方法の徹底的な評価を可能にするための、きめ細かいステップレベルのデータセットは提供されていない。 ReVEAL: Reasoning Verification Evaluationは複雑なチェーン・オブ・ソート推論の自動検証をベンチマークするデータセットである。
  論文  参考訳（メタデータ） (2024-02-01T12:46:45Z)

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

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