Skip to content

ACGN v2.1

Choose a tag to compare

View all tags
@AlexandervonWu AlexandervonWu released this 28 Aug 09:51
· 32 commits to aislop since this release
v2.1
431ca32

ACGN v2.1

This release publishes the August 28, 2026 clean full-corpus replay and the
certified Set-carrier repair that closes the targeted capability matrix.

Provenance

  • Result-producing source commit: 88363ea23728329948ccc9d5cdad690cc5787ca5
  • Clean publication run: 57f5a2d8-f501-494d-81d5-b3f1396dbe18
  • Final packaging and tag commit: 431ca3229e9f5e7464bf86521659b0caa7b9ca17
  • Dataset: 66,080 Alloy files; 61,598 eligible AST-different pairs
  • Imported manifest-bound stage outputs: 5,808 files
  • Configuration: Java 17.0.20, 16 workers, 8 GiB heap, reward pool 100

Reviewers must run git lfs pull before verifying the two large JSON result
files. Run ./scripts/verify_imported_publication_snapshot.sh to check every
imported stage artifact against the archived run manifest.

Headline results

  • Paired evaluation: 61,598 successes, 4,482 AST-identical skips, 0 failures,
    and 0 incorrect certificate-integrated zeroes.
  • Augmented evaluation: all 42,386 incorrect predicates ranked and rewarded,
    with 0 preparation, ranking, or reward failures and 0 certified
    incorrect-to-truth zeroes.
  • Seven-arm ablation: all 431,186 eligible arm rows succeeded; the
    Certificate-Integrated IR found 4,088 CORRECT zeroes and retained every
    Fast Rewrite IR zero.
  • Bounded natural-corpus semantic replay: 4,088 unique claims, 0
    counterexamples, 0 errors; four targeted negative controls remained
    unmerged.
  • Functionality matrix: slotted e-graph, Fast Rewrite IR, and
    Certificate-Integrated IR each recovered 5,500/5,500 generated pairs.
  • Rewards and reward correlations are present; both rewarded stages used pool
    size 100 and reported 0 reward failures.

Certificate and assurance boundary

Certificate coverage remains bounded and fixture-scoped. The exported
certificate census is 1 VERIFIED, 2 UNCHECKABLE, and 0 REJECTED; it is
not a corpus-wide proof of Alloy equivalence.

The bounded Section 3 harness executed 77 steps with 0 failed executable
steps, including every mapped Lean file and the forbidden-token scan. Its
overall assurance state remains honestly INCOMPLETE because 132 declared
metatheoretical and traceability diagnostics remain open. The capability
soundness sample has 0 conclusive non-temporal failures; six temporal checks
remain explicitly inconclusive because this installation has no temporal
backend.

Assets

  • acgn-experiments.jar: 2,285,442 bytes; SHA-256
    7b308e3156fbb36dfeda4af52f8ec339132546a0fcabb24129227f41debbad71
  • SHA256SUMS: SHA-256
    f33c5e61345f697c3575e69f74af9a0fe1d4581ca16081ec3659c2fa5175c89f

The JAR is the byte-identical archived experiment artifact from the clean run;
it was not rebuilt for this release.

Assets 4
Loading