BliStrTune: hierarchical invention of theorem proving strategies

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

Page numbers below refer to the 10-page arXiv version (arXiv:1611.08733v1).

result and setting

BliStrTune extends BliStr to automatically invent E-prover strategies. The abstract describes its core: “BliStrTune allows exploring much larger space of E strategies by interleaving search for high-level parameters with their fine-tuning.” (Abstract, p. 1.) It targets clause-selection protocols for saturation theorem proving and evaluates them on Mizar@Turing problems. The central claim is empirical: “We show that the new strategies significantly improve E’s performance in solving problems from the Mizar Mathematical Library.” (Abstract, p. 1.)

An E protocol is the set of selected values of the parameters that control proof search: term ordering, literal selection, and a weighted list of clause-evaluation functions (CEFs). Each CEF is specified by a priority function, a weight function, and the weight function’s arguments; it selects the clause with the smallest (priority, weight) pair. In the protocol, an integer in front of each CEF says how often that CEF is used to select the given clause. E also has an auto-schedule mode that tries several expert heuristics, each for a selected time period (Section 2.1, p. 2). Example 1 gives -tKBO6 -WSelectComplexG -H'(13*Refinedweight(PreferGoals,1,2,2,3,2), 2*Clauseweight(ByCreationDate,-2,-1,0.5))' and explains term ordering, literal selection, frequencies, and arguments (Section 2.1, p. 2).

Inference: Verus can use this as a design for proof automation tuning, where each candidate solver context or lemma policy is a protocol and a verified proof is the objective. The paper’s E-specific parameters and empirical solved counts do not transfer directly to Verus or Rust.

technique: conjecture-oriented clause weights

The paper defines several weight functions that score clauses by similarity to the conjecture; they come from the authors’ earlier work (Jakubův and Urban 2016). Term counts the subterms a term shares with the conjecture: the weight of a term is δf, δc, δp, or δv for functional terms, constants, predicates, or variables, possibly multiplied by γconj when the term appears in the conjecture, and a clause weight is the sum over its subterms (Section 2.2.1, pp. 2–3). TfIdf uses term frequency in the conjecture and document frequency across a fixed clause set Docs (either the axioms including the conjecture, or all processed clauses): tfidf(t) = tf(t) * log((1+|Docs|)/(1+df(t))), then assigns weight 1/(1+tfidf(t)) (Section 2.2.2, p. 3). Pref scores the longest shared term prefix, with match and miss costs. Lev uses the minimal Levenshtein distance from a term to some conjecture term, with separate insertion, deletion, and change costs. Ted uses tree-edit distance with node insertion, deletion, and renaming operations. Struc instead counts generalization and instantiation operations, with penalties for variable mismatch and operation costs (Sections 2.2.3–2.2.6, p. 3).

These scores are combined with priorities and frequencies in CEF protocols. The point is to expose a large but structured family of heuristics to automated configuration rather than hand-pick one weight. The authors observe that four of the new weight functions were not used often in the final schedulers, “which we attribute to their higher time complexity” (Section 5.3, p. 7; see also Section 6, p. 8, on Lev and Ted).

Inference: a Verus proof-search controller could rank candidate lemmas by syntactic or semantic features, but ranking must remain outside the soundness boundary. The selected proof is checked by Verus; a heuristic score cannot establish a lemma. If a ranking function is itself verified, its contract should state only ordering properties actually needed by the scheduler.

technique: BliStr baseline and ParamILS

BliStr interleaves iterated low-timelimit local search for new protocols on small sets of similar easy problems with higher-timelimit evaluation of the new protocols on all problems. Its main criterion (Criterion 1, Max) is to invent a set of E protocols that together solve as many of the given benchmark problems as possible; Criterion 2 (Gen) asks for reasonably general protocols and Criterion 3 (Size) for a set that is not too large (Section 3, pp. 3–4). ParamILS is an iterated local search: starting from an initial configuration, it loops between perturbing the configuration to escape a local optimum and iteratively improving the perturbed configuration; the result of the improvement step is accepted if it improves the previous best configuration (Section 3.1, p. 4). In the BliStr instantiation, A is E run with a low time limit tcutoff, Θ is the set of expressible E protocols, and the performance metric is the number of given-clause loops; if E cannot solve a problem within the low limit, a sufficiently high value (10^6) is used (Section 3.1, p. 4).

