PaperlayerView exact revision on arXiv

Source-linked AI summary

Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization

Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal, Seungone Kim, Jannis Limperg, Cedric Flamant, Kanna Shimizu, Bryan Parno, Sean Welleck

arXiv:2605.26457v1cs.SEcs.AIcs.CLcs.PL

TL;DR

Formal specifications can fail to capture a programming problem’s intended behavior, even when generated code is correct. This paper introduces a benchmark and executable-testing environment for evaluating specification autoformalization, finding that Gemini 3.1 Pro solves 77.8% of tasks while specification faithfulness remains brittle.

  • Problem

    The paper asks whether LLM agents can translate informal programming intent into formal specifications that are both sound and complete.

  • Method

    The authors build a 581-task Verus benchmark and agentic environment with executable specifications tested on official cases and adversarial hacks.

  • Results

    77.8% of tasks are solved by Gemini 3.1 Pro, while other frontier models solve 51.1–57.8% and open-source models solve 21.5–25.5%.

  • Takeaways & Limitations

    Specification autoformalization is within reach for frontier agents but remains a distinct and brittle bottleneck even when they generate correct code.

  • Takeaways & Limitations

    The evaluation focuses on single-file competition problems, and finite test suites cannot rule out all specification errors.

Abstract

from arXiv · show

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

1 Introduction

Specification autoformalization asks whether agents can faithfully translate informal programming intent into machine-checkable Verus specifications. The paper introduces Verus-SpecBench and Verus-SpecGym, an executable, test-based evaluation framework that reveals strong frontier performance but persistent brittleness.

  • Motivation: Verified code generation guarantees correctness only relative to its formal specification, making faithful translation from informal requirements a central challenge.Specifications must accept valid inputs and correct outputs while rejecting invalid inputs and incorrect outputs; weak specs can certify incorrect programs, whereas strong specs can reject correct ones.
  • Benchmark and environment: 581 specification-writing tasks comprise Verus-SpecBench, paired with Verus-SpecGym, where agents iteratively develop specifications using Verus, bash, and the filesystem.The benchmark derives tasks from Codeforces problems and targets Verus, a verification framework for Rust.
  • Evaluation: Executable specifications are evaluated against official Codeforces tests and adversarial inputs extracted from human-written hacks, avoiding reliance on expert references or LLM judges.The evaluator extends Verus’s exec_spec mechanism to provide deterministic testing of specification faithfulness.
  • Results: 77.8% of tasks are solved by gemini-3.1pro, compared with 51.1–57.8% for other frontier models and 21.5–25.5% for evaluated open-source models.These results show a substantial capability gap between frontier and open systems, while agents can still fail to specify faithfully on problems where they generate correct code.
  • Evaluation findings: Increasing test-case number and diversity lowers measured success, while adversarial hacks expose failures that official tests miss.The ablations support comprehensive evaluation and show that human-written adversarial inputs complement ordinary test cases.

2 Specification Autoformalization and Evaluation

This section frames specification autoformalization as generating Verus specifications whose input-output relation faithfully matches the informal problem, and evaluates faithfulness through executable tests of pre- and postconditions. It also motivates extending Verus execution support to cover richer specification types while avoiding proof-related testing failures.

  • Evaluation: Unlike finite test-based code evaluation, verified code generation uses v(s_F, p) to check a program against a formal specification across valid inputs.Finite tests establish behavior only on their listed cases, whereas verification provides a broader guarantee when the specification is faithful.
  • Formal setup: Specification autoformalization requires the formal relation R_sF to match the informal relation R_sI, requiring both soundness and completeness.Soundness requires R_sF ⊆ R_sI, while completeness requires R_sI ⊆ R_sF.
  • Formal setup: Verus specifications separate valid-input requirements from acceptable-output guarantees through pre_spec and post_spec.Pre-specification concerns the domain of valid inputs; post-specification defines acceptable outputs for each valid input.
  • Evaluation: Evaluation uses four testcase buckets: pre-completeness, pre-soundness, post-completeness, and post-soundness.A faithful specification accepts both completeness buckets and rejects both soundness buckets, using tests and hacks populated later from Codeforces.
  • Evaluation: The evaluator extends exec_spec with sequences, sets, multisets, maps, richer methods, and bounded multi-variable quantification, while adding exec_spec_unverified to avoid unnecessary proof failures.The original execution support is insufficient for many Codeforces specifications, and correspondence proofs can fail even when executable code suffices for concrete-input testing.

