論文の概要: How Powerful are LLMs in Generating Formal Program Specifications?
- arxiv url: http://arxiv.org/abs/2608.13077v1
- Date: Thu, 13 Aug 2026 10:45:18 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-14 18:29:38.480153
- Title: How Powerful are LLMs in Generating Formal Program Specifications?
- Title（参考訳）: 形式的プログラム仕様の生成におけるLLMはどの程度強力か?
- Abstract要約: Coinsは、信頼できるテストケースの評価下で仕様をインスタンス化し、具体的な証明義務を生成することで仕様品質を評価する評価フレームワークである。
我々はHumanEvalに関する大規模な研究を、人間によるRocq仕様のキュレートされたセットで実施する。
以上の結果から, 仕様生成は依然として重大な課題であり, 検証の複雑さは仕様品質の真の相違を曖昧にする可能性があることが示唆された。
- 参考スコア（独自算出の注目度）: 20.791968710071973
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal verification provides strong guarantees of software correctness, but its adoption is limited by the high cost of writing precise formal specifications. While recent large language models (LLMs) have shown strong capabilities in theorem proving and verified code generation, their true ability to generate program specifications remains unclear. Existing evaluations require either verifying implementation conformance or proving semantic equivalence between specifications, both of which are formidably difficult and may conflate proof difficulty with specification quality. To address this problem, we introduce Coins, a Rocq based evaluation framework that assesses specification quality by instantiating specifications under evaluation on trusted test cases and generating concrete proof obligations. This design aligns with the asymmetric nature of formal reasoning, where successful proofs provide reliable evidence while proof failures are inherently ambiguous. Using Coins, we conduct a large scale study on HumanEval with a curated set of human written Rocq specifications. Our results show that specification generation remains a formidable challenge, and that verification complexity can obscure genuine differences in specification quality. Overall, we find that accurate specification evaluation, rather than model scaling alone, is central to understanding the power of LLMs for specification synthesis, and that test case based formal reasoning offers a more faithful and discriminative measure of progress.
- Abstract（参考訳）: 形式検証は、ソフトウェアの正しさを強く保証するが、その採用は、正確な形式仕様を書くのに高いコストで制限される。
最近の大規模言語モデル(LLM)は、定理証明と検証コード生成において強力な能力を示しているが、プログラム仕様を生成する真の能力は、まだ不明である。
既存の評価では、実装の適合性を検証するか、仕様間の意味的等価性を証明する必要がある。
この問題に対処するために,信頼性のあるテストケース上で仕様をインスタンス化し,具体的な証明義務を生成することで仕様品質を評価する,Rocqベースの評価フレームワークであるCoinsを紹介した。
この設計は形式的推論の非対称的な性質と一致し、証明の失敗は本質的に曖昧である一方、証明が成功すると信頼できる証拠が得られる。
Coinsを用いて、我々は、人間の記述したRocq仕様のキュレートされたセットを用いて、HumanEvalに関する大規模な研究を行う。
以上の結果から, 仕様生成は依然として重大な課題であり, 検証の複雑さは仕様品質の真の相違を曖昧にする可能性があることが示唆された。
全体として、モデルスケーリングのみでなく、正確な仕様評価は、仕様合成のためのLLMのパワーを理解する中心であり、テストケースに基づく形式推論は、より忠実で差別的な進捗測定を提供する。
関連論文リスト
- ProofPulse: Interactive Proof Coverage Analysis for Dafny [47.23158426199152]
帰納的検証は、実装がその仕様を満たすことを保証しますが、成功した検証は仕様の品質を保証しません。
本稿では,3値の証明カバレッジモデルを用いて,仕様品質を診断するDafny用ツールであるProgrampulseを提案する。
論文 参考訳（メタデータ） (2026-08-31T14:00:31Z) - SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs [10.916179875278326]
我々は、形式的なコード合成をアトミックで再利用可能なスキルのライブラリに分解するフレームワークであるSKILLFORGEを紹介する。
検証駆動ハーネスはこれらのスキルを編成する。
Dafny仕様のペアに対する自然言語のキュレートされたベンチマークでは、SKILLFORGEは最先端のエージェントアプローチよりも大幅に優れている。
論文 参考訳（メタデータ） (2026-08-30T15:15:00Z) - TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability [59.079078796751496]
我々は,研究レベルの理論計算機科学(TCS)証明生成において,Large Language Models(LLMs)を評価するためのベンチマークであるTCS-Benchを紹介する。
TCS-Benchは、理論計算機科学の会場で発表された論文の定理証明タスクで構成されている。
論文 参考訳（メタデータ） (2026-08-10T12:36:16Z) - VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation [2.2194977808724405]
大規模言語モデルは自然言語から有用なコードを生成することができるが、その出力は正確性を保証することなく得られる。
検証可能なコード生成は、モデルに実行可能なコードだけでなく、正式な仕様やマシンチェック可能な証明を生成することを要求することによって、テストを越える道を提供する。
We present VeriContest, a benchmark of 946 competitive-playming problem from LeetCode and Codeforces for verible code generation in Rust with Verus。
論文 参考訳（メタデータ） (2026-05-08T23:25:05Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
本稿では,機械チェック可能な証明を通じて推論を評価するベンチマークスイートProofGridを紹介する。
ProofGridには、証明記述、証明チェック、証明マスキング、証明ギャップ埋めを含む15のタスクが含まれている。
タスクは最小の形式表記、特に短いプロンプトに適合するコンパクトな自然言語推論言語であるNDLで表現される。
論文 参考訳（メタデータ） (2026-04-07T01:19:41Z) - VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
自動JML仕様合成における古典的手法と急進的手法を比較した。
提案手法は,構造化された検証フィードバックを用いて,プロンプトを進化させることにより,合成品質をさらに向上させることができるかを検討する。
本稿では,検証誘導型エージェントフレームワークであるVeriActを提案する。
論文 参考訳（メタデータ） (2026-03-31T22:12:15Z) - Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。
多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。
自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
論文 参考訳（メタデータ） (2026-02-02T17:42:53Z) - VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code [25.916111156888235]
我々は,Large Language Models (LLM) の形式的検証のための新しいベンチマークを導入する。
筆者らのフレームワークは, 基調整合を定式化された基準, 等価スコアに置き換え, 生成された仕様やコードの品質を厳格に検証する。
以上の結果から,形式的検証可能なコードを生成することは,最先端のLLMにとって依然として大きな課題であることがわかった。
論文 参考訳（メタデータ） (2025-10-07T13:19:05Z) - VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。
LLM生成コードの正確性を保証することは依然として困難である。
検証可能なコード生成は、この制限に対処するための有望なパスを提供する。
論文 参考訳（メタデータ） (2025-05-29T06:12:52Z) - VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。
評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
論文 参考訳（メタデータ） (2025-05-25T19:00:52Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。