This folder contains code for the experiments run in the paper Feedback & Synthesis in LLM-Assisted Termination Proofs.

The actual running of these experiments is unfortunately/necessarily fairly specific to the Northeastern HPC cluster they were ran on. Some details follow. If you'd just like to see how the LLM theorem-prover integration works, the key files are ablation_experiment.py and ablation_prompt.py. These run an experiment and configure how error messages are shown to the LLM respectively. See run_ablation_experiment.py for an example of using these to compare model performance with different kinds of error feedback.

To run these experiments, you'll need:

• acl2s available on PATH
• Python 3.10+
• Python packages pexpect, sexpdata, sympy, tqdm, transformers, vllm, openai, openai_harmony
• A H200 GPU, preferably running on a slurm cluster (experiments expect to be launched this way, i.e. use SLURM_ARRAY_TASK_ID, SLURM_ARRAY_TASK_COUNT)

sbatch.sh is the original cluster launcher used for these runs. Submit with sbatch sbatch.sh. It is configured for Northeastern RC (gpu partition, H200, array 0-5%4), and hardcodes server paths for model weights and the python venv. You'll need to modify this for your setup.

Paper experiment runners

• Section 7 (ablation on stacked synthetic corpus): run_ablation_experiment.py
• Section 8 (ACL2s built-in analysis / CCG): run_ccg_experiment.py
• Section 8 (LLM + CCG/CCMS hints): run_ccg_ccms_experiment.py
• Section 9 (baseline on selected hard decomposition set): run_decomposition_experiment.py
• Section 9 ("revealed" decomposition prompt): run_revealed_experiment.py
• Section 9 constituent-function sampling (for expected rates): run_baseline_experiment.py

Notes that run_ccg_ccms_experiment.py expects baseline measure logs in baseline_logs/ (produced by run_baseline_experiment.py), so you'll need to run the baseline first.