ShotTx.Benchmark.HolRunner (ShotTx v0.0.3)

Copy Markdown View Source

Evaluates ShotTx on one ShotTx.Benchmark.HolSuite problem and renders the outcome as a CSV row.

The configuration evaluated is the @params module attribute below. It is %Parameters{} — the shipped defaults — so the numbers this produces are what a user gets from a bare ShotTx.Prover.prove/1. Edit the attribute, or pass a %Parameters{} to evaluate/2, to evaluate a different one.

One problem per BEAM

This module deliberately evaluates a single problem per invocation. ShotTx keeps shared state across proof sessions (the global :term_cache, the session registries), and a session that crashes or is killed leaves enough of it behind to change the answer for later problems in the same node — during development of this suite, one problem returned thm, csa and prover_error depending on what ran before it. Sweeping the suite inside one node therefore does not measure the prover; it measures the prover plus its history. scripts/run_hol_benchmark.sh drives the sweep with a fresh node per problem for that reason.

Independent of ordering, a handful of problems are genuinely nondeterministic run-to-run — the search is parallel, and which worker reaches a verdict first is a race. Repeat a surprising row before believing it.

CSV columns

id, section, variant, livebook_note, result, time_ms, steps,
rules_total, active_branches_max, branches_closed, branches_saturated,
csp_calls, csp_succeeded, details

  • result — thm | csa | unk | timeout | parser_error | prover_error | hard_timeout.

  • livebook_note — what structured_hol_problems.livemd claims for this problem (THM, Timeout, or empty). Recorded for reference only; it is the author's observation, not ground truth.
  • time_ms — wall-clock milliseconds for parse plus proof search, measured after warm_up/1 so it excludes module loading.

Summary

Functions

csv_header()

The CSV header line, newline included.

csv_row(row)

Renders a row from evaluate/2 as a CSV line, newline included.

evaluate(problem, params \\ %{__struct__: ShotTx.Data.Parameters, atom_decomposition: true, beta_variant: true, contradiction_agent: true, demodulation: true, equivalence_processing: :bidirectional_imp, finite_o_quantification: true, formula_cost: &ShotTx.Prover.Rules.rule_cost/1, formula_cost_strategy: :default, initial_gamma_limit: 1, initial_prim_limit: 1, instance_based_gamma: true, instance_based_gamma_limit: 0, iterative_deepening: true, model_agent_backend: :none, model_agent_budget_ms: 5000, model_agent_max_frontier: 100, model_agent_max_in_flight: 2, model_agent_min_delta_ms: 200, model_agent_min_frontier: 3, orient: :none, prim_subst_after: 1, prim_subst_batch_size: 8, primitive_substitution: true, progress_interval_ms: 2000, simplification: :deep, suggestion_cascade_ceiling: 3, suggestions_enabled: true, term_order: %{__struct__: ShotTo.Parameters, accessible: :all, basic_sorts: :all, const_precedence: &:erlang.phash2/1, sort_precedence: %{}, status: %{}}, timeout: 5000, unfold_defs: :lazy, unification_depth: 8, worker_pool_size: :auto})

Proves one problem and returns its row as a map.

params()

The parameter configuration this runner evaluates.

warm_up(params \\ %{__struct__: ShotTx.Data.Parameters, atom_decomposition: true, beta_variant: true, contradiction_agent: true, demodulation: true, equivalence_processing: :bidirectional_imp, finite_o_quantification: true, formula_cost: &ShotTx.Prover.Rules.rule_cost/1, formula_cost_strategy: :default, initial_gamma_limit: 1, initial_prim_limit: 1, instance_based_gamma: true, instance_based_gamma_limit: 0, iterative_deepening: true, model_agent_backend: :none, model_agent_budget_ms: 5000, model_agent_max_frontier: 100, model_agent_max_in_flight: 2, model_agent_min_delta_ms: 200, model_agent_min_frontier: 3, orient: :none, prim_subst_after: 1, prim_subst_batch_size: 8, primitive_substitution: true, progress_interval_ms: 2000, simplification: :deep, suggestion_cascade_ceiling: 3, suggestions_enabled: true, term_order: %{__struct__: ShotTo.Parameters, accessible: :all, basic_sorts: :all, const_precedence: &:erlang.phash2/1, sort_precedence: %{}, status: %{}}, timeout: 5000, unfold_defs: :lazy, unification_depth: 8, worker_pool_size: :auto})

