論文の概要: Finding Inductive Loop Invariants using Large Language Models

• arxiv url: http://arxiv.org/abs/2311.07948v1
• Date: Tue, 14 Nov 2023 06:58:09 GMT
• ステータス: 処理完了
• システム内更新日: 2023-11-15 15:18:05.363324
• Title: Finding Inductive Loop Invariants using Large Language Models
• Title（参考訳）: 大規模言語モデルを用いた帰納的ループ不変量探索
• Authors: Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma
• Abstract要約: 帰納ループ不変量を見つけることは決定不可能な問題である。 実用化に向けた長い研究の歴史にもかかわらず、解決された問題には程遠い。 本稿では,新たなソリューションを提供する上での大規模言語モデルの有用性について検討する。
• 参考スコア（独自算出の注目度）: 14.846222005558666
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to establish strong mathematical guarantees about program's runtime behavior. The inductiveness ensures that the invariants can be checked locally without consulting the entire program, thus are indispensable artifacts in a formal proof of correctness. Finding inductive loop invariants is an undecidable problem, and despite a long history of research towards practical solutions, it remains far from a solved problem. This paper investigates the capabilities of the Large Language Models (LLMs) in offering a new solution towards this old, yet important problem. To that end, we first curate a dataset of verification problems on programs with loops. Next, we design a prompt for exploiting LLMs, obtaining inductive loop invariants, that are checked for correctness using sound symbolic tools. Finally, we explore the effectiveness of using an efficient combination of a symbolic tool and an LLM on our dataset and compare it against a purely symbolic baseline. Our results demonstrate that LLMs can help improve the state-of-the-art in automated program verification.
• Abstract（参考訳）: ループ不変量はループを持つプログラムの推論に基本的である。 与えられたループの振る舞いに関する特性を確立する。 それらはさらに帰納的であれば、プログラムの実行動作に関する強力な数学的保証を確立するための形式的検証のタスクに有用になる。 帰納性は、プログラム全体について相談することなく不変量を局所的にチェックできることを保証するため、正しさの形式的証明において必須のアーティファクトである。 帰納ループ不変量を見つけることは決定不可能な問題であり、実用的な解に対する長い研究の歴史にもかかわらず、解決された問題には程遠い。 本稿では、この古い重要な問題に対する新しい解決策を提供する上で、LLM(Large Language Models)の機能について検討する。 そこで我々はまず,ループ付きプログラムにおける検証問題のデータセットをキュレートする。 次に、音の記号ツールを用いて正当性をチェックする帰納的ループ不変量を求めるLLMを利用するプロンプトを設計する。 最後に,当社のデータセットにおけるシンボリックツールとllmの効率的な組み合わせの有効性を検討し,純粋シンボリックベースラインと比較する。 その結果,llmはプログラムの自動検証における最先端の改善に役立つことがわかった。

関連論文リスト

• 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)
• Prover-Verifier Games improve legibility of LLM outputs [12.532113917099885]
  小学校数学の問題を解く上での妥当性について検討する。 本稿では,Anil et al の Prover-Verifier Game にヒントを得たトレーニングアルゴリズムを提案する。 本研究は,解の正当性を検証することを目的とした,時間制約のある人間への正当性訓練の伝達を示す。
  論文  参考訳（メタデータ） (2024-07-18T16:58:18Z)
• Case2Code: Learning Inductive Reasoning with Synthetic Data [105.89741089673575]
  プログラムの表現性と正確性を利用したtextbfCase2Code タスクを提案する。 まず、合成したCase2Codeタスクにおける代表LLMを評価し、LLMにおいてケース・ツー・コード誘導が困難であることを実証する。 実験結果から,このような帰納的学習は,Case2Codeの性能だけでなく,学習用LLMの各種符号化能力の向上にも寄与することがわかった。
  論文  参考訳（メタデータ） (2024-07-17T11:35:00Z)
• Inductive Predicate Synthesis Modulo Programs (Extended) [1.7372615815088566]
  プログラム解析のトレンドは、入力プログラムの言語内で検証条件を符号化することである。 Inductive Predicate Synthesis Modulo Programs (IPS-MP) を提案する。
  論文  参考訳（メタデータ） (2024-07-11T12:51:08Z)
• LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
  本研究では,自然言語フィードバック型検証器Math-Minosを提案する。 実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
  論文  参考訳（メタデータ） (2024-06-20T06:42:27Z)
• Distilling Algorithmic Reasoning from LLMs via Explaining Solution Programs [2.3020018305241337]
  大きな言語モデルの推論能力を改善する効果的な方法として、明確な推論経路を蒸留する手法が登場している。 本稿では, LLM から推論能力を抽出する手法を提案する。 提案実験は,ReasonerがCoderによるプログラム実装をより効果的にガイドできることを示す。
  論文  参考訳（メタデータ） (2024-04-11T22:19:50Z)
• Evaluating and Improving Tool-Augmented Computation-Intensive Math Reasoning [75.74103236299477]
  CoT(Chain-of- Thought prompting)とツール拡張は、大きな言語モデルを改善するための効果的なプラクティスとして検証されている。 ツールインターフェース,すなわち textbfDELI を用いた推論ステップを考慮に入れた新しい手法を提案する。 CARPと他の6つのデータセットの実験結果から、提案されたDELIは、主に競合ベースラインを上回っていることが示された。
  論文  参考訳（メタデータ） (2023-06-04T17:02:59Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)
• Will Bilevel Optimizers Benefit from Loops [63.22466953441521]
  AID-BiOとITD-BiOの2つの一般的な双レベルマトリクスは、自然に1つまたは2つのサブプロブレムを解決する。 AID-BiO と ITD-BiO の両ループ実装選択に適用可能な統合収束解析をまず確立する。
  論文  参考訳（メタデータ） (2022-05-27T20:28:52Z)

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

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