論文の概要: Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

• arxiv url: http://arxiv.org/abs/2606.05792v1
• Date: Thu, 04 Jun 2026 07:22:01 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-05 22:39:44.617683
• Title: Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation
• Title（参考訳）: LLMは正しいTLA+仕様を書けるか? : 自然言語からTLA+生成の評価
• Authors: Arslan Bisharat, Brian Ortiz, Eric Spencer, Khushboo Bhadauria, TaiNing Wang, George K. Thiruvathukal, Konstantin Laufer, Mohammed Abuhamad,
• Abstract要約: TLA+はAmazonやMicrosoftなどの企業での工業的検証をサポートしているが、自然言語から正しいTLA+仕様を書くには時間と専門知識が必要である。 本稿では,LLMをベースとしたTLA+仕様合成を自然言語から初めて体系的に評価する。
• 参考スコア（独自算出の注目度）: 1.550528651800741
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: TLA+ has supported industrial verification at companies such as Amazon and Microsoft, yet writing correct TLA+ specifications from natural language still requires time and expertise, which limits adoption. LLMs show promise, but no prior study measures whether they produce semantically correct TLA+ specifications from natural language. This paper presents the first systematic evaluation of LLM-based TLA+ specification synthesis from natural language. Our study evaluates 30 LLMs across eight families on a curated dataset of 205 TLA+ specifications: 25 open-weight models across four prompting strategies (2,600 runs) and 5 proprietary models under few-shot prompting (130 runs), all validated by the SANY parser and TLC model checker. LLMs achieve up to 26.6% syntactic correctness but only 8.6% semantic correctness, with successes exclusive to progressive prompting. Results show that model size does not predict quality, e.g., DeepSeek r1:8b outperforms its 70B variant across all strategies, which suggests the importance of reasoning alignment for formal languages. Code-specialized models consistently underperform due to negative transfer from mainstream language training. We identify five recurring hallucination categories, all traceable to specific training data biases. These results suggest that current LLMs do not generate reliable TLA+ specifications without expert oversight. We release the evaluation framework, code, and dataset to support reproducibility and future research.
• Abstract（参考訳）: TLA+はAmazonやMicrosoftなどの企業での産業的検証をサポートしているが、自然言語から正しいTLA+仕様を書くには時間と専門知識が必要であるため、採用が制限されている。 LLMは将来性を示すが、自然言語から意味論的に正しいTLA+仕様を作成するかどうかの事前の研究は行われていない。 本稿では,LLMをベースとしたTLA+仕様合成を自然言語から初めて体系的に評価する。 本研究は,4つのプロンプト戦略にまたがる25のオープンウェイトモデル (2,600ラン) と5つのプロプライエタリモデル (130ラン) を,SANYパーサとTLCモデルチェッカーで検証した8つのファミリーにまたがる30のLLMを評価した。 LLMは最大26.6%の構文的正当性を達成するが、意味的正当性はわずか8.6%であり、成功はプログレッシブプロンプトのみである。 結果から,モデルサイズが品質を予測できないこと,例えばDeepSeek r1:8bは,すべての戦略で70Bを上回り,形式言語における推論アライメントの重要性が示唆された。 コード特化モデルは、主流言語のトレーニングからの否定的な移行により、一貫してパフォーマンスが低下する。 特定のトレーニングデータバイアスに追従可能な5つの幻覚カテゴリーを同定した。 これらの結果から,現在のLLMは専門家の監視なしに信頼性の高いTLA+仕様を作成できないことが示唆された。 再現性と今後の研究を支援するための評価フレームワーク、コード、データセットをリリースする。

関連論文リスト

• TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation [1.550528651800741]
  TLA+は、分散システムと安全クリティカルプロトコルを検証するための正式な仕様言語である。 大規模言語モデル(LLM)は、意味的な理由でTLCモデルチェッカーをフェールさせるTLA+仕様をしばしば生成する。 TLA+仕様合成のための20ビリオンパラメータモデルであるTLA-Proverを提案する。
  論文  参考訳（メタデータ） (2026-06-04T13:17:06Z)
• An Empirical Study of Many-to-Many Summarization with Large Language Models [82.10000188179168]
  大規模言語モデル(LLM)は強い多言語能力を示しており、実アプリケーションでM2MS(Multi-to-Many summarization)を実行する可能性を秘めている。 本研究は,LLMのM2MS能力に関する系統的研究である。
  論文  参考訳（メタデータ） (2025-05-19T11:18:54Z)
• Idiosyncrasies in Large Language Models [54.26923012617675]
  大規模言語モデル(LLM)における慣用句の公開と研究 LLM生成テキストへの微調整テキスト埋め込みモデルにより,優れた分類精度が得られることがわかった。 我々はLLMを審査員として利用し、各モデルの慣用句の詳細かつオープンな記述を生成する。
  論文  参考訳（メタデータ） (2025-02-17T18:59:02Z)
• What do Large Language Models Need for Machine Translation Evaluation? [12.42394213466485]
  大規模言語モデル(LLM)は、微調整された多言語事前訓練言語モデルに匹敵する結果が得られる。 本稿では,LLMの機械翻訳品質を評価するために,ソース,参照,翻訳エラー,ガイドラインなどの翻訳情報が必要であるかを検討する。
  論文  参考訳（メタデータ） (2024-10-04T09:50:45Z)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
  論文  参考訳（メタデータ） (2024-07-03T15:36:18Z)
• Native Language Identification with Large Language Models [60.80452362519818]
  我々はGPTモデルがNLI分類に熟練していることを示し、GPT-4は0ショット設定でベンチマーク11テストセットで91.7%の新たなパフォーマンス記録を樹立した。 また、従来の完全教師付き設定とは異なり、LLMは既知のクラスに制限されずにNLIを実行できることを示す。
  論文  参考訳（メタデータ） (2023-12-13T00:52:15Z)
• Statistical Knowledge Assessment for Large Language Models [79.07989821512128]
  ファクトイドの問題に関する様々なプロンプトを考慮すれば、大きな言語モデル(LLM)は事実的に正しい答えを確実に生成できるだろうか? LLMの事実知識を評価する統計的手法であるKaRRを提案する。 この結果から,同じバックボーン構造を持つLLMの知識はスケーリング法則に則っており,命令追従データに基づくチューニングは,実際に正しいテキストを確実に生成するモデルの能力を損なう場合があることがわかった。
  論文  参考訳（メタデータ） (2023-05-17T18:54:37Z)
• Multilingual Machine Translation with Large Language Models: Empirical Results and Analysis [103.89753784762445]
  大規模言語モデル(LLM)は多言語機械翻訳(MMT)の処理において顕著な可能性を示した。 本稿では, MMT における LLM の利点と課題を体系的に検討する。 また,ChatGPTとGPT-4を含む8つのLLMを徹底的に評価した。
  論文  参考訳（メタデータ） (2023-04-10T15:51:30Z)

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

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