論文の概要: Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny

• arxiv url: http://arxiv.org/abs/2507.16331v2
• Date: Fri, 25 Jul 2025 08:30:10 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-28 12:12:30.211421
• Title: Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny
• Title（参考訳）: Re:Form -- LLMにおけるRLによるスケーラブルな形式的ソフトウェア検証における人間の優先順位の低減 - Dafnyに関する予備的研究
• Authors: Chuanhao Yan, Fengdi Che, Xuhan Huang, Xu Xu, Xin Li, Yizhi Li, Xingwei Qu, Jingzhe Shi, Zhuangzhuang He, Chenghua Lin, Yaodong Yang, Binhang Yuan, Hang Zhao, Yu Qiao, Bowen Zhou, Jie Fu,
• Abstract要約: 強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
• 参考スコア（独自算出の注目度）: 68.00108157244952
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Existing informal language-based (e.g., human language) Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes, which provide crucial training signals, are neither reliable nor scalable. In fact, the prevalent large proprietary models could hardly generate verifiable programs. A promising yet largely uncharted alternative is formal language-based reasoning. Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes. This capability is pivotal for achieving large-scale, reliable formal software verification. It is a common practice to employ human-annotated chain-of-thought and other human priors to induce the reasoning and coding capabilities of LLMs. Unfortunately, it becomes unacceptably all-consuming to provide such priors for supervising complex programming tasks. In this work, we systematically explore ways to reduce human priors with the formal language, Dafny, as the main environment for our pilot study. Our pipeline mainly relies on introducing an automatic and scalable data curation pipeline, and careful RL designs integrated with feedback from the formal language verifier. We introduce DafnyComp, a benchmark of compositional formal programs with auto-formalized specifications for specification reasoning. Our supervised fine-tuning (SFT) stage enables even small models (e.g., 0.5B) to generate syntactically valid and verifiable Dafny code, surpassing proprietary models. RL with regularization further improves performance, achieving stronger generalization to out-of-domain tasks and outperforming all strong baselines on the challenging DafnyComp benchmark.
• Abstract（参考訳）: 既存の非公式言語ベース(例えば、人間言語) 強化学習(RL)で訓練された大規模言語モデル(LLM)は、重大な課題に直面している。 実際、広く普及している大規模プロプライエタリモデルは、検証可能なプログラムをほとんど生成できなかった。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。 この能力は、大規模で信頼性の高いフォーマルなソフトウェア検証を実現する上で重要である。 LLMの推論能力とコーディング能力を誘導するために、人間の注釈付きチェーンや、他の人間の先駆的手法を用いるのが一般的である。 残念なことに、複雑なプログラミングタスクを監督するためにそのような先入観を提供するのに、受け入れがたいほど時間がかかります。 本研究では,本研究の主な環境として,フォーマルな言語であるDafnyによる人的先行性を減らす方法を体系的に検討する。 我々のパイプラインは主に、自動でスケーラブルなデータキュレーションパイプラインの導入と、形式言語検証器からのフィードバックと統合された注意深いRL設計に依存しています。 本稿では,DafnyCompについて紹介する。DafnyCompは,仕様推論のための自動形式化仕様を備えた構成形式プログラムのベンチマークである。 教師付きファインチューニング(SFT)ステージでは、たとえ小さなモデル(例:0.5B)であっても、構文的に有効で検証可能なDafnyコードを生成することができ、プロプライエタリなモデルを上回る。 正規化によるRLは、パフォーマンスをさらに向上し、ドメイン外タスクへのより強力な一般化を実現し、挑戦的なDafnyCompベンチマークにおいて、すべての強力なベースラインを上回ります。

関連論文リスト

• Do Large Language Models Excel in Complex Logical Reasoning with Formal Language? [20.53475791645822]
  大規模言語モデル(LLM)は、複雑な論理的推論タスクにおいてブレークスルーのパフォーマンスを達成することが示されている。 本稿では,形式言語を用いた論理的推論問題に対して,LLMを包括的に評価することを目的とする。
  論文  参考訳（メタデータ） (2025-05-22T17:57:23Z)
• From Reasoning to Code: GRPO Optimization for Underrepresented Languages [0.7864304771129751]
  本稿では,Qwen 2.5モデルの小型コードバージョンとグループ相対ポリシー最適化を組み合わせた一般化可能なアプローチを提案する。 推論によるフィードバックを直接強化学習ループに統合することにより、論理的に一貫性があり、構文的に正確なコードを生成する。
  論文  参考訳（メタデータ） (2025-05-20T11:28:48Z)
• The First Few Tokens Are All You Need: An Efficient and Effective Unsupervised Prefix Fine-Tuning Method for Reasoning Models [69.798277882245]
  大規模言語モデルの推論効率を向上させるために,Unsupervised Prefix Fine-Tuning (UPFT)を導入した。 UPFTはラベル付きデータや徹底的なサンプリングの必要性を取り除く。 実験の結果,UPFTは教師付き手法の性能と一致していることがわかった。
  論文  参考訳（メタデータ） (2025-03-04T18:56:03Z)
• Exploring RL-based LLM Training for Formal Language Tasks with Programmed Rewards [49.7719149179179]
  本稿では,PPOを用いた強化学習(RL)の実現可能性について検討する。 我々は,生成した出力の質を自動的に評価するために,明示的な報酬関数をプログラムできるプログラミングなどの形式言語で表されるタスクに焦点をあてる。 以上の結果から,2つの形式言語タスクに対する純粋なRLベースのトレーニングは困難であり,単純な算術タスクにおいても成功は限られていることがわかった。
  論文  参考訳（メタデータ） (2024-10-22T15:59:58Z)
• Boosting the Capabilities of Compact Models in Low-Data Contexts with Large Language Models and Retrieval-Augmented Generation [2.9921619703037274]
  本稿では,形態素解析の言語タスクにおいて,より小さなモデルの出力を補正するために,大言語モデル(LLM)を基盤とした検索拡張生成(RAG)フレームワークを提案する。 データ不足や訓練可能なパラメータの不足を補うために,言語情報を活用するとともに,LLMを通して解釈・蒸留された記述文法からの入力を許容する。 コンパクトなRAG支援モデルがデータスカース設定に極めて有効であることを示し、このタスクとターゲット言語に対する新しい最先端技術を実現する。
  論文  参考訳（メタデータ） (2024-10-01T04:20:14Z)
• Reference Trustable Decoding: A Training-Free Augmentation Paradigm for Large Language Models [79.41139393080736]
  大規模言語モデル(LLM)は急速に進歩し、印象的な機能を示している。 In-Context Learning (ICL) など。 効率的なファインチューニング(PEFT)は、現在2つの主要な拡張方法である。 下流タスクへのLLM。 我々は、モデルが微調整なしで新しいタスクに迅速に適応できるパラダイムである参照信頼復号(RTD)を提案する。
  論文  参考訳（メタデータ） (2024-09-30T10:48:20Z)
• Generative Verifiers: Reward Modeling as Next-Token Prediction [29.543787728397643]
  本研究では,ユビキタスな次世代予測目標を用いて,検証とソリューション生成を併用したトレーニング検証手法を提案する。 標準検証器と比較して、そのような生成検証器(genRM)はLLMのいくつかの利点の恩恵を受けることができる。 我々は、MATHで28%$rightarrow$44.6%、MMLU抽象代数学で37.9%$rightarrow$53.5%の改善を観察する。
  論文  参考訳（メタデータ） (2024-08-27T17:57:45Z)
• Accelerating Large Language Model Inference with Self-Supervised Early Exits [0.0]
  本稿では,大規模・事前学習型言語モデル(LLM)における推論を高速化する新しい手法を提案する。 本稿では,既存の変圧器層上に早期出口「頭部」を統合し,信頼度基準に基づく条件付き項化を容易にすることを提案する。
  論文  参考訳（メタデータ） (2024-07-30T07:58:28Z)
• Alice in Wonderland: Simple Tasks Showing Complete Reasoning Breakdown in State-Of-the-Art Large Language Models [13.532180752491954]
  大規模言語モデル(LLM)は、しばしばスケーリング法則に従う強力な一般化を持つ基礎モデルの例として記述される。 ここでは、強い関数を主張する全てのSOTAモデルの一般化と基本的推論の劇的な分解を示す。 また、間違った解法において強い過信感を観察し、妥当な音響的説明のような折り畳みの形で表現する。
  論文  参考訳（メタデータ） (2024-06-04T07:43:33Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。 このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。 LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
  論文  参考訳（メタデータ） (2023-11-29T08:29:54Z)
• Leap-Of-Thought: Teaching Pre-Trained Models to Systematically Reason Over Implicit Knowledge [96.92252296244233]
  大規模な事前学習言語モデル(LM)は推論能力を得るが、制御は困難である。 本研究では,暗黙的,事前学習された知識と明示的な自然言語文を併用して,体系的推論を確実に行うことができることを示す。 我々の研究は、シンプルな自然言語文を追加することで、モデルを簡単に修正できるユーザと対話することで、常に改善されるオープンドメインシステムへの道を開く。
  論文  参考訳（メタデータ） (2020-06-11T17:02:20Z)

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

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