論文の概要: Crash-free Deductive Verifiers

• arxiv url: http://arxiv.org/abs/2604.19448v1
• Date: Tue, 21 Apr 2026 13:29:03 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-22 22:41:49.784068
• Title: Crash-free Deductive Verifiers
• Title（参考訳）: クラッシュフリーデダクティブ検証器
• Authors: Wander Nauta, Marcus Gerhold, Marieke Huisman,
• Abstract要約: 本稿では,導出検証器の品質とロバスト性を改善するためのファジィングの実践的手法としての利用を提唱する。 我々は,AValAnCHEがVerCorsのいくつかの問題を発見した実験について報告する。
• 参考スコア（独自算出の注目度）: 1.4699455652461724
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: As deductive verifiers mature, their potential user base is growing from the initial core developers to other users. To convince external users of the suitability of verifiers, these tools must run reliably out of the box, give meaningful error messages and display correct results. Yet deductive verifiers are large and complex software systems and their own full verification is often out of reach. We therefore need complementary means to provide such guarantees. This paper advocates the use of fuzzing as a practical way to improve the quality and robustness of deductive verifiers. We outline how fuzz testing can be applied to deductive verifiers, and demonstrate the idea with the prototype tool AValAnCHE, which is integrated with the VerCors verifier. We report on our experiments in which AValAnCHE uncovered several issues in VerCors and demonstrate that the approach also works for other deductive verifiers
• Abstract（参考訳）: デダクティブ検証が成熟するにつれて、その潜在的なユーザベースは、初期コア開発者から他のユーザへと成長しています。 検証者の適合性を外部のユーザに納得させるためには、これらのツールは確実に実行され、意味のあるエラーメッセージを与え、正しい結果を表示する必要がある。 しかし、帰納的検証は大規模で複雑なソフトウェアシステムであり、彼ら自身の完全な検証は到達できないことが多い。 したがって、そのような保証を提供するための補完的な手段が必要です。 本稿では,導出検証器の品質とロバスト性を改善するためのファジィングの実践的手法としての利用を提唱する。 導出検証にファジテストをどのように適用できるかを概説し、VerCors検証と統合されたプロトタイプツールであるAValAnCHEでそのアイデアを実証する。 AValAnCHEがVerCorsのいくつかの問題を発見した実験について報告し、本手法が他の導出検証にも有効であることを実証した。

関連論文リスト

• CoVerRL: Breaking the Consensus Trap in Label-Free Reasoning via Generator-Verifier Co-Evolution [52.691495954442985]
  CoVerRLは1つのモデルがジェネレータと検証ロールを交換するフレームワークで、各機能が他方をブートストラップする。 Qwen と Llama のモデルファミリーでの実験では、CoVerRL は数理推論のベンチマークで4.7-5.9% でラベルなしのベースラインを上回っている。 自己検証の精度は55%から85%以上改善され、両方の能力が真に共存することを確認した。
  論文  参考訳（メタデータ） (2026-03-18T14:38:55Z)
• Verifiable Reasoning for LLM-based Generative Recommendation [106.7765000777685]
  大規模言語モデル(LLM)における推論は、最近、生成的レコメンデーションの強化に強い可能性を示している。 本稿では,信頼性の高いフィードバックを提供するために,検証と推論をインターリーブする新しいTextbftextitreason-verify-recommendパラダイムを提案する。 4つの実世界のデータセットの実験は、VRecが効率を損なうことなく、推奨の有効性とスケーラビリティを大幅に向上することを示した。
  論文  参考訳（メタデータ） (2026-03-08T16:55:45Z)
• InFi-Check: Interpretable and Fine-Grained Fact-Checking of LLMs [48.98720183285795]
  InFi-Checkは、大規模な言語モデルの解釈ときめ細かい事実チェックのためのフレームワークである。 InFi-Checkerは、サポートエビデンスを提供し、きめ細かいエラータイプを分類し、修正と共に正当化を生成する。 実験の結果,InFi-CheckerはInFi-Check-FGの最先端性能を実現することがわかった。
  論文  参考訳（メタデータ） (2026-01-10T20:00:17Z)
• Critical or Compliant? The Double-Edged Sword of Reasoning in Chain-of-Thought Explanations [60.27156500679296]
  系統的な推論連鎖の摂動とデリバリートーンの操作による道徳シナリオにおけるCoT(Chain-of-Thought)の説明の役割について検討した。 1) 利用者は, 根拠に欠陥がある場合でも, 信頼感を保ち, 結果合意を信頼する傾向がみられた。 これらの結果は、CoTの説明が同時に明確化と誤解を招き、視覚的信頼よりも精査と批判的思考を奨励する説明を提供するNLPシステムの必要性を強調している。
  論文  参考訳（メタデータ） (2025-11-15T02:38:49Z)
• Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models [0.0]
  本稿では,Slither-based detectors, Large Language Models (LLMs), Kontrol, Forgeを統合した新しい検出パイプラインを提案する。 私たちのアプローチは、欠陥を確実に検出し、証明を生成するように設計されています。
  論文  参考訳（メタデータ） (2025-09-16T12:46:11Z)
• VerifiAgent: a Unified Verification Agent in Language Model Reasoning [10.227089771963943]
  本稿では,メタ検証とツールベース適応検証の2つのレベルを統合した統合検証エージェントを提案する。 VerifiAgentは推論型に基づいて適切な検証ツールを自律的に選択する。 推論スケーリングに効果的に適用でき、より少ないサンプルとコストでより良い結果が得られる。
  論文  参考訳（メタデータ） (2025-04-01T04:05:03Z)
• On the Rationale and Use of Assertion Messages in Test Code: Insights from Software Practitioners [10.264620067797798]
  単体テストは、一連のテストケースを通じてその振る舞いを検証することによって、ソフトウェアシステムの品質を保証するための重要なプラクティスである。 これらのテストケースの中核となるのはアサーションステートメントであり、それによってソフトウェア実践者がシステムの振る舞いの正しさを検証することができる。 テストケース障害の理解とトラブルシューティングを支援するため、実践者はアサーションステートメントにメッセージ(すなわちアサーションメッセージ)を含めることができる。
  論文  参考訳（メタデータ） (2024-08-03T11:13:36Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。 本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。 その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
  論文  参考訳（メタデータ） (2023-10-19T15:40:00Z)
• Towards a Certified Proof Checker for Deep Neural Network Verification [1.0485739694839669]
  本稿では,DNN検証のための検証チェッカーの実装について述べる。 数値安定性と高い妥当性を提供することにより、既存の実装を改善する。
  論文  参考訳（メタデータ） (2023-07-12T16:53:32Z)

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

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