3 Data and Agent Environment

Verus-SpecBench is built from Codeforces problems by losslessly converting tests and hacks into four evaluation buckets, then exposing each task as a Verus specification-writing environment for agents.

  • Testcase conversion: The benchmark converts raw Codeforces testcases into typed Verus/Rust values and requires byte-for-byte parser–printer round trips to prevent evaluating incorrect concrete cases.Failed round trips trigger parser and printer revisions or discard the attempt.
  • Evaluation test cases: Official tests populate completeness buckets, while Codeforces hacks provide adversarial cases targeting edge cases and implicit constraints absent from ordinary tests.Hacks are routed by validity and checker acceptance into pre-sound, pre-complete, post-complete, or post-sound buckets.
  • Dataset statistics: 581 problems span diverse topics and difficulty ratings, with every problem containing at least five test cases in each evaluation bucket.Average counts are 21 pre-sound, 80 pre-complete, 55 post-sound, and 78 post-complete cases per problem.
  • Agent environment: Each task gives an agent a problem directory and Verus skeleton with fixed input/output types and holes for pre_spec and post_spec bodies.The agent reads and edits files, uses local evaluation feedback, and submits the completed specification.

4 Experiments

Experiments show that frontier agents outperform open-source models on specification generation, but soundness testing, executable fallback, and adversarial evaluation reveal substantial remaining brittleness. Specification generation also remains difficult when code generation succeeds, and LLM judges miss verifiable specification errors.

  • Overall performance: gemini-3.1pro achieves the highest end-to-end Pass@1 at 0.778, followed by gpt5.3-codex at 0.578 and opus4.6 at 0.511.Open-source models achieve Pass@1 between 0.215 and 0.255 under the same cost cap.
  • Specification versus code generation: Specification generation remains difficult even when code generation succeeds, as shown by gpt5.3-codex solving 153 of 187 corresponding Python programming tasks after writing incorrect specifications.The comparison uses problems with unique correct outputs and available code-generation runs.
  • Evaluator design: Soundness tests reduce Pass@1 from 77% to 58% for gpt5.3-codex, 82% to 78% for gemini-3.1pro, and 59% to 51% for opus4.6.The drops show that completeness-only evaluation misses unsound specifications.
  • Evaluator design: Adding more testcases increases failure-detection coverage, but each additional testcase provides diminishing marginal benefit once the testcase budget is sufficiently large.The benchmark estimates the probability of catching at least one specification failure as testcase coverage expands.
  • Evaluator design: exec_spec resolves concrete testcases that symbolic checking leaves inconclusive by compiling specifications into executable Rust and obtaining concrete accept/reject verdicts.The executable fallback is especially important for postcondition checking, where gemini-3.1pro and gpt5.3-codex resolve many cases symbolically classified as unknown.
  • Evaluation failures: 25.7% of incorrect but compilable specifications were misclassified as correct by the gpt5.3-codex LLM judge, which marked 49 of 191 such specifications correct.The benchmark found a verifiable failing testcase for each of these missed errors.
  • Failure modes: Recurring failures include omitting input assumptions, rejecting correct outputs, and accepting incorrect outputs in generated specifications.Examples include missing global structural promises or existence guarantees and an overly complex interval-union postcondition that rejects valid answers.

5 Related Work

Related work spans verified code generation, formal-specification evaluation, and agentic software-engineering benchmarks. Verus-SpecGym differs by focusing on natural-language-to-specification autoformalization without requiring a reference formal specification.

  • Verified Code Generation: Verified code-generation systems use LLMs to generate proofs from code and specifications, or code and proofs from specifications, sometimes synthesizing specifications as well.Verifier guarantees apply only relative to the specification, so a specification that misses user intent limits what verification establishes.
  • Evaluating Formal Specifications: Existing formal-specification evaluation methods compare reference specifications or semantic metrics, test rejection of buggy mutants, or reconstruct code to detect weak specifications.These approaches address specification evaluation as distinct from checking whether code verifies.
  • Evaluating Formal Specifications: Prior approaches rely on existing artifacts or reference specifications, whereas this work benchmarks autoformalization from natural language without a reference formal specification.The approach uses Verus’s exec_spec to test generated specifications.
  • Agentic Evaluation: Agentic benchmarks evaluate autonomous software-engineering agents, while formal-verification work studies Verus proof generation, iterative code-and-proof refinement, and multi-agent specification generation.These efforts provide adjacent agentic settings but cover different primary tasks or evaluation contexts.

