Mining Tactics for Automated Theorem Proving

Artifact and Data for LLM2Ltac=============================== This repository contains the data and implementation of LLM2Ltac for our paper Mining Tactics for Automated Theorem Proving, submitted to ASE'26, for review. Folders rq1-rq7 correspond to the raw data of RQ1-RQ7 in the Evaluationsection of the paper. Below we describe the contents of each folder andthe steps to reproduce/verify the reported results. Prerequisites------------- - Python 3.8+- Standard Unix tools (tar, grep, wc) RQ1 -- Tactic Mining Results----------------------------- Contents: File Description -------------------------- ----------------------------------------------------------- log_gpt_all.tar.gz Archived evaluation logs for tactics mined from GPT log_deepseek_all.tar.gz Archived evaluation logs for tactics mined from DeepSeek strategy_gpt.tar.gz Archived strategy (natural language) count files for GPT strategy_deepseek.tar.gz Archived strategy (natural language) count files for DeepSeek gpt_count.py Counts valid tactics mined from GPT and their success-rate distribution across 10%-bins; also sums total strategies ds_count.py Same as gpt_count.py but for DeepSeek Verification steps: cd rq1 # 1. Extract all archives tar -xzf log_gpt_all.tar.gz tar -xzf log_deepseek_all.tar.gz tar -xzf strategy_gpt.tar.gz tar -xzf strategy_deepseek.tar.gz # 2. Run scripts python3 gpt_count.py python3 ds_count.py The output will show the total number of strategies, the number of validtactics, and the success-rate distribution (0%, 0%-10%, 10%-20%, ..., 100%)for each LLM. RQ2 -- Impact of k on Tactic Selection--------------------------------------- Contents: File / Directory Description ----------------- ----------------------------------------------------------- log_k_10/ Proof attempt logs with k=10 log_k_20/ Proof attempt logs with k=20 log_k_30/ Proof attempt logs with k=30 find_succ.py Walks each log_k_* directory, counts build_0.txt files and reports the number of successfully proved theorems per k value Verification steps: cd rq2 python3 find_succ.py The output will show the number of theorems successfully proved fork=10, k=20, and k=30. RQ3 -- Theorem Proving with Learned Tactics (DeepSeek vs GPT)-------------------------------------------------------------- Contents: File / Directory Description -------------------------- ----------------------------------------------------------- res_theorems_ds.tar.gz Archived proof logs using tactics mined from DeepSeek res_theorems_gpt.tar.gz Archived proof logs using tactics mined from GPT res_theorems_hammer.tar.gz Archived proof logs using CoqHammer thmjson/ Theorem JSON files per project (may already be extracted) check_log.py Prints total success counts Verification steps: cd rq3 # 1. Extract archives tar -xzf res_theorems_ds.tar.gz tar -xzf res_theorems_gpt.tar.gz # 2. Run script python3 check_log.py The output will show the number of theorems successfully proved usingtactics learned from DeepSeek and GPT respectively and the number oftheorems successfully proved by using CoqHammer. RQ4 -- Proving without Generalization Testing Tactics------------------------------------------------------ Contents: File / Directory Description ----------------- ----------------------------------------------------------- log/ Proof attempt logs organized by project (compcert/, coq-art/, coq-ext-lib/, vfa/) thmjson/ Theorem definition JSON files per project check_log.py Counts successfully proved theorems (without generalization testing) from DeepSeek-learned tactics. Verification steps: cd rq4 python3 check_log.py The output will show the number of theorems successfully proved. RQ5 -- Ablation Study---------------------- Contents: File Description -------------------------- ----------------------------------------------------------- log_ablation1_all.tar.gz Archived evaluation logs for ablation variant 1 log_ablation2_all.tar.gz Archived evaluation logs for ablation variant 2 ablation1.py Reads result*.json from log_ablation1_all/, computes each tactic's success rate, and reports the distribution across 10%-bins ablation2.py Same as ablation1.py but for ablation variant 2 (log_ablation2_all/) Verification steps: cd rq5 # 1. Extract archives tar -xzf log_ablation1_all.tar.gz tar -xzf log_ablation2_all.tar.gz # 2. Run scripts python3 ablation1.py python3 ablation2.py The output will show the success-rate distribution and total valid tacticcount for each ablation variant. RQ6 -- Start2Rocq Baseline Verification----------------------------------------- Contents: File Description ----------------- ----------------------------------------------------------- log_compcert.txt Start2Rocq verification log for CompCert log_coqart.txt Start2Rocq verification log for Coq'Art log_coqext.txt Start2Rocq verification log for coq-ext-lib log_vfa.txt Start2Rocq verification log for VFA These files are the Start2Rocq verification logs. Each log records theCoq compilation process where the enhanced-hammer tactic is applied totheorems. Verification steps: cd rq6 # Count the number of theorems successfully proved by the hammer # across all projects grep -r "The tactics have finished Proof process" | wc -l # Or verify per project grep -c "The tactics have finished Proof process" log_compcert.txt | wc -l grep -c "The tactics have finished Proof process" log_coqart.txt | wc -l grep -c "The tactics have finished Proof process" log_coqext.txt | wc -l grep -c "The tactics have finished Proof process" log_vfa.txt | wc -l The count from each file represents the number of theorems that Start2Rocqsuccessfully proved in the corresponding Coq project. RQ7 -- Claude Code Baseline----------------------------- Contents: File Description ----------------------- ----------------------------------------------------------- only_agent.tar.gz Archived results of the agent-only experiment only_agent_log.tar.gz Archived Claude Code execution logs These archives contain the Claude Code execution logs from the agent-onlybaseline experiment, where an LLM agent attempts to prove theorems withoutusing any mined tactics. Verification steps: cd rq7 # Extract archives to inspect the logs tar -xzf only_agent.tar.gz After extraction, you can inspect the logs manually. Since the agent'sproof output format is not standardized, this step is verified throughmanual inspection rather than automated scripts.