論文の概要: Specula: Scaling formal specifications for autonomous model checking of system code

• arxiv url: http://arxiv.org/abs/2607.25333v1
• Date: Tue, 28 Jul 2026 06:33:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-29 20:50:42.733195
• Title: Specula: Scaling formal specifications for autonomous model checking of system code
• Title（参考訳）: Specula: システムコードの自律的モデルチェックのための正式な仕様のスケーリング
• Abstract要約: Speculaはプッシュボタンエージェントシステムであり、大規模で複雑なシステムコードの高品質な形式仕様を生成する。 Speculaは、大規模言語モデル(LLM)ベースのコーディングエージェントを使用して、TLA+仕様を自律的に開発している。
• 参考スコア（独自算出の注目度）: 8.484545401876316
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Specula is a push-button agentic system that generates high-quality formal specifications for large, complex system code and uses the specifications for highly effective model checking and bug finding. Specula employs large language model (LLM) based coding agents to autonomously develop TLA+ specifications, including invariants that describe correctness properties of the target system and formal models that describe the system implementation with the right level of abstractions. Specula is fully autonomous and thus eliminates the barrier of applying formal methods to real-world system code (as in traditional human-centric approaches). Meanwhile, Specula addresses limitations of LLM-driven techniques like reward hacking and hallucinations through self-evolving loops that iteratively improve specification quality by enabling the agents to deepen their understanding of system code and its behaviors. We have used Specula to check 48 open-source system projects; Specula found 249 bugs including many deep bugs that are hard to find by existing approaches. Specula has been used by several companies and is maintained at https://github.com/specula-org/Specula.
• Abstract（参考訳）: Speculaは、大規模で複雑なシステムコードの高品質な形式仕様を生成するプッシュボタンエージェントシステムであり、非常に効率的なモデルチェックとバグ発見のために仕様を使用する。 Speculaは大規模言語モデル(LLM)ベースのコーディングエージェントを使用してTLA+仕様を自律的に開発する。 Speculaは完全に自律的であるため、(従来の人間中心のアプローチのように)現実のシステムコードにフォーマルなメソッドを適用するという障壁を取り除くことができる。 一方Speculaは、自己進化ループを通じて報酬ハックや幻覚といったLLM駆動のテクニックの制限に対処し、エージェントがシステムコードとその動作に対する理解を深めることによって、仕様品質を反復的に改善する。 Speculaは249のバグを発見し、その中には既存のアプローチでは見つからない多くの深いバグが含まれています。 Speculaはいくつかの企業で使われており、https://github.com/specula-org/Specula.comでメンテナンスされている。

関連論文リスト

• SpecCoder: Specification-Aware Code Generation with Curriculum Dual-Task Reinforcement Learning [30.588079618949447]
  SpecCoderは、コード生成のための2段階のトレーニングフレームワークである。 まず、GRPを訓練し、構造化された仕様分析を導出し、それらに条件付きコードを生成する。 このカリキュラムは仕様誘導生成と識別を共同で最適化し、仕様とコード動作のより強力な対応を促進する。
  論文  参考訳（メタデータ） (2026-09-05T11:52:54Z)
• KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base [9.796586560498026]
  本稿では,多言語モデル(LLM)を形式仕様言語コーパスのデュアルソース知識で拡張するKBSpecを提案する。 その結果,KBSpec は最新の LLM ベースのアプローチよりも10-25% の検証パス率向上を実現していることがわかった。
  論文  参考訳（メタデータ） (2026-06-19T11:37:00Z)
• CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
  本稿では,実行ベース評価プロトコルの下で実行可能な動作仕様生成のためのベンチマークであるCodeSpecBenchを紹介する。 CodeSpecBenchは関数レベルとリポジトリレベルのタスクの両方をサポートし、仕様を実行可能なPython関数としてエンコードする。 リポジトリレベルのタスクでは、最高のモデルが20.2%のパス率しか達成できないため、パフォーマンスが大幅に低下するのを観察します。
  論文  参考訳（メタデータ） (2026-04-14T04:31:45Z)
• MASEval: Extending Multi-Agent Evaluation from Models to Systems [77.09381093359598]
  MASEvalはフレームワークに依存しないライブラリで、システム全体を分析の単位として扱う。 研究者はエージェントシステムのすべてのコンポーネントを探索し、原則化されたシステム設計のための新たな道を開くことができる。
  論文  参考訳（メタデータ） (2026-03-09T18:46:17Z)
• Sharpen the Spec, Cut the Code: A Case for Generative File System with SYSSPEC [6.536447932095715]
  本稿では,生成ファイルシステムを開発するためのフレームワークであるSYSSPECを紹介する。 不正確なプロンプトの代わりに、SYSSPECはファイルシステムの機能を正確に記述するマルチパート仕様を採用している。 進化を管理するため,仕様自体で動作するDAG構造化パッチを開発した。
  論文  参考訳（メタデータ） (2025-12-15T07:15:01Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。 本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
  論文  参考訳（メタデータ） (2025-10-02T06:25:10Z)
• SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems [12.181911851729614]
  我々は、AIが大規模で複雑なシステムを正式にモデル化する能力を評価するベンチマークであるSysMoBenchを紹介する。 私たちは、今日の重要なコンピューティングインフラストラクチャのキーストーンである、並列および分散システムに重点を置いています。
  論文  参考訳（メタデータ） (2025-09-27T05:24:54Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。 そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。 提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
  論文  参考訳（メタデータ） (2025-04-12T15:03:00Z)
• Multi-Grained Specifications for Distributed System Model Checking and Verification [9.14614889088682]
  我々はTLA+を用いて、ZooKeeperとTLCモデルチェッカーのきめ細かい挙動をモデル化し、その正確性を検証する。 複数きめの仕様を書くことは現実的な実践であり、不安定な状態空間を伴わずにモデルコードギャップに対処できることを示す。
  論文  参考訳（メタデータ） (2024-09-22T02:59:56Z)
• TurboSpec: Closed-loop Speculation Control System for Optimizing LLM Serving Goodput [37.56866491624234]
  大規模言語モデル (LLM) システムは、効率的なサービスを実現するために、同時ユーザー要求をバッチ化する。 本稿では,実行環境を自動的にプロファイリングする投機制御システムTurboSpecを提案する。 さまざまなワークロードとハードウェア構成にまたがって、その効果を実証します。
  論文  参考訳（メタデータ） (2024-06-20T07:43:33Z)
• InfiBench: Evaluating the Question-Answering Capabilities of Code Large Language Models [56.723509505549536]
  InfiBenchは、私たちの知識に合ったコードのための、最初の大規模フリーフォーム質問回答(QA)ベンチマークです。 慎重に選択された234の高品質なStack Overflow質問で構成されており、15のプログラミング言語にまたがっている。 InfiBench上で100以上の最新のコードLLMに対して,系統的評価を行い,新しい知見と洞察に富んだ結果を得た。
  論文  参考訳（メタデータ） (2024-03-11T02:06:30Z)
• Exploring Continual Learning for Code Generation Models [80.78036093054855]
  継続的学習(CL)は、コードドメインの中でまだ過小評価されていない重要な側面である。 コード生成,翻訳,要約,改良など,幅広いタスクをカバーするCodeTask-CLというベンチマークを導入する。 即時選択機構の不安定な訓練により,プロンプトプール (PP) などの有効手法が破滅的な忘れ込みに悩まされることが判明した。
  論文  参考訳（メタデータ） (2023-07-05T16:58:39Z)

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

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