6 Conclusion · A Example of Formally Verified Code · B Task Format and Evaluation: A Worked Example

The paper introduces Verus-SpecBench and Verus-SpecGym, using executable specifications, official tests, and adversarial hacks to evaluate faithful specification autoformalization. A worked example shows how agents write Verus specifications that are checked through symbolic verification and executable Rust, while limitations remain for broader software and exhaustive faithfulness.

  • 6 Conclusion: Verus-SpecBench pairs Codeforces problems with official tests and human-written hacks, while executable specifications test whether generated pre_spec and post_spec accept and reject concrete cases.This provides a scalable faithfulness signal without requiring expert-written reference specifications.
  • 6 Conclusion: 26% of failures caught by the evaluator are missed by the LLM-as-judge baseline, while adversarial hacks expose specification failures that official tests miss.The findings identify specification autoformalization as a distinct bottleneck, even when frontier models can generate correct code for the same problem.
  • 6 Conclusion: The evaluation focuses on single-file competition-style problems, and finite test suites cannot rule out every possible specification error.Repository-level specifications for multi-file, real-world systems may expose additional weaknesses.
  • A Example of Formally Verified Code: The running example presents a complete Verus-verified binary search for first occurrence, separating the formal specification, data model, executable code, and proof annotations.The specification uses pre_spec, post_spec, and sorted_nondecreasing; proof annotations include loop invariants, decreases clauses, and assert hints, with deep_view() linking executable values to specifications.
  • B.1 Problem Statement: Each worked-example task gives the agent a Codeforces statement and asks it to maximize the cost of a possibly empty subarray under stated input constraints.The example uses Codeforces 1197-D with n ≤ 3 · 10^5, m ≤ 10, k ≤ 10^9, and −10^9 ≤ ai ≤ 10^9.
  • B.2 Skeleton File: The agent fills pre_spec and post_spec in solve.rs, while the input/output types and checker functions are fixed and evaluator placeholders are injected before compilation.The skeleton is not standalone because exec_in1 and exec_out remain undefined until testcase-specific injection.
  • B.2 Skeleton File: The evaluator runs each submitted specification against four testcase buckets and uses injected concrete inputs and outputs to decide whether each testcase is accepted or rejected.The four buckets are τpre-comp, τpre-sound, τpost-comp, and τpost-sound.
  • B.3 Evaluation via Symbolic Verification / B.4 Evaluation via Executable Specifications (exec_spec): Symbolic verification first classifies testcases as accept-via-symbolic, reject-via-symbolic, or symbolically unknown; unknown cases fall back to executable Rust evaluation.Executable evaluation compiles generated exec_pre_spec and exec_post_spec, then returns accept-via-exec, reject-via-exec, or indeterminate-during-exec for errors or timeouts.

C Specification to Executable Code Translation in Verus with exec_spec

This section describes Verus’s exec_spec feature and the subset of the Verus specification language that it supports.

  • The section introduces the exec_spec feature in Verus.
  • It explains which subset of Verus’s specification language exec_spec supports.
  • The discussion focuses on exec_spec and its supported specification-language subset.

C.1 Implementation Details … D Additional Details About Data Creation

The benchmark executes Verus specifications by macro-compiling them into Rust equivalents, enabling executable testing while distinguishing unverified translation from proof-producing equivalence checking. Examples illustrate the generated structs and functions, and the supported constructs include arithmetic, logic, control flow, recursive calls, primitive types, strings, and options.

  • C.1 Implementation Details: The exec_spec feature is a macro that compiles specification code into executable equivalents usable by other executable code.The user applies the macro to specification code, which is automatically compiled to executable equivalents.
  • C.1 Implementation Details: The benchmark uses exec_spec_unverified!, whereas exec_spec_verified! additionally produces Verus-checked equivalence proofs despite generating identical executable code.The verified macro is intended to support proof-producing validation of the translation.
  • C.2 Example: The example defines Point and Polygon structs plus on_line and is_rect specification functions inside exec_spec_unverified!.These declarations provide the source specification code for demonstrating macro translation.
  • C.2 Example: The macro converts each struct to an Exec-prefixed struct with executable field types and each specification function to an executable function using loops for quantified expressions.For example, Seq is converted to Vec, and forall expressions are translated into loop-based executable code.
  • C.2 Example: The generated executable code runs in Rust without panics and supports assertions that on_line returns true while is_rect returns false for the example inputs.The example constructs two points, evaluates both executable functions, and checks the results with assertions.
  • C.3 Supported Specification Constructs: The documented construct support is bounded by the macro’s available translation rules at the time of writing.The section presents the supported specification constructs as a current implementation list rather than an unrestricted language definition.
  • C.3 Supported Specification Constructs: Supported constructs include arithmetic, logical operators, conditionals and pattern matching, specification-function calls including recursion, primitive Rust types, SpecString operations, and Option equality and unwrap.The listed primitive types include integer variants, bool, and char; Verus int and nat are not supported as arguments or fields in user-defined types.

