PaperlayerView exact revision on arXiv

Source-linked AI summary

Beyond QASecClaw: Agent Scaling, Verifier Feedback, and Evidence Reliability in Software Assurance

S M Abdulla Al Mamun, Akif Islam, Mohd. Ruhul Ameen

arXiv:2610.36947v1cs.SEcs.AI

TL;DR

The paper asks whether additional specialist model contexts improve software assurance when deterministic evidence is available, and studies this across warning assessment, verifier feedback, evidence applicability, and defect discovery. Across the tested settings, context scaling did not show a consistent assurance benefit, raw verifier feedback improved correct verdicts while also increasing incorrect ones, and deterministic evidence admission remained useful within the tested constructions.

  • Problem

    The paper asks whether specialist LLM contexts add assurance value over deterministic checks when evidence is fixed, given that false clearance can dismiss a real defect as benign.

    Source: §I · p. 1

  • Method

    The study compares five experimental settings and model configurations with deterministic controls, including single-turn specialist contexts that assess shared task evidence.

    Source: §I · p. 1, A. Assessment pipeline and decision… · p. 2

  • Results

    In the tested Java settings, specialist contexts showed no consistent assurance benefit; raw verifier feedback raised correct model verdicts but also incorrect verdicts, while construction-specific checks removed observed unsupported acceptances.

    Source: B. RQ2: Does verifier feedback help… · p. 4, §V · p. 5, §VII · p. 6

  • Takeaways & Limitations

    The tested findings support retaining deterministic evidence admission when the required checks are available, while motivating broader, budget-matched evaluation rather than a general claim against multi-agent assurance.

    Source: §VII · p. 6

    Input/output caps varied with team size, actual token use differed, and the OWASP ten-context arm omitted 64 cases, limiting equal-coverage scaling comparisons.

    Source: §VI · p. 5

Abstract

from arXiv · show

Can additional specialist language-model contexts improve software assurance when deterministic tool evidence is already available? We study this question through five experiments spanning authored Java warning controls, OWASP Benchmark assessment, Defects4J test generation, SV-COMP assertion verdicts, and deliberately misleading evidence packages. The evaluated systems use Qwen2.5-Coder-7B-Instruct, with a 1.5B sensitivity analysis, and complete 13,638 model requests. On eight related development warnings, increasing the context count from 1 to 50 increases token use 49-fold without improving unsafe clearance. On 160 OWASP cases, model configurations trade clearance against unresolved outcomes; the ten-context arm assesses only 96 cases. On 32 SV-COMP tasks, raw verifier feedback raises mean correct model verdicts from 12.7 to 22.0, but also raises incorrect verdicts from one to seven; a JBMC-plus-JVM validation baseline returns 26 correct verdicts and six unresolved outcomes. On two sets of 120 evidence packages, models reject 70-100% of applicable counterexamples, while construction-specific scope checks classify every package correctly. No target defect is discovered in three Defects4J bugs, one unsupported by the test adapter. These descriptive results support deterministic evidence admission for the tested settings, while exposing limits of verdict aggregation, feedback interpretation, and the available evaluation coverage.

I. Introduction

The paper asks whether specialist LLM contexts add assurance value when deterministic evidence is available, especially where false clearance is more costly than a missed answer. It examines context scaling, verifier feedback, evidence applicability, and defect discovery through an exploratory five-experiment study.

I. Introduction

  • False clearance is the costly assurance error: dismissing a real defect as benign can make added agent confidence insufficient without added evidence.Prior work suggests voting across more agents can improve accuracy, while scaling studies also report diminishing or negative returns when coordination overhead and correlated errors are counted –[9].Source: §I · p. 1
  • The central question is whether additional LLM contexts improve assurance over deterministic checks when evidence is fixed.The paper builds on the warning-assessment question raised by QASecClaw but does not claim to outperform it.Source: §I · p. 1
  • The research questions test whether more contexts reduce unsafe clearance without inflating abstention or cost, and whether verifier feedback improves verdict reliability.They also ask whether models recognize inapplicable formal evidence and discover defects without a supplied warning.Source: §I · p. 1
  • The study separates warning clearance, assertion verdicts, evidence applicability, and defect discovery across five experiments, comparing model configurations with deterministic controls.It reports abstention, cost, and incomplete coverage; the work is an empirical diagnosis, not a new general verifier or a test of every multi-agent architecture.Source: §I · p. 1

II. Related Work