Runs one proof attempt so the measured attempt does not pay for loading the prover's modules and warming the JIT — on the order of a third of a second, which would otherwise be charged to every problem.

Functions

csv_header()

@spec csv_header() :: String.t()

The CSV header line, newline included.

csv_row(row)

@spec csv_row(map()) :: String.t()

Renders a row from evaluate/2 as a CSV line, newline included.

evaluate(problem, params \\ %{__struct__: ShotTx.Data.Parameters, atom_decomposition: true, beta_variant: true, contradiction_agent: true, demodulation: true, equivalence_processing: :bidirectional_imp, finite_o_quantification: true, formula_cost: &ShotTx.Prover.Rules.rule_cost/1, formula_cost_strategy: :default, initial_gamma_limit: 1, initial_prim_limit: 1, instance_based_gamma: true, instance_based_gamma_limit: 0, iterative_deepening: true, model_agent_backend: :none, model_agent_budget_ms: 5000, model_agent_max_frontier: 100, model_agent_max_in_flight: 2, model_agent_min_delta_ms: 200, model_agent_min_frontier: 3, orient: :none, prim_subst_after: 1, prim_subst_batch_size: 8, primitive_substitution: true, progress_interval_ms: 2000, simplification: :deep, suggestion_cascade_ceiling: 3, suggestions_enabled: true, term_order: %{__struct__: ShotTo.Parameters, accessible: :all, basic_sorts: :all, const_precedence: &:erlang.phash2/1, sort_precedence: %{}, status: %{}}, timeout: 5000, unfold_defs: :lazy, unification_depth: 8, worker_pool_size: :auto})

@spec evaluate(ShotTx.Benchmark.HolSuite.problem(), ShotTx.Data.Parameters.t()) ::
  map()

Proves one problem and returns its row as a map.

params()

@spec params() :: ShotTx.Data.Parameters.t()

The parameter configuration this runner evaluates.

warm_up(params \\ %{__struct__: ShotTx.Data.Parameters, atom_decomposition: true, beta_variant: true, contradiction_agent: true, demodulation: true, equivalence_processing: :bidirectional_imp, finite_o_quantification: true, formula_cost: &ShotTx.Prover.Rules.rule_cost/1, formula_cost_strategy: :default, initial_gamma_limit: 1, initial_prim_limit: 1, instance_based_gamma: true, instance_based_gamma_limit: 0, iterative_deepening: true, model_agent_backend: :none, model_agent_budget_ms: 5000, model_agent_max_frontier: 100, model_agent_max_in_flight: 2, model_agent_min_delta_ms: 200, model_agent_min_frontier: 3, orient: :none, prim_subst_after: 1, prim_subst_batch_size: 8, primitive_substitution: true, progress_interval_ms: 2000, simplification: :deep, suggestion_cascade_ceiling: 3, suggestions_enabled: true, term_order: %{__struct__: ShotTo.Parameters, accessible: :all, basic_sorts: :all, const_precedence: &:erlang.phash2/1, sort_precedence: %{}, status: %{}}, timeout: 5000, unfold_defs: :lazy, unification_depth: 8, worker_pool_size: :auto})

@spec warm_up(ShotTx.Data.Parameters.t()) :: :ok

Runs one proof attempt so the measured attempt does not pay for loading the prover's modules and warming the JIT — on the order of a third of a second, which would otherwise be charged to every problem.