D.1 Data Collection Pipeline

Verus-SpecBench is constructed through a five-stage pipeline that sources Codeforces problems, filters and categorizes tests, converts them into executable Verus/Rust values, and selects a balanced evaluation set of 581 problems.

  • Stage 1: Sourcing: 10k problems from Codeforces contests held up to Dec 2025 form the initial source pool.
  • Stage 3: Hack collection and categorization: The pipeline collects official tests and user-submitted hacks, assigning them to four pre/post soundness/completeness buckets based on validator and checker verdicts.Invalid inputs enter τpre-sound; valid inputs with incorrect outputs contribute to τpre-comp and τpost-sound, while valid inputs with correct outputs contribute to τpre-comp and τpost-comp.
  • Cleaning and coverage filtering: Syntactically invalid hacks are discarded, while semantically invalid inputs are retained for pre_spec soundness testing; duplicate, incomplete, or truncated cases are also removed.A final coverage filter removes problems with fewer than 5 remaining test cases in any required bucket.
  • Stage 4: Test-case conversion: Converted test cases must pass the lossless round-trip check Treproduced = P(R(t)) == t, with at least 5 successfully converted cases retained per bucket and no bucket exceeding 200 sampled cases.The conversion agent constructs a parser R and printer P, and failed conversions can eliminate a problem.
  • Stage 5: Final selection: 581 problems spanning varied difficulty ratings and topics comprise the final VERUS-SPECBENCH dataset.The final selection balances coverage across difficulty ratings and topic tags.

E Additional Dataset Statistics · F Additional Insights

VERUS-SPECBENCH spans Codeforces problems from ratings 800 to 2700, with broad topic coverage and a median rating of 1200. Evaluations use fixed per-problem budgets and infrastructure constraints, while API latency and prompt caching affect practical agent interaction capacity and spending.

  • E Additional Dataset Statistics: Ratings span 800–2700, with a median of 1200 and a mean of 1289.Most problems fall in the 900–1499 range, with diminishing but non-trivial representation at higher difficulty levels.
  • E Additional Dataset Statistics: The benchmark covers diverse Codeforces topics, including implementation, dynamic programming, graph search, and number theory.Problems may carry multiple topic tags.
  • F Additional Insights: Each agent receives a budget of $2.5 per problem, with SWE-AGENT additionally limited to 400 API calls per problem.The base agent timeout is 75 minutes.
  • F Additional Insights: The additional insights include an informal natural-language specification example for Codeforces 1027-C.The example describes selecting four distinct sticks that form a rectangle, with no cutting or reuse, under a guarantee that a valid selection exists.
  • F Additional Insights: Experiments run on Modal cloud and Docker containers using 4 CPUs and 8 GB RAM per task.These are the stated per-task resource allocations.
  • F Additional Insights: API latency limits how many interaction rounds agents complete before the 75-minute wall-clock timeout.This affects practical evaluation capacity even when the nominal budget is fixed.
  • F Additional Insights: Prompt-cache behavior partly determines dollar-budget consumption because providers price cached tokens differently and cache-hit rates vary with cache duration.The passage notes that budgeted evaluations depend on practical API-level details beyond the nominal dollar limit.
  • F Additional Insights: A figure summarizes Pass@1 and testcase-bucket performance across the evaluated models.The supplied passage identifies this as Figure 13’s content without reporting additional values.

F.1 Does problem difficulty affect specification-generation success?

Specification-generation success declines consistently as Codeforces difficulty increases across all models, with open-source models starting from lower baselines. Even frontier agents leave 10–16% of the easiest problems unsolved, indicating challenges beyond algorithmic difficulty.

  • Difficulty effects: Pass@1 declines with problem difficulty for every model, while open-source models start lower and all models score near zero on problems rated 2100+.gemini-3.1pro falls from 0.90 at 600–900 to 0.50 at 2400–2700, while gpt5.3-codex falls from 0.73 to 0.27 over the same range.
  • Difficulty effects: 10–16% of the easiest problems still defeat frontier agents, with gemini-3.1pro scoring 0.90 at 600–900 and 0.84 at 900–1200.The results suggest that even straightforward problems can contain subtle input constraints or edge cases that are difficult to formalize completely.
  • Difficulty effects: Figure 14 confirms that performance degrades consistently with Codeforces difficulty, while also reporting the number of problems in each rating bucket.The best model solves only 90% of easy problems rated 600–900.

F.2 How are testcases resolved, and how does exec_spec help? … F.5 Do models solve the same problems or different problems?

The evaluator combines symbolic Verus reasoning with executable Rust fallback, which is especially valuable for postcondition checking and distinguishes semantic specification failures from unresolved cases. Across runs and models, specification generation remains brittle but complementary: repeated sampling and combining models substantially increase coverage, while weak or overly strong specifications cause failures.

  • F.2 How are testcases resolved, and how does exec_spec help?: Each testcase is first checked symbolically in Verus, then resolved with executable Rust via exec_spec when symbolic reasoning is inconclusive, producing six outcome categories.Indeterminate cases arise when neither symbolic reasoning nor runtime execution yields a verdict, such as after timeout or memory-limit failure.
  • F.2 How are testcases resolved, and how does exec_spec help?: Stronger models produce fewer compile/syntax errors, while weaker models are dominated by such errors across several evaluation buckets.This indicates that model differences reflect both semantic precision and the ability to remain within Verus and Rust’s analyzable constraints.
  • F.2 How are testcases resolved, and how does exec_spec help?: exec_spec resolves a large fraction of postcondition testcases for gemini-3.1pro and gpt5.3-codex that would otherwise remain indeterminate under symbolic checking alone.Executable fallback is especially useful when postconditions involve richer output relations than symbolic reasoning can handle.
  • F.3 Examples of unsuccessful cases: Case studies show weak preconditions can omit essential input promises, such as requiring at least n−1 of n rectangles to share a common point.Such omissions can block downstream verification because the missing property is necessary to prove correctness.
  • F.3 Examples of unsuccessful cases: Weak postconditions accept incorrect outputs, including non-coprime pairs when only parity is checked and feasible but non-optimal rectangles when optimality is omitted.These examples demonstrate that checking output shape or partial feasibility is insufficient for faithful specification.
  • F.3 Examples of unsuccessful cases: Overly strong postconditions can reject correct solutions, as gemini-3.1pro’s complex interval-union specification did on Problem 2074D.opus4.6 succeeded on the same problem with a simpler column-wise characterization, making over-specification distinct from under-specification.
  • F.4 pass@k and passk: pass@3 reaches 75.6% for gpt5.3-codex, with 439 of 581 problems solved by at least one attempt, but pass3 is only 34.8%, with 202 solved by all three attempts.The gap shows that specification generation is unreliable across independent runs even when the model can solve a problem.
  • F.5 Do models solve the same problems or different problems?: The three closed-source models share 214 solved problems, while their union covers 486 of 581, with gemini-3.1pro contributing the most unique solves.The overlap pattern indicates substantial complementarity beyond the shared core.

F.6 Do models find code-generation easier than specification generation? … G Case studies of LLM performance on specific tasks

The analysis finds that specification failures often persist despite successful code generation, while LLM judging produces false acceptances and small, diverse test budgets capture most failures.

  • F.6 Do models find code-generation easier than specification generation?: 489 problems had unique correct outputs, enabling testcase-based measurement of code-generation performance without rejecting alternative valid outputs.The uniqueness condition applied because multiple valid outputs can make testcase evaluation misleading.
  • F.6 Do models find code-generation easier than specification generation?: 81.8% of uniquely evaluable failed-specification problems were solved by gpt5.3-codex through Python code generation.The model solved 153 of 187 problems with available code-generation runs.
  • F.7 Can LLMs evaluate specifications in a judge setting?: The judge received the informal problem, several original testcases, their Verus representations, and the generated specification before classifying correctness.This describes the prompting setup for judging specifications generated by the same model.
  • F.7 Can LLMs evaluate specifications in a judge setting?: 527 compile-clean specifications were evaluated: the benchmark accepted 336 and rejected 191.The LLM-judge analysis excluded 54 benchmark-incorrect specifications that did not compile.
  • F.7 Can LLMs evaluate specifications in a judge setting?: The judge marked 49 benchmark-rejected specifications correct and 142 incorrect, making false acceptance the main failure mode.Among benchmark-accepted specifications, it marked 310 correct and 26 incorrect.
  • F.8 Could more testcases have helped?: For specifications failing the full suite, failure detection was already very high with a small budget, with most buckets nearing saturation within the first few dozen tests.The retrospective estimate used uniform subsampling without replacement and combined bucket probabilities assuming independence.
  • F.8 Could more testcases have helped?: After roughly m = 25–50 tests, expected Pass@1 curves entered a long shallow tail as additional tests exposed increasingly redundant failure patterns.At m = 0, every submission passed vacuously, producing artificially strong scores before the initial sharp decline.
  • F.8 Could more testcases have helped?: Postcondition completeness had the slowest saturation, indicating that this bucket contained a broader diversity of edge cases.Figure 17 reports estimated failure-catching probability conditioned on tasks failing under the full test-case budget.

