PaperlayerView exact revision on arXiv

Source-linked AI summary

ArgGYM: A Procedural, Engine-Verified Benchmark for Structured Defeasible Reasoning

İbrahim Ethem Deveci, Funda Tan Çalık, Barış Deniz Sağlam, Duygu Ataman

arXiv:2609.38409v1cs.AIcs.CL

TL;DR

Reasoning under incomplete, conflicting, and revisable information remains a challenge beyond fixed-specification benchmark domains. ArgGYM provides twelve engine-verified tasks and frozen and fresh instances for evaluation and training. The results identify distinct weaknesses in global argumentative composition and constructive search.

  • Problem

    It remains unclear how well reasoning success in fixed-specification domains transfers to defeasible reasoning, where conclusions may be revised as information changes.

    Source: §1 · pp. 1–2

  • Method

    ArgGYM decomposes structured defeasible reasoning into twelve ASPIC+-based tasks, scored using a symbolic engine, with a frozen benchmark and generators for fresh instances.

    Source: §1 · p. 2

  • Results

    The evaluated models can recover locally correct components yet struggle to compose full argumentative states, with global composition and constructive search emerging as distinct challenges.

    Source: §6 · p. 8, §8 · p. 9

  • Takeaways & Limitations

    Final-answer accuracy alone can obscure operation-specific weaknesses, so the findings support evaluating and training models across distinct reasoning operations.

    Source: §6 · p. 8, §8 · p. 9

    Curriculum and ordering comparisons are diagnostic: curricula vary multiple structural properties, and ordering conditions use independently generated rather than matched theories.

    Source: §7 · p. 9

Abstract

from arXiv · show

Recent progress in large language model reasoning has been driven by benchmarks and reinforcement learning environments with automatically verifiable rewards, particularly in mathematics, code, and formal logic. These settings make model accuracy easier to evaluate and optimize, but it remains unclear how far success under fixed problem specifications and stable evaluation criteria transfers to reasoning outside such domains. Real-world reasoning often proceeds under incomplete and revisable information: conclusions may be supported provisionally, defeated by counter-evidence, reinstated by further arguments, or revised when stronger reasons become available. Reasoning of this kind is generally referred to as defeasible reasoning. We introduce ArgGYM, a procedural benchmark and RLVR-compatible training environment for structured defeasible reasoning. ArgGYM decomposes this reasoning into twelve tasks and grounds task-specific scoring in a symbolic argumentation engine that computes the formal states used to evaluate model outputs. It includes a frozen benchmark of 1,440 verified instances across fifteen curriculum configurations, two argument preference orderings (weakest-link and last-link), and two set orderings (elitist and democratic), while the same generators and verifiers can produce fresh instances for evaluation that reduces dependence on static test sets and for verifiable-reward training. On the frozen benchmark, frontier and open-weight models show sharply different reasoning profiles: they can recover substantial parts of structured answers without solving the complete task, and performance declines in later curriculum configurations with longer dependencies and more interacting structures. We release the benchmark, generators, and verifiers for reproducible evaluation and RLVR training.

1 Introduction

Defeasible reasoning concerns conclusions that may be withdrawn as new or conflicting information arrives, but evaluation and training infrastructure for it remain less developed than for fixed-specification reasoning. ArgGYM addresses this gap with a multi-task, engine-verified environment, and the reported models show distinct strengths and weaknesses across reasoning operations.

1 Introduction

  • Defeasible conclusions are provisional: adding information can invalidate an earlier conclusion when stronger or conflicting reasons arise.The introduction frames this as non-monotonic reasoning under incomplete, conflicting, and revisable information.Source: §1 · pp. 1–2
  • The open problem is a unified executable environment that combines separately verified defeasible-reasoning tasks with frozen evaluation and fresh generation.The shared verification machinery is intended to support both reproducible comparison and mechanically rewarded training.Source: §1 · p. 2
  • Structured argumentation connects defeasible inference to arguments, attacks, preferences, and semantics, with states that can be computed mechanically.This makes it a basis for decomposing reasoning capabilities and verifying outputs.Source: §1 · p. 2
  • ArgGYM provides twelve ASPIC+-based tasks, a frozen benchmark of 1,440 verified instances, and generators and verifiers for fresh instances.Its configurations span fifteen curricula, two argument preference orderings, and two set orderings.Source: §1 · p. 2
  • Models with similar aggregate accuracy can have different task profiles, and success on formalization or support recovery does not ensure reliable performance on other operations.The reported weaknesses span semantic evaluation, defeat analysis, revision, and intervention.Source: §1 · p. 2