The paper states: “The pragmatic solution used in the original BliStr consisted of re-using manually pre-designed high-level strategy components, rather than allowing the system to explore the space of all possible strategies.” (Section 1, p. 1.) Concretely, BliStr extracts a small set (a dozen, currently 12) of CEFs from existing E protocols and hard-codes it into its configuration space (Section 3, p. 4; Section 4.1, p. 4). Separately, BliStr partitions the set of all solvable problems into subsets on which particular protocols perform best, and its loop co-evolves the set of protocols, the set of solved problems, the matrix of best results, and the set of protocols eligible for ParamILS improvement with their problem sets (Section 3.1, p. 4).

Inference: for Verus, the analogue is to tune a proof tactic policy on clusters of verification goals. A training objective should count completed proofs under a fixed timeout and preserve a held-out goal set. The E metric, cutoff, and local-search acceptance policy are engineering choices, not correctness arguments.

technique: hierarchical invention

The authors describe the basic idea as “iterated hierarchical invention: The large space of the optimized parameters is naturally factored into two (in general several) layers”, with only one layer subjected to invention at a time while the others stay fixed (Section 4, p. 4). Directly adding CEF arguments to the ParamILS configuration space would grow it from ca. 10^7 to 10^120 combinations, and the authors report that preliminary experiments showed ParamILS “does not produce satisfactory results in a reasonable time” at that size (Section 4, p. 4). BliStrTune factors parameters into layers. In global tuning, ParamILS changes the top-level arguments (term ordering, literal selection, CEF frequencies) and whole CEF blocks and their count, choosing each CEF from a collection C and never changing a CEF’s own arguments; BliStrTune also adds an argument ccef limiting the number of CEFs in one protocol (ccef = 12 for BliStr) (Section 4.1, pp. 4–5). In fine tuning, the global result is fixed and new parameters allow changing the priority function and weight function arguments of the CEFs it uses, from pre-designed sets of reasonable values per argument type; the weight functions themselves stay fixed (Section 4.2, p. 5). The result is converted back into a global configuration (extending C with any new CEFs), and the phases iterate (Section 4.2, p. 5).

The implementation limits global runs to a collection C of at most 50 CEFs. It starts with 21 CEFs: for each weight function defined in E, the CEF most often used in E’s auto-schedule mode, plus one CEF for each of the new weight functions. It stores every CEF used in an invented protocol in a global database with a usage counter, groups the CEFs by weight function, and repeatedly moves the most-used CEF of each group into C until C reaches its size limit, so C contains at least one CEF per weight function (Section 4.3, p. 5). The paper uses two iterations in practice, that is two global and two fine-tuning phases, “which was experimentally evaluated to provide good results” (Section 4.2, p. 5); in one iteration ParamILS runs four times (Section 4.3, p. 5).

Inference: this hierarchical pattern applies to proof automation: first choose tactic families and ordering, then tune thresholds, solver facts, or lemma budgets. Keep layer interfaces explicit so a fine-tuned policy can be replayed and audited. The policy generator must not be trusted with proof validity.

technique: scheduler construction

BliStrTune produces many protocols (more than 900 from the BliStrTune runs of Section 5.2, Section 5.3, p. 6), so the paper constructs schedulers in which the time limit for a problem is distributed equally among the protocols of the scheduler; building a scheduler then reduces to selecting the protocols (Section 5.3, p. 6). A greedy scheduler greedy_t evaluates all protocols on all training problems with a fixed time limit t, starts with the best protocol, and repeatedly adds the protocol that adds the most solutions to the union already solved. For SOTAC (state-of-the-art contribution, as used by CASC), the SOTAC of a problem is the inverse of the number of protocols that solved it, and the SOTAC of a protocol is the average SOTAC over the problems it solves; the first n protocols by SOTAC form SOTAC_n. Σ-SOTAC instead sums the problem SOTAC over all problems the protocol solves, because plain SOTAC is high for a protocol that solves only one problem no other protocol solves (Section 5.3, pp. 6–7).

