View on GitHub

PSL

News

Smart_Isabelle

This repository contains various tools to support interactive theorem proving in Isabelle/HOL using artificial intelligence. This repository contains the implementation of proof strategy language (PSL) and its default strategy, try_hard, for Isabelle2025. Past versions of Isabelle, such as Isabelle2022-1, are no longer supported.

YouTube

We opened a YouTube channel to introduce aspects of this project.

Video Thumbnail

Installation (of SeLFiE, PSL, and sem_ind in one go) (for MacOS/Lunux users)

  1. Install Isabelle2025-2.
  2. Download or clone this repository (git clone https://github.com/data61/PSL.git).
  3. Open Isabelle/jEdit with PSL and all that. You can do this by opening Isabelle/jEdit as following:
    • (path to the Isabelle binary)isabelle jedit -d (path to the directory that contains this README file) -l Smart_Isabelle
    • If you are a MacOS user and your current directory is this one with this README.md, probably you should type something like this in Terminal:
    • /Applications/Isabelle2025.app/bin/isabelle jedit -d . -l Smart_Isabelle
  4. Then, You can use SeLFiE/PSL/sem_ind to your theory files with the Isabelle keyword, imports as imports "Smart_Isabelle.Smart_Isabelle".
  5. Open Example/Example.thy to see if the installation is successful.

Note on installation for Windows users

The basic steps are the same as MacOS and Linux. However, instead of using the binary file directly, use Isabelle2025-2\Cygwin-Terminal in Command Prompt. Once you start Isabelle2025-2\Cygwin-Terminal, you can install our tools by typing isabelle jedit -d (path to the directory that contains this README file) -l Smart_Isabelle. Note that once you started Isabelle2025-2\Cygwin-Terminal, you should not specify the path to the Isabelle binary file. Therefore, the command you need after starting Isabelle2025-2\Cygwin-Terminal is something like isabelle jedit -d . -l Smart_Isabelle, assuming that your current directory is this one with this README.md/

Screenshot

If you find it difficult to install our tool, please refer to the Isabelle System Manual. Alternatively, you can just send an email to Yutaka at united.reasoning+gmail.com (reaplace + with @).

Hints

Invoking AbductionProver mid-proof

prove/prove_by_abduction only work at the very start of a proof attempt: they parse a fresh top-level goal statement, so they cannot be used inside a structured Isar proof (after proof (induct x), at a show/case) or partway through a chain of apply steps. suggest/solve lift this restriction: like sledgehammer/find_proof/try_hard, they read the goal from whichever proof is currently open, wherever that is - inside a structured proof, or mid an apply chain - and only ever attack subgoal 1, matching apply’s own convention.

suggest prints a suggested proof script rather than closing the goal itself, for you to copy in by hand:

lemma foo: "..."
proof (induct x)
  case (Suc x)
  suggest  (* suggests a script for this subgoal, using Suc.IH etc. as available *)
  ...

Any auxiliary lemmas it needed are suggested as their own have name: "..." for ... blocks nested inside the current proof (a top-level lemma would be illegal syntax while a proof is already open); the goal itself is suggested as a bare tactic script with no such header, ready to paste in directly as the continuation of the current proof.

solve runs the same search but, if successful, applies the found proof directly and closes the goal itself - no copying required:

lemma foo: "..."
proof (induct x)
  case (Suc x)
  solve  (* closes this subgoal automatically, if AbductionProver finds a proof *)
  ...

It works equally well directly after proof - (with no show yet) and mid an apply chain at the bottom of a proof, closing exactly as done would there. If AbductionProver cannot find a proof, solve raises an error rather than silently leaving the goal open - try suggest at that point to see whatever progress it made.

PSL’s runtime tactic generation can result in a large number of messages in Isabelle/jEdit’s output panel. This might cause Isabelle/jEdit to pause PSL’s proof search after reaching its default upper limit for tracing messages.

Proof search unexpectedly slow on cloud/VM machines: set threads explicitly

Isabelle’s default threads = 0 (“guess from hardware”) relies on Poly/ML’s physical-core detection (Thread.Thread.numPhysicalProcessors), which can badly under-count CPU cores on cloud/KVM virtual machines whose /proc/cpuinfo reports each vCPU as its own single-core physical id (a common vCPU topology on many cloud providers). When this happens, isabelle build/isabelle jedit can end up running with effectively 1 worker thread, even on an 8-, 16-, or 32-core VM. PSL, TBC, and AbductionProver rely heavily on Par_List/POrs-style parallelism (e.g. Par_List.get_some, which does run alternative tactics in parallel and cancel the losers once one succeeds, exactly as documented) — but with only 1 thread available, those “parallel” alternatives are effectively tried one at a time, so even a trivial one-step-induction goal can take minutes instead of seconds.

Symptom: a goal that should take a few seconds instead takes minutes, and isabelle build -v reports (1 threads, ...) in its timing summary even though the machine has many more cores (check with nproc).

Fix: always pass the real core count explicitly, e.g.:

isabelle build -o threads=$(nproc) -d . <session>
isabelle jedit -o threads=$(nproc) -d . -l Smart_Isabelle

Note: a threads value baked into a session’s ROOT file options [...] clause takes priority over -o threads=... on the command line (confirmed empirically), so we deliberately do not hardcode a threads default in this repository’s ROOT files — always pass -o threads=$(nproc) per invocation instead, so it stays correct across machines of any size.

Sledgehammer exhausting machine memory: bound each prover, and size the hammer budget to RAM

Isabelle bounds an external prover’s time but not its memory — veriT, for instance, is invoked with only --max-time. A prover that starts diverging therefore allocates freely until it finishes, its time budget expires, or the machine runs out of memory. Measured here: a single diverging veriT reached 6.35GB while the Isabelle ML process held only 1.9GB, so capping the ML heap alone does not help — it merely leaves more room for the provers to take.

Symptom: a run dies with the OS OOM killer, with Poly/ML’s Run out of store, or with AbductionProver’s own stopping early: running low on memory. In the recorded position matrix this was 12 of 37 runs.

There are two limits, at two levels, and they share one number.

1. How many Sledgehammer invocations run at once (on by default). The budget used to be derived from processors alone — cores / 2, so six concurrent invocations on a 12-core machine, each launching every prover in sledgehammer_provers, against a machine one prover can fill by itself. It now answers to memory as well:

slots = max(1, min(cores / 2, free_memory_MB / hammer_memory_quota_mb))

Read against free memory rather than total, so the budget narrows as a search grows. Override either part from a theory:

declare [[max_parallel_hammers = 4]]     (* explicit slot count, wins outright *)
declare [[hammer_memory_quota_mb = 3072]] (* memory assumed per invocation; default 2048 *)

2. A ceiling on each external prover process (off by default, opt-in). Isabelle locates every prover through a settings variable, so the only place a per-process limit can be imposed is between that variable and the real binary — not from ML, which never sees the launch. Register this repository as an Isabelle component and its etc/settings points those variables at wrappers in contrib/prover_wrappers, keeping the originals in PSL_REAL_<VARIABLE>:

echo /path/to/PSL >> "$(isabelle getenv -b ISABELLE_HOME_USER)/etc/components"

With that done, nothing changes until you ask for a limit:

PSL_PROVER_MEMORY_MB=2048 isabelle build -o threads=$(nproc) <session>

Each prover then runs in its own transient cgroup with that resident-memory ceiling (systemd-run --user --scope -p MemoryMax=..., plus MemorySwapMax=0, because a ceiling a solver can page around is not a ceiling). A prover that exceeds it is killed; Sledgehammer records that prover as failed and carries on with the others, and the session survives. Keep this number and hammer_memory_quota_mb in step: one decides how many provers are admitted, the other what each is allowed, and if they disagree the search admits more provers than the machine has ceilings for.

Three things to know before enabling it:

The validated fallback, if you would rather not enable the wrappers, remains an ML heap ceiling plus the hammer budget (see Eval/run_eval.sh): those converted every SIGKILL tested into a completed run and left 6/6 previously-succeeding targets still succeeding.

Documentations

We published academic papers describing the ideas implemented in this project.

We presented the final goal of this project at AITP2017. Our position paper “Towards Smart Proof Search for Isabelle” is available at arXiv.

We also plan to improve the proof automation using evolutionary computation. We presented our plan during the poster session at GECCO2019. Our poster-only paper is available at ACM digital library and arXiv.

Preferred Citation

Screenshots

PSL example

Screenshot

Abduction Prover example

Screenshot