2 Related Work

Prior work evaluates defeasible reasoning, computational argumentation, and procedurally generated verifiable reasoning, but typically covers particular problems, formalisms, or task collections. ArgGYM brings shared formal semantics and task-specific verification to a broader structured-argumentation environment.

Defeasible reasoning

  • Defeasible-reasoning benchmarks cover natural-language evidence updates, defaults, source preferences, belief revision, and formal rule-based inference.The surveyed work generally targets particular inference problems or formalisms rather than a broad set of separately verifiable structured-argumentation operations.Source: §2 · p. 3

Computational argumentation

  • Computational argumentation research treats argumentation both as a model capability and as formal machinery for verifying, explaining, or revising outputs.The surveyed capability evaluations range from argument mining to abstract-argument acceptability; pipeline work uses argumentation to support claim verification and repairs.Source: §2 · p. 3

Procedural and verifiable reasoning

  • Procedural reasoning benchmarks use generated problems with programmatic verification, including recent defeasible-reasoning generators and verifiers.The examples span controlled logical reasoning, multi-task RLVR environments, defeasible abduction, belief updating, and structured DeLP knowledge bases.Source: §2 · p. 3

Positioning

  • ArgGYM combines shared ASPIC+ semantics, analysis and constructive-intervention tasks, and task-specific verification for frozen and fresh instances.This positioning is complementary to broader argumentation datasets and benchmarks focused on particular defeasible-reasoning problems.Source: §2 · pp. 3–4

3 ArgGYM

ArgGYM uses a common ASPIC+ substrate to generate and verify twelve structured defeasible-reasoning tasks, with controlled variation in problem structure and preferences. Its task-specific contracts apply to both a fixed benchmark and newly generated instances.

3.1 Formal Setting and Verification

  • ASPIC+ theories build arguments from premises and inference rules; attacks, preferences, and semantics determine which arguments and claims are accepted.Undermining targets ordinary premises, rebutting targets defeasible conclusions, and undercutting targets defeasible inference applicability.Source: §3.1 · p. 4
  • ArgGYM uses a pinned PyArg backend to compute and verify formal states, while the engine is unavailable to models during inference.For constructive tasks it executes submitted interventions and recomputes the resulting state; other outputs are scored against task-specific structured targets.Source: §3.1 · p. 4

3.2 Procedural Generation

  • Generators construct candidate instances, which pass structural gates and symbolic-engine checks before acceptance with validated verification targets.Fifteen curriculum configurations vary structural features such as derivation depth, branching, interacting attackers and defenders, and multi-goal interactions; they represent increasing richness, not guaranteed increasing empirical difficulty.Source: §3.2 · p. 4

3.3 Task Suite

  • The twelve-task suite spans representation, support recovery, diagnosis, semantic evaluation, revision, and intervention; its six constructive tasks are scored by executing legal interventions.Constructive solutions need not reproduce a stored intervention if they satisfy the task requirements; the other six tasks return structured outputs.Source: §3.3 · p. 5, Table 1 · p. 5

3.4 Frozen Benchmark

  • The frozen benchmark contains 1,440 instances across twelve tasks, fifteen curricula, two argument preference orderings, and two set orderings.The same scoring contracts apply to fresh instances, whose verifier outputs can provide mechanical RLVR rewards without a separate learned reward model.Source: §3.4 · p. 5

4 Experimental Setup

The evaluation compares model and inference configurations on the same frozen benchmark, using complete-task success as the primary metric alongside task-specific partial scores. Model-specific inference settings and serving configurations are not fully uniform.

4.1 Models and Inference Configuration

  • The evaluation covers 18 language-model variants from five families, yielding 42 model–reasoning configurations.The panel includes Gemma, GPT-OSS, Qwen, DeepSeek, and Gemini systems, with multiple inference-time reasoning settings where supported.Source: §4.1 · p. 6
  • Every configuration uses the same frozen benchmark, taskset, prompt version, response template, and scoring version, although model-specific limits and serving settings may differ.Inference settings are fixed within each model–reasoning configuration.Source: §4.1 · p. 6

4.2 Evaluation Metrics and Success Criteria

  • Complete-task success is the primary metric and requires satisfying the full task-specific output contract, including executed postconditions and consistency for constructive tasks.Formalization success is behavioral: the executable theory must reproduce reference engine-derived statuses over the named literals, not exactly reconstruct the directives.Source: §4.2 · p. 6
  • Each task also has a native partial-correctness score from 0 to 1, interpreted only within that task and never averaged across the benchmark.The score captures task-dependent properties such as partial output recovery, diagnostic accuracy, semantic progress, or intervention economy.Source: §4.2 · p. 6

5 Results

ArgGYM separates models across complete-task success and reveals distinct operation-specific profiles. Partial correctness often fails to compose into complete solutions, with performance also varying across structural curricula, preference regimes, and intervention conditions.

5.1 Overall Performance and Capability Profiles

  • 82.4% complete-task success for Gemini 3.8 Flash at high reasoning effort contrasts with near-zero performance in the smallest configurations.Across 18 model variants, aggregate performance does not imply a uniform capability profile.Source: §5.1 · p. 6, Table 2 · p. 7
  • Qwen3.5-27B with thinking enabled scores 88.7 native but only 35.8% complete success on status_query, illustrating partial correctness that fails to compose.DeepSeek-v4.1-Flash similarly scores 89.7 native and 34.2% complete success on status_query; Gemini 3.8 Flash reaches 93.6 native but 57.5% complete success on defeat_diagnosis.Source: §5.1 · p. 7
  • Complete-task success generally falls in later curriculum bands, while native correctness can remain comparatively high.For Qwen3.5-27B with thinking enabled on status_query, L1–L5 yields 72.5% complete success and 95.1 native, while L11–L15 yields 10.0% complete success and 84.5 native.Source: §5.1 · p. 7
  • Preference regimes change model behavior without a universal difficulty ordering, and independently generated ordering cells make the benchmark-wide comparison descriptive rather than causal.Gemini 3.8 Flash at high effort scores 92.9% under last-link versus 71.8% under weakest-link, while DeepSeek-v4.1-Flash reverses that pattern on claim_chain and defeat_diagnosis.Source: §5.1 · p. 7
  • A cheaper strict-rule intervention route does not uniformly improve constructive success, and models differ in whether they exploit the available affordance.Gemini 3.8 Flash at high effort falls from 86.7% in counter_argument to 60.0% in the strict-rule-enabled condition; Qwen3.5-9B with thinking enabled rises from 20.8% to 44.2% across the matched conditions.Source: §5.1 · pp. 7–8

6 Discussion

The discussion identifies global composition of argumentative information and constructive search over interventions as distinct bottlenecks. ArgGYM’s shared formal environment and fresh verified instances provide a way to test operation-specific improvements and their transfer.

6 Discussion

  • Correct local judgments may still misrepresent the overall argumentative state because attacks, preferences, and revisions interact across support and defeat relations.The gap between native and complete-task performance indicates that integration itself is a major source of failure, not merely lack of knowledge about individual components.Source: §6 · p. 8
  • Longer dependencies, interacting attackers and defenders, preference-sensitive conflicts, and multi-goal structure make complete solutions less reliable even when local correctness remains comparatively high.Task behavior depends on the interaction between the reasoning operation and the formal regime; weakest-link is not simply a harder version of last-link.Source: §6 · p. 8
  • Constructive tasks require searching backward from a desired outcome for an intervention, a capability distinct from evaluating the resulting formal state.An additional cheaper intervention operation changes the search problem, and models differ in recognizing and using the available route.Source: §6 · p. 8
  • ArgGYM’s shared ASPIC+ substrate and fresh verified instances let future work test operation-specific training gains, their transfer, and whether local improvements yield more reliable global states.The discussion identifies maintaining and composing distributed argumentative information, and searching interventions, as separable bottlenecks that benchmark-wide accuracy alone does not represent.Source: §6 · pp. 8–9

7 Limitations