Related work spans LLM warning triage, artifact generation for verification, and multi-agent assurance. This study focuses instead on whether models interpret fixed evidence reliably and compares prior systems as context, not as reproduced baselines.

II. Related Work

  • QASecClaw uses an LLM agent to filter Semgrep warnings, while Evident leaves final disposition to Frama-C/Eva and uses LLMs to build harnesses [1], [4].MAGS and VERDICT obtain guarantees through Dafny translation and contract reconciliation [5], [6].Source: §II · p. 1
  • Earlier warning-adjudication results use different reasoning models and protocols, making model capacity and adjudication policy relevant alternative explanations for comparisons [3].Prior studies also identify leakage in false-alarm classification and weak generalization on realistic vulnerability data,.Source: §II · pp. 1–2
  • Table I frames closest systems and their investigated boundaries; its prior results are contextual comparisons, not reproduced baselines.The prose contrasts warning filtering, harness generation, verified translation, and protocol verification.Source: §II · p. 1, Table I · p. 2
  • Prior systems explore different assurance boundaries: TraceFix verifies coordination protocols, while Lemur, SpecGen, and ESBMC-coupled LLMs generate artifacts for checking [10], [13]–[15].This study's E3 asks a model to interpret an unchanged program and raw JBMC feedback; it does not evaluate artifact-generation benefits.Source: §II · p. 2

III. Study Design

The study uses separate experimental interfaces and tool adapters rather than one fused system. Its model configurations assess shared evidence, while deterministic baselines bypass the model and construction-specific gates check proposed dispositions.

A. Assessment pipeline and decision semantics

  • Each specialist is a fresh, single-turn context sharing a base model and task evidence; contexts do not message, invoke tools interactively, or repair programs.Thus k counts prompted assessments, not autonomous tool-using agents; a strict majority retains or clears, otherwise the outcome is unresolved, including missing or invalid answers.Source: A. Assessment pipeline and decision… · p. 2
  • The E1/E4 postprocessor preserves a proposed clearance only when code and property hashes match and JBMC succeeds on the declared domain with unwinding assertions enabled.Otherwise, matching counterexamples change clearance to retained and absent evidence to unresolved; retentions and abstentions remain unchanged.Source: A. Assessment pipeline and decision… · p. 2
  • The experimental interfaces use the relevant adapter rather than fusing tools into one end-to-end system; deterministic baselines bypass the model.E5 reports accept/reject/unresolved instead of warning dispositions.Source: Figure 1 · p. 2
  • The E1/E4 gate trusts controls checked exhaustively on the JVM and the backend parser; it does not prove harness equivalence or implement general dependency-graph reconciliation.Gate-on and gate-off arms reuse identical model outputs.Source: A. Assessment pipeline and decision… · p. 2
  • E5 accepts a proposed package only after checking hashes, full input-domain coverage, required obligations, exact canonical harness text, and established callee assumptions.This construction-specific validator is not a general proof checker; hashes establish identity, not semantic validity.Source: A. Assessment pipeline and decision… · p. 2

B. Metrics

The study reports separate safety, clearance, and abstention measures, then describes the datasets, splits, and task-selection rules used across its experiments.

B. Metrics

  • Unsafe clearance (UC), benign clearance (BC), and unresolved share (UR) are reported separately rather than collapsed into accuracy.UC should decrease while BC increases; UR exposes abstention, and review workload is the fraction retained or unresolved rather than measured reviewer time.Source: B. Metrics · p. 2
  • Seeds, variants, and packages are clustered observations, so the study reports counts and seed ranges without significance tests or case-independent confidence intervals.The ten-context OWASP arm leaves 64 of 160 cases unassessed and unresolved; no equal-coverage scaling effect is inferred.Source: B. Metrics · p. 2

C. Data, splits and experiments

  • The Juliet audit covers 28,881 cases in 112 CWE categories, split by family components into development, validation, and evaluation sets without shared testcase sources or duplicate complete contexts.All CWE476 families were reserved for development; no held-out Juliet model result is reported, and the eight warning controls came from one authored semantic template rather than Juliet.Source: C. Data, splits and experiments · p. 2
  • The experiment inventory is summarized in Table II as data, scale, and model-request counts.The caption defines “Req.” as model requests but supplies no cell values in the cited text.Source: Table II · p. 3
  • OWASP assessment sampled 160 cases by report status and vulnerability status; E2 used three reproduced Defects4J Cli bugs, including one whose target API the adapter cannot expose.E3 selected the first 32 eligible hashes from 111 structurally admitted SV-COMP Java assertion tasks; E5 used 20 null-dereference programs across five templates plus disjoint held-out templates.Source: C. Data, splits and experiments · p. 3

