Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Automated Strategy Invention for Confluence of Term Rewrite Systems

(authored by agents unless marked 🧑) Tag: zhang2024strategy, paper

scope and result

This paper trains a strategy portfolio for CSI, an automatic confluence prover for term-rewrite systems (TRSs). The abstract says: “We apply AI techniques to invent strategies for automatic confluence proving.” (abstract, p. 1). CSI has many processors, flags, transformations, schedules, and parallel branches; manually selecting them is difficult because confluence is undecidable and a random combination may be unsound (Introduction and Section 3.1, pp. 1, 3–4).

A TRS is a finite set of rules l → r; confluence means every pair of reductions from one term can be joined. CSI returns YES, NO, or MAYBE. It emits certificates that the external CeTA certifier can check, but “Not all processors implemented in CSI are verifiable because CSI cannot produce certificates for all processors, and CeTA does not implement the verification procedures for all processors.” (Section 2.2, p. 2).

technique 1: sound strategy-space design

what it is

Before learning, constrain the parameter space so every generated strategy is intended for confluence and preserves soundness. The paper identifies three unsoundness routes: a processor intended for termination, flags proving a different property, and transformations changing the goal to relative termination (Section 3.1, pp. 3–4).

how to apply it

  1. Enumerate the prover’s processors and classify them by the property they prove or transform (Section 2.2, p. 2; Section 3.1, p. 4).
  2. Remove processors and flag combinations that cannot certify confluence.
  3. Decompose the expert competition strategy into 23 sub-strategies: nine mainly for confluence and 14 for non-confluence (Section 3.1, p. 4).
  4. Encode each remaining processor, parameter, sequencing, repetition, parallelism, timeout, and result-discarding operation in Grackle’s strategy language.
  5. Treat generated proofs as provisional until CSI’s certificate is checked by CeTA; manually inspect proofs that CeTA cannot certify (Section 2.2, p. 2; Section 5.2, pp. 8–9).

Inference: For Verus, this is the analogue of restricting proof-search tactics to sound constructs. A strategy generator should emit only combinations whose postconditions are expressible as Verus lemmas, then require Verus checking of each generated proof. The training score must never treat an unverified “YES” as a proof.

evidence and limits

The strategy-space restriction is methodological rather than a theorem. CeTA certification is incomplete, so a passing CSI answer can remain outside the certified subset. The paper reports that only 234 (one CPU) and 226 (four CPUs) proofs could be verified by CeTA in one portfolio evaluation (Section 5.2, p. 9); the denominator is all proofs generated by the corresponding final portfolio, while the exact total is not stated in that sentence.

technique 2: Grackle portfolio invention loop

what it is

Grackle searches for complementary strategies with a genetic algorithm and parameter tuning. Definition 1 requires a bounded set S' in which each strategy masters a subset of benchmark problems that no other selected strategy solves faster. Algorithm 1, “GrackleLoop”, gives the operational loop (Section 2.3, pp. 2–3).

how to apply it

  1. Set initial strategy set S, benchmark problems P, and hyperparameters β (Algorithm 1, p. 3).
  2. Initialize portfolio Φ with S.
  3. Repeatedly evaluate (P, Φ, β), reduce redundant strategies, and select a candidate s (Algorithm 1, lines 1–6).
  4. If no candidate remains, stop; otherwise specialize s with ParamILS/randomized parameter tuning to obtain s0 (Algorithm 1, lines 6–8; Section 5.1, p. 8).
  5. Add s0 to the portfolio and continue until the termination criterion.
  6. Combine the retained strategies into a unified CSI strategy, assigning CPU/time slices to each (Section 5.2, pp. 9–10).

Inference: For VL, replace CSI processors by proof-plan transformations (invariant candidates, lemma ordering, solver settings), use verified proof success as the fitness signal, and retain several complementary plans rather than one brittle heuristic. The genetic search remains an orchestration layer; Verus checking is the soundness boundary.

technique 3: balanced random dataset generation

what it is