The evaluation has limited model and language coverage, and the benchmark’s single framework and diagnostic curriculum and ordering analyses constrain how broadly its findings can be interpreted.

7 Limitations

  • The evaluation omits major proprietary API-served systems, whose capability profiles may differ from those tested.The paper names Anthropic Claude and OpenAI’s proprietary GPT-series models as examples.Source: §7 · p. 9
  • Almost all tasks use symbolic theories, leaving transfer to natural language uncertain; the formalization task uses template-generated descriptions.More varied language could help distinguish argumentative competence from lexical choice, semantic plausibility, and world knowledge.Source: §7 · p. 9
  • ArgGYM uses one structured-argumentation framework, so the findings are not established across alternative argumentation semantics.Most tasks use grounded semantics.Source: §7 · p. 9
  • Curriculum and ordering analyses are diagnostic: configurations can vary multiple properties, and ordering conditions use independently generated theories.Observed differences are systematic associations, not isolated causal effects of the ordering principle.Source: §7 · p. 9

8 Conclusion

ArgGYM decomposes structured defeasible reasoning into twelve engine-verified tasks, with a frozen benchmark and procedural generators for fresh instances. The conclusion reports distinct model weaknesses in composing argumentative states, handling interacting structures, preference regimes, and intervention routes.

8 Conclusion

  • ArgGYM combines twelve ASPIC+-based analysis and constructive tasks with a frozen 1,440-instance benchmark and generators for fresh verified instances.The same task generators, formal semantics, and verification contracts support evaluation and mechanically verifiable training problems.Source: §8 · p. 9
  • Models can recover locally correct components yet fail to compose full argumentative states; interacting structures, preference regimes, and intervention routes expose distinct weaknesses.The authors argue that final-answer accuracy alone obscures global argumentative composition and constructive search challenges.Source: §8 · p. 9

AI Use Statement

  • Generative AI tools assisted with manuscript preparation, literature discovery, and code work; authors designed the research and verified AI-assisted changes.The authors state that interpretation of results was also carried out by them.Source: AI Use Statement · pp. 9–10

Reproducibility Statement

  • The release includes the frozen benchmark, generators, scorers, verifiers, harness, and model configurations; fresh instances can be generated without modifying the frozen suite.The frozen benchmark remains separate from procedurally generated training instances.Source: Reproducibility Statement · p. 10

A.1 Formal Engine and Argumentation Configuration

  • Task-specific generators accept candidates only after structural and engine-computed checks, while PyArg computes formal states under varied argument and set preference orderings.The benchmark crosses last-link and weakest-link argument orderings with elitist and democratic set orderings.Source: §A.1 · p. 14
  • Most tasks use grounded semantics, while semantics_query probes additional semantics; stored formal states enable independent rescoring under task-specific verification contracts.A frozen-gold re-execution audit reproduced complete-task success with zero reported decoding, rescoring, ordering-propagation, or engine-invariant failures.Source: §A.1 · p. 15
  • Constructive tasks establish intervention minima within generator-defined candidate spaces, and successful answers are evaluated by execution rather than reference matching.A recorded minimum is not a claim of global minimality; successful interventions exceeding it receive lower native credit, and those exceeding twice it fail before execution.Source: §A.1 · pp. 15–16

A.2 Procedural Generation and Curriculum

  • The fifteen curriculum configurations vary task-relevant structures, so level number marks progression rather than guaranteed monotonic empirical difficulty.Generation uses recorded seeds and rejection statistics to support reproducibility within controlled task distributions.Source: §A.2 · p. 16

A.3 Task Definitions

The twelve tasks divide into structured analyses or formalizations and executable interventions. Their contracts assess either recovered structure and statuses or the consequences of submitted changes to an argumentation theory.