The evaluation uses 1,000 training and 400 testing problems from Mizar@Turing (Section 5, p. 6). In the comparison of Section 5.1 both BliStr and BliStrTune use tcutoff=1 and teval=5, BliStrTune uses ccef=6, and Timprove is 100 for BliStrTune and 400 for BliStr, so that the time used to improve a protocol is equal (four ParamILS runs per BliStrTune iteration). The total number of training problems solved by all protocols invented so far, each given teval, was 673 for the original BliStr, 702 for BliStrTune with only the original E 1.9 weight functions, and 711 for BliStrTune with the new weight functions (Section 5.1, p. 6; Figure 1). The authors read this as showing that “the greatest improvement is thanks to the hierarchical parameter invention”, with the new weight functions adding 9 more solved problems (Section 5.1, p. 6). Table 1 (p. 7) lists the BliStrTune runs of Section 5.2; the text there speaks of 6 runs, while the table has 8 rows.

Table 2 evaluates 12 schedulers on the training problems under a 60-second limit (Section 5.3, p. 7): greedy1 has 33 protocols and solves 744/1000 training problems (+9.8% over Vampire 4.0) and 280/400 testing problems (+5.2% over Vampire 4.0’s 266). Table 3 compares greedy1 with other provers under the 60-second limit: on the 400 testing problems E with BliStrTune solves 280, Vampire 4.0 266, and E 1.9 auto-schedule 231; on the training problems the counts are 744, 677, and 605 (Table 3, p. 7; Section 5.4, p. 8). The text under Table 2 says Vampire 4.0 “solves 667 of the 1000 training problems”, while Table 3 gives 677 and the percentages in both tables are consistent with 677 (744/677 is about 9.9%, 744/667 about 11.5%). Inference: the text’s 667 is probably a typo for 677; the paper does not say. Experiments ran on 2x16 cores of Intel Xeon E5-2698 v3 at 2.30GHz with 128 GB memory; one prover run was limited to 1 GB (footnote 1, p. 5).

The paper reports these specific benchmark results, not a universal theorem-proving gain. It has no Verus experiments, and it makes no soundness claim about the learned heuristics.

evidence, limits, and VL implications

The measured result depends on the Mizar translation (MPTP), the 1,000/400 train-test split of the CASC 2012 Mizar@Turing problems, the 60-second evaluation, and the E 1.9 and Vampire 4.0 versions (Sections 5 and 5.4, pp. 5–8). The paper does not discuss correctness or soundness of the heuristics. The authors name as future work weight functions with lower time complexity, perhaps approximate ones; “smarter” schedulers; enhancements of the BliStr/Tune main loop (various parameter settings, selection of training problems, parameter improvement methods other than ParamILS); and an easier-to-use software package (Section 6, p. 8).

Inference: the threat to VeruLaw is indirect but useful. Agent-generated proof strategies can overfit a goal corpus, waste solver time, or hide regressions behind a training metric. A safe integration should keep strategy search separate from Verus’s proof checker, use held-out goals and deterministic budgets, record every selected lemma or solver fact, and reject any strategy whose generated proof does not verify. VL should not redo the basic idea of hierarchical strategy invention; a contribution would need Verus-specific measurements of proof stability, maintenance, and solver-context size.

techniques for the catalog

• conjecture-oriented clause weights: rank proof-search clauses by symbols, subterms, term frequency, prefixes, edit distance, or tree structure
• ParamILS local search: perturb and iteratively improve proof-search parameter configurations under a bounded benchmark metric
• hierarchical invention: alternate global protocol-structure search with fine tuning of component arguments
• CEF collection maintenance: keep a bounded, usage-ranked and weight-function-balanced library of candidate clause evaluators
• protocol scheduling: choose a greedy or SOTAC-ranked subset and run each protocol for an equal time slice Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Then we use a global database (shared by different BliStrTune runs) in which we store all CEFs together with the usage counter which states how often each CEF was used in a protocol invented by BliStrTune.”): I read the whole 10-page text and checked every quotation, number, section and page reference, and technique step in the study against it; I changed one inexact quotation (abstract), one quotation missing a word (the BliStr “pragmatic solution” sentence), the ParamILS 10^6 and CEF-collection details, the SOTAC definition, several page references (the 10-page arXiv pagination), the misattributed reason for BliStr’s reduced space, and removed an unsupported correctness claim and a meaningless “denominator” phrase; I replaced the link with the arXiv link from the paper text and noted the 667/677 and 6-runs/8-rows inconsistencies; I did not check the cited prior work (Jakubův and Urban 2016, Urban 2015), the 10^7/10^120 superscripts beyond the text extraction, or the Table 1 and Table 4 numbers cell by cell.

Last edited: 2026-10-17