論文の概要: Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization

• arxiv url: http://arxiv.org/abs/2605.26457v1
• Date: Tue, 26 May 2026 02:12:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-27 17:51:41.575684
• Title: Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
• Title（参考訳）: Verus-SpecGym:仕様自動化評価のためのエージェント環境
• Authors: Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal, Seungone Kim, Jannis Limperg, Cedric Flamant, Kanna Shimizu, Bryan Parno, Sean Welleck,
• Abstract要約: LLMエージェントが非公式なプログラミング問題を忠実な形式仕様に変換することができるかどうか、仕様自動書式化について検討する。 Codeforces問題から派生した581の仕様記述タスクのベンチマークであるVerus-SpecBenchを紹介する。 フェールモードの解析は、モデル生成仕様が重要な入力仮定を受け入れ、誤った出力を受け入れ、有効な仕様を拒否できることを示している。
• 参考スコア（独自算出の注目度）: 26.123396123145415
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: AI coding agents are increasingly used to write real-world software, but ensuring that their outputs are correct remains a fundamental challenge. Formal verification offers a promising path: an agent generates code together with a machine-checked proof, guaranteeing that the code satisfies a formal specification. However, there is no guarantee that the formal spec itself matches the user's intent. In this work, we study specification autoformalization: whether LLM agents can translate informal programming problems into faithful formal specifications. We introduce Verus-SpecBench, a benchmark of 581 spec-writing tasks derived from Codeforces problems targeting Verus, a verifier for Rust, and Verus-SpecGym, an agentic environment in which models interact with Verus, bash, & the filesystem to develop these specs. The central challenge is evaluation: expert-written reference specs are expensive to write, & LLM judges can miss subtle mistakes. We address this by (a) extending Verus's exec_spec mechanism so that generated specs can be executed as Rust code, & (b) testing them against official Codeforces tests & adversarial cases extracted from Codeforces "hacks", which are edge cases written by competitors to break incorrect solutions. On Verus-SpecBench, the strongest model, Gemini 3.1 Pro, solves 77.8% of tasks, other frontier models solve 51.1--57.8% & OSS models reach only 21.5--25.5%. Our analysis of failure modes shows that model-generated specs can omit important input assumptions, accept incorrect outputs, & reject valid ones. We also find that LLM-as-a-judge evaluation misses 26% of the failures our evaluator catches. Overall, our results suggest that spec autoformalization is within reach for frontier agents but remains brittle even on problems where they can already generate correct code. The code, data, & logs can be found at https://github.com/formal-verif-is-cool/verus-spec-gym
• Abstract（参考訳）: AIコーディングエージェントは、現実世界のソフトウェアを書くのにますます使われていますが、アウトプットが正しいことを保証することは、依然として根本的な課題です。 エージェントは、マシンチェックされた証明と共にコードを生成し、コードが正式な仕様を満たすことを保証します。 しかし、正式な仕様自体がユーザの意図と一致するという保証はない。 本研究では, LLMエージェントが非公式なプログラミング問題を忠実な形式仕様に変換することができるかどうか, 仕様の自動書式化について検討する。 我々は、VerusをターゲットとするCodeforces問題から派生した581の仕様記述タスクのベンチマークであるVerus-SpecBenchと、モデルがVerus、bash、ファイルシステムと相互作用するエージェント環境であるVerus-SpecGymを紹介した。 専門家が書いた参照仕様は書けず、LCMの審査員は微妙なミスを犯すことがある。 我々はこの問題に対処する (a)Verusのexec_specメカニズムを拡張して、生成された仕様をRustコードとして実行できるようにする。 b) 公式のCodeforcesテストとCodeforcesの"ハック"から抽出した敵のケースに対するテスト。 最も強力なモデルであるVerus-SpecBenchでは、Gemini 3.1 Proが77.8%のタスクを解決し、他のフロンティアモデルでは51.1-57.8%とOSSモデルは21.5-25.5%にしか達していない。 フェールモードの解析は、モデル生成スペックが重要な入力仮定を省略し、誤った出力を受け入れ、有効なものを拒否できることを示している。 また、LCM-as-a-judge評価では、評価者がキャッチする失敗の26%を見逃していることもわかりました。 全体としては,仕様の自動書式化はフロンティアエージェントの手が届く範囲内にあるが,すでに正しいコードを生成できる問題でさえも脆弱な状態にあることが示唆されている。 コード、データ、ログはhttps://github.com/formal-verif-is-cool/verus-spec-gymにある。

関連論文リスト

• ContraFix: Agentic Vulnerability Repair via Differential Runtime Evidence and Skill Reuse [10.503895811137095]
  大規模言語モデル(LLM)エージェントは、自動脆弱性修復にますます利用されている。 最近の実証的な結果は、これらのエージェントがいまだに現実世界の脆弱性と戦っていることを示している。 ContraFixは、再利用可能な修復スキルとランタイムエビデンスを結合するエージェントフレームワークである。
  論文  参考訳（メタデータ） (2026-05-17T13:48:25Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• Project Prometheus: Bridging the Intent Gap in Agentic Program Repair via Reverse-Engineered Executable Specifications [14.657771106188115]
  現在のソリューションは、自然言語の要約や敵のサンプリングに頼っているが、手術の修理に必要な決定論的制約を与えていないことが多い。 コード生成よりもtextitSpecification Inference を優先することで、このギャップを埋める新しいフレームワークである textscPrometheus を紹介します。 我々のフレームワークは textbf93.97% (639/680) の完全なパッチレートを達成した。
  論文  参考訳（メタデータ） (2026-04-19T14:27:27Z)
• AutoReSpec: A Framework for Generating Specification using Large Language Models [1.0026496861838448]
  大きな言語モデル(LLM)は形式的な仕様生成において有望であるが、初期の結果にはいくつかの制限がある。 提案するAutoReSpecは,オープンソースとクローズドソースのLLMを組み合わせて,検証可能な仕様生成を行う協調フレームワークである。 我々はAutoReSpecを72の現実世界および合成Javaプログラムの新しいベンチマークで評価する。
  論文  参考訳（メタデータ） (2026-04-04T15:17:08Z)
• Is Your Automated Software Engineer Trustworthy? [0.850206009406913]
  大規模言語モデル(LLM)は、ソフトウェア工学のタスクでますます使われています。 LLMはすべての問題に応答し、入力があいまいであったり、出力が間違っていたとしても、すべてのケースに対してパッチを生成する。 これは、幻覚的なコード変更や、あいまいな問題レポートに基づいたレスポンスといった、信頼性の低い振る舞いにつながります。 我々は、LLMベースのソフトウェアエージェントが入力が未定義の場合に動作しないかどうかを評価するベンチマークであるBouncerBenchを紹介する。
  論文  参考訳（メタデータ） (2025-06-21T20:56:20Z)
• CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
  $rm Csmall LEVER$は、リーンにおけるエンドツーエンドのコード生成のための161の問題を、高品質でキュレートしたベンチマークである。 それぞれの問題は、(1)堅実な仕様と一致する仕様を生成するタスク、(2)この仕様を確実に満足するリーン実装を生成するタスクで構成されています。
  論文  参考訳（メタデータ） (2025-05-20T05:15:47Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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