G.1 Case Study: Problem 1051B

The case study shows that gpt5.3-codex generated an unfaithful specification for Codeforces 1051B by replacing the required gcd condition with a weaker parity check, thereby accepting invalid outputs containing (3, 6).

  • Problem requirements: The task requires pairing every integer in [l, r] exactly once so each pair has gcd equal to 1.The specification also requires exactly (r−l+1)/2 pairs and permits any valid pairing or no solution.
  • Specification failure: gpt5.3-codex checks only that each pair is not composed of two even numbers, rather than verifying gcd(a,b) == 1.The parity condition is necessary for relative primality but not sufficient; (3, 6) passes it although gcd(3,6)=3.
  • Adversarial evaluation: Both hack cases contain the non-coprime pair (3, 6), which the generated specification accepts because 3 % 2 != 0.The evaluator therefore records a post-soundness failure: the specification permits output rejected by Codeforces.

G.2 Case Study: Problem 1027C … H Specification Generation Background Prompt

The case studies expose specification failures involving omitted optimality and input assumptions, incorrect computations, and rejection of valid outputs. The generation prompt therefore requires complete structural preconditions, semantically correct postconditions, and specifications that are both sound and complete under evaluation.

  • G.2 Case Study: Problem 1027C: Problem 1027C: Generated specifications may enforce rectangle feasibility without requiring the chosen rectangle to minimize P^2/S.The task requires choosing four available sticks that form a rectangle while minimizing P^2/S among feasible choices.
  • G.2 Case Study: Problem 1027C: Problem 1027C: gpt5.3-codex defines a comparison helper but never uses it, accepting feasible yet nonoptimal output 9 9 15 15.On hack_477544__participant, 1 1 1 1 achieves a smaller P^2/S value than the accepted rectangle.
  • G.2 Case Study: Problem 1027C: Problem 1027C: kimi-k2.6 checks only for two equal pairs, omitting input membership, output ranges, optimality, and rectangle-existence assumptions.It accepts 12 12 1 1 when the input contains only 1 1 10000 10000, and accepts an invalid all-distinct input.
  • G.3 Case Study: Problem 1028C: Problem 1028C: gpt5.3-codex and gemini-3.1pro accept inputs lacking the guaranteed common point among n − 1 rectangles.Their preconditions verify counts, coordinate bounds, and rectangle validity but omit the existence of a point contained in at least n − 1 rectangles.
  • G.4 Case Study: Problem 2074D: Problem 2074D: gemini-3.1pro’s large interval-union computation rejects correct outputs, demonstrating post-completeness failure from specification complexity.The specification constructs, sorts, merges, and sums horizontal intervals, but valid answers from post-completeness hacks are rejected.
  • G.4 Case Study: Problem 2074D: Problem 2074D: opus4.6 uses a simpler column-wise characterization, counting symmetric vertical intervals determined by the maximum covered radius at each integer x-coordinate.This decomposition avoids maintaining and merging many horizontal intervals and passes all benchmark test cases.
  • H Specification Generation Background Prompt: The background prompt instructs agents to encode all input structure and ranges in pre_spec and mathematical output semantics in post_spec, not merely formatting.It explicitly gives minimal-cost matching as an example of intended postcondition semantics.
  • H Specification Generation Background Prompt: The prompt directs agents to match the problem’s true validity notion and make specifications sound and complete on symbolic tests, while using visible failures diagnostically rather than overfitting.Final scoring includes hidden tests, so specifications should be written from the problem statement rather than only visible samples.
Loading 2605.26457v1…