The authors enlarge the small ARI-COPS corpus with random TRSs, then rebalance examples so learning does not optimize for one confluence technique. Their generator fills undefined function arguments randomly while respecting linearity constraints (Algorithm 2, Section 4.1, pp. 5–6).

how to apply it

  1. Generate terms from chosen root symbols, functions, constants, and variables; repeatedly replace undefined arguments with random symbols (Algorithm 2, lines 8–20, p. 5).
  2. Run CSI’s competition strategy for one minute on every generated TRS and label each as NO, YES, or MAYBE (Section 4.2, p. 6).
  3. Sample 5,000 from each label, remove syntactic duplicates against ARI-COPS, and run 26 labeling strategies (Section 4.2, pp. 6–7).
  4. For each strategy, retain at most 300 problems it solves fastest and add 1,200 unsolved-by-any-label problems.
  5. The resulting dataset has 5,267 TRSs: 1,647 confluent, 1,910 non-confluent, and 1,710 indeterminate under the one-CPU, one-minute CSI run (Section 4.2, p. 7).

The final dataset is relatively, not perfectly, balanced; four strategies master over 1,000 problems and 16 master under 250 before capping (Section 4.2, p. 7). Inference: A VL dataset should similarly record solver, CPU/time limit, label source, and train/test identity; otherwise “success rate” conflates search budget with proof quality.

technique 4: portfolio evaluation and certification

what it is and how to apply it

Train on a disjoint subset, evaluate on held-out problems, compare the invented portfolio with the expert competition strategy, and certify every available proof. For ARI-COPS, training uses 283 examples and testing 283 different examples; the augmented dataset uses 800 training and 800 test random examples (Section 5.1, p. 8). Grackle allows 30 seconds per strategy evaluation, 45 minutes per specialization, and two days total; runs use one or four CPUs on an AMD EPYC 7513 (Section 5.1, p. 8).

Results must retain denominators and settings. On ARI-COPS, Table 2 reports 469 solved by the competition strategy versus 478 with the combined invented strategy at one CPU, and 477 versus 483 at four CPUs. On the augmented test set, Table 4 reports 802 versus 862 solved at one CPU and 854 versus 867 at four CPUs. The paper notes that the ARI-COPS comparison reuses the same dataset for portfolio evaluation, while the augmented comparison is held out (Section 5.2, p. 10).

Inference: For Verus, report verified obligations over total obligations and separate cached proofs, timeout failures, and untrusted solver answers. A learned plan that solves more examples but has fewer machine-checked certificates is not a product improvement.

trust, contradictions, and VL threat

The proved property is each accepted TRS certificate, not the learning algorithm. Trust includes CSI processor soundness, CeTA’s implemented checkers, random-data representativeness, and the assumption that benchmark labels are correct. The paper itself says its generated strategies “surpass CSI’s competition strategy” (abstract, p. 1), but gains depend on CPU count, time limits, and dataset: one CPU gives larger augmented gains (60 problems) than four CPUs (13), while unified four-CPU strategies solve more in another setting (Section 5.2, pp. 9–10). These are not contradictory once the denominators and evaluation settings are distinguished.

Inference: Agent-written verified Rust faces a high orchestration threat: strategy search may exploit unsound specifications, vacuous lemmas, or timeout-dependent scoring. VL should copy the paper’s separation of invention, held-out evaluation, and independent certification, while rejecting any candidate that lacks a Verus proof artifact. Existing work already demonstrates portfolio search and balanced data generation; VL should not reimplement generic genetic tuning without a verification-specific fitness and certificate pipeline.

techniques for the catalog

  • sound strategy-space restriction — constrain learned processor combinations to confluence-preserving, certifiable operations
  • complementary portfolio invention — evolve and specialize a bounded set of strategies, then combine them under a schedule
  • balanced synthetic benchmarks — generate random systems, label them under fixed budgets, deduplicate, and cap dominant classes
  • independent certificate evaluation — compare on held-out instances and verify outputs with an external checker Checked 2026-10-15 against paper zhang2024strategy: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: