Add Erdős benchmark suite: 1,183 problems with ground truth and expert context - #3
Add Erdős benchmark suite: 1,183 problems with ground truth and expert context#3JunjieAraoXiong wants to merge 3 commits into
Conversation
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.
- 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
![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 scripts to build and convert an Erdős problem corpus for benchmarking, along with an autoresearch loop for proving these problems using an external binary. The code changes are functional and well-structured. I have provided feedback on improving the robustness of subprocess command parsing using shlex, ensuring safe timeout values, and improving the LaTeX-to-text conversion and data persistence logic to avoid unnecessary truncation of mathematical content.
| import argparse | ||
| import json | ||
| import random | ||
| import subprocess |
There was a problem hiding this comment.
Consider importing shlex to safely parse the mathcode_cmd string, especially if it contains paths with spaces or multiple arguments.
| import subprocess | |
| import shlex | |
| import subprocess |
|
|
||
| start = time.monotonic() | ||
| try: | ||
| cmd_parts = mathcode_cmd.split() |
There was a problem hiding this comment.
Using split() on a command string is fragile as it fails if the path to the binary contains spaces. shlex.split() is the standard way to handle this.
| cmd_parts = mathcode_cmd.split() | |
| cmd_parts = shlex.split(mathcode_cmd) |
| ) | ||
| break | ||
|
|
||
| strategy_timeout = min(int(remaining), max_time_per_problem) |
There was a problem hiding this comment.
If remaining is less than 1 second, int(remaining) will be 0. Passing a timeout of 0 to subprocess.run might lead to immediate timeouts or unexpected behavior. It's safer to ensure a minimum timeout of at least 1 second.
| strategy_timeout = min(int(remaining), max_time_per_problem) | |
| strategy_timeout = max(1, min(int(remaining), max_time_per_problem)) |
| text = re.sub(r'\\\[', '', text) | ||
| text = re.sub(r'\\\]', '', text) | ||
| text = re.sub(r'\$\$', '', text) |
There was a problem hiding this comment.
Removing LaTeX display math delimiters without replacing them with a space causes adjacent words to merge (e.g., then\[N becomes thenN). This degrades the quality of the generated problem statements.
| text = re.sub(r'\\\[', '', text) | |
| text = re.sub(r'\\\]', '', text) | |
| text = re.sub(r'\$\$', '', text) | |
| text = re.sub(r'\\\\[', ' ', text) | |
| text = re.sub(r'\\\\]', ' ', text) | |
| text = re.sub(r'\\$\\\$', ' ', text) |
| except Exception: | ||
| return [] |
There was a problem hiding this comment.
Catching all exceptions silently here makes it difficult to diagnose issues like network failures or changes in the website's structure. Consider logging the error or catching more specific exceptions.
| author = meta.split(sep)[0].strip() | ||
| break | ||
| if body: | ||
| self.results.append({"author": author, "text": body[:1000]}) |
There was a problem hiding this comment.
Truncating expert comments to 1000 characters may cut off significant mathematical context and reasoning, which is a key part of this benchmark suite. Consider removing this limit.
| self.results.append({"author": author, "text": body[:1000]}) | |
| self.results.append({"author": author, "text": body}) |
| stats["has_lean"] += 1 | ||
| if md_path.exists(): | ||
| md_text = md_path.read_text(encoding="utf-8") | ||
| record["reference_proof_hint"] = md_text[:1000] |
There was a problem hiding this comment.
Truncating proof hints to 1000 characters might remove essential parts of the candidate solutions. Since these are intended for expert context and evaluation, it's better to preserve the full text.
| record["reference_proof_hint"] = md_text[:1000] | |
| record["reference_proof_hint"] = md_text |
| text = re.sub(r'\\\[', '', text) | ||
| text = re.sub(r'\\\]', '', text) | ||
| text = re.sub(r'\$\$', '', text) |
There was a problem hiding this comment.
Removing LaTeX delimiters without adding a space leads to merged words (e.g., is$$\sum becomes is\sum). Replacing them with a space ensures the text remains readable for LLMs.
| text = re.sub(r'\\\[', '', text) | |
| text = re.sub(r'\\\]', '', text) | |
| text = re.sub(r'\$\$', '', text) | |
| text = re.sub(r'\\\\[', ' ', text) | |
| text = re.sub(r'\\\\]', ' ', text) | |
| text = re.sub(r'\\$\\\$', ' ', text) |
| if md_path.exists(): | ||
| # Store first 500 chars as hint | ||
| md_text = md_path.read_text(encoding="utf-8") | ||
| autolean_json["reference_proof_hint"] = md_text[:500] |
There was a problem hiding this comment.
Truncating proof hints to 500 characters is very restrictive and likely removes the most useful parts of the candidate proofs. It's better to include the full text.
| autolean_json["reference_proof_hint"] = md_text[:500] | |
| autolean_json["reference_proof_hint"] = md_text |
1 participant
Summary
Comprehensive benchmark suite for evaluating automated theorem provers on Erdős problems.
Data sources integrated
Tools
run_benchmark.py— benchmark runner with GPT-erdos comparison modeautoresearch_erdos.py— standalone autoresearch loop (subprocess-based)build_erdos_corpus.py— corpus builder merging all 4 data sourcesintegrate_formal_conjectures.py— matches DeepMind Lean files to corpusscrape_top_comments.py— forum comment scraperHand-picked problems (9)
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
Benchmark runner features
--use-mathcode) and AUTOLEAN API mode--gpt-erdos-solutions)Test plan