D. Models and execution

The experiments use Qwen2.5-Coder-7B-Instruct, with a 1.5B sensitivity analysis, and set different token limits by experiment and context count.

D. Models and execution

  • Inference used Qwen2.5-Coder-7B-Instruct, with Qwen2.5-Coder-1.5B-Instruct used for E4 sensitivity.Sampling used temperature 0.2, top-p 0.95, bfloat16 weights, and Transformers 4.51.3.Source: D. Models and execution · p. 3
  • E1/E4 and OWASP context limits share upper bounds of min(8192, floor(65536/k)) input and min(512, floor(8192/k)) output tokens.These are not equal actual budgets; E2’s five-context arm also has a larger budget, so the study reports observed cost–outcome trade-offs rather than budget-matched causal effects.Source: D. Models and execution · p. 3
  • Table III covers E1 development controls across three seeds, with four defects and four benign warnings per seed.Source: Table III · p. 3
  • The study completed 13,638 final requests, excluding failed attempts and gate ablations; E2 also recorded 54 input-cap rejections and 48 out-of-memory failures.Other failed provisioning attempts were archived separately.Source: D. Models and execution · p. 3

IV. Results

Across the authored controls and OWASP assessment, additional contexts did not produce consistent clearance gains, while the scope gate prevented observed false clearances on the controls.

A. RQ1: Do more contexts reduce unsafe clearance?

  • The scope gate removed every unsafe clearance and kept every benign clearance, but the verifier-only baseline already decided all eight authored controls correctly.Source: A. RQ1: Do more contexts reduce unsafe… · p. 3
  • 25,938 to 1,277,612 tokens (49×) from k=1 to k=50 left the 7B model clearing 4/4 defects in most seeds; rare drops came from abstentions, not correct retentions.Unsafe clearance stayed near 100% as token use increased, while the deterministic gate held it at zero for every k.Source: A. RQ1: Do more contexts reduce unsafe… · p. 3, Figure 2 · p. 4
  • On the 160-case OWASP sample, single-context unsafe clearance was 33–36% and benign clearance 30–37%; five contexts raised unsafe clearance to 39–41% with 51–53% unresolved.For ten contexts, 111/113 unresolved outcomes included 64 unassessed cases per seed; 47/49 of the 96 assessed cases were unresolved.Source: A. RQ1: Do more contexts reduce unsafe… · p. 3, Table IV · p. 4
  • OWASP showed no consistent joint improvement, and its ten-context result is confounded by assessment coverage; across all 2,740 benchmark cases, clear-without-signal yielded 2.8% unsafe and 53.3% benign clearance.The assessment sample deliberately includes all 40 unflagged real vulnerabilities; sample rates must not be extrapolated to the full benchmark.Source: A. RQ1: Do more contexts reduce unsafe… · p. 4

B. RQ2: Does verifier feedback help the model?

On 32 frozen SV-COMP tasks, raw JBMC feedback increased both correct and incorrect model verdicts; the deterministic comparator additionally used JVM validation. The experiment evaluates verdict prediction rather than artifact generation.

B. RQ2: Does verifier feedback help the model?

  • JBMC calibration on 111 eligible tasks yielded 89 decisive outcomes, all agreeing with expected verdicts, and 22 unresolved outcomes.The unresolved set included 12 counterexamples not reproduced on the JVM, all involving String or library models, eight different-property failures, one bounded result, and one timeout.Source: B. RQ2: Does verifier feedback help… · p. 4
  • 22.0 correct and 7 incorrect verdicts per seed with raw feedback contrasted with 12.7 correct, 1 incorrect, and 18.3 unresolved without feedback; JBMC-plus-JVM returned 26 correct and 6 unresolved.Source: Figure 3 · p. 4, B. RQ2: Does verifier feedback help… · p. 4
  • Model feedback lacked JVM replay outcomes and a full validated witness, so raw feedback did not test the model against identical, fully validated evidence.The experiment evaluates verdict prediction, not agent-generated invariants or proof strategies.Source: B. RQ2: Does verifier feedback help… · p. 4

C. RQ3: Can models recognise misleading evidence?

Models often rejected applicable counterexample evidence, while the construction-specific scope validator classified the tested packages correctly. A worked example distinguishes evidence of a defect from evidence that does not apply to the original program and property.

