From 7047a770d12d0d9f9f44324bbeb620788b4a31e3 Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Fri, 29 May 2026 02:42:04 -0500 Subject: [PATCH] feat: AlphaProof batch mode with copy-if pre-filter MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit New CLI mode: python alphaproof_loop.py --batch Pipeline: 1. Pre-filter scans Lean codebase (11,434 theorems) 2. Classifies trivial (63.5%) vs non-trivial (36.5%) 3. Prioritizes non-trivial by tactic count + sorry weight 4. Feeds hardest problems to Ollama LLM first 5. Skips trivial theorems entirely (zero deltas) Usage: python alphaproof_loop.py --batch ../../0-Core-Formalism/lean/Semantics/Semantics python alphaproof_loop.py --batch . --max-iter 20 --model deepseek-coder-v2:16b Same pattern as vectorized copy_if: - Skip zero deltas → 40x faster (blog post) - Skip trivial theorems → 2.7x faster (pre-filter) - Focus solver on residuals → fewer iterations --- 4-Infrastructure/shim/alphaproof_loop.py | 165 ++++++++++++++++++++++- 1 file changed, 164 insertions(+), 1 deletion(-) diff --git a/4-Infrastructure/shim/alphaproof_loop.py b/4-Infrastructure/shim/alphaproof_loop.py index fb863811..2cd51d74 100644 --- a/4-Infrastructure/shim/alphaproof_loop.py +++ b/4-Infrastructure/shim/alphaproof_loop.py @@ -16,7 +16,7 @@ import tempfile import time from datetime import datetime, timezone from pathlib import Path -from typing import Optional +from typing import Optional, List, Dict try: import requests @@ -24,6 +24,13 @@ try: except ImportError: HAS_REQUESTS = False +# Import pre-filter for copy-if pattern +try: + from lean_proof_prefilter import analyze_file, classify_theorem, extract_theorems + HAS_PREFILTER = True +except ImportError: + HAS_PREFILTER = False + # --------------------------------------------------------------------------- # Configuration @@ -260,6 +267,138 @@ def fpga_accelerate(candidates: list[dict]) -> list[dict]: # --------------------------------------------------------------------------- +# Proof prioritization (copy-if pre-filter) +# --------------------------------------------------------------------------- + + +def prioritize_problems(lean_dir: str, max_problems: int = 20) -> List[Dict]: + """Pre-filter and prioritize proof problems using the copy-if pattern. + + Scans the Lean codebase, classifies theorems as trivial/non-trivial, + and returns the highest-priority non-trivial problems for the LLM. + + This is the Lean equivalent of the vectorized copy_if: + - Trivial theorems (zero deltas) = skip + - Non-trivial theorems (non-zero deltas) = feed to solver + + Args: + lean_dir: Path to Lean source directory. + max_problems: Maximum number of problems to return. + + Returns: + List of prioritized problem dicts with file, theorem, and priority. + """ + if not HAS_PREFILTER: + print("[alphaproof] pre-filter not available, using default order") + return [] + + problems = [] + lean_path = Path(lean_dir) + + for lean_file in sorted(lean_path.rglob('*.lean')): + if '.lake' in str(lean_file): + continue + try: + analysis = analyze_file(str(lean_file)) + for thm in analysis['theorems']: + if thm['classification'] == 'non_trivial': + # Priority: more tactics = harder = higher priority + tactic_count = len(thm.get('category', '').split(',')) + has_sorry = 'sorry' in thm.get('category', '') + priority = tactic_count + (10 if has_sorry else 0) + + problems.append({ + 'file': str(lean_file), + 'theorem': thm['name'], + 'kind': thm['kind'], + 'line': thm['line'], + 'category': thm['category'], + 'priority': priority, + 'block': thm['block'], + }) + except Exception: + continue + + # Sort by priority (highest first = hardest problems first) + problems.sort(key=lambda p: p['priority'], reverse=True) + + # Deduplicate by theorem name + seen = set() + unique = [] + for p in problems: + if p['theorem'] not in seen: + seen.add(p['theorem']) + unique.append(p) + + return unique[:max_problems] + + +def batch_proof_search(lean_dir: str, max_iterations: int = 10, + model: str = DEFAULT_MODEL, + lake_project: Optional[str] = None) -> Dict: + """Run AlphaProof on prioritized non-trivial theorems. + + Uses the copy-if pre-filter to skip trivial theorems and focus + the LLM solver on the hardest problems first. + """ + problems = prioritize_problems(lean_dir) + + if not problems: + print("[alphaproof] no non-trivial problems found") + return {'problems': [], 'results': []} + + print(f"[alphaproof] found {len(problems)} non-trivial problems") + print(f"[alphaproof] top 5: {[p['theorem'] for p in problems[:5]]}") + + results = [] + for i, problem in enumerate(problems): + print(f"\n[alphaproof] [{i+1}/{len(problems)}] {problem['theorem']}" + f" (priority={problem['priority']}, category={problem['category']})") + + # Build prompt from the theorem block + prompt = ( + f"Prove this Lean 4 theorem. The file is {problem['file']}, " + f"line {problem['line']}.\n\n" + f"```lean\n{problem['block']}\n```\n\n" + f"Replace the sorry with a complete proof. " + f"Use omega, simp, decide, norm_num, ring, or linarith as appropriate." + ) + + result = search_loop( + problem=prompt, + max_iterations=max_iterations, + model=model, + lake_project=lake_project, + ) + + results.append({ + 'theorem': problem['theorem'], + 'file': problem['file'], + 'priority': problem['priority'], + 'success': result['success'], + 'iterations': result['iterations'], + 'solution': result.get('solution', ''), + }) + + if result['success']: + print(f"[alphaproof] SOLVED {problem['theorem']} " + f"in {result['iterations']} iterations") + else: + print(f"[alphaproof] FAILED {problem['theorem']} " + f"after {result['iterations']} iterations") + + # Summary + solved = sum(1 for r in results if r['success']) + print(f"\n[alphaproof] summary: {solved}/{len(results)} solved") + + return { + 'problems': problems, + 'results': results, + 'solved': solved, + 'total': len(results), + } + + # Main search loop # --------------------------------------------------------------------------- @@ -372,9 +511,33 @@ if __name__ == '__main__': if len(sys.argv) < 2: print("Usage: python alphaproof_loop.py " "[--max-iter N] [--model MODEL]") + print(" python alphaproof_loop.py --batch " + "[--max-iter N] [--model MODEL]") sys.exit(1) problem_arg = sys.argv[1] + + # Batch mode: run pre-filter on Lean codebase + if problem_arg == '--batch': + lean_dir = sys.argv[2] if len(sys.argv) > 2 else '.' + max_iter = 10 + model_name = DEFAULT_MODEL + + for i, arg in enumerate(sys.argv[3:], 3): + if arg == '--max-iter' and i + 1 < len(sys.argv): + max_iter = int(sys.argv[i + 1]) + elif arg == '--model' and i + 1 < len(sys.argv): + model_name = sys.argv[i + 1] + + result = batch_proof_search(lean_dir, max_iterations=max_iter, + model=model_name) + + print(f"\n{'='*60}") + print(f"Solved: {result['solved']}/{result['total']}") + print(f"{'='*60}") + sys.exit(0 if result['solved'] > 0 else 1) + + # Single problem mode if os.path.isfile(problem_arg): problem_text = Path(problem_arg).read_text() else: