Add decomposition, Aristotle integration, and autoresearch loop - #2
Add decomposition, Aristotle integration, and autoresearch loop#2JunjieAraoXiong wants to merge 19 commits into
Conversation
…hing Break up the 1,776-line core.py into single-responsibility modules: - providers.py (449 lines): OpenRouter, Codex Exec backends and response parsing - compiler.py (208 lines): Lean compilation, error extraction, error memory - evaluation.py (230 lines): semantic fidelity grading prompts and payload parsing - cache.py (123 lines): SHA256-based LLM response cache to avoid redundant API calls core.py is now 831 lines focused purely on pipeline orchestration. Cache features: - Keyed by (prompt_hash, model) to deduplicate identical requests - Only caches successful responses (returncode == 0) - Sharded storage in .autolean_cache/ with 2-char subdirectories - New CLI flags: --no-cache, --cache-dir
…licate EVAL_GRADES - Cache writes now use temp file + os.replace() for atomicity - Removed mkdir from cache __init__ (deferred to put) - Renamed _CODEX_EXEC_CODING_MODEL to CODEX_EXEC_CODING_MODEL (public) - Consolidated _EVAL_GRADES into EVAL_GRADES in evaluation.py, imported elsewhere - Removed indent=2 from cache JSON for compact storage
Tier 1 (in Mathlib, test retrieval): Erdős-Szekeres, Erdős-Ko-Rado, Erdős-Ginzburg-Ziv, Bertrand's postulate, ∑1/p diverges, primes ≡3 mod 4 Tier 2 (not in Mathlib, test proving): Ramsey R(3,3)=6, Erdős-Gallai, Erdős-Mordell inequality Runner supports MathCode binary mode and AUTOLEAN Python API mode, outputs JSON + markdown summary tables.
…tion - Wrap prompt sections in XML tags (context, file_header, theorem, retrieved_premises, do_not_change, task) per Claude best practices - Add goal_state_near_failure and failing_proof tags to repair prompts - New build_sketch_prompt() for have...sorry skeleton generation (max 5 holes) - Add retrieved_premises_block parameter to build_prompts() for retrieval injection (backward compatible, None = no change) - Strengthen anti-trivialization constraints
New module axle_provider.py: - AxleVerifier class: sync wrapper around async AxleClient - verify(), sorry_to_lemmas(), extract_theorems(), repair() methods - compile_via_axle() drop-in replacement for local lake compilation - Rate limiting (semaphore=20), exponential backoff on transient errors - Lazy import: works without axiom-axle installed, clear error at runtime
New module retrieval.py: - MathLibIndex: FAISS-backed nearest-neighbor search over Mathlib theorems - Embeds corpus with sentence-transformers (default: all-MiniLM-L6-v2) - retrieve(query, k=25) returns ranked RetrievedPremise list - format_premises_for_prompt() for injection into LLM prompts - build_corpus_from_lean_project() extracts theorem signatures from .lean files - Save/load precomputed indices to disk - CLI: build corpus, index, and query subcommands - Lazy imports: works without torch/faiss installed
- build_erdos_corpus.py: merges 3 data sources: 1. Tao's erdosproblems GitHub (problems.yaml) — metadata, tags, status 2. gpt-erdos dataset (unsolved.jsonl) — LaTeX problem statements 3. gpt-erdos solutions/ — GPT 5.2 Pro candidate proofs + Lean files 4. erdosproblems.com forum threads — expert discussions incl Tao's comments - convert_erdos_dataset.py: simpler converter for gpt-erdos JSONL only - Full corpus: 1183 problems, 675 with LaTeX, 387 formalized on site - Comment scraper: working on forum threads (87 comments on #728, 10 from Tao) - Filter by tags, status, problem numbers
Data integration: - 1183 Erdős problems from Tao's database + gpt-erdos LaTeX - 387 DeepMind formal-conjectures Lean files matched to corpus - 366 expert comments scraped (43 from Tao across 13 problems) - GPT-5.2 Pro candidate proofs from gpt-erdos for comparison New tools: - integrate_formal_conjectures.py: match DeepMind Lean files to corpus - scrape_top_comments.py: scrape erdosproblems.com forum discussions - build_erdos_corpus.py: merge all data sources into unified corpus - convert_erdos_dataset.py: simpler gpt-erdos JSONL converter Benchmark runner updates: - GPT-erdos comparison mode (--gpt-erdos-solutions) - Side-by-side table: Our Prover vs GPT-5.2+Aristotle vs Ground Truth Autoresearch loop: - autoresearch_erdos.py: autonomous proving loop (karpathy-inspired) - 4 strategies: direct, retrieval, decomposition, expert - Resume support, live logging, per-problem time budget - Summary generation with by-strategy and by-tag breakdowns
New module aristotle_provider.py: - AristotleAutoformalize class: sync wrapper around async aristotlelib - formalize_latex(): LaTeX proof → Lean 4 via Aristotle API - formalize_lean_file(): submit Lean with sorry holes for completion - Lazy import: works without aristotlelib installed - Matches Kevin Barreto's workflow: GPT proof → Aristotle → Lean
New module autoresearch.py — autonomous proving loop that uses all AUTOLEAN modules natively (not subprocess): - 5 strategies: direct, retrieval, decomposition, expert, aristotle - Uses core.py compile-repair loop, retrieval.py FAISS index, decomposition.py sorry2lemma pipeline, aristotle_provider.py - Resume support via JSONL log - Per-problem time budget - Filter by status/tags, shuffle support - Generates markdown summary with by-strategy and by-tag breakdowns
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request introduces three new modules: aristotle_provider.py for LaTeX to Lean 4 autoformalization, autoresearch.py for an autonomous proving loop, and decomposition.py for a sketch-then-solve proof pipeline. The reviewer identified several issues, including a bug in command-line argument splitting for paths with spaces, a resource leak due to uncleaned temporary directories, an unused timeout parameter, and fragile JSON parsing that fails when LLM responses include markdown fences.
| cmd = compile_cmd.replace("{file}", str(tmp_path.resolve())) | ||
| import shlex | ||
| proc = subprocess.run(shlex.split(cmd), cwd=str(cwd), |
There was a problem hiding this comment.
Using shlex.split on a command string after replacing a placeholder with a file path is unsafe if the path contains spaces. For example, if tmp_path contains a space, it will be split into multiple arguments, causing the command to fail. It is safer to split the template first and then replace the placeholder in the resulting list of arguments.
import shlex
argv = [arg.replace("{file}", str(tmp_path.resolve())) for arg in shlex.split(compile_cmd)]
proc = subprocess.run(argv, cwd=str(cwd), capture_output=True, text=True, check=False)| timeout_seconds: int = 1800, # 30 min default | ||
| ): | ||
| lib = _import_aristotle() | ||
| key = api_key or os.environ.get("ARISTOTLE_API_KEY") | ||
| if key: | ||
| lib.set_api_key(key) | ||
| self.polling_interval = polling_interval | ||
| self.timeout_seconds = timeout_seconds | ||
| self._lib = lib |
There was a problem hiding this comment.
The timeout_seconds parameter is stored in self.timeout_seconds but is never utilized in the subsequent API calls (e.g., in wait_for_completion). This makes the timeout configuration ineffective. If the underlying library supports a timeout, it should be passed through; otherwise, the parameter should be removed or implemented via asyncio.wait_for.
| CommandResult with stdout=Lean code if successful, returncode=0. | ||
| """ | ||
| prompt = self._build_prompt(latex_proof, problem_statement, theorem_name) | ||
| output_dir = output_dir or Path(tempfile.mkdtemp(prefix="aristotle_")) |
There was a problem hiding this comment.
The temporary directory created by tempfile.mkdtemp is never cleaned up. This can lead to an accumulation of temporary directories in the system's temp folder, especially during long-running autonomous research loops. Consider using tempfile.TemporaryDirectory as a context manager or ensuring shutil.rmtree is called in a finally block after the Lean code has been extracted. This issue also occurs at line 152.
| obj = json.loads(response_text) if response_text.strip().startswith("{") else {} | ||
| lean_code = obj.get("lean", response_text) |
There was a problem hiding this comment.
The JSON parsing logic is fragile. LLMs often wrap JSON responses in markdown code blocks (e.g., json ... ), which would cause response_text.strip().startswith("{") to be false. This results in the entire response (including markdown fences) being treated as Lean code, leading to compilation errors. Consider using a more robust extraction method that handles markdown fences or searches for the first '{'. This issue also occurs at line 292.
- Parses Lean compiler output into structured diagnostics - Shows source code with inline error annotations and pointer arrows - Extracts goal state at failure point (hypotheses + remaining goals) - Suggests fixes for common errors (type mismatch, tactic failure, etc.) - Optional LLM-powered plain English explanation - Useful for education: students see exactly which proof step broke
… Erdős) Reliable demo for presentations — no API dependency. Supports --live mode (try MathCode first, fallback to cached). 8 theorems: det(AB), det(Aᵀ), even+even, even², √2, primes, Bertrand, e.
1 participant
Summary
Three new modules that extend AUTOLEAN's proving capabilities:
1.
decomposition.py— Sub-goal decomposition via sorry2lemmahave ... := by sorryholessorry2lemma()extracts each sorry into a standalone lemma2.
aristotle_provider.py— Aristotle (Harmonic) autoformalizationaristotlelibpackage)formalize_latex(): submit natural language proof for autoformalizationformalize_lean_file(): submit Lean with sorry holes for completionaristotlelibinstalled3.
autoresearch.py— Autonomous proving loop (5 strategies)Inspired by karpathy/autoresearch. Iterates through problems trying multiple strategies:
directretrievaldecompositionexpertaristotleFeatures: resume support, per-problem time budget, filter by tags/status, live JSONL logging, markdown summary generation.
All modules use lazy imports and work without optional dependencies installed.
Context
Building toward an Erdős theorem benchmark — testing AUTOLEAN on 1,183 problems from erdosproblems.com with comparison against GPT-5.2 + Aristotle results.
Test plan