論文の概要: Ranking LLM-Generated Loop Invariants for Program Verification

• arxiv url: http://arxiv.org/abs/2310.09342v1
• Date: Fri, 13 Oct 2023 18:13:52 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-17 22:23:08.306654
• Title: Ranking LLM-Generated Loop Invariants for Program Verification
• Title（参考訳）: プログラム検証のためのLLM生成ループ不変量ランキング
• Authors: Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Madanlal Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy
• Abstract要約: 大規模言語モデルは、0ショット設定でプログラムのクラスに対するループ不変量を合成することができる。 これは、不変性を確立するためのプログラム検証者への多数の呼び出しにつながる可能性がある。 我々は正しい帰納的不変量と誤った試みを区別できるランク付け器を設計した。
• 参考スコア（独自算出の注目度）: 14.7590099354867
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable of synthesizing loop invariants for a class of programs in a 0-shot setting, yet require several samples to generate the correct invariants. This can lead to a large number of calls to a program verifier to establish an invariant. To address this issue, we propose a {\it re-ranking} approach for the generated results of LLMs. We have designed a ranker that can distinguish between correct inductive invariants and incorrect attempts based on the problem definition. The ranker is optimized as a contrastive ranker. Experimental results demonstrate that this re-ranking mechanism significantly improves the ranking of correct invariants among the generated candidates, leading to a notable reduction in the number of calls to a verifier.
• Abstract（参考訳）: 帰納ループ不変量の合成は、プログラム検証の自動化に不可欠である。 本稿では,大規模言語モデル(gpt-3.5 や gpt-4 など)が,0-shot 設定のプログラムのクラスに対してループ不変量の合成が可能であるが,正しい不変量を生成するにはいくつかのサンプルが必要であることを検証した。 これは、不変性を確立するためのプログラム検証者への多数の呼び出しにつながる可能性がある。 この問題に対処するために, LLM の生成結果に対して, {\it re-level} アプローチを提案する。 我々は問題定義に基づいて正しい帰納的不変量と誤った試みを区別できるランク付け器を設計した。 ランク付けは対照的なランク付けに最適化されている。 実験結果から、この再ランク機構は、生成した候補の正しい不変量ランキングを大幅に改善し、検証者への呼び出し数が顕著に減少することを示した。

関連論文リスト

• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• Generative Verifiers: Reward Modeling as Next-Token Prediction [29.543787728397643]
  検証や報酬モデルはしばしば、大きな言語モデル(LLM)の推論性能を高めるために使われる。 本研究では,ユビキタスな次世代予測目標を用いて,検証とソリューション生成を併用したトレーニング検証手法を提案する。 GenRMは差別的, DPO 検証, LLM-as-a-Judge に優れていた。
  論文  参考訳（メタデータ） (2024-08-27T17:57:45Z)
• Code Repair with LLMs gives an Exploration-Exploitation Tradeoff [16.80314690163063]
  大きな言語モデル(LLM)でソースコードを反復的に改善し、修復することは、1ショットで構築するには複雑すぎるプログラムを生成する一般的な方法として現れている。 ここでは、リファインメントが探索と露見のトレードオフを露呈していることを示します。ほとんどのテストケースをパスするプログラムをリファイン化したり、考慮の少ないプログラムをリファインダでリファインダすることです。
  論文  参考訳（メタデータ） (2024-05-26T04:00:30Z)
• Finding Inductive Loop Invariants using Large Language Models [14.846222005558666]
  帰納ループ不変量を見つけることは決定不可能な問題である。 実用化に向けた長い研究の歴史にもかかわらず、解決された問題には程遠い。 本稿では,新たなソリューションを提供する上での大規模言語モデルの有用性について検討する。
  論文  参考訳（メタデータ） (2023-11-14T06:58:09Z)
• Winning Prize Comes from Losing Tickets: Improve Invariant Learning by Exploring Variant Parameters for Out-of-Distribution Generalization [76.27711056914168]
  Out-of-Distribution (OOD) 一般化は、分散固有の特徴に適合することなく、様々な環境によく適応する堅牢なモデルを学ぶことを目的としている。 LTH(Lottery Ticket hypothesis)に基づく最近の研究は、学習目標を最小化し、タスクに重要なパラメータのいくつかを見つけることでこの問題に対処している。 Invariant Learning (EVIL) における変数探索手法を提案する。
  論文  参考訳（メタデータ） (2023-10-25T06:10:57Z)
• ALGO: Synthesizing Algorithmic Programs with LLM-Generated Oracle Verifiers [60.6418431624873]
  大きな言語モデル(LLM)は、機能記述からコードを実装するのに優れているが、アルゴリズムの問題に悩まされている。 我々は,アルゴリズムプログラムを LLM 生成 Oracle で合成するフレームワーク ALGO を提案し,その生成をガイドし,その正確性を検証する。 実験の結果,ALGOを装着すると,Codexモデルよりも8倍,CodeTよりも2.6倍の1サブミッションパス率が得られることがわかった。
  論文  参考訳（メタデータ） (2023-05-24T00:10:15Z)
• Large Language Models are Better Reasoners with Self-Verification [48.534270563880845]
  大規模言語モデル(LLM)は、いくつかの自然言語処理タスクにおいて強力な推論能力を示している。 思考の連鎖(CoT)を促進させるLLMは、個別のミスに非常に敏感な、多段階のプロンプトと多段階の予測を必要とする。 また,LLMにも同様な自己検証能力があることを示す。
  論文  参考訳（メタデータ） (2022-12-19T15:51:52Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。 我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
  論文  参考訳（メタデータ） (2022-06-04T22:01:05Z)
• Discovering Non-monotonic Autoregressive Orderings with Variational Inference [67.27561153666211]
  我々は、訓練データから高品質な生成順序を純粋に検出する、教師なし並列化可能な学習装置を開発した。 エンコーダを非因果的注意を持つトランスフォーマーとして実装し、1つのフォワードパスで置換を出力する。 言語モデリングタスクにおける経験的結果から,我々の手法は文脈認識であり,一定の順序と競合する,あるいはより優れた順序を見つけることができる。
  論文  参考訳（メタデータ） (2021-10-27T16:08:09Z)

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

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