論文の概要: SERIAL-7: Deriving, Realizing, and Preserving Machine-Verifiable Outputs Across Representations
- arxiv url: http://arxiv.org/abs/2610.41308v1
- Date: Fri, 30 Oct 2026 06:15:59 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-11-02 22:05:31.629571
- Title: SERIAL-7: Deriving, Realizing, and Preserving Machine-Verifiable Outputs Across Representations
- Title（参考訳）: SERIAL-7: 表現全体にわたるマシン検証アウトプットの導出、実現、保存
- Abstract要約: SERIAL-7は、7つの表現にまたがる機械検証可能な生成のための韓国語によるベンチマークである。
信頼性のある構造化生成には、表現間でアーティファクトがどのように実現され、保存されるかを明確にし、実行可能な検証が必要であることを示す。
- 参考スコア（独自算出の注目度）: 4.45333508491417
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Large language models increasingly generate structured outputs consumed by programs and downstream systems, where semantic correctness alone does not guarantee reliable execution. We introduce SERIAL-7, a Korean-English benchmark built around an executable verification framework for machine-verifiable generation across seven representations. Using 177 validated canonical artifacts, SERIAL-7 separates semantic derivation (Derive), constrained artifact generation (Realize), and cross-representation preservation (Preserve). Its 43 atomic representation constraints are paired with executable checks over format, structure, and task-specific semantics, enabling progressively stricter verification from representation compliance to full artifact validity. Across ten models, REALIZE-L3 HSR ranges from 42.0% to 93.9%, while Full Compliance exposes additional artifact-level failures beyond correct final answers and valid representations. These results show that reliable structured generation requires explicit, executable verification of how artifacts are realized and preserved across representations.
- Abstract（参考訳）: 大規模言語モデルは、プログラムや下流システムによって消費される構造化された出力をますます生成する。
SERIAL-7は7つの表現にまたがってマシン検証が可能な生成のための実行可能検証フレームワークを中心に構築された韓国語のベンチマークである。
177の検証された標準的アーティファクトを使用して、SERIAL-7は意味的導出(Derive)、制約されたアーティファクト生成(Realize)、相互表現保存(Preserve)を分離する。
43のアトミック表現制約は、フォーマット、構造、タスク固有のセマンティクスに対する実行可能チェックと組み合わせられ、表現コンプライアンスから完全なアーティファクトの妥当性まで、徐々に厳格な検証を可能にする。
10モデル全体では、REALIZE-L3 HSRは42.0%から93.9%の範囲で、Full Complianceは正しい最終回答と有効な表現以上のアーティファクトレベルの失敗を露呈する。
これらの結果は、信頼性のある構造化生成には、表現全体にわたってアーティファクトがどのように実現され、保存されるかの明示的で実行可能な検証が必要であることを示している。
関連論文リスト
- From Natural Language to Verified C: Verification-Guided Generation with ACSL Specifications [13.473192257235732]
本稿では,CプログラムとACSL仕様を自然言語要求から合成するための形式的検証に適したフレームワークであるVeriGen-Cを紹介する。
コード生成と修復は、証明関連状態の公開、推論検証のための制御フローの合理化、自動証明探索の妨げとなる実装パターンの排除に制約される。
論文 参考訳（メタデータ） (2026-10-22T04:48:23Z) - Evaluating Local Language Model Agents for Reproducible Data Engineering: An Empirical Software Engineering Study of Mobility Workflows [74.39138492851343]
大規模言語モデル(LLM)エージェントは、ソフトウェアやデータエンジニアリングアシスタントとしてますます使われている。
ローカルオープンウェイトエージェントが正しい再現可能なデータエンジニアリングアーティファクトを作成できるかどうかを評価する。
論文 参考訳（メタデータ） (2026-10-08T08:26:46Z) - Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence [9.32030540168344]
セキュリティ標準は、実行された法的効果や、それが持つ証拠やリバース義務を特定せずに、特権的なコントロールを公開します。
我々はIsabelle/HOLで、FREEZE、SEIZE、CONFISCATE、LIQUIDATE、RESTRICT、RECOVERの6つのERC-8319の参照実行セマンティクスを定式化する。
論文 参考訳（メタデータ） (2026-08-29T08:23:27Z) - Can Large Language Models Recover Semantic Optimization Opportunities That Compilers Miss? [5.989315760622425]
大型言語モデル(LLM)は異種C/C++コンテキストから有効セマンティクスを復元することができる。
SeGaBenchは、100の合成ケースと20のソースバックケースを含む実行可能なベンチマークである。
最強のモデルは94.8%のレスポンスで正しいアーティファクトを生成し、83.3%で少なくとも1.05倍のスピードアップを達成し、93.3%のケースでパフォーマンスに成功している。
論文 参考訳（メタデータ） (2026-08-04T17:47:25Z) - Weave of Formal Thought [51.56484100374058]
WoFT(Weave of Formal Thought)は、厳密な構文的検証と学習された構造的表現を結合したパラダイムである。
本稿では,非終端文法記号を直接生成にインターリーブするために,言語モデルを訓練する潜時可変微調整法を提案する。
Pythonでは、RWS目的のStarCoder2-3Bを微調整することで、テキストのみのSFTベースラインと比較して、トーケン毎のクロスエントロピーが14.3%削減される。
論文 参考訳（メタデータ） (2026-06-24T15:58:11Z) - Intent-aligned Formal Specification Synthesis via Traceable Refinement [43.72968325799861]
VeriSpecGenは、要求レベルの属性と局所的な修復を通じて、リーンで意図に整合した仕様を合成する、トレーサブルな改善フレームワークです。
VeriSpecGenは自然言語をアトミックな要件に分解し、明示的なトレーサビリティマップで要求対象のテストを生成する。
我々は、Claude Opus 4.5を使用してVERINA SpecGenタスクの86.6%を達成し、モデルファミリとスケールで最大31.8ポイントのベースラインを改善する。
論文 参考訳（メタデータ） (2026-04-12T00:52:27Z) - VIRO: Robust and Efficient Neuro-Symbolic Reasoning with Verification for Referring Expression Comprehension [51.76841625486355]
Referring Expression (REC) は、自然言語クエリに対応する画像領域をローカライズすることを目的としている。
最近のニューロシンボリックRECアプローチは、大規模言語モデル(LLM)と視覚言語モデル(VLM)を利用して構成推論を行う。
推論ステップ内に軽量な演算子レベルの検証器を組み込む,ニューロシンボリックなフレームワークであるVIROを紹介する。
論文 参考訳（メタデータ） (2026-01-19T07:21:19Z) - LongWeave: A Long-Form Generation Benchmark Bridging Real-World Relevance and Verifiability [60.451734326001564]
textbfLongWeaveを導入し、Constraint-Verifier Evaluation(CoV-Eval)による実世界と検証のバランスをとる。
LongWeaveは7つの異なるタスクに対して、カスタマイズ可能な入出力長(最大64K/8Kトークン)をサポートする。
23大言語モデルの評価は、実世界の複雑さと出力長の増加に伴い、最先端モデルでさえ、長文生成において重大な課題に直面していることを示している。
論文 参考訳（メタデータ） (2025-10-28T12:11:12Z) - VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。
評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
論文 参考訳（メタデータ） (2025-05-25T19:00:52Z) - FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving [53.43068330741449]
大規模言語モデル(LLM)を用いた対話型形式検証環境FVELを提案する。
FVELは、検証対象のコードをIsabelleに変換し、LLMで証明された神経自動定理を用いて検証を行う。
FVELERデータセットには、Isabelleで定式化されたコード依存関係と検証プロセスが含まれており、758の理論、29,125のレムマ、200,646の証明ステップが含まれている。
論文 参考訳（メタデータ） (2024-06-20T15:31:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。