PaperlayerView exact revision on arXiv

Source-linked AI summary

From Prose to Properties: Testing Research Claims with ARATest for Agent-Native Science

Yifeng He, Jiachen Liu, Hao Chen

arXiv:2610.30495v1cs.AIcs.SE

TL;DR

Research claims state their implied properties only in prose, limiting direct tests of which evidence would falsify them. ARATest binds claims to typed, executable property skeletons and tests them against reported evidence and fresh cases. It detected all seeded table faults without false alarms, and fresh runs exposed behaviors unavailable in reported evidence.

  • Problem

    Research claims imply properties but state them only in prose, leaving no explicit test for which evidence would falsify them.

    Source: §1 · pp. 1–2

  • Method

    ARATest binds each claim to a typed property skeleton and checks the fixed property using reported-evidence or auto-research generators.

    Source: §1 · p. 2

  • Results

    ARATest detected all 553 seeded faults with no false alarms on 19 valid controls; two LLM judges detected 342 and 319 faults on the same evidence.

    Source: §1 · p. 3

  • Takeaways & Limitations

    The same explicit property can be checked against reported evidence and fresh cases, while fresh runs can expose behaviors the reported evidence could not show.

    Source: §1 · pp. 2–3

    The evaluation used AI reviewers rather than human experts, so it does not establish that declarations, designs, or verdicts would survive independent human review.

    Source: §5.5 · p. 24

Abstract

from arXiv · show

AI agents now run experiments and report findings, so research produces claims faster than researchers can check them. Each empirical claim implies a property that must hold over its cases, but it states that property only in prose. Without an explicit property, no test can decide which evidence would falsify a claim, so validation cannot keep pace with the claims agents produce. To make claims testable, we approximate a claim's semantics by abstracting its property skeleton, a parameterized relation that recurs across claims. We present ARATest, a property-based testing library that checks these skeletons as executable tests. A typed declaration binds a claim to a skeleton and fixes the claim's compared quantities, cases, scope, and numerical policy. A shared case type makes every generator supply cases in the claim's statistical unit. A three-valued semantics assigns each property one of three verdicts: holds, violated, or inconclusive. Every violation carries a replayable witness. A default generator reads the evidence that agent-native research artifacts (ARA) link to each claim, and auto-research generators dispatch an agent to run released code for fresh cases. Our DissClaimer plugin supplies that agent and runs these generators as continuous testing. Of 243 claims in 33 ARA artifacts, 54 received faithful declarations bound to evidence: 32 held, eight were violated, and 14 remained inconclusive. Two violations exposed errors in published papers that their authors confirmed. ARATest detected all 553 seeded faults without a false alarm on 19 valid controls, outperforming two LLM judges. Fresh runs exposed behaviors that reported evidence could not show. These results suggest that one fixed test can check explicit claim properties against both reported and fresh evidence.

1 Introduction

As agents accelerate research, claims remain difficult to validate because their implied properties are stated only in prose. ARATest binds claims to typed, executable properties and checks them against reported evidence and fresh experimental cases.

1 Introduction

  • Research claims are hard to validate at agent speed because they state implied properties only in prose, leaving LLM judges to assess them.The introduction describes those judges as slow, costly, and inconsistent across runs on the same evidence.Source: §1 · pp. 1–2
  • A faithful test must preserve both a claim’s comparison and its observation scope, so an excluded dataset is not mistaken for a counterexample.Table 1 illustrates the boundary: the claim excludes ImageNet-v2 despite a reversal there.Source: §1 · p. 2, Table 1 · p. 2
  • Typed declarations bind reusable property skeletons to a claim’s compared quantities, cases, scope, and numerical policy.Reported-evidence and auto-research generators supply cases to the same property; violations carry replayable witnesses, while passes corroborate only checked cases.Source: §1 · p. 2
  • Of 243 claims across 33 artifacts, 54 were fully bound to evidence; ARATest decided 40, with 32 holding, eight contradicted, and 14 inconclusive.Two violations were errors in published papers confirmed by their authors; four other violations came from the compiled artifact.Source: §1 · pp. 2–3
  • ARATest detected all 553 seeded faults with no false alarms on 19 valid controls; LLM judges detected 342 and 319 faults on the same evidence.The judges took nine to ten times longer per check; two violations in published papers were confirmed by their authors.Source: §1 · p. 3

