Local ATP Benchmark

Mix.install([
  {:atp_benchmark_runner, github: "penthooose/atp_benchmark_runner", force: true}
])

1. Configure paths from .env

# Load .env values into the OS environment (Config.get() and hpc_connect pick them up).
env_map = AtpBenchmarkRunner.load_env!(Path.expand("../.env", __DIR__))

IO.puts("Configured paths:")
IO.puts("  TPTP_ROOT:      #{AtpBenchmarkRunner.tptp_dir()}")
IO.puts("  Store dir:      #{AtpBenchmarkRunner.store_dir()}")
IO.puts("  SMT temp dir:   #{AtpBenchmarkRunner.Config.smt_tmp_dir()}")
IO.puts("  THF temp dir:   #{AtpBenchmarkRunner.Config.thf_tmp_dir()}")

This notebook is the local counterpart to benchmark_hpc.livemd. It runs the same prover images (via Docker or Apptainer) and applies the same input preparation as on the cluster:

• :cvc5 - problems are converted to SMT-LIB (TPTPToSMT) before cvc5 sees them (cvc5 has no TPTP input dialect); its bare sat/unsat/unknown answer is mapped to an SZS status.
• :lash - FOF/CNF/TFF problems are converted to THF (TPTP.ToTHF) because lash is a THF-$o-only prover.
• All other provers read the TPTP file directly.

2. Detect available execution methods

AtpBenchmarkRunner.LocalRunner.print_image_status_summary()

Available provers:

• :tableaux - uses the local escript (always available after mix escript.build in item #12)
• :eprover, :vampire, :cvc5, :zipperposition, :leo3, :leo2, :lash - run via Docker images built from their Containerfiles

Native binaries of the reference provers are not distributed for Windows. The Docker images are built from the same sources as the HPC Apptainer .defs, so results are directly comparable with the cluster.

3. Build / pull Docker images for all provers

This builds images for all registered provers from their Containerfiles (Docker) or apptainer.defs (Apptainer). The first build downloads dependencies and may take a few minutes; subsequent runs are instant. force: true rebuilds everything. Returns {:ok, name} / {:error, name, reason} per prover.

# Build (or pull) local images for all registered provers in one call.
# backend: :auto (default) | :docker | :apptainer   ·   force: true rebuilds all.
results = AtpBenchmarkRunner.build_local_images!(:all, backend: :docker)

4. Download problems

Single problems are downloaded from the TPTP distribution into TPTP_ROOT (C:\tmp\tptp from .env). download_tptp_problems!/2 returns the resolved Problem structs plus any download warnings.

selected_problems = [
  "ALG001+0.p",
  "GRP001-0.p",
  "GRP002+0.p",
  "GRP003+0.p",
  "GRP004+0.p",
  "GRP720+1.p",
  "GRP752-1.p",
  "LAT001+0.p",
  "PUZ001+0.p",
  "REL001+0.p",
  "SET001^0.p",
  "SMT001+0.p",
  "SYN000+0.p",
  "THF001+0.p"
]

{downloaded, download_warnings} =
  AtpBenchmarkRunner.download_tptp_problems!(selected_problems, force: false)

IO.puts("Downloaded #{length(downloaded)} problem(s):")
Enum.each(downloaded, fn problem ->
  IO.puts("  ✅ #{problem.name}  status=#{problem.expected_status}  rating=#{problem.rating}")
  IO.puts("     -> #{problem.path}")
end)

if download_warnings == [] do
  IO.puts("No warnings.")
else
  IO.puts("Warnings (#{length(download_warnings)}):")
  Enum.each(download_warnings, fn w ->
    IO.puts("  ⚠️  #{w.name}: #{inspect(w.reason)}")
  end)
end

Tip: download_tptp_problems!/2 is the "single problem download" entry point. Pass any TPTP problem name (e.g. "GRP001-0.p"); problems already present under TPTP_ROOT are reused (set force: true to re-download).

5. Select provers and problems

Problems are selected by name. They resolve from TPTP_ROOT, the bundled examples, or a livebook cache automatically.

selected_provers = [
  :tableaux,
  :shot_tx,
  :eprover,
  :vampire,
  :cvc5,
  :zipperposition,
  :leo3,
  :leo2,
  :lash
]

problems =
  AtpBenchmarkRunner.select_problems(
    names: selected_problems,
    limit: 10
  )

IO.puts("Provers (#{length(selected_provers)}): #{inspect(selected_provers)}")
IO.puts("")
IO.inspect(Enum.map(problems, &%{name: &1.name, path: &1.path}), label: "Problems")

6. Run the local benchmark

Each prover runs against each problem sequentially, exactly like the single-node sequential HPC mode. auto_ensure_images: true builds any missing Docker image on demand, and the same SMT/THF input preparation as on HPC is applied per prover.

IO.puts("Starting local benchmark...")
IO.puts("  Provers: #{inspect(selected_provers)}")
IO.puts("  Problems: #{length(problems)}")
IO.puts("")

{t_ms, results} =
  :timer.tc(fn ->
    AtpBenchmarkRunner.local_benchmark(selected_provers, problems,
      timeout_seconds: 30,
      auto_ensure_images: true,
      include_raw_output: true
    )
  end)

elapsed_s = t_ms / 1_000_000
IO.puts("Benchmark completed in #{Float.round(elapsed_s, 2)}s")
IO.puts("Total results: #{length(results)}")

7. Results table

# Guard: fall back to an empty list if this cell is evaluated before section 6.
results = binding()[:results] || []

AtpBenchmarkRunner.results_table(results)

8. Aggregated report

report = AtpBenchmarkRunner.report(results)

IO.puts("Run ID: #{report.run_id}")
IO.puts("Generated: #{report.generated_at}")
IO.puts("")
AtpBenchmarkRunner.print_report_markdown(report)

Per-prover breakdown

IO.puts("| Prover | Total | Solved | Failed | Solve Rate |")
IO.puts("|--------|------:|-------:|-------:|-----------:|")

Enum.each(report.by_prover, fn p ->
  IO.puts("| #{p.prover} | #{p.total} | #{p.solved} | #{p.failed} | #{Float.round(p.solve_rate * 100, 1)}% |")
end)

Per-problem comparison

AtpBenchmarkRunner.print_per_problem(report)

Full explained results

IO.puts("Full explained results with proofs:\n")
AtpBenchmarkRunner.print_explain_full(results)

Filtered results by prover

target_prover = :shot_tx

AtpBenchmarkRunner.print_verbose_report(results, prover: target_prover, solved_only: false)

View a specific proof

target_prover = :shot_tx
target_problem = "GRP001-0"

AtpBenchmarkRunner.show_proof(results, target_prover, target_problem)

Raw prover debug output

AtpBenchmarkRunner.print_raw_output(results, :shot_tx, "GRP001-0")

Interesting findings

interesting = report.interesting

IO.puts("### Easy problems our prover failed (rating <= 0.3)")
if interesting.easy_failed_by_ours == [] do
  IO.puts("  (none) 🎉")
else
  Enum.each(interesting.easy_failed_by_ours, &IO.puts("  - #{&1}"))
end

IO.puts("")
IO.puts("### Hard problems our prover solved (rating >= 0.7)")
if interesting.hard_solved_by_ours == [] do
  IO.puts("  (none)")
else
  Enum.each(interesting.hard_solved_by_ours, &IO.puts("  - #{&1}"))
end

IO.puts("")
IO.puts("### Solved only by our prover")
if interesting.only_ours == [] do
  IO.puts("  (none)")
else
  Enum.each(interesting.only_ours, &IO.puts("  - #{&1}"))
end

IO.puts("")
IO.puts("### Solved only by reference provers")
if interesting.only_others == [] do
  IO.puts("  (none)")
else
  Enum.each(interesting.only_others, &IO.puts("  - #{&1}"))
end

9. Visualizations

Mermaid-based visual companions to explain/1 / explain_full/1. Each cell returns a Kino.Mermaid diagram (or a fenced markdown block outside Livebook).

results = binding()[:results] || []
results = if results == [], do: VisualizeSample.results(), else: results

target =
  Enum.find(results, fn r ->
    r.prover == :eprover and AtpBenchmarkRunner.Result.solved?(r)
  end)

if target, do: AtpBenchmarkRunner.visualize(target), else: "No solved eprover result found."

9b. Proof dependency graph

For provers that emit machine-readable TPTP clause refutations (E, Vampire) this renders the proof as a dependency DAG. Other provers fall back to a pipeline diagram.

results = binding()[:results] || []
results = if results == [], do: VisualizeSample.results(), else: results

target =
  Enum.find(results, fn r ->
    match?({:ok, _}, AtpBenchmarkRunner.Visualize.Proof.parse(r))
  end)

if target, do: AtpBenchmarkRunner.visualize_proof(target), else: "No parseable proof found."

9c. Run summary (status + wall-time chart)

AtpBenchmarkRunner.visualize(results) is the one-call shortcut for Visualize.status_pie/2 + Visualize.timeline/2; it pushes both diagrams as Livebook outputs.

results = binding()[:results] || []
results = if results == [], do: VisualizeSample.results(), else: results

case AtpBenchmarkRunner.visualize(results) do
  :ok -> :ok
  markdowns -> Enum.each(markdowns, &IO.puts/1)
end

9d. Report scoreboard

results = binding()[:results] || []
results = if results == [], do: VisualizeSample.results(), else: results

report = AtpBenchmarkRunner.report(results)
AtpBenchmarkRunner.visualize(report)

9e. Raw Mermaid source (copy into a markdown cell)

results = binding()[:results] || []
results = if results == [], do: VisualizeSample.results(), else: results

target =
  Enum.find(results, fn r ->
    match?({:ok, _}, AtpBenchmarkRunner.Visualize.Proof.parse(r))
  end)

if target do
  IO.puts(AtpBenchmarkRunner.Visualize.markdown(AtpBenchmarkRunner.Visualize.proof(target)))
else
  IO.puts("No parseable proof; nothing to show.")
end

10. Persist results to local store

run = AtpBenchmarkRunner.new_run(
  title: "Local smoke test",
  problems: problems,
  provers: selected_provers,
  walltime: "00:30:00",
  problem_timeout_seconds: 30
)

paths = AtpBenchmarkRunner.persist_run!(run, results, report)
IO.puts("Run saved: #{paths.run_path}")
IO.puts("Results saved: #{paths.results_path}")
IO.puts("Report saved: #{paths.report_path}")

Runs are persisted to the store directory from .env (ATP_BENCHMARK_RUNNER_STORE_DIR, e.g. C:\tmp\atp_benchmark_runner_store).

11. Compare with a previous run (longitudinal diff)

prev_results_path = nil

if prev_results_path && File.exists?(prev_results_path) do
  prev_results = AtpBenchmarkRunner.Store.load_results!(prev_results_path)
  diff = AtpBenchmarkRunner.compare_runs(prev_results, results)
  AtpBenchmarkRunner.print_diff(diff)
else
  IO.puts("No previous results to compare against. Set `prev_results_path` to enable.")
end

12. Cross-run comparison & statistics

Compares all stored runs at once. Results stay in JSON files under the store dir.

Ranking counts Timeout/GaveUp as real attempts (never excluded). By default InputError/TypeError/UnsupportedLogic/Error are treated as non-attempts (prover not applicable to that problem); override with :exclude_statuses (pass [] to include them).

# One call: load all runs, aggregate, and print the comparison tables.
stats = AtpBenchmarkRunner.compare_all_runs()

# Livebook-friendly panel (Kino.Markdown when available).
AtpBenchmarkRunner.MultiRun.panel(stats)

# Save the comparison as a Markdown file.
path =
  AtpBenchmarkRunner.save_multi_run_stats!(
    Path.join(AtpBenchmarkRunner.store_dir(), "comparison.md")
  )

IO.puts("Comparison saved: #{path}")

# Same-problem-set ranking + error-status control.
# only_common_problems: rank only on problems every prover ran.
# exclude_statuses: [] keeps input/type errors as real attempts.
stats_common =
  AtpBenchmarkRunner.multi_run_stats(nil,
    only_common_problems: true,
    exclude_statuses: []
  )

AtpBenchmarkRunner.MultiRun.print(stats_common)

13. Inspect raw output (optional)

target_index = 0

if results != [] do
  r = Enum.at(results, target_index)

  if r && r.raw_output do
    IO.puts("Raw output for #{r.problem_id} / #{r.prover}:")
    IO.puts("")
    IO.puts(r.raw_output)
  else
    IO.puts("No raw output stored (rerun with include_raw_output: true)")
  end
else
  IO.puts("No results available.")
end