論文の概要: TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation

• arxiv url: http://arxiv.org/abs/2606.06133v1
• Date: Thu, 04 Jun 2026 13:17:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-05 22:39:44.80515
• Title: TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
• Title（参考訳）: TLA-Prover: 優先最適化低ランク適応による検証可能なTLA+仕様合成
• Authors: Eric Spencer, Arslan Bisharat, Brian Ortiz, Khushboo Bhadauria, TaiNing Wang, George K. Thiruvathukal, Konstantin Laufer, Mohammed Abuhamad,
• Abstract要約: TLA+は、分散システムと安全クリティカルプロトコルを検証するための正式な仕様言語である。 大規模言語モデル(LLM)は、意味的な理由でTLCモデルチェッカーをフェールさせるTLA+仕様をしばしば生成する。 TLA+仕様合成のための20ビリオンパラメータモデルであるTLA-Proverを提案する。
• 参考スコア（独自算出の注目度）: 1.550528651800741
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: TLA+ is a formal specification language for verifying distributed systems and safety-critical protocols. Large language models (LLMs) frequently produce TLA+ specifications that fail the TLC model checker for semantic reasons. Across 25 LLMs, the best public baseline is 26.6% syntactic parse and 8.6% semantic model-check. We present TLA-Prover, a 20-billion-parameter model for TLA+ specification synthesis. Training combines supervised fine-tuning (SFT) on verified examples with repair-based group-relative policy optimization (GRPO). In the GRPO stage, the model learns to fix its own rejected specifications. We also train a direct preference optimization (DPO) variant from the same SFT checkpoint as an ablation. TLC provides the reward signal directly, with no learned reward model. Four tiers grade each output: Bronze (parses), Silver (no warnings), Gold (passes TLC), and Diamond. To reach Diamond, the model's correctness property is automatically altered in a small way; TLC must then detect a violation. If TLC still passes, the property was always-true and contributes nothing; the output fails Diamond. TLA-Prover reaches 9/30 (i.e. pass@1 = 30%) at both Gold and Diamond on a held-out 30-problem benchmark. This is roughly 3.5x the 8.6% untuned baseline. The DPO variant reaches 20% at Diamond. Gold and Diamond coincide at every checkpoint; this prevents the trivial-property failure mode.
• Abstract（参考訳）: TLA+は、分散システムと安全クリティカルプロトコルを検証するための正式な仕様言語である。 大規模言語モデル(LLM)は、意味的な理由でTLCモデルチェッカーをフェールさせるTLA+仕様をしばしば生成する。 25 LLMで最高の公開ベースラインは26.6%の構文解析と8.6%のセマンティックモデルチェックである。 TLA+仕様合成のための20ビリオンパラメータモデルであるTLA-Proverを提案する。 トレーニングは、教師付き微調整(SFT)と修復ベースのグループ相対ポリシー最適化(GRPO)を組み合わせる。 GRPOの段階では、モデルは独自の拒否された仕様を修正することを学ぶ。 また、同じSFTチェックポイントから直接選好最適化(DPO)の変種をアブレーションとして訓練する。 TLCは、学習した報酬モデルなしで、報酬信号を直接提供する。 出力は青銅(パース)、銀(警告なし)、金(TLC通過)、ダイヤモンドの4段階である。 ダイアモンドに到達するためには、モデルの正確性は小さな方法で自動的に変更され、TLCは違反を検出する必要がある。 TLCがまだパスしている場合、そのプロパティは常に真実であり、何も貢献しない。 TLA-Proverは30プロブレムのベンチマークでゴールドとダイアモンドの両方で9/30に達する(pass@1 = 30%)。 これは、修正されていないベースラインの8.6%の3.5倍である。 DPOの変種はダイアモンドで20%に達する。 金とダイヤモンドはすべてのチェックポイントで一致します。

関連論文リスト

• Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation [1.550528651800741]
  TLA+はAmazonやMicrosoftなどの企業での工業的検証をサポートしているが、自然言語から正しいTLA+仕様を書くには時間と専門知識が必要である。 本稿では,LLMをベースとしたTLA+仕様合成を自然言語から初めて体系的に評価する。
  論文  参考訳（メタデータ） (2026-06-04T07:22:01Z)
• Distributional Energy-Based Models for Uncertainty-Aware Structured LLM Reasoning [40.342912574072024]
  大規模言語モデルは、旅行計画やコードソリューションのような構造化されたアウトプットを生成する。 個々の推論ステップは正しく見えるが、アウトプット全体が予算に違反したり、テストケースに失敗したり、あるいは以前の推論に矛盾することがある。 構造化LCM出力の検証のための決定論的解析制約付き学習品質スコアラを提案する。
  論文  参考訳（メタデータ） (2026-05-15T17:08:27Z)
• COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery [0.0]
  COBALT-TLAは、TLC(TLA+モデルチェッカー)とLCMをペアリングする神経象徴的検証ループである。 我々は,Nomad $190Mエクスプロイトの忠実なモデルを含む,3つのクロスチェーンブリッジターゲットに対してシステムを評価する。
  論文  参考訳（メタデータ） (2026-04-14T00:56:58Z)
• Self-Calibrating Language Models via Test-Time Discriminative Distillation [18.46710400838861]
  大規模言語モデル(LLM)は、しばしば間違って答える質問に対して体系的に過度に信頼されている。 我々は、テスト時間トレーニング(TTT)パイプラインである$textbfSECL$ ($textbfSE$lf-$textbfC$alibrating $textbfL$anguage Modelsを紹介します。
  論文  参考訳（メタデータ） (2026-03-18T13:28:50Z)
• Valid Stopping for LLM Generation via Empirical Dynamic Formal Lift [6.908972852063454]
  シーケンシャルEDFLは、シーケンシャルベースラインに対して22～28%生成を減少させる。 EDFLは第1段階のフィルタとして機能し、検証負荷を83%削減する。
  論文  参考訳（メタデータ） (2025-10-07T21:28:53Z)
• Large Language Diffusion Models [93.26422905620008]
  大規模言語モデル(LLM)は自己回帰モデル(ARM)に依存していると考えられている。 我々は,事前学習および教師付き微調整パラダイムの下で,ゼロから学習した拡散モデルであるLLaDAを紹介する。 一般的なタスクや数学、コードなどに関する広範なベンチマークを通じて、LLaDAは強力なスケーラビリティを示し、自己構築されたARMベースラインと互換性のあるパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2025-02-14T08:23:51Z)
• Language Models are Hidden Reasoners: Unlocking Latent Reasoning Capabilities via Self-Rewarding [74.31981011985681]
  大きな言語モデル(LLM)は印象的な機能を示しているが、それでも複数のステップを必要とする複雑な推論タスクに苦戦している。 LaTRO(LaTent Reasoning Optimization)は、潜在分布からのサンプリングとして推論を定式化するためのフレームワークである。 複数のモデルアーキテクチャを用いて、GSM8KおよびARC-Challengeデータセットの実験を通してLaTROを検証する。
  論文  参考訳（メタデータ） (2024-11-06T22:02:30Z)
• Self-Play Preference Optimization for Language Model Alignment [75.83359213697854]
  近年の進歩は、嗜好の確率で直接作業することで、人間の嗜好をより正確に反映できることを示している。 本稿では,言語モデルアライメントのためのセルフプレイ方式を提案する。 我々の手法はSPPO(Self-Play Preference Optimization)と呼ばれ、繰り返しポリシー更新を利用してナッシュ均衡を確実に近似する。
  論文  参考訳（メタデータ） (2024-05-01T17:59:20Z)

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

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