論文の概要: Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification

• arxiv url: http://arxiv.org/abs/2604.17010v1
• Date: Sat, 18 Apr 2026 14:43:00 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-21 21:52:52.287151
• Title: Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification
• Title（参考訳）: 形式検証による意味等価自己再生によるLLM符号推論の改善
• Authors: Antonio Valerio Miceli Barone, Poon Tsz Nok,
• Abstract要約: 本稿ではHaskellにおける意味的等価性のためのセルフプレイフレームワークを提案する。 我々は, 発電機と評価器間の対向訓練を指導するために, 形式的検証を用いる。 トレーニングパイプライン全体とデータセットはそれぞれGitHubとHugging Faceで公開されている。
• 参考スコア（独自算出の注目度）: 2.3081405020721975
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce a self-play framework for semantic equivalence in Haskell, utilizing formal verification to guide adversarial training between a generator and an evaluator. The framework leverages Liquid Haskell proofs for validating equivalence and execution-based counterexamples for inequivalence, organized via a difficulty-aware curriculum. To facilitate this, we release \textbf{OpInstruct-HSx}, a synthetic dataset of $\approx$28k validated Haskell programs. Empirical experiments show that our evaluator transfers effectively to downstream tasks, achieving up to 13.3pp accuracy gain on EquiBench and consistent gains on PySecDB. Ablation studies on the SEQ-SINQ regimes indicate that while inequivalence supervision provides data volume, equivalence proofs are uniquely responsible for the model's reasoning capabilities. The entire training pipeline and dataset are publicly released on GitHub and Hugging Face respectively.
• Abstract（参考訳）: 本稿では,Haskellにおける意味的等価性のためのセルフプレイフレームワークを提案する。 このフレームワークはLiquid Haskellの証明を利用して、不等式に対する等価性と実行ベースの反例を検証する。 これを容易にするために、$$\approx$28kのHaskellプログラムの合成データセットである \textbf{OpInstruct-HSx} をリリースする。 EquiBenchでは最大13.3ppの精度向上,PySecDBでは一貫したゲインを実現している。 SEQ-SINQ体制に関するアブレーション研究は、等価性監視がデータボリュームを提供する一方で、同値証明がモデルの推論能力に固有の責任を負っていることを示している。 トレーニングパイプライン全体とデータセットはそれぞれGitHubとHugging Faceで公開されている。

関連論文リスト

• Verify Implementation Equivalence of Large Models [9.854606980804016]
  本稿では,大規模モデル実装のグラフ上での実装等価性をチェックするためのフレームワークであるEmergeを紹介する。 手動でルールを書く代わりに、Emergeは2つの実装をEグラフで表現し、実行値から候補関係を推測し、要求に応じて書き直しルールを合成する。
  論文  参考訳（メタデータ） (2026-03-23T11:39:56Z)
• SWE-QA-Pro: A Representative Benchmark and Scalable Training Recipe for Repository-Level Code Understanding [41.98672557723593]
  SWEQA-Proは,多種多様な長期リポジトリと実行可能な環境から構築されたベンチマークである。 さらに,2段階のトレーニングレシピであるSupervised Fine-Tuning(SFT)とReinforcement Learning from AI Feedback(RLAIF)という,スケーラブルな合成データパイプラインを提案する。 SWE-QA-ProのGPT-4oを2.3ポイント超え、最先端モデルとのギャップを大幅に狭める。
  論文  参考訳（メタデータ） (2026-03-17T05:12:48Z)
• Reasoning Core: A Scalable Procedural Data Generation Suite for Symbolic Pre-training and Post-Training [2.62112541805429]
  Reasoning Coreは、コア形式ドメイン間で検証可能なシンボリック推論データを手続き的に生成するスケーラブルなスイートである。 各タスクは厳密な検証のための外部解決器と組み合わせられ、カリキュラム設計のための継続的な難易度制御が認められる。 実験によると、Reasoning Coreのデータを事前トレーニングに混ぜることによって、下流の推論が改善され、保存されたり、わずかに改善された言語モデリングの品質が向上する。
  論文  参考訳（メタデータ） (2026-03-02T18:59:29Z)
• InFi-Check: Interpretable and Fine-Grained Fact-Checking of LLMs [48.98720183285795]
  InFi-Checkは、大規模な言語モデルの解釈ときめ細かい事実チェックのためのフレームワークである。 InFi-Checkerは、サポートエビデンスを提供し、きめ細かいエラータイプを分類し、修正と共に正当化を生成する。 実験の結果,InFi-CheckerはInFi-Check-FGの最先端性能を実現することがわかった。
  論文  参考訳（メタデータ） (2026-01-10T20:00:17Z)
• Refinement Provenance Inference: Detecting LLM-Refined Training Prompts from Model Behavior [58.751981587234916]
  本稿では,Refinement Provenance Inference (RPI)監査タスクをRefinement Provenance Inference (RPI)として定式化する。 本稿では,ロジットレベルの信号で教師が強制する可能性機能を融合させるロジットベースのフレームワークであるReProを提案する。 トレーニング中、ReProはシャドウファインチューニングを通じて転送可能な表現を学び、訓練データアクセスなしで、見えない犠牲者の証明を推測するために軽量のリニアヘッドを使用する。
  論文  参考訳（メタデータ） (2026-01-05T10:16:41Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.26763498831034044]
  組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。 LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。 我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
  論文  参考訳（メタデータ） (2025-04-23T18:04:38Z)
• 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)
• Log Probabilities Are a Reliable Estimate of Semantic Plausibility in Base and Instruction-Tuned Language Models [50.15455336684986]
  意味的妥当性を評価するため,LogProbsの有効性と基本的なプロンプトを評価した。 LogProbsは、直接ゼロショットプロンプトよりも、より信頼性の高いセマンティックな妥当性を提供する。 我々は,プロンプトベースの評価の時代においても,LogProbsは意味的妥当性の有用な指標である,と結論付けた。
  論文  参考訳（メタデータ） (2024-03-21T22:08:44Z)

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

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