論文の概要: TLA$^{+}$-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation
- arxiv url: http://arxiv.org/abs/2607.23425v1
- Date: Sun, 26 Jul 2026 02:49:56 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-28 22:34:15.098536
- Title: TLA$^{+}$-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation
- Title（参考訳）: TLA$^{+}$-Bench:TLA+仕様生成のためのベンチマークとデータセット
- Abstract要約: TLA$+$-Benchは、実行毎にグレードするデータセットとベンチマークである。
データセットには、13のパブリックリポジトリから403のモデルチェックゴールドと897のパースのみの銀仕様がある。
- 参考スコア（独自算出の注目度）: 1.4044130719425245
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models increasingly write TLA$^{+}$ formal specifications from natural-language descriptions, but progress is hard to measure: existing resources grade by resemblance to a reference or by whether the output parses, neither of which shows correctness. We present TLA$^{+}$-Bench, a dataset and benchmark that grades by execution. Every gold specification ships a configuration the TLA$^{+}$ model checker runs over the full reachable state space, deciding exactly whether the specification holds the properties that configuration names. The dataset holds 403 model-checked gold and 897 parse-only silver specifications from 13 public repositories, subsumes prior TLA$^{+}$ generation data, and carries four model-written descriptions in two styles from two providers, with difficulty and category labels. Our main finding is about measurement itself: an exact oracle gives not one correctness number but a range. Varying only the grading choices earlier benchmarks leave unstated, on one fixed set of model outputs, the correct rate moves sixfold, from 10.0\% to 1.7\%; adding the interface-supply choice, where the model is told the configuration's names, widens the range to elevenfold, from 18.7\% to 1.7\%. We call this range the correctness envelope and measure each of its bounds. The findings inside it are stable. Every model writes valid TLA$^{+}$ far more often than correct TLA$^{+}$: the strongest is correct 16\% of the time by default and 26\% when given the interface names, open models at most 1\%, and correctness falls sharply with difficulty.
- Abstract（参考訳）: 大規模な言語モデルでは、TLA$^{+}$形式仕様を自然言語の記述から記述することが多いが、既存のリソースが参照に類似しているか、あるいは出力がパースするかどうかで評価することは難しい。
TLA$^{+}$-Benchは、実行によってグレードするデータセットとベンチマークである。
すべてのゴールド仕様は、TLA$^{+}$モデルチェッカーをフルリーチ可能な状態空間上で実行し、仕様が設定名を持つプロパティを持っているかどうかを正確に決定する。
このデータセットは、13のパブリックリポジトリから403のモデルチェックゴールドと897のパースオンリーの銀仕様を持ち、TLA$^{+}$生成データを仮定し、2つのプロバイダからの2つのスタイルで4つのモデル記述を格納する。
私たちの主な発見は測定そのものに関するもので、正確なオラクルは1つの正確性番号ではなく、範囲を与えます。
以前のベンチマークのグレーディング選択のみを定式化せずに残し、モデル出力の固定セットでは、正しいレートが10.0\%から1.7\%に6倍に移動し、インターフェース供給の選択を追加し、モデルが設定の名前を告げられ、範囲を18.7\%から1.7\%に拡大する。
我々はこの範囲を正当性エンベロープと呼び、それぞれの境界を測る。
内部の発見は安定している。
すべてのモデルが有効な TLA$^{+}$ を正しい TLA$^{+}$ よりもはるかに頻繁に書く: 最強はデフォルト値の 16 % で、インターフェース名、最大 1 % のオープンモデルが与えられたとき 26 % であり、正確性は困難で急激に低下する。
関連論文リスト
- IndicQE-APE: A Benchmark for Quality Estimation and Automatic Post-Editing for Indic Languages [77.88427845181154]
我々はWMT 2020-2024の共有タスクの系統を、英語のリソースを拡張してインディクシーに集約する:9つの方向対に対して126,754ドルのインスタンス。
セグメントレベルのQEでは,LSMが6つ,COMETが3つ,APEでは3つのシステムをベンチマークした。
論文 参考訳（メタデータ） (2026-08-17T09:50:52Z) - Context-Aware Distillation and Ablation for Text2DSL [78.29352305480285]
我々は、コンテクスト対応蒸留により、プロンプトのみの合成生成を置き換える。
教師の大きな言語モデルは、明示的に定義された構造化コンテキストの下で機能する。
これは、検証されたポルキットベンチコーパスを4,204対から10,073対にスケールする。
論文 参考訳（メタデータ） (2026-06-21T16:27:24Z) - 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) - 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) - Models Can Model, But Can't Bind: Structured Grounding in Text-to-Optimization [54.749573452394664]
定式化自体が単純である場合でも、インスタンスデータが大きくなるにつれて精度が低下する。
我々は, 数値データを構造化ファイルに外部化する単純な推論時アプローチであるBINDを用いて, モデルがプロンプトプロンプトからではなく, データをバインドする。
我々は,モデルのみをバインディングのみに微調整することで仮説を検証し,3つの構造的に異なる最適化カテゴリにおいて,エンドツーエンドのSFTおよびRLよりも優れていることを示す。
論文 参考訳（メタデータ） (2026-05-20T21:25:41Z) - DocAtlas: Multilingual Document Understanding Across 80+ Languages [58.715440331861295]
本稿では,82言語を対象とした高忠実度OCRデータセットとベンチマークを構築するフレームワークDocAtlasを紹介する。
我々のデュアルパイプライン、ネイティブDOCX文書の微分レンダリング、左右スクリプトの合成ベース生成は正確な構造アノテーションを生成する。
論文 参考訳（メタデータ） (2026-05-12T18:09:38Z) - Semantic Layers for Reliable LLM-Powered Data Analytics: A Paired Benchmark of Accuracy and Hallucination Across Three Frontier Models [0.0]
解析データベースの自然言語クエリ用にデプロイされたLLMは、2つの障害に悩まされる。
ClickHouseのCleaned Contoso Retailデータセットに対して,100の自然言語質問に対して,3つのフロンティアLSMをベンチマークした。
論文 参考訳（メタデータ） (2026-04-28T02:53:23Z) - CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
$rm Csmall LEVER$は、リーンにおけるエンドツーエンドのコード生成のための161の問題を、高品質でキュレートしたベンチマークである。
それぞれの問題は、(1)堅実な仕様と一致する仕様を生成するタスク、(2)この仕様を確実に満足するリーン実装を生成するタスクで構成されています。
論文 参考訳（メタデータ） (2025-05-20T05:15:47Z) - Do Large Language Models Truly Grasp Addition? A Rule-Focused Diagnostic Using Two-Integer Arithmetic [21.014229380679975]
大規模言語モデル(LLM)は高度な数学のベンチマークでは印象的な結果を得るが、基本的な算術的なタスクでは失敗することがある。
基本演算規則を真に把握したのか、それとも単にパターンマッチングに依存しているのかを考察する。
モデルでは高い数値精度を達成できるが、これらの診断は体系的に失敗する。
論文 参考訳（メタデータ） (2025-04-07T16:57:10Z) - Reasoning Robustness of LLMs to Adversarial Typographical Errors [49.99118660264703]
大規模言語モデル(LLM)は、Chain-of-Thought(CoT)プロンプトを使用した推論において、印象的な機能を示している。
本研究では,LLMのタイポグラフィ的誤りに対するロバスト性について検討する。
我々は,クエリに重要な単語の型を反復的にサンプリングし,攻撃に成功しそうな編集を選択する,Adversarial Typo Attack(texttATA$)アルゴリズムを設計する。
論文 参考訳（メタデータ） (2024-11-08T05:54:05Z) - Weak-to-Strong Search: Align Large Language Models via Searching over Small Language Models [22.425339110551743]
我々は,テストタイムの欲求検索として,大規模言語モデルのアライメントをフレーミングする,$textitweak-to-strong検索を導入する。
制御された知覚生成と要約では、チューニングされていない$textttgpt2$sを使用して、追加のトレーニングなしで大規模モデルのアライメントを改善する。
より難しい命令追従ベンチマークでは、市販の小型モデルの再利用により、ホワイトボックスモデルとブラックボックスモデルの両方の長制御された勝利率を改善することが示されている。
論文 参考訳（メタデータ） (2024-05-29T16:55:32Z) - RALL-E: Robust Codec Language Modeling with Chain-of-Thought Prompting for Text-to-Speech Synthesis [84.57932472551889]
RALL-Eは、音声合成のための堅牢な言語モデリング手法である。
RALL-Eは、ゼロショットTSのWERを、それぞれ5.6%$(リランクなし)から2.5%$と1.0%$に改善した。
論文 参考訳（メタデータ） (2024-04-04T05:15:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。