論文の概要: Property-Guided LLM Program Synthesis for Planning

• arxiv url: http://arxiv.org/abs/2605.16142v2
• Date: Mon, 18 May 2026 14:26:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-19 17:57:46.197721
• Title: Property-Guided LLM Program Synthesis for Planning
• Title（参考訳）: 計画立案のためのプロパティ誘導LDMプログラムの合成
• Authors: André G. Pereira, Augusto B. Corrêa, Jendrik Seipp,
• Abstract要約: 評価後にプログラムを採点する代わりに、候補が正式に定義された性質を満たすかどうかを確認する。 このフィードバックは、プログラム生成数と評価コストの両方を大幅に削減します。
• 参考スコア（独自算出の注目度）: 6.88204255655161
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: LLMs have shown impressive success in program synthesis, discovering programs that surpass prior solutions. However, these approaches rely on simple numeric scores to signal program quality, such as the value of the solution or the number of passed tests. Because a score offers no guidance on why a program failed, the system must generate and evaluate many candidates hoping some succeed, increasing LLM inference and evaluation costs. We study a different approach: property-guided LLM program synthesis. Instead of scoring programs after evaluation, we check whether a candidate satisfies a formally defined property. When the property is violated, we stop the evaluation early and provide the LLM with a concrete counterexample showing exactly how the program failed. This feedback drastically reduces both the number of program generations and the evaluation cost, and can guide the LLM to generate stronger programs. We evaluate this approach on PDDL planning domains, asking the LLM to synthesize direct heuristic functions: every state reachable by strictly improving transitions has a strictly improving successor. A heuristic with this property leads hill-climbing algorithm directly to a goal state. A counterexample-guided repair loop generates one candidate program, checks the property over a training set, and returns the first case that violates the property. We evaluate our approach on ten planning domains with an out-of-distribution test set. The synthesized heuristics are effectively direct on virtually all test tasks, and compared to the best prior generation method our approach generates seven times fewer programs per domain on average, solves more tasks without using search, and requires several orders of magnitude less computation to evaluate candidates. Whenever a problem admits a verifiable property, property-guided LLM synthesis can reduce cost and improve program quality.
• Abstract（参考訳）: LLMは、プログラム合成において顕著な成功を示し、以前のソリューションを超越したプログラムを発見した。 しかしながら、これらのアプローチは、ソリューションの値やパステストの数など、プログラムの品質を示すための単純な数値スコアに依存している。 スコアは、プログラムが失敗した理由に関するガイダンスを提供しないので、システムは、何らかの成功を期待する多くの候補を生成し、評価し、LSM推論と評価コストを増大させなければならない。 我々は、プロパティ誘導LLMプログラム合成という、異なるアプローチについて研究する。 評価後にプログラムを採点する代わりに、候補が正式に定義された性質を満たすかどうかを確認する。 資産が侵害された場合、我々は早期に評価を中止し、プログラムの失敗を正確に示す具体的な反例をLSMに提供する。 このフィードバックは、プログラム生成数と評価コストの両方を大幅に削減し、LCMがより強力なプログラムを生成するように誘導することができる。 我々は、PDDLプランニング領域におけるこのアプローチを評価し、LCMに直接ヒューリスティック関数の合成を求める。 この性質を持つヒューリスティックは、ヒルクライミングアルゴリズムを直接ゴール状態に導く。 逆例誘導修理ループは、1つの候補プログラムを生成し、トレーニングセット上のプロパティをチェックし、そのプロパティに違反した最初のケースを返す。 アウト・オブ・ディストリビューションテストセットを用いて,10のプランニング領域に対するアプローチを評価した。 合成されたヒューリスティックスは、事実上全てのテストタスクに事実上直接的であり、最も優れた事前生成手法と比較して、我々の手法は、平均してドメイン当たりの7倍のプログラムを生成し、探索を使わずにより多くのタスクを解決し、候補を評価するために数桁の計算を必要とします。 検証可能な性質を許容する問題が発生すると、プロパティ誘導LDM合成はコストを低減し、プログラム品質を向上させることができる。

関連論文リスト

• LLM-ERM: Sample-Efficient Program Learning via LLM-Guided Search [23.97383442759484]
  LLM-ERM は、全列挙を LLM 誘導探索に置き換える提案と検証のフレームワークである。 コーディネート的にオンラインのミニバッチSGDは,特定のショートプログラムを学習するために多くのサンプルを必要とすることを示す。 これらの結果は,言語誘導型プログラム合成が有限クラスEMMの統計効率の多くを回復することを示している。
  論文  参考訳（メタデータ） (2025-10-16T06:10:11Z)
• Do AI models help produce verified bug fixes? [62.985237003585674]
  大規模言語モデルは、ソフトウェアバグの修正に使用される。 本稿では,プログラマが大規模言語モデルを用いて,自身のスキルを補完する方法について検討する。 その結果は、プログラムバグに対する保証された修正を提供するAIとLLMの適切な役割への第一歩となる。
  論文  参考訳（メタデータ） (2025-07-21T17:30:16Z)
• Towards Effectively Leveraging Execution Traces for Program Repair with Code LLMs [13.708569727719434]
  大きな言語モデル(LLM)は、様々なプログラミングタスクにおいて有望なパフォーマンスを示す。 我々は,標準的なAPRプロンプトをプログラム実行トレースで強化することで,この潜在的な盲点を修復することを目指している。
  論文  参考訳（メタデータ） (2025-05-07T14:12:41Z)
• AIME: AI System Optimization via Multiple LLM Evaluators [79.03422337674664]
  AIME は複数の LLM を利用した評価プロトコルであり、それぞれが独立した基準で評価を生成し、結合を通してそれらを結合する。 コード生成タスクにおける AIME のベースラインメソッドのパフォーマンスは,LeetCodeHard と HumanEval データセットの単一 LLM 評価プロトコルよりも最大 62% 高いエラー検出率,最大 16% 高い成功率で向上している。
  論文  参考訳（メタデータ） (2024-10-04T04:03:24Z)
• Human-Instruction-Free LLM Self-Alignment with Limited Samples [64.69906311787055]
  本研究では,人間の関与なしに,大規模言語モデル(LLM)を反復的に自己調整するアルゴリズムを提案する。 既存の研究と異なり、我々のアルゴリズムは人造指示にも報酬にも依存せず、人間の関与を著しく減らしている。 提案手法は,LLMの自己一般化能力を解き明かし,ほぼゼロに近い人的監督と整合性を持たせることができることを示す。
  論文  参考訳（メタデータ） (2024-01-06T14:00:12Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)

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

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