2 Background

Agent-native research artifacts record claims, evidence, and provenance, but their claim fields do not themselves provide an executable oracle. Property-based testing supplies properties, generators, and an oracle, while property skeletons capture reusable shapes that must also specify applicability and comparison rules.

2.1 Structured research artifacts

  • ARA claim entries record assertions, scope, falsification criteria, evidence links, and provenance, but do not specify an executable oracle.ARATest adds a typed contract while retaining the source claim and its provenance for fidelity review.Source: §2.1 · p. 3

2.2 Property-based testing and property skeletons

  • Property-based testing combines a property, a generator of inputs, and an oracle; a failing input is a replayable counterexample.Passing generated cases supports the property only on those cases, not on all possible inputs.Source: §2.2 · pp. 3–4
  • A property skeleton parameterizes a recurring relation, but a valid test also needs applicability conditions and a comparison rule.Research claims additionally require scope: a reversal outside that scope marks a boundary, not a counterexample.Source: §2.2 · p. 4

3 Property-based testing for research claims

ARATest turns a claim into a fixed, typed property that can be checked against reported evidence or fresh experimental cases. Its declarations and generators preserve the claim’s operands, scope, decision policy, and statistical unit.

3 Property-based testing for research claims

  • One fixed property checks cases from reported evidence or fresh experiments, while retaining the evidence that decides each case.The declaration preserves the claim’s operands, scope, and decision rule as generators change the case source.Source: §3 · p. 4, Figure 1 · p. 4

3.1 The claim-testing contract

  • A typed contract fixes admissible cases, selected observations, comparison, aggregation, and uncertainty policy; outcomes are holds, violated, or inconclusive.Cases retain the claim’s statistical unit; universal claims fail if any admitted case fails, while count claims require enough passing cases. Fixed evidence and a fixed declaration yield a repeatable verdict, and models do not decide it.Source: §3.1 · pp. 5–6

3.2 Abstracting reusable property skeletons

  • Reusable property skeletons encode recurring relations, while declarations supply the scientific operands and obligations that determine their scope.The catalog classifies 136 claims from 23 artifacts, but this classification is not whole-claim coverage; unsupported property kinds remain untested.Source: §3.2 · p. 7, Figure 2 · p. 7

3.3 Instantiating a skeleton from an ARA claim

  • A declaration adds Kind and Domain to an ARA claim: Kind selects a supported skeleton, and Domain binds its quantities, scope, comparator, aggregation, and policy.Declarations are fidelity-reviewed because a bound declaration can still select the wrong metric or an easier fragment of the claim.Source: §3.3 · pp. 7–8

3.4 Generating cases from reported evidence

  • The reported-evidence generator enumerates declared table cells and applies fixed rules using the comparator and displayed precision.It does not sample or run experiments; approximate or insufficiently separated values can be inconclusive, and widened cases are checked only after in-scope pairs pass.Source: §3.4 · pp. 8–9, Table 3 · p. 9

3.5 Generating cases with auto-research

  • Auto-research generators dispatch an agent to run claim-bound experiment families on released code and return fresh cases for the same property.Family controls preserve the declared task and statistical unit; failures on this path are feedback rather than claim refutations.Source: §3.5 · pp. 9–10, Figure 4 · p. 10

3.5.1 Generators and experiment families

  • Four default family types vary seeds, row order, null data, or an admitted configuration value; the research agent binds applicable families to claims.For each instance, the agent first attempts to reproduce the reported result, then runs a frozen plan, varies the specified dimension, and returns logged measurements and controls. Retained plans and cases support replay.Source: §3.5.1 · pp. 10–11, §3.5.2 · pp. 11–12