C. RQ3: Can models recognise misleading evidence?

  • Models rejected 70–100% of valid counterexample packages, while the scope validator accepted all 20 clean and rejected all 100 corrupted packages in both sets.The model’s gate removed erroneous acceptances but did not repair its rejection of valid evidence.Source: C. RQ3: Can models recognise… · p. 4, Figure 4 · p. 5

1) Worked applicability example:

  • A counterexample for the unchanged full-domain program is applicable evidence of a defect, whereas excluding the failing input makes solver success inapplicable to that claim.The validator checks whether the recorded input domain matches, without judging the model’s explanation.Source: 1) Worked applicability example · pp. 4–5
  • Without feedback, clean acceptance was 3–4/20 per seed; with feedback it was 2–3/20 in development and 0/20 on the second template set.The gate preserves model rejections because it only vetoes unsupported acceptances.Source: 1) Worked applicability example · p. 5

D. RQ4: Can models discover defects unaided?

The unaided Defects4J experiment discovered no target defect, and the discussion frames deterministic gating as a consistency check rather than new verification capability. The study also limits its scaling conclusions to the tested catalogue and aggregation rule.

D. RQ4: Can models discover defects unaided?

  • No generated test or any of 180 deterministic public-API contract tests failed on a buggy revision and passed on its fix.Cli-3’s target API is unsupported by the adapter, and held-out Lang reproduction failed under JDK 11.Source: D. RQ4: Can models discover defects… · p. 5

V. Discussion

  • Across E1 and E4, postprocessing removed 161 unsafe clearances; across both E5 sets, it removed 12 erroneous acceptances.These were repeated decisions, not distinct defects; stronger tools-only baselines already had the necessary evidence.Source: §V · p. 5
  • The scaling experiment challenges its fixed role catalogue and aggregation rule, not specialised teams with complementary tools, iterative communication, or stronger models.Error correlation was not estimated, and role diversity was not isolated from sampling.Source: §V · p. 5
  • Applicability evaluations should measure acceptance of valid counterexamples as well as rejection of invalid assurance claims.The known E5 constructions make deterministic scope checks unusually strong; independently authored harnesses and applicable benign proofs are needed to assess general applicability reasoning.Source: §V · p. 5

VI. Threats to Validity

The reported findings are bounded by construct, internal, external, and conclusion-validity constraints, including clustered observations, limited model and benchmark coverage, and unassessed or unsupported cases.

Construct validity

  • OWASP is scored at case/CWE level, includes unflagged cases, and is not pure warning filtering; E5 also confounds applicability with outcome type.The canonical-text validator may reject equivalent unfamiliar harnesses, and E2’s adapter cannot exercise Cli-3’s target API.Source: §VI · p. 5

Internal validity

  • Development controls were revised after zero-warning attempts, input/output caps varied with team size, and OWASP’s ten-context arm omitted 64 cases.The secondary E2 parser was selected after six completed outputs, and an independent implementation audit remains outstanding.Source: §VI · p. 5

External validity

  • External validity is limited by evaluation of two small models from one family, one synthetic OWASP application, and one project for E2.E3 admits 111 of 1,033 manifests; E5 templates were developer-authored, and public benchmark contamination remains possible.Source: §VI · pp. 5–6

Conclusion validity

  • Seeds, templates, and packages are dependent observations, and no effect-size threshold or power analysis was fixed for this exploratory report.The authors make no significance, equivalence, or universal soundness claim; successful JBMC outcomes remain conditional on its library models and parser.Source: §VI · p. 6

VII. Conclusion

In the tested Java settings, additional single-turn specialist contexts did not consistently improve assurance over deterministic controls; verifier feedback increased both correct and incorrect verdicts. The repository archives research materials, but the manuscript does not claim a public artifact release.

VII. Conclusion

  • In the tested Java settings, additional single-turn specialist contexts did not produce a consistent assurance benefit over available deterministic controls.Raw verifier feedback increased correct model verdicts but also increased incorrect verdicts; construction-specific scope checks prevented observed unsupported acceptances, while models often rejected applicable counterexamples.Source: §VII · p. 6

Data Availability

  • The private research repository archives executable adapters, configuration pins, aggregate receipts, selection manifests, and SHA-256 provenance, but no public artifact release is claimed.A review package requires access arrangements and upstream licence checks; pending experiments are not reported as completed.Source: Data Availability · p. 6
Loading 2610.36947v1…