A.3 Task Definitions

  • Twelve tasks span six structured analyses or formalizations and six executable interventions, with correctness checked through task-specific contracts.Intervention consequences are recomputed by the formal engine.Source: §A.3 · p. 16
  • Formalization translates controlled natural-language descriptions into executable ASPIC+ theories; complete success requires matching reference statuses across all named literals, not exact directives.The native score also measures structural and type-sensitive agreement with the reference theory.Source: §A.3 · pp. 16–17
  • claim_chain recovers all required support directives in dependency-consistent order, while defeat_diagnosis identifies where support fails and the relevant defeat type.Diagnosis may also require recognizing when an apparent attack on a defeater is itself defeated.Source: §A.3 · p. 17
  • status_query labels queried claims as justified, overruled, or undecided; semantics_query tests acceptance under grounded, eager, stable, and preferred semantics.Stable instances may have no stable extension, which models must distinguish from non-acceptance.Source: §A.3 · p. 17
  • perturbation identifies claims whose statuses change after an update, while preference_construction seeks status changes using preferences without adding premises or rules.Perturbation instances retain unchanged claims to distinguish real changes from spurious predictions.Source: §A.3 · p. 17
  • counter_argument and counter_argument_strict share matched theories and goals, but only the latter permits strict-rule additions as an intervention.Across 120 matched pairs, the strict-enabled condition has a recorded candidate-space minimum lower by one directive in 112 pairs and by two in eight.Source: §A.3 · p. 18
  • attack, defence, and attack_defense require executable changes that respectively overrule a target, justify an attacked target, or meet both outcomes together.attack_defense requires both postconditions simultaneously and a consistent resulting theory.Source: §A.3 · p. 18

B Task Verification

Task Verification separates complete-task success from task-specific partial-credit scores, then applies different scoring contracts to structured predictions, diagnoses, formalizations, and interventions. The examples show that claim-status outputs and failure-route explanations encode distinct levels of argumentative information.

B Task Verification

  • Pair-valued tasks score exact key–status matches with F1, and complete success requires exact equality with the gold map.The maps represent queried claims, claim–semantics pairs, or status changes, depending on the task.Source: B Task Verification · p. 18
  • Claim-chain scoring combines directive-content overlap with dependency-order correctness, while complete success requires all and only the required directives in a consistent order.The scorer also tracks whether submitted rules appear after their antecedents.Source: B Task Verification · pp. 18–19
  • Defeat-diagnosis scoring weights failure-point F1 at 0.85 and target-status correctness at 0.15, adding survival-explanation F1 at 0.25 when required.Complete success requires exact agreement on target status, failure points and attack types, and any required survival explanations.Source: B Task Verification · p. 19
  • Formalization receives separate behavioral, structural, and type-decision scores, but complete success requires matching engine-derived statuses for every literal named by the reference theory.Matching only queried statuses is insufficient, and exact reconstruction of the reference directives is not required.Source: B Task Verification · p. 19
  • Constructive interventions are executed against the base theory, and success requires all requested postconditions plus consistency of the resulting theory.Successful interventions can earn efficiency credit against a verified candidate-space minimum; that minimum is not claimed to be globally minimal.Source: B Task Verification · p. 20
  • Complete-task success is the cross-task comparison metric, while task-native scores capture partial correctness and are interpreted only within their task.Native scores are not averaged into a benchmark-wide score because they represent different notions of partial correctness.Source: B Task Verification · pp. 18, 20

C.1 Grounded Claim-Status

  • The grounded claim-status example requires a justified, overruled, or undecided label for each queried claim, matching the engine-derived reference statuses.The example includes all three statuses among its six claims.Source: §C.1 · p. 21

C.2 Defeat Diagnosis

  • The defeat-diagnosis example requires locating failed support routes and distinguishing undermine, undercut, and rebut attacks, including a higher-order survival explanation.That explanation records when an attack on a defeater is itself defeated.Source: §C.2 · pp. 21–22

C.3 Strict Counterargument Ablation

Across most model configurations, complete-task success decreases in later curriculum bands as generated structures become richer. The section also describes the task-level reporting, evaluation configurations, and a matched ablation that varies the permitted intervention language.

C.3 Strict Counterargument Ablation

  • The strict counterargument ablation holds the theory and semantic objective fixed while varying whether strict-rule additions are permitted.A verified reference intervention for the strict variant uses two directives, the recorded minimum in its generator-defined candidate space.Source: §C.3 · pp. 22, 24

D.1 Model and Inference Configurations

  • The evaluation covers 18 model variants under 42 model–reasoning configurations, with reasoning controls and inference settings varying by model.For locally served models, context denotes the configured max_model_len; Qwen3.8-27B uses low, medium, and xhigh reasoning-effort settings.Source: §D.1 · p. 24

