ai-research-survey

scan.json (29892B)

---

 {
   "paper": {
     "title": "Proving the Coding Interview: A Benchmark for Formally Verified Code Generation",
     "authors": [
       "Quinn Dougherty",
       "Ronak Mehta"
     ],
     "year": 2025,
     "venue": "2025 IEEE/ACM International Workshop on Large Language Models for Code (LLM4Code)",
     "arxiv_id": "2502.05714",
     "doi": "10.1109/LLM4Code66737.2025.00014"
   },
   "scan_version": 3,
   "active_modules": [
     "experimental_rigor",
     "data_leakage"
   ],
   "methodology_tags": [
     "benchmark-eval"
   ],
   "key_findings": "FVAPPS is the largest formal verification benchmark with 4,715 Lean 4 samples (1,083 curated), derived from the APPS programming benchmark. On 406 theorems from 101 randomly sampled problems, Claude 3.5 Sonnet proved 30% and Gemini 1.5 Pro proved 18%, with most successes being trivial or syntactic rather than deeply nontrivial proofs. A human baseliner spent 10 hours on a single problem and completed the definition but no proofs, suggesting formal verification remains extremely challenging for both humans and current LLMs.",
   "checklist": {
     "artifacts": {
       "code_released": {
         "applies": true,
         "answer": true,
         "justification": "The paper states 'All code and prompts used for the generation can be found at our open-source GitHub repository' (footnote 7: https://github.com/quinn-dougherty/fvapps)."
       },
       "data_released": {
         "applies": true,
         "answer": true,
         "justification": "The benchmark dataset is released on HuggingFace at https://huggingface.co/datasets/quinn-dougherty/fvapps, mentioned multiple times including in the abstract."
       },
       "environment_specified": {
         "applies": true,
         "answer": false,
         "justification": "The paper specifies Lean 4.12.0 with commit hash and Mathlib commit (809c3fb3b5c8f5d7dace56e200b426187516535a), but does not provide comprehensive environment specifications for the Python side of the pipeline (pytest, Python version, other dependencies). No requirements.txt or Dockerfile is mentioned."
       },
       "reproduction_instructions": {
         "applies": true,
         "answer": false,
         "justification": "The paper describes the pipeline at a high level (Section II.B) and references the GitHub repo, but does not include step-by-step reproduction instructions in the paper itself. The pipeline stages are described narratively but without specific commands or scripts to run."
       }
     },
     "statistical_methodology": {
       "confidence_intervals_or_error_bars": {
         "applies": true,
         "answer": false,
         "justification": "Main results are reported as point estimates only: '30%' and '18.5%' theorem proving rates with no confidence intervals, error bars, or uncertainty measures."
       },
       "significance_tests": {
         "applies": true,
         "answer": false,
         "justification": "The paper compares Sonnet (30%) vs Gemini (18.5%) without any statistical significance tests. The claim that Sonnet outperforms Gemini rests solely on comparing two raw percentages."
       },
       "effect_sizes_reported": {
         "applies": true,
         "answer": true,
         "justification": "Raw counts and percentages are given with full context: 'Sonnet accomplished 121 (30%) and Gemini accomplished 74 (18.5%)' out of 406 theorems, and Table II breaks down by quality level. The reader can compute effect sizes from these numbers."
       },
       "sample_size_justified": {
         "applies": true,
         "answer": false,
         "justification": "The paper evaluates 101 randomly sampled problems from 4,715 but does not justify why 101 was chosen or discuss whether this sample size provides sufficient statistical power."
       },
       "variance_reported": {
         "applies": true,
         "answer": false,
         "justification": "Results are from single experimental runs. No variance, standard deviation, or spread measures are reported across multiple runs or seeds."
       }
     },
     "evaluation_design": {
       "baselines_included": {
         "applies": true,
         "answer": true,
         "justification": "Two model baselines (Claude 3.5 Sonnet, Gemini 1.5 Pro) and one human baseline are included. They also attempted open-source models (DeepSeek-Prover-V1.5-RL) which could not make progress."
       },
       "baselines_contemporary": {
         "applies": true,
         "answer": true,
         "justification": "Claude 3.5 Sonnet (October 2024) and Gemini 1.5 Pro (November 2024) were contemporary frontier models at the time of evaluation."
       },
       "ablation_study": {
         "applies": true,
         "answer": false,
         "justification": "The scaffolding loop has multiple design decisions (one-theorem-at-a-time approach, max iterations, prompt engineering choices) but no ablation study systematically varies these components. The paper notes they moved to one-at-a-time solving but doesn't report controlled comparisons."
       },
       "multiple_metrics": {
         "applies": true,
         "answer": true,
         "justification": "Multiple metrics are reported: definition completion rate, theorem proving rate, qualitative categorization of proof types (Figure 6), number of iterations to convergence (Figures 7-8), and breakdown by quality assurance level (Table II)."
       },
       "human_evaluation": {
         "applies": true,
         "answer": true,
         "justification": "Qualitative human assessment of theorem proofs is provided in Figure 6 and Table III, categorizing solutions into buckets like 'Actually nontrivial', 'Bug', 'Too trivial', 'Easy branch of if', etc."
       },
       "held_out_test_set": {
         "applies": true,
         "answer": true,
         "justification": "The 101 problems were randomly sampled from the full 4,715-sample benchmark. The benchmark was not used for any model tuning or development decisions."
       },
       "per_category_breakdown": {
         "applies": true,
         "answer": true,
         "justification": "Results are broken down by quality assurance level (Unguarded/Guarded/Guarded and Plausible) in Table II, and by qualitative proof category in Figure 6 and Table III."
       },
       "failure_cases_discussed": {
         "applies": true,
         "answer": true,
         "justification": "Section III.E discusses Sonnet's reliance on imperative programming with Id.run do that doesn't lend itself to proofs. Section III.B describes the human's stack overflow issues. Section III.A notes open-source models couldn't make progress."
       },
       "negative_results_reported": {
         "applies": true,
         "answer": true,
         "justification": "Multiple negative results: DeepSeek-Prover failed entirely (Section III.A), the human baseline couldn't complete any proofs in 10 hours (Section III.B), Sonnet diverged after 100 loops on sample 23's second theorem (Section III.C)."
       }
     },
     "claims_and_evidence": {
       "abstract_claims_supported": {
         "applies": true,
         "answer": true,
         "justification": "Abstract claims of 4,715 samples, 1,083 curated, 30% Sonnet and 18% Gemini theorem proving rates are all supported by the results. Minor discrepancy: abstract says '100 randomly selected samples' while body says 101, but this is a rounding issue."
       },
       "causal_claims_justified": {
         "applies": true,
         "answer": false,
         "justification": "Section III.A.1 states 'We found significantly higher success rates by following a number of key insights' regarding prompt engineering, but this claim is based on informal observation without controlled comparison or ablation."
       },
       "generalization_bounded": {
         "applies": true,
         "answer": true,
         "justification": "Claims are largely bounded to Lean 4 and the specific models tested. The paper frames results as preliminary baselines on their specific benchmark rather than making broad generalizations about LLM verification capabilities."
       },
       "alternative_explanations_discussed": {
         "applies": true,
         "answer": false,
         "justification": "The paper does not discuss alternative explanations for the low proving rates. Could the low success be due to the quality of the benchmark's theorem statements, the scaffolding design, the prompt quality, or Lean 4's evolving API? These alternatives are not considered."
       },
       "proxy_outcome_distinction": {
         "applies": true,
         "answer": true,
         "justification": "The paper measures sorry-completion rates and reports them as such ('correctly proves 30%'). Claims match the granularity of measurements. The qualitative categorization in Figure 6 explicitly distinguishes trivial proofs from nontrivial ones, avoiding overclaiming."
       }
     },
     "setup_transparency": {
       "model_versions_specified": {
         "applies": true,
         "answer": false,
         "justification": "Claude is specified precisely as 'claude-3-5-sonnet-20241022'. However, Gemini is specified only as 'Gemini 1.5 Pro' with footnote 'Retrieved in early November 2024' — no API version or snapshot date. Per schema rules, marketing names without a snapshot date do not count."
       },
       "prompts_provided": {
         "applies": true,
         "answer": true,
         "justification": "The paper states 'All code and prompts used for the generation can be found at our open-source GitHub repository' (footnote 7). The prompting strategy is described in Section III.A.1 and full prompts are available in the repository."
       },
       "hyperparameters_reported": {
         "applies": true,
         "answer": false,
         "justification": "No mention of temperature, top-p, max tokens, or other sampling parameters for any of the LLM API calls. Only the maximum number of scaffolding loop iterations is reported."
       },
       "scaffolding_described": {
         "applies": true,
         "answer": true,
         "justification": "The scaffolding loop is well-described in Section II.B with Figure 3, including error feedback mechanism, max iterations per stage (5 for stages 1-3, 10 for stage 4, 25/50 for baseline), and the one-theorem-at-a-time strategy."
       },
       "data_preprocessing_documented": {
         "applies": true,
         "answer": true,
         "justification": "The 5-stage pipeline is described in detail in Section II.B: preprocessing APPS, generating property-based tests with pytest, converting to Lean, adding unit test quality assurance, and Plausible filtering. Sample counts at each stage are given (4715, 2089, 1083)."
       }
     },
     "limitations_and_scope": {
       "limitations_section_present": {
         "applies": true,
         "answer": true,
         "justification": "Section V (Discussion) opens with 'Our current presentation has a few limitations, and clear directions for future work' and discusses multiple specific limitations over two paragraphs."
       },
       "threats_to_validity_specific": {
         "applies": true,
         "answer": true,
         "justification": "Section V discusses specific threats: theorem statements may not correspond to desirable properties, theorems may not cover the full range of ideal properties, particular theorems may be vacuous, and the gap between imperative solutions and proof-amenable structures."
       },
       "scope_boundaries_stated": {
         "applies": true,
         "answer": false,
         "justification": "The paper does not explicitly state what the results do NOT show. While limitations are discussed, there are no explicit scope boundaries like 'our results do not generalize to X' or 'we do not claim Y'. The discussion of limitations is about potential quality issues, not about claims the authors are not making."
       }
     },
     "data_integrity": {
       "raw_data_available": {
         "applies": true,
         "answer": true,
         "justification": "The full dataset of 4,715 Lean 4 files is publicly available on HuggingFace with quality assurance tagging. All baseline code is available on GitHub."
       },
       "data_collection_described": {
         "applies": true,
         "answer": true,
         "justification": "Section II describes starting from the APPS dataset (scraped from CodeForces and LeetCode), then details the 5-stage pipeline for converting Python problems to Lean 4 theorem specifications."
       },
       "recruitment_methods_described": {
         "applies": true,
         "answer": false,
         "justification": "The paper includes a human baseline ('a baseliner' who spent 10 hours) but provides no information about who this person was, how they were selected, or their qualifications beyond being able to write Lean."
       },
       "data_pipeline_documented": {
         "applies": true,
         "answer": true,
         "justification": "The full pipeline from APPS to final benchmark is documented across 5 stages with Table I showing iteration counts, and final sample counts at each quality level (4715 → 2089 → 1083)."
       }
     },
     "conflicts_of_interest": {
       "funding_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Acknowledgments section states: 'We are also grateful to the Anthropic External Researcher program for providing API credits for benchmark generation, and to FAR.ai for providing operations and administrative support.'"
       },
       "affiliations_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Author affiliations are listed: Quinn Dougherty at Beneficial AI Foundation, Ronak Mehta as Independent."
       },
       "funder_independent_of_outcome": {
         "applies": true,
         "answer": false,
         "justification": "Anthropic provided API credits for benchmark generation, and Anthropic's Claude 3.5 Sonnet is one of the two models evaluated. Anthropic has a financial interest in their model performing well on benchmarks."
       },
       "financial_interests_declared": {
         "applies": true,
         "answer": false,
         "justification": "No competing interests or financial interests statement is provided in the paper."
       }
     },
     "contamination": {
       "training_cutoff_stated": {
         "applies": true,
         "answer": false,
         "justification": "The paper states model access dates (October/November 2024) but does not state the training data cutoff dates for either Claude 3.5 Sonnet or Gemini 1.5 Pro."
       },
       "train_test_overlap_discussed": {
         "applies": true,
         "answer": false,
         "justification": "APPS problems are derived from CodeForces and LeetCode, which are heavily represented in LLM training data. The paper does not discuss whether the evaluated models may have seen the original problems or their solutions during training."
       },
       "benchmark_contamination_addressed": {
         "applies": true,
         "answer": false,
         "justification": "APPS was published in 2021 and its source problems are from public competitive programming platforms. Both evaluated models were trained well after 2021 and could have seen these problems. This contamination risk is not discussed, despite the Lean translation preserving the underlying algorithmic problems."
       }
     },
     "human_studies": {
       "pre_registered": {
         "applies": false,
         "answer": false,
         "justification": "This is primarily a benchmark paper. The single human baseliner is an informal data point, not a human subjects study."
       },
       "irb_or_ethics_approval": {
         "applies": false,
         "answer": false,
         "justification": "No human subjects study was conducted. The single human baseline is an informal demonstration, not a research study requiring ethics review."
       },
       "demographics_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human subjects study. The paper mentions a single 'baseliner' without characterization, but this is not a human study."
       },
       "inclusion_exclusion_criteria": {
         "applies": false,
         "answer": false,
         "justification": "No human subjects study was conducted."
       },
       "randomization_described": {
         "applies": false,
         "answer": false,
         "justification": "No human subjects study was conducted."
       },
       "blinding_described": {
         "applies": false,
         "answer": false,
         "justification": "No human subjects study was conducted."
       },
       "attrition_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human subjects study was conducted."
       }
     },
     "cost_and_practicality": {
       "inference_cost_reported": {
         "applies": true,
         "answer": false,
         "justification": "No API costs, tokens consumed, or wall-clock time are reported for either the benchmark generation pipeline or the baseline evaluation experiments, despite both involving substantial LLM API usage."
       },
       "compute_budget_stated": {
         "applies": true,
         "answer": false,
         "justification": "No total computational budget is stated. The paper does not report GPU hours, total API spend, or the aggregate cost of running the benchmark generation or baseline evaluations."
       }
     },
     "experimental_rigor": {
       "seed_sensitivity_reported": {
         "applies": true,
         "answer": false,
         "justification": "All results appear to be from single experimental runs. No analysis of sensitivity to random seeds or LLM sampling stochasticity is reported."
       },
       "number_of_runs_stated": {
         "applies": true,
         "answer": false,
         "justification": "The number of scaffolding loop iterations is stated (25 for defs, 50 per theorem), but the number of independent experimental runs is not stated. Results appear to be from a single run."
       },
       "hyperparameter_search_budget": {
         "applies": true,
         "answer": false,
         "justification": "Prompt engineering was guided by insights from Victor Taelin (Section III.A.1) but no systematic hyperparameter search was conducted or budgeted. The paper does not report how many prompt variants were tried."
       },
       "best_config_selection_justified": {
         "applies": true,
         "answer": false,
         "justification": "The paper describes arriving at prompt design choices through informal iteration ('We found significantly higher success rates by following a number of key insights') but does not justify the selection through systematic comparison or validation."
       },
       "multiple_comparison_correction": {
         "applies": false,
         "answer": false,
         "justification": "No statistical tests are performed, so multiple comparison correction is not applicable."
       },
       "self_comparison_bias_addressed": {
         "applies": true,
         "answer": false,
         "justification": "Claude 3.5 Sonnet was used to GENERATE the benchmark (all 5 pipeline stages) and is then evaluated on it. This creates a potential bias where the benchmark may be systematically easier or harder for the generating model. This bias is not acknowledged or discussed."
       },
       "compute_budget_vs_performance": {
         "applies": true,
         "answer": false,
         "justification": "Both models are given the same iteration budget (25/50 loops) but actual compute (tokens, cost) is not reported or compared. Sonnet and Gemini may have very different token costs per iteration, making the budget effectively unequal."
       },
       "benchmark_construct_validity": {
         "applies": true,
         "answer": false,
         "justification": "Section V briefly mentions that theorem statements 'may not correspond to desirable properties' but does not substantively analyze whether the benchmark measures formal verification capability as claimed. No comparison with alternative benchmarks or analysis of what skills the benchmark actually tests."
       },
       "scaffold_confound_addressed": {
         "applies": true,
         "answer": true,
         "justification": "Both Sonnet and Gemini use the same scaffolding loop with the same iteration limits ('Both Sonnet and Gemini ran for a maximum of 25 loops for the defs and a max of 50 loops for each theorem'), controlling for scaffold effects."
       }
     },
     "data_leakage": {
       "temporal_leakage_addressed": {
         "applies": true,
         "answer": false,
         "justification": "APPS was published in 2021 from problems scraped from CodeForces and LeetCode. Models evaluated in late 2024 could have trained on these problems. The temporal leakage risk is not discussed."
       },
       "feature_leakage_addressed": {
         "applies": true,
         "answer": false,
         "justification": "The scaffolding provides the English-language problem description from APPS alongside the Lean file. If models have seen APPS problems and solutions during training, the English description could leak algorithmic solutions. This is not discussed."
       },
       "non_independence_addressed": {
         "applies": true,
         "answer": false,
         "justification": "No discussion of whether APPS problems (from CodeForces/LeetCode) or similar problems appeared in the models' training data. The independence of test problems from training data is not verified."
       },
       "leakage_detection_method": {
         "applies": true,
         "answer": false,
         "justification": "No leakage detection or prevention method is applied. No canary strings, membership inference, n-gram overlap analysis, or decontamination is performed."
       }
     }
   },
   "claims": [
     {
       "claim": "FVAPPS is the largest formal verification benchmark with 4,715 samples including 1,083 curated and quality-controlled samples.",
       "evidence": "Section II.C reports 4,715 successful samples (Unguarded), 2,089 Guarded, 1,083 Guarded and Plausible. Section IV.A compares to prior benchmarks: Clover and dafny-synthesis ~100 programs each, DafnyBench 782.",
       "supported": "strong"
     },
     {
       "claim": "Claude 3.5 Sonnet correctly proves 30% and Gemini 1.5 Pro correctly proves 18.5% of theorems on 101 randomly selected samples.",
       "evidence": "Section III.D: 'Of the 406 theorems attempted, Sonnet accomplished 121 (30%) and Gemini accomplished 74 (18.5%).' Table II provides breakdown by quality level.",
       "supported": "moderate"
     },
     {
       "claim": "Higher-quality (guarded and plausible) samples are somewhat more likely to be solvable by current models.",
       "evidence": "Table II shows proportions: Unguarded has 41/69 Sonnet successes (59%), Guarded 12/18 (67%), Guarded and Plausible 7/14 (50%). The paper states 'we roughly find that our higher-quality samples...are somewhat more likely to be solvable.'",
       "supported": "weak"
     },
     {
       "claim": "A full human baseline is not feasible for this benchmark due to the extreme difficulty of formal verification.",
       "evidence": "Section III.B: A human spent 10 hours on sample 0023, completed the function definition but no proofs, encountering stack overflow issues.",
       "supported": "weak"
     },
     {
       "claim": "Sonnet's reliance on imperative programming (Id.run do) creates a tension between functional solutions and proof-amenable structures.",
       "evidence": "Section III.E observes that 'Sonnet solved many problems via imperative programming with the identity monad (Id.run do)' and notes this 'fails to capture inductive structure that lends itself to proofs.'",
       "supported": "moderate"
     }
   ],
   "red_flags": [
     {
       "flag": "Generator-evaluator conflation",
       "detail": "Claude 3.5 Sonnet was used to generate all 4,715 benchmark samples and is then evaluated on the same benchmark. This creates potential bias: the benchmark may be systematically shaped by Sonnet's capabilities and failure modes."
     },
     {
       "flag": "No contamination analysis",
       "detail": "APPS problems are derived from CodeForces and LeetCode, which are extensively represented in LLM training corpora. The evaluated models (trained after 2021) may have memorized the underlying problems and solutions, but this contamination risk is completely unaddressed."
     },
     {
       "flag": "Single-run results with no uncertainty",
       "detail": "All baseline results come from single experimental runs with no error bars, confidence intervals, or repeated trials. LLM outputs are stochastic, so results could vary substantially across runs."
     },
     {
       "flag": "Tiny human baseline (n=1)",
       "detail": "The human baseline consists of a single unnamed person attempting a single problem. This is presented alongside model results as if it provides a meaningful comparison, but n=1 cannot support any conclusions about human performance."
     },
     {
       "flag": "Non-independent funder",
       "detail": "Anthropic provided API credits for benchmark generation, and Anthropic's Claude 3.5 Sonnet is one of two evaluated models, scoring highest. While the conflict is disclosed in acknowledgments, it is not highlighted as a potential bias."
     }
   ],
   "cited_papers": [
     {
       "title": "Measuring Coding Challenge Competence With APPS",
       "authors": ["Dan Hendrycks"],
       "year": 2021,
       "relevance": "Source dataset for FVAPPS; major benchmark for code generation evaluation."
     },
     {
       "title": "Evaluating large language models trained on code",
       "authors": ["Mark Chen"],
       "year": 2021,
       "arxiv_id": "2107.03374",
       "relevance": "Codex paper introducing HumanEval; foundational LLM code generation benchmark."
     },
     {
       "title": "Swe-bench: Can language models resolve real-world github issues?",
       "authors": ["Carlos E Jimenez"],
       "year": 2023,
       "arxiv_id": "2310.06770",
       "relevance": "Major benchmark for autonomous software engineering agents."
     },
     {
       "title": "LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code",
       "authors": ["Naman Jain"],
       "year": 2024,
       "relevance": "Contamination-free code evaluation benchmark addressing temporal leakage."
     },
     {
       "title": "DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search",
       "authors": ["Huajian Xin"],
       "year": 2024,
       "arxiv_id": "2408.08152",
       "relevance": "State-of-the-art model for formal theorem proving, attempted as baseline in this paper."
     },
     {
       "title": "DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data",
       "authors": ["Huajian Xin"],
       "year": 2024,
       "arxiv_id": "2405.14333",
       "relevance": "Formal theorem proving model using synthetic data for training."
     },
     {
       "title": "OpenHands: An Open Platform for AI Software Developers as Generalist Agents",
       "authors": ["Xingyao Wang"],
       "year": 2024,
       "arxiv_id": "2407.16741",
       "relevance": "Autonomous software engineering agent platform representative of the agentic coding trend."
     },
     {
       "title": "Code Llama: Open Foundation Models for Code",
       "authors": ["Baptiste Rozière"],
       "year": 2023,
       "relevance": "Open-source code generation foundation model relevant to LLM programming capabilities."
     },
     {
       "title": "Clover: Closed-loop verifiable code generation",
       "authors": ["Chuyue Sun"],
       "year": 2024,
       "relevance": "Directly comparable formal verification benchmark (~100 programs); FVAPPS is positioned as much larger."
     },
     {
       "title": "DafnyBench: A Benchmark for Formal Software Verification",
       "authors": ["Chloe Loughridge"],
       "year": 2024,
       "arxiv_id": "2406.08467",
       "relevance": "Formal software verification benchmark (782 programs in Dafny); direct comparison point for FVAPPS."
     },
     {
       "title": "AutoVerus: Automated Proof Generation for Rust Code",
       "authors": ["Chenyuan Yang"],
       "year": 2024,
       "arxiv_id": "2409.13082",
       "relevance": "Automated formal verification for Rust, bridging the gap between code generation and formal proofs."
     },
     {
       "title": "Program Synthesis with Large Language Models",
       "authors": ["Jacob Austin"],
       "year": 2021,
       "arxiv_id": "2108.07732",
       "relevance": "Early work on LLM-based program synthesis foundational to the code generation field."
     }
   ],
   "engagement_factors": {
     "practical_relevance": {
       "score": 1,
       "justification": "The benchmark is useful for formal verification researchers but not immediately applicable to typical software engineering practice."
     },
     "surprise_contrarian": {
       "score": 1,
       "justification": "The finding that LLMs struggle with formal proofs is expected; the paper confirms rather than challenges conventional wisdom."
     },
     "fear_safety": {
       "score": 1,
       "justification": "The introduction motivates the work with safety-critical applications (medical, military, autonomous vehicles) but the results themselves are about capability gaps rather than novel risks."
     },
     "drama_conflict": {
       "score": 0,
       "justification": "No controversy or conflict; straightforward benchmark introduction and baseline evaluation."
     },
     "demo_ability": {
       "score": 2,
       "justification": "Dataset is on HuggingFace and code on GitHub; researchers can download and try it immediately, though it requires Lean 4 expertise."
     },
     "brand_recognition": {
       "score": 1,
       "justification": "Evaluates Claude and Gemini (known models) but the paper is from a small independent foundation, not a major lab."
     }
   }
 }