論文の概要: InvBench: Can LLMs Accelerate Program Verification with Invariant Synthesis?

• arxiv url: http://arxiv.org/abs/2509.21629v1
• Date: Thu, 25 Sep 2025 21:47:02 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-29 20:57:54.039126
• Title: InvBench: Can LLMs Accelerate Program Verification with Invariant Synthesis?
• Title（参考訳）: InvBench: LLMは不変合成によるプログラム検証を加速できるか?
• Authors: Anjiang Wei, Tarun Suresh, Tianran Sun, Haoze Wu, Ke Wang, Alex Aiken,
• Abstract要約: 不変合成におけるLCMの評価のための原理的フレームワークを提案する。 提案手法は,形式的な音質保証を備えた検証器に基づく決定手順を用いる。 我々は,従来の解法UAutomizerに対して,最先端のLLMと既存のLLMベースの検証器を7つ評価した。
• 参考スコア（独自算出の注目度）: 13.240989975977302
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Program verification relies on loop invariants, yet automatically discovering strong invariants remains a long-standing challenge. We introduce a principled framework for evaluating LLMs on invariant synthesis. Our approach uses a verifier-based decision procedure with a formal soundness guarantee and assesses not only correctness but also the speedup that invariants provide in verification. We evaluate 7 state-of-the-art LLMs, and existing LLM-based verifiers against the traditional solver UAutomizer. While LLM-based verifiers represent a promising direction, they do not yet offer a significant advantage over UAutomizer. Model capability also proves critical, as shown by sharp differences in speedups across models, and our benchmark remains an open challenge for current LLMs. Finally, we show that supervised fine-tuning and Best-of-N sampling can improve performance: fine-tuning on 3589 instances raises the percentage of speedup cases for Qwen3-Coder-480B from 8% to 29.2%, and Best-of-N sampling with N=16 improves Claude-sonnet-4 from 8.8% to 22.1%.
• Abstract（参考訳）: プログラム検証はループ不変量に依存するが、強い不変量を自動的に発見することは長年にわたる課題である。 不変合成におけるLCMの評価のための原理的フレームワークを提案する。 提案手法では,形式的な音質保証を備えた検証器に基づく決定手法を用いて,精度だけでなく,不変量による検証の高速化も評価する。 我々は,従来の解法UAutomizerに対して,最先端のLLMと既存のLLMベースの検証器を7つ評価した。 LLMベースの検証器は有望な方向を示すが、UAutomizerに対してまだ大きな優位性を提供していない。 モデル能力はまた、モデル間のスピードアップの急激な違いによって示されるように、重要なものでもある。 最後に,3589インスタンスの微調整はQwen3-Coder-480Bの高速化率を8%から29.2%に引き上げ,N=16によるベストオブNサンプリングはClaude-sonnet-4を8.8%から22.1%に改善する。

関連論文リスト

• MCTS-Refined CoT: High-Quality Fine-Tuning Data for LLM-Based Repository Issue Resolution [18.314436803012434]
  本稿では,モンテカルロ木探索(MCTS)に基づく中間推論ステップの動的検証と最適化を行うMCTS-INEを提案する。 SWE-bench LiteとSWE-bench Verifiedの実験は、我々のCoTデータセットで微調整されたLLMがベースラインよりも大幅に改善されたことを示す。
  論文  参考訳（メタデータ） (2025-06-15T05:42:01Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [8.056359341994941]
  APOLLOは、Leanコンパイラの強みとLLMの推論能力を組み合わせた、モデルに依存しないパイプラインである。 エージェントのセットが証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定します。 修理されたサブステイストは再結合され、再検証され、ユーザ制御された最大試行回数まで反復される。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• LLM2: Let Large Language Models Harness System 2 Reasoning [65.89293674479907]
  大規模言語モデル(LLM)は、無数のタスクにまたがって印象的な機能を示してきたが、時には望ましくない出力が得られる。 本稿では LLM とプロセスベースの検証器を組み合わせた新しいフレームワーク LLM2 を紹介する。 LLMs2は妥当な候補を生成するのに責任を持ち、検証者は望ましい出力と望ましくない出力を区別するためにタイムリーなプロセスベースのフィードバックを提供する。
  論文  参考訳（メタデータ） (2024-12-29T06:32:36Z)
• Language Models are Hidden Reasoners: Unlocking Latent Reasoning Capabilities via Self-Rewarding [74.31981011985681]
  大きな言語モデル(LLM)は印象的な機能を示しているが、それでも複数のステップを必要とする複雑な推論タスクに苦戦している。 LaTRO(LaTent Reasoning Optimization)は、潜在分布からのサンプリングとして推論を定式化するためのフレームワークである。 複数のモデルアーキテクチャを用いて、GSM8KおよびARC-Challengeデータセットの実験を通してLaTROを検証する。
  論文  参考訳（メタデータ） (2024-11-06T22:02:30Z)
• Enhancing Mathematical Reasoning in LLMs by Stepwise Correction [39.67266805233599]
  Best-of-N復号法は、大規模言語モデル(LLM)に複数の解を生成するように指示し、それぞれがスコアリング関数を使用してスコアし、数学的な推論問題に対する最終解として最も高いスコアを選択する。 本稿では,LLMが生成した推論経路の誤りステップを特定し,修正するのに役立つ,ステップワイズ補正(StepCo)という新しいプロンプト手法を提案する。 バリデーション・then-reviseプロセスは、回答の正しさを向上するだけでなく、生成に必要なパスを減らしてトークン消費を減らす。
  論文  参考訳（メタデータ） (2024-10-16T18:18:42Z)
• Adaptive Inference-Time Compute: LLMs Can Predict if They Can Do Better, Even Mid-Generation [51.127054971591924]
  本稿では,生成サンプル数を適応的に削減する新たな自己評価手法を提案する。 平均1.2サンプルだけで16サンプルの使用による改善の74%が達成できることを実証した。
  論文  参考訳（メタデータ） (2024-10-03T17:47:29Z)
• Generative Verifiers: Reward Modeling as Next-Token Prediction [29.543787728397643]
  本研究では,ユビキタスな次世代予測目標を用いて,検証とソリューション生成を併用したトレーニング検証手法を提案する。 標準検証器と比較して、そのような生成検証器(genRM)はLLMのいくつかの利点の恩恵を受けることができる。 我々は、MATHで28%$rightarrow$44.6%、MMLU抽象代数学で37.9%$rightarrow$53.5%の改善を観察する。
  論文  参考訳（メタデータ） (2024-08-27T17:57:45Z)
• Let's Sample Step by Step: Adaptive-Consistency for Efficient Reasoning and Coding with LLMs [60.58434523646137]
  大規模言語モデル(LLM)からの出力の正確性を改善するための一般的なアプローチは、自己整合性である。 コスト効率のよいモデルに依存しない手法であるAdaptive-Consistencyを導入し,各質問のサンプル数を動的に調整する。 実験の結果,Adaptive-Consistencyはサンプル予算を最大7.9倍に削減し,平均精度は0.1%以下であった。
  論文  参考訳（メタデータ） (2023-05-19T17:49:25Z)

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

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