D.2 Task-Level Performance

  • Tables 4 and 5 report complete-task success alongside task-native scores, which retain task-specific meanings and should be compared only within the same task.The tables cover analysis and evaluation tasks and constructive intervention tasks, respectively.Source: §D.2 · p. 24, Table 4 · p. 25, Table 5 · p. 26

D.3 Curriculum Analysis

  • Complete-task success decreases in later curriculum bands across most configurations, while stronger models and higher reasoning settings generally retain more performance as structures become richer.The three five-configuration bands are not a calibrated one-dimensional difficulty scale.Source: §D.3 · p. 27

D.3.1 Task-Specific Curriculum Profiles

Across curriculum bands, complete-task success can fall much more sharply than task-native partial correctness, while constructive operations respond unevenly rather than following one universal difficulty scale.

D.3.1 Task-Specific Curriculum Profiles

  • Each task-specific band contains 40 frozen instances per model–reasoning configuration, and task-native scores retain task-specific semantics for within-task comparisons only.Tables 6–12 cover complete-task success across bands and task-specific success alongside task-native scores.Source: §D.3.1 · p. 27, Table 6 · p. 28, Table 7 · p. 29
  • 72.5% complete success with a 95.1 native score in L1–L5 falls to 10.0% with an 84.5 native score in L11–L15 for Qwen3.5-27B with thinking enabled on status_query.The analysis/evaluation tables report task-specific results across L1–L5, L6–L10, and L11–L15.Source: §D.3.1 · p. 27, Table 7 · p. 29, Table 9 · p. 31
  • Constructive tasks show uneven profiles: some intervention types remain comparatively robust for stronger models, while strict-rule counter-arguments remain challenging for many systems.Other constructive operations can improve substantially, and occasional changes across bands are non-monotonic.Source: §D.3.1 · p. 27, Table 8 · p. 30, Table 10 · p. 32

D.4 Argument-Ordering Analysis

Argument-ordering comparisons show substantial performance differences across preference regimes, but set-ordering contrasts are often inactive and task-level reversals complicate aggregate readings. Protocol diagnostics identify severe truncation and answer-region compliance problems in two small Qwen configurations, with more modest conditioned-success shifts elsewhere.

D.4 Argument-Ordering Analysis

  • Under last-link, democratic and elitist variants induce the same defeat relation on eleven of twelve tasks; status_query is the designed exception.A same-theory diagnostic found that switching the link principle changed grounded status maps in 107 of 120 status_query theories and 101 of 120 defeat_diagnosis theories, and in all 120 theories for three other tasks.Source: §D.4 · p. 35
  • 92.9% under last-link versus 71.8% under weakest-link for Gemini 3.8 Flash at high effort illustrates large benchmark-wide differences between argument comparison principles.Qwen3.5-27B with thinking enabled scores 50.1% versus 28.5%, and DeepSeek-v4.1-Flash scores 50.7% versus 39.3%.Source: §D.4 · p. 35, Table 13 · p. 36
  • Benchmark-wide democratic–elitist differences are not a uniform estimate of model sensitivity because the distinction is formally inactive in many cells, especially under last-link.The benchmark-wide aggregates can mix set-ordering-sensitive instances with variation among independently generated theories.Source: §D.4 · p. 35

D.4.1 Task-Specific Last-Link and Weakest-Link Results

  • DeepSeek-v4.1-Flash reverses the aggregate direction on claim_chain (66.7% versus 53.3%) and defeat_diagnosis (73.3% versus 28.3%), so weakest-link is not uniformly harder.Tables 14 and 15 report last-link and weakest-link success separately by task.Source: §D.4 · p. 35, Table 14 · p. 37, Table 15 · p. 38

D.5 Generation and Answer-Protocol Diagnostics

  • 99.2% and 82.6% generation truncation for Qwen3.5-0.8B and Qwen3.5-2B, respectively, accompanies answer-region compliance of 32.4% and 28.7%.Across remaining configurations, conditioning on compliant responses changes success only modestly; canonical success remains because a valid submitted answer is part of the benchmark contract.Source: §D.5 · p. 39, Table 16 · p. 40
Loading 2609.38409v1…