論文の概要: HoarePrompt: Structural Reasoning About Program Correctness in Natural Language

• arxiv url: http://arxiv.org/abs/2503.19599v1
• Date: Tue, 25 Mar 2025 12:30:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-26 16:52:41.502123
• Title: HoarePrompt: Structural Reasoning About Program Correctness in Natural Language
• Title（参考訳）: HoarePrompt: 自然言語におけるプログラムの正確性に関する構造的推論
• Authors: Dimitrios Stamatios Bouras, Yihan Dai, Tairan Wang, Yingfei Xiong, Sergey Mechtaev,
• Abstract要約: HoarePromptは、プログラム分析や検証から自然言語アーティファクトへの基本的な考え方を適応する、新しいアプローチである。 ループを管理するために,モデル検査に広く用いられているk-induction法の適応として,数発のk-inductionを提案する。 実験の結果,HoarePromptはZero-shot-CoTプロンプトを正当性分類に用いた場合に比べて,MCCを62%改善することがわかった。
• 参考スコア（独自算出の注目度）: 6.0749049701897295
• License:
• Abstract: While software requirements are often expressed in natural language, verifying the correctness of a program against natural language requirements is a hard and underexplored problem. Large language models (LLMs) are promising candidates for addressing this challenge, however our experience shows that they are ineffective in this task, often failing to detect even straightforward bugs. To address this gap, we introduce HoarePrompt, a novel approach that adapts fundamental ideas from program analysis and verification to natural language artifacts. Drawing inspiration from the strongest postcondition calculus, HoarePrompt employs a systematic, step-by-step process in which an LLM generates natural language descriptions of reachable program states at various points in the code. To manage loops, we propose few-shot-driven k-induction, an adaptation of the k-induction method widely used in model checking. Once program states are described, HoarePrompt leverages the LLM to assess whether the program, annotated with these state descriptions, conforms to the natural language requirements. For evaluating the quality of classifiers of program correctness with respect to natural language requirements, we constructed CoCoClaNeL, a challenging dataset of solutions to programming competition problems. Our experiments show that HoarePrompt improves the MCC by 62% compared to directly using Zero-shot-CoT prompts for correctness classification. Furthermore, HoarePrompt outperforms a classifier that assesses correctness via LLM-based test generation by increasing the MCC by 93%. The inductive reasoning mechanism contributes a 28% boost to MCC, underscoring its effectiveness in managing loops.
• Abstract（参考訳）: ソフトウェア要件は自然言語で表されることが多いが、自然言語要求に対するプログラムの正しさを検証することは困難で未解決の問題である。 大規模な言語モデル(LLM)は、この問題に対処する上で有望な候補ですが、私たちの経験からは、これらのモデルがこのタスクでは効果がないことが示されています。 このギャップに対処するために、プログラム分析や検証から自然言語アーティファクトへの基本的な考え方を適応させる新しいアプローチであるHoarePromptを紹介します。 最強の条件計算からインスピレーションを得たHoarePromptは、LLMがコード内の様々な点で到達可能なプログラム状態の自然言語記述を生成する、体系的なステップバイステップのプロセスを採用している。 ループを管理するために,モデル検査に広く用いられているk-induction法の適応として,数発のk-inductionを提案する。 プログラム状態が記述されると、HoarePrompt は LLM を利用して、これらの状態記述に注釈を付けたプログラムが自然言語の要求に適合するかどうかを評価する。 自然言語要求に対するプログラム正当性の分類器の品質を評価するために,プログラム競合問題に対する解の挑戦的データセットであるCoCoClaNeLを構築した。 実験の結果,HoarePromptはZero-shot-CoTプロンプトを正当性分類に用いた場合に比べて,MCCを62%改善することがわかった。 さらに、HoarePromptは、MCCを93%増加させることで、LCMベースのテスト生成による正確性を評価する分類器よりも優れている。 誘導的推論機構はMCCを28%向上させ、ループ管理の有効性を裏付ける。

関連論文リスト

• 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)
• 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)
• Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages [21.18996339478024]
  SPEAC(emphsynthetic programming elicitation and compilation)を紹介する。 SPEACは、より頻繁に、意味的正しさを犠牲にすることなく、構文的に正しいプログラムを生成する。 UCLID5形式検証言語のケーススタディにおいて,SPEACの性能を実証的に評価した。
  論文  参考訳（メタデータ） (2024-06-05T22:16:19Z)
• From Effectiveness to Efficiency: Comparative Evaluation of Code Generated by LCGMs for Bilingual Programming Questions [32.464611304079234]
  大規模コード生成モデル(LCGM)は、様々なプログラミングタスクにおいて大きな注目を集め、有望な結果を得た。 既存のベンチマークは、LCGMが生成したコードの品質を不十分に評価する、英語のプログラミング問題と限定的なユニットテストケースに依存していることが多い。 本稿では,異なる自然言語を入力として使用する場合のコード品質の違い,特に有効性と効率について検討する。
  論文  参考訳（メタデータ） (2024-06-02T03:22:30Z)
• Natural Language as Policies: Reasoning for Coordinate-Level Embodied Control with LLMs [7.746160514029531]
  ロボットのタスク計画問題に対処するLLMによる実験結果を示す。 提案手法はタスクとシーンオブジェクトのテキスト記述を取得し,自然言語推論によるタスクプランニングを定式化する。 提案手法はマルチモーダル・プロンプト・シミュレーション・ベンチマークを用いて評価する。
  論文  参考訳（メタデータ） (2024-03-20T17:58:12Z)
• The Consensus Game: Language Model Generation via Equilibrium Search [73.51411916625032]
  言語モデル復号のための学習不要なゲーム理論を新たに導入する。 本手法では,正規化不完全情報シーケンシャルシグナリングゲームとして,言語モデルの復号化を行う。 EQUILIBRium-RANKINGをLLaMA-7Bに適用すると、より大型のLLaMA-65BとPaLM-540Bより優れた性能を発揮する。
  論文  参考訳（メタデータ） (2023-10-13T14:27:21Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  本稿では,プログラムの実行結果の検証を学習することで,言語からコードへの生成を改善するシンプルな手法であるLEVERを提案する。 具体的には、LLMからサンプリングされたプログラムが、自然言語入力、プログラム自体とその実行結果に基づいて正しいか否かを判定するために、検証者を訓練する。 LEVER はベースコード LLMs (4.6% から 10.9% まで) を継続的に改善し、それらすべてに対して新しい最先端の結果を得る。
  論文  参考訳（メタデータ） (2023-02-16T18:23:22Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  実行結果-プログラム選択のための最小ベイズリスク復号化。 そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
  論文  参考訳（メタデータ） (2022-04-25T06:06:08Z)

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

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