3.6 What a verdict does and does not establish

  • A verdict decides the instantiated property on recorded evidence, not the source claim, and a violation retains a replayable witness.Readers must verify declaration fidelity and, for fresh runs, that the agent implemented the family and preserved its controls; by default, auto-research violations are feedback, not status recommendations.Source: §3.6 · p. 12

4 Using ARATest

ARATest walks through declaring claims, checking them against reported evidence, replaying violations, and binding experiment families for continuous testing. Its extension interface lets users add new families and relations without editing the library.

4.1 Declaring a claim

  • A claim declaration names evidence-table cells and binds C01 to a comparative property over LCA and Top-1 across the four datasets in the claim.The walkthrough declaration covers only the comparison; a complete declaration would also check LCA’s R^2 and Pearson correlation against 0.7.Source: §4.1 · p. 13, Figure 6 · p. 13

4.2 Testing the claim

  • C01 holds on its four named datasets; ImageNet-v2 reverses the comparison but is classified as a documented boundary, not a fault.The command returns exit code 0 when all declared claims hold, 1 when any is violated, and 4 when a claim remains undecided.Source: §4.2 · p. 13, Figure 7 · p. 14

4.3 Replaying a violation

  • APT’s C02 is violated because its reported RoBERTa speedup of 8.4× conflicts with a cell-derived ratio of 8.660–8.662.The declaration also checks the stated 8.2× T5 speedup; both properties are violated, and the check saves a replay record.Source: §4.3 · p. 14, Figure 8 · p. 14

4.4 Binding experiment families

  • Reported evidence cannot test unmeasured behavior, so bound experiment families supply fresh cases that an agent runs on released code.A continuous campaign dispatches the agent, checks returned cases, and lists violations with records and replay commands.Source: §4.4 · p. 15

4.5 Extending the library

  • Users extend ARATest by installing packages that register experiment families, relations, agents, or commands through Python entry points.A family’s case model fixes the type of every supplied case; a relation implements binding, observation, folding, and refinement.Source: §4.5 · pp. 15–16, Figure 10 · p. 16

5 Evaluation

The evaluation tests declaration fidelity and fault detection on reported evidence, then examines fresh experiments on released author code. Subjects and runs are restricted to artifacts whose code and execution requirements meet the study’s criteria.

5.1 Experimental setup

  • The study drew subjects from 33 ARA artifacts and divided evaluation into reported-evidence integration tests and continuous tests on author code.RQ1 examined all 243 claims after withholding existing declarations; RQ2 seeded faults into reported evidence, while RQ3 ran tests on author code.Source: §5 · p. 16, §5.1 · p. 16, §5.1.1 · p. 17

5.1.1 Integration testing on reported evidence

  • RQ2 seeded 553 mechanically validated faults into SEMA and CFG, paired records with originals and controls, and compared deterministic checking with two LLM judges.The 1,124 records collapsed to 504 packets: 485 violating and 19 holding; judges received the same evidence, and valid-witness detection determined scoring.Source: §5.1.1 · pp. 17–18, Table 5 · p. 18

5.1.2 Continuous testing on artifact code

  • Only two of six candidate artifacts qualified for fresh-code testing: MMD-FUSE and Simformer, whose released code reproduced reported values in pinned containers.The other candidates missed a frozen interval, required unavailable hardware, exceeded the time limit, or lacked a license grant.Source: §5.1.2 · p. 18
  • Six property-based tests paired claims with auto-research generators on unmodified code, using all four family types on MMD-FUSE and two on Simformer.Neither artifact had recorded generator bindings, so the study supplied them; a separate test paired reported and fresh evidence for MMD-FUSE.Source: §5.1.2 · p. 18
  • Continuous campaigns admitted three targets—MMD-FUSE C12, PINN C06, and three SMM subclaims—after code and data availability and runtime screening.Adopted violations required fresh-context review, deterministic replay, and confirmation with new random draws.Source: §5.1.2 · p. 18

5.2 RQ1: Declaration fidelity on existing artifacts

On 243 claims, ARATest fully bound 54 and decided 40; catalog coverage, declaration review, and the precision of reported numbers shaped which claims could be checked. Source triage found both paper-level numerical errors and violations introduced during artifact compilation.

5.2 RQ1: Declaration fidelity on existing artifacts

  • 54 claims (22.2%) were fully bound and 40 (16.5%) decided: 32 held and eight were violated, while 14 remained inconclusive.Excluding five decisions based only on reported summaries leaves 35 decided claims (14.4%); all 187 reported-property records replayed without mismatch or drift.Source: §5.2 · p. 19, Table 6 · p. 19
  • Removing source-preserving readers cost two bound claims, removing source contracts cost nine more, and removing numeric skeletons cost 26 more.The base relation catalog alone bound 17 claims; the ablation removes components cumulatively.Source: §5.2 · p. 19, Table 6 · p. 19
  • With the base catalog, missing relations limited coverage more than the agent did; review also rejected declarations that omitted substantive claim details.The agent declared 24 claims, and 111 of 219 skips cited a missing relation; review accepted 18 declarations as faithful.Source: §5.2 · p. 19
  • Source triage traced four violations to published papers, including numerical errors in APT and Knappe et al., and four others to the compiled artifact.The paper errors compare stated values with their papers’ own tables; artifact issues included swapped SEMA columns and hedged claims made strict.Source: §5.2 · pp. 19–20
  • Seven inconclusive claims agreed with printed numbers but derived stated values from rounded operands, whose uncertainty exceeded the claims’ stated bands.The two author CPU-helper checks also remained inconclusive: agreement on sampled inputs cannot establish universal correctness.Source: §5.2 · p. 20
  • The 189 unbound claims mark the current catalog’s scope: most require a verification method other than property testing.The first applicable audit labels assign 123 to another method, 49 to unresolved meaning, 16 to missing or unusable evidence, and one to an unexecuted invariant.Source: §5.2 · p. 20

5.3 RQ2: Seeded-fault detection on common evidence

On common recorded evidence, ARATest detected every seeded fault without false alarms, while the LLM judges missed faults; replay also exposed an error introduced during artifact compilation.

5.3 RQ2: Seeded-fault detection on common evidence

  • 553/553 seeded faults were detected with no false alarms on 19 valid controls; direct and calculator-assisted judges detected 61.8% and 57.7%.The checker was nine to ten times faster per attempt; on the small executed-code population, all three methods detected all three faults and returned correct verdicts on all four packets.Source: §5.3 · p. 20, Table 8 · p. 21
  • 127 of 211 direct-judge misses and 75 of 234 calculator-assisted misses refuted the property through a different comparison rather than identifying the injected fault.Both judges also sometimes accepted a listed counterexample; all 26 scorer-labeled arithmetic witness errors had the correct magnitude but opposite sign.Source: §5.3 · pp. 20–21, Figure 11 · p. 21
  • Only 44 of 504 first calculator trajectories called the tool, and 37 of those stopped when the continuation exceeded the input limit.On 447 packets where both judges completed, calculator-assisted detection was 318/484 versus 307/484 for direct judging, but it returned fewer correct verdicts, 383 versus 415.Source: §5.3 · p. 21
  • At the 0.005 resolution width, both reviewed and literal-scope specifications detected every tested mutant; at 0.01 floating-point error hid 12 of 18 one-unit mutants.At widths of 0.02 and above, only the six value swaps remained detected, while no unedited original was flagged at any width.Source: §5.3 · p. 21, Figure 12 · p. 22

5.3.1 Replay and input drift

  • Replay recomputed all 508 packets and 3,382 saved property records without source drift, and traced an unseeded SEMA inconsistency to swapped accuracy headers in the compiler skill.After the headers were corrected, the source-bound comparison held on 42 of 42 comparisons.Source: §5.3.1 · p. 22

5.4 RQ3: Scope-preserving experimental workflow

Fresh-code tests returned holds for four of six tests and exposed behaviors that reported evidence could not show, but registered rules left the new behaviors inconclusive. The evaluation remains bounded by agent review, execution, and scope limitations.

5.4 RQ3: Scope-preserving experimental workflow

  • Four of six tests returned holds and none returned a violation; one MMD-FUSE seed above the claimed band was averaged with two other seeds, keeping the mean inside the band.A per-seed check would have reported a violation.Source: §5.4 · p. 22
  • Fresh runs found Simformer pool reordering raised C2ST by up to +0.018, while the MMD-FUSE paper-stated temperature lowered rejection rate by 0.041,5 versus the released temperature.Both behaviors were inconclusive: the Simformer rule had no bound, and the MMD-FUSE interval crossed the registered ±0.05 equivalence margin.Source: §5.4 · p. 22
  • A paired reported/fresh property on released MMD-FUSE and MMD-Median implementations returned holds, showing one rule applied to both evidence sources.Because the operands agreed, the result did not show that the rule distinguishes the sources.Source: §5.4 · p. 23
  • Only seven of 60 scheduled campaign runs produced complete reports, yielding 11 checks: six held and five were inconclusive.Many runs failed, were canceled, or exceeded the campaign window; most complete MMD-FUSE batches reused registered seeds or row orders, and no adopted batch covered SMM subclaim C03.Source: §5.4 · p. 23
  • The released PINN NNCG optimizer crashed on the required reaction seed at all five damping values in all four attempts, preventing verdicts on two properties.The authors pin CUDA 11.7, whereas the tests used CUDA 11.8; the seed was retained rather than dropped to obtain a verdict.Source: §5.4 · p. 24
  • Within the tested scope, auto-research generators ran experiments on unmodified author code, and fresh execution exposed behaviors absent from reported evidence without turning undecidable cases into violations.The evaluation does not establish that agent-reviewed declarations would survive independent human review.Source: §5.4 · p. 24

5.5 Threats to validity

  • Fresh-context AI reviewers checked the declarations and designs, but no human checked campaign runs or seeded mutants, so independent human review remains untested.The authors report no reviewer-agreement measure.Source: §5.5 · p. 24
  • The 553-of-553 seeded-fault result assumes faithful declarations, and an omitted hard case could escape a reviewer; a passing verdict therefore does not certify a claim.The seeded population comes from two artifacts, and 19 valid controls provide weak evidence about specificity.Source: §5.5 · p. 24

6 Discussion

ARATest holds a claim’s declared property fixed across evidence sources and makes failures traceable to the binding and witness. Its reach is bounded by the properties and methods encoded in the current catalog.

6 Discussion

  • A fixed declaration keeps the scientific question constant across tests by making the relation, comparison cohort, scope, and numerical policy explicit.A failed relation points to its binding rather than counting against the source claim; witnesses let users trace outcomes to evidence and interpretation.Source: §6 · p. 25
  • Many of the 189 unbound claims fall outside property-based testing; a violation of an executable consequence can support refutation, but passing it cannot verify the complete assertion.New property forms can be added by implementing and registering a skeleton while keeping the contract, generators, and witness format unchanged.Source: §6 · p. 25
  • Fresh-code experiments exposed a paper/code temperature mismatch, a PINN optimizer crash, and a Simformer C2ST change, but all remained inconclusive under the registered rules.Counting such behaviors as defects would require registering a deciding rule before execution and running unmodified controls beside each test.Source: §6 · p. 25
  • Stored-evidence integration checks averaged 1.66 seconds per attempt in RQ2, while DissClaimer runs fresh experiments offline and returns failing cases as feedback.The evaluation added declarations to finished artifacts; the intended in-process use would require the compiler skill to emit Kind and Domain with each claim.Source: §6 · p. 25
  • Reviewers could run ARATest on submitted ARA artifacts, and downstream artifacts could rerun upstream tests as upstream evidence changes.The passage notes a venue requirement for ARAs alongside submissions.Source: §6 · p. 25

7 Related work

Related work spans software contracts and property testing, execution-backed scientific review, claim-evidence binding, and autonomous research. ARATest focuses on testing a fixed relation after a declaration binds it to a claim.

7 Related work

  • Unlike routine contracts and specifications, a claim contract fixes a relation over measurements, including the comparison cohort, statistical unit, and numerical policy.ARATest types generators by statistical unit rather than by value, unlike QuickCheck and Luck.Source: §7 · pp. 25–26
  • FactReview [53], MechEvalAgent [2], ExecutableClaims, SciFact, and SCITAB [35] locate or interpret evidence, while ARATest tests new observations against a bound relation.Its witness supports inspection, but a reviewer must still check that the binding represents the source claim.Source: §7 · p. 26
  • Structured declarations and deterministic binding checks can enforce form and real evidence references, but neither establishes semantic fidelity to the source claim.The experiment-generator agent likewise cannot show that a run faithfully tests the source claim, so failing runs are feedback rather than refutation.Source: §7 · p. 26
  • ARATest gives autonomous research search a fixed target: agents supply evidence, while the registered contract fixes the verdict rule and failing runs return as artifact-revision feedback.The related work situates this approach alongside autonomous research systems, externally validated oracles [12], and fuzzing-inspired searches [22].Source: §7 · p. 26

8 Conclusion

ARATest makes prose-only research claims testable by binding them to executable properties that remain fixed across reported and fresh evidence. Its evaluations found confirmed paper errors, detected seeded faults, and exposed behaviors visible only in fresh runs.

8 Conclusion

  • ARATest binds claims to property skeletons through typed declarations that fix scope and decision rules across reported and fresh evidence.Most claims left unbound need a verification method other than property testing.Source: §8 · p. 26
  • Two violations exposed published papers whose prose contradicted their own tables, and both errors were confirmed by the authors.Source: §8 · p. 26
  • ARATest detected more seeded faults than LLM judges in about a tenth of the time.Source: §8 · p. 26
  • Fresh runs of author code exposed behaviors absent from reported evidence, including code using a different temperature than its paper states.Source: §8 · p. 26
  • Credible fault discovery will require preregistered studies with independent review of declarations.Source: §8 · p. 26

Ethics and privacy statement

The study uses published papers and publicly released artifacts, which contain no private personal data. Findings concern claims and evidence, not author conduct, and numerical-error findings were disclosed to the authors.

Ethics and privacy statement

A Generator interface

The paper presents the Python library's generator interface and directs readers to separate sections for class descriptions and generator combinators.

A Generator interface

B LLM judge prompt

The LLM-judge appendix specifies shared decision rules and a response schema, then describes the evidence packet and calculator available to the judges. The schema leaves the sign of margin undefined, a flaw linked to opposite-sign witness errors.

B LLM judge prompt

  • The schema leaves the sign of margin undefined, explaining opposite-sign witness errors in Section 5.3.Source: B LLM judge prompt · p. 30, Figure 15 · p. 31
  • The evidence packet contains the property description, observations, comparisons, clause rows, coverage and completeness limits, and—when recorded—the raw table and claim text.Source: B LLM judge prompt · p. 30
  • The calculator-assisted judge receives bounded exact arithmetic over supplied decimal operands, while the direct judge receives no tool.The calculator supports ten operations and returns exact results with a decimal rendering of up to 36 significant digits.Source: B LLM judge prompt · p. 30
  • Figures 14 and 15 present the shared judge prompt's decision rules and response schema, respectively.Source: B LLM judge prompt · p. 29, Figure 14 · p. 31, Figure 15 · p. 31

Related papers

Loading 2610.30495v1…