ai-research-survey

scan.json (28004B)

---

 {
   "paper": {
     "title": "miniCodeProps: a Minimal Benchmark for Proving Code Properties",
     "authors": ["Evan Lohn", "Sean Welleck"],
     "year": 2024,
     "venue": "arXiv.org",
     "arxiv_id": "2406.11915",
     "doi": "10.48550/arXiv.2406.11915"
   },
   "scan_version": 3,
   "active_modules": ["experimental_rigor", "data_leakage"],
   "methodology_tags": ["benchmark-eval"],
   "key_findings": "miniCodeProps is a 201-property benchmark in Lean 4 for evaluating neural theorem provers on code verification, sourced from Tons of Inductive Problems. GPT-4o (pass@32) proves 75.6% of easy properties but only 4.34% of medium+hard; a small specialized model (ntp-ctx-1.3B, 35.8% overall) matches or exceeds GPT-4o (34.8%). A many-to-one refinement technique yields modest gains (37.3% overall). The benchmark demonstrates that current LLM-based provers cannot handle even relatively simple code verification beyond basic induction.",
   "checklist": {
     "artifacts": {
       "code_released": {
         "applies": true,
         "answer": true,
         "justification": "Evaluation code released at https://github.com/cmu-l3/minicodeprops-eval, linked in footnote 1. The benchmark dataset is published on HuggingFace."
       },
       "data_released": {
         "applies": true,
         "answer": true,
         "justification": "The benchmark is published as a public dataset on HuggingFace (Section 3.3: 'We have published our benchmark as a public dataset on Huggingface'). Source is derived from the public TIP repository."
       },
       "environment_specified": {
         "applies": true,
         "answer": false,
         "justification": "No requirements.txt, Dockerfile, or detailed environment setup is provided in the paper. The paper mentions Lean 4 but does not specify library versions or dependencies needed to run the evaluation."
       },
       "reproduction_instructions": {
         "applies": true,
         "answer": false,
         "justification": "The paper states evaluation code is publicly available but does not provide step-by-step reproduction instructions. No commands, scripts, or detailed procedure for replicating the baseline experiments are given in the paper."
       }
     },
     "statistical_methodology": {
       "confidence_intervals_or_error_bars": {
         "applies": true,
         "answer": false,
         "justification": "Table 3 reports only point estimates (e.g., '75.6% (65/86)') with no confidence intervals or error bars."
       },
       "significance_tests": {
         "applies": true,
         "answer": false,
         "justification": "No statistical significance tests are reported. Claims like ntp-ctx showing 'comparable, or better, performance than GPT-4o' are based solely on comparing raw percentages without any formal test."
       },
       "effect_sizes_reported": {
         "applies": true,
         "answer": true,
         "justification": "Results in Table 3 report both percentages and raw counts (e.g., '75.6% (65/86)'), with baseline comparisons providing sufficient context to assess magnitude. The refinement improvement is reported as 77.9% vs 75.6% on easy and 6.96% vs 4.34% on medium+hard."
       },
       "sample_size_justified": {
         "applies": true,
         "answer": true,
         "justification": "Section 3: 'We specifically make miniCodeProps fairly small, since evaluating theorem proving models requires many calls to the language model... is hence time-consuming and prohibitively expensive for large datasets.' Section 5: 'it is unlikely that these high-level conclusions would change given more properties drawn from the same distribution, thereby justifying miniCodeProps' size of 201 properties.'"
       },
       "variance_reported": {
         "applies": true,
         "answer": false,
         "justification": "No variance, standard deviation, or spread measures are reported. Results appear to be from single experimental runs."
       }
     },
     "evaluation_design": {
       "baselines_included": {
         "applies": true,
         "answer": true,
         "justification": "Three baselines are compared: GPT-4o full proof generation (pass@32), GPT-4o with refinement, and ntp-ctx-1.3B tactic-by-tactic generation with best-first search (Table 3)."
       },
       "baselines_contemporary": {
         "applies": true,
         "answer": true,
         "justification": "GPT-4o was a highly performant general-purpose model at the time. ntp-ctx-1.3B is described as 'the only tactic generation model specifically trained to accept both the current proof state and an additional input context' at the time of experimentation (Section 4)."
       },
       "ablation_study": {
         "applies": true,
         "answer": false,
         "justification": "No systematic ablation study is performed. The comparison between GPT-4o base and +refinement shows the effect of refinement, but no ablation of benchmark design choices, prompt formatting, or context components is conducted."
       },
       "multiple_metrics": {
         "applies": true,
         "answer": false,
         "justification": "Only one metric is used: pass rate (percentage of specifications proven). No secondary metrics such as proof length, generation time, or partial progress measures are reported."
       },
       "human_evaluation": {
         "applies": false,
         "answer": false,
         "justification": "Human evaluation is irrelevant here — the Lean 4 kernel provides a definitive, formal verification of proof correctness."
       },
       "held_out_test_set": {
         "applies": true,
         "answer": false,
         "justification": "The refinement parameters (k=16, T=2) were selected via 'a small scale experiment' on an unspecified dataset, possibly the benchmark itself. No explicit dev/test split is described, and no held-out validation procedure is documented."
       },
       "per_category_breakdown": {
         "applies": true,
         "answer": true,
         "justification": "Table 3 breaks down results by Medley (Easy), Termination + Sorting (Medium + Hard), and Overall. Table 1 provides composition breakdown by subject matter (Numbers, Lists, Trees, Heaps) and difficulty level."
       },
       "failure_cases_discussed": {
         "applies": true,
         "answer": true,
         "justification": "Appendix A shows a detailed incorrect proof from GPT-4 for a sorting property, discussing specific failure modes including invalid induction strategies and placeholder arguments. Section 3.3 discusses what makes certain properties difficult."
       },
       "negative_results_reported": {
         "applies": true,
         "answer": true,
         "justification": "The core finding is negative: all methods fail on nearly all medium and hard properties (4.34%-8.69% on medium+hard). The paper is designed to demonstrate the limitations of current methods."
       }
     },
     "claims_and_evidence": {
       "abstract_claims_supported": {
         "applies": true,
         "answer": true,
         "justification": "The abstract claims are well-supported: state-of-the-art methods show promise on easy properties (72-78%) yet fail on medium and hard (4-9%). Table 3 directly supports these claims."
       },
       "causal_claims_justified": {
         "applies": true,
         "answer": true,
         "justification": "The paper's causal claims are modest. 'Changing the generation algorithm (namely, to refinement) leads to some additional successes' is supported by a controlled comparison (same model, same benchmark, added refinement). The comparison is adequate for this claim."
       },
       "generalization_bounded": {
         "applies": true,
         "answer": true,
         "justification": "Section 5 'Scope': 'performing well on this subset is only a proxy for the ability to perform well on all realistic code properties.' The title ('Minimal Benchmark') and throughout the paper, claims are bounded to the tested setting of simple Lean 4 properties."
       },
       "alternative_explanations_discussed": {
         "applies": true,
         "answer": false,
         "justification": "The paper does not substantively discuss alternative explanations for why methods fail on medium/hard properties. Possible confounds — such as proof length vs. conceptual difficulty, or the effect of Lean-specific syntax unfamiliarity — are not explored."
       },
       "proxy_outcome_distinction": {
         "applies": true,
         "answer": true,
         "justification": "The paper measures exactly what it claims: whether neural provers can generate correct formal proofs for code properties in Lean 4. No proxy gap exists — pass/fail on the Lean kernel directly measures the stated capability."
       }
     },
     "setup_transparency": {
       "model_versions_specified": {
         "applies": true,
         "answer": false,
         "justification": "The paper says 'GPT-4o' without a specific API version or snapshot date. ntp-ctx-1.3B is named specifically as a DeepSeek-Coder 1.3B fine-tune, but GPT-4o lacks version specificity per the schema criterion."
       },
       "prompts_provided": {
         "applies": true,
         "answer": false,
         "justification": "The paper describes what information is provided in prompts ('dependent code and the property being proven') but does not provide the actual prompt text or templates used for GPT-4o or ntp-ctx-1.3B. For refinement, the prompt is described in natural language ('learn from the failed attempts') without the actual text."
       },
       "hyperparameters_reported": {
         "applies": true,
         "answer": false,
         "justification": "GPT-4o uses 'default generation parameters' without specifying temperature, top-p, or max tokens. Refinement uses k=16, T=2. ntp-ctx references [37] for search settings. Key generation hyperparameters for GPT-4o are missing."
       },
       "scaffolding_described": {
         "applies": true,
         "answer": true,
         "justification": "Section 4 describes two proving modes: full-proof generation (sample 32 candidates, check with Lean kernel) and tactic-by-tactic best-first search. The refinement technique is described as a 'many-to-one' approach with k=16 samples over T=2 rounds. The workflow is clear enough to understand."
       },
       "data_preprocessing_documented": {
         "applies": true,
         "answer": true,
         "justification": "Section 3.1 describes the collection process: filtered TIP files to remove primarily mathematical induction, translated remaining Haskell to Lean 4, associated metadata. Section 3.2 describes the three categories and Table 1 provides the breakdown."
       }
     },
     "limitations_and_scope": {
       "limitations_section_present": {
         "applies": true,
         "answer": true,
         "justification": "Section 5 contains a 'Scope' subsection that substantively discusses limitations, including that the benchmark is only a proxy for realistic code properties and is sourced from a single dataset (TIP)."
       },
       "threats_to_validity_specific": {
         "applies": true,
         "answer": true,
         "justification": "The Scope subsection discusses threats specific to this study: the benchmark is sourced from TIP (may not represent all code properties), it tests self-contained problems rather than complex projects, and good performance is 'only a proxy for the ability to perform well on all realistic code properties.'"
       },
       "scope_boundaries_stated": {
         "applies": true,
         "answer": true,
         "justification": "The paper explicitly states it tests self-contained properties rather than complex verification projects, focuses on Lean 4 only, and draws from a single source (TIP). Section 1: 'Rather than evaluating on complex projects, our goal is to find a minimal set of meaningful program properties that breaks current LLM-based provers.'"
       }
     },
     "data_integrity": {
       "raw_data_available": {
         "applies": true,
         "answer": true,
         "justification": "The benchmark is publicly released on HuggingFace and GitHub, including all 201 property definitions, metadata, and evaluation code."
       },
       "data_collection_described": {
         "applies": true,
         "answer": true,
         "justification": "Section 3.1 describes the collection: properties sourced from TIP, translated from Haskell to Lean 4, filtered to focus on programming rather than mathematical induction, with metadata associated per Table 2."
       },
       "recruitment_methods_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants. Data source is the public TIP benchmark repository."
       },
       "data_pipeline_documented": {
         "applies": true,
         "answer": true,
         "justification": "Section 3.1-3.2 document the pipeline: TIP Haskell source → filter mathematical files → translate to Lean 4 → write termination lemmas → associate metadata → format as JSONL. Table 1 provides the composition breakdown (201 properties from 95 functions)."
       }
     },
     "conflicts_of_interest": {
       "funding_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Acknowledgements: 'Sean Welleck thanks Convergent Research, the Lean FRO, and the OpenAI Researcher Access Program for their support.'"
       },
       "affiliations_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Both authors are listed as Carnegie Mellon University. No affiliation with OpenAI or other companies whose products are evaluated."
       },
       "funder_independent_of_outcome": {
         "applies": true,
         "answer": false,
         "justification": "The OpenAI Researcher Access Program provided support, and GPT-4o (an OpenAI product) is one of the primary baselines evaluated. OpenAI has a financial interest in GPT-4o's perceived capabilities."
       },
       "financial_interests_declared": {
         "applies": true,
         "answer": false,
         "justification": "No competing interests or financial interests statement is present in the paper."
       }
     },
     "contamination": {
       "training_cutoff_stated": {
         "applies": true,
         "answer": false,
         "justification": "No training data cutoff date is stated for GPT-4o or for the DeepSeek-Coder base of ntp-ctx-1.3B."
       },
       "train_test_overlap_discussed": {
         "applies": true,
         "answer": false,
         "justification": "The benchmark is newly translated into Lean 4, providing some natural contamination protection, but this is not explicitly discussed. The underlying TIP problems (Haskell, 2015) could appear in model training data."
       },
       "benchmark_contamination_addressed": {
         "applies": true,
         "answer": false,
         "justification": "TIP was published in 2015, well before GPT-4o's training. While the Lean 4 translations are new, the logical structure and solutions are publicly available in Haskell. This contamination risk is not discussed."
       }
     },
     "human_studies": {
       "pre_registered": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "irb_or_ethics_approval": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "demographics_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "inclusion_exclusion_criteria": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "randomization_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "blinding_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "attrition_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       }
     },
     "cost_and_practicality": {
       "inference_cost_reported": {
         "applies": true,
         "answer": false,
         "justification": "No API costs, token counts, or wall-clock time reported despite extensive GPT-4o usage (32 candidates × 201 properties + refinement rounds)."
       },
       "compute_budget_stated": {
         "applies": true,
         "answer": false,
         "justification": "No total computational budget stated for GPT-4o API calls or ntp-ctx-1.3B inference."
       }
     },
     "experimental_rigor": {
       "seed_sensitivity_reported": {
         "applies": true,
         "answer": false,
         "justification": "Results appear to be from a single experimental run. No seed sensitivity analysis or results across multiple random seeds are reported."
       },
       "number_of_runs_stated": {
         "applies": true,
         "answer": true,
         "justification": "The number of generation attempts is clearly stated: pass@32 for GPT-4o (32 candidates), k=16 per round with T=2 rounds for refinement. ntp-ctx uses settings from [37]."
       },
       "hyperparameter_search_budget": {
         "applies": true,
         "answer": false,
         "justification": "GPT-4o uses 'default generation parameters' with no search. Refinement parameters (k=16, T=2) were selected via 'a small scale experiment' but no search budget or number of configurations tried is reported."
       },
       "best_config_selection_justified": {
         "applies": true,
         "answer": false,
         "justification": "The refinement configuration is justified only by 'In a small scale experiment we confirmed that this outperformed sampling 64 candidates without refinement.' No details of this experiment are provided, and it may have been conducted on the test set."
       },
       "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": "The authors created both the benchmark and the refinement baseline, and evaluate all methods themselves. No discussion of potential author-evaluation bias."
       },
       "compute_budget_vs_performance": {
         "applies": true,
         "answer": false,
         "justification": "GPT-4o pass@32, GPT-4o+refinement (32+32 additional), and ntp-ctx-1.3B best-first search use very different compute budgets. This is not discussed or controlled for."
       },
       "benchmark_construct_validity": {
         "applies": true,
         "answer": true,
         "justification": "Section 5 'Scope' explicitly discusses construct validity: 'performing well on this subset is only a proxy for the ability to perform well on all realistic code properties.' The paper justifies the benchmark design as testing 'minimum level of competency' (Section 3.2)."
       },
       "scaffold_confound_addressed": {
         "applies": true,
         "answer": false,
         "justification": "GPT-4o uses full proof generation while ntp-ctx-1.3B uses tactic-by-tactic best-first search — fundamentally different scaffolding. The paper notes ntp-ctx shows 'comparable, or better, performance' without controlling for the scaffold difference."
       }
     },
     "data_leakage": {
       "temporal_leakage_addressed": {
         "applies": true,
         "answer": false,
         "justification": "TIP was published in 2015 and the Haskell source code is publicly available. GPT-4o could have seen the original problems and solutions during training. This temporal leakage risk is not discussed."
       },
       "feature_leakage_addressed": {
         "applies": true,
         "answer": false,
         "justification": "The evaluation provides code dependencies as context, which is necessary for the task. However, whether the provided context could inadvertently leak proof strategies is not discussed."
       },
       "non_independence_addressed": {
         "applies": true,
         "answer": false,
         "justification": "All 201 properties are drawn from the same source (TIP) and share structural patterns (inductive proofs over lists, trees, natural numbers). Potential non-independence across benchmark items is not discussed."
       },
       "leakage_detection_method": {
         "applies": true,
         "answer": false,
         "justification": "No concrete leakage detection or prevention method is applied. The Lean 4 translation provides some natural protection but this is incidental, not a deliberate decontamination measure."
       }
     }
   },
   "claims": [
     {
       "claim": "miniCodeProps is sufficient to break current LLM-based provers, with state-of-the-art methods failing to prove nearly all medium and hard properties.",
       "evidence": "Table 3: GPT-4o proves 4.34% (5/115) of medium+hard properties; ntp-ctx-1.3B proves 8.69% (10/115). Even with refinement, GPT-4o only reaches 6.96% (8/115).",
       "supported": "strong"
     },
     {
       "claim": "Current neural theorem provers show nontrivial performance on easy (medley) properties, demonstrating some ability for basic inductive proofs in code verification.",
       "evidence": "Table 3: GPT-4o proves 75.6% (65/86) of easy properties; ntp-ctx-1.3B proves 72.1% (62/86); GPT-4o+refinement proves 77.9% (67/86).",
       "supported": "strong"
     },
     {
       "claim": "The small ntp-ctx-1.3B model trained on Mathlib shows comparable or better overall performance than GPT-4o.",
       "evidence": "Table 3: ntp-ctx-1.3B achieves 35.8% overall vs GPT-4o's 34.8%. On medium+hard, ntp-ctx achieves 8.69% vs GPT-4o's 4.34%.",
       "supported": "moderate"
     },
     {
       "claim": "Refinement (many-to-one technique) leads to additional successes on medium and hard properties.",
       "evidence": "Table 3: GPT-4o+refinement proves 8/115 medium+hard properties vs 5/115 without refinement (3 additional proofs).",
       "supported": "weak"
     }
   ],
   "red_flags": [
     {
       "flag": "No uncertainty quantification",
       "detail": "All results in Table 3 are single-run point estimates with no error bars, confidence intervals, or variance across runs. Pass@32 involves stochastic sampling, so results could vary across runs."
     },
     {
       "flag": "No cost reporting despite extensive API usage",
       "detail": "The evaluation requires 32 GPT-4o generations per property (201 properties) plus refinement rounds, yet no API costs or compute time are reported. This makes it difficult to assess practical reproducibility."
     },
     {
       "flag": "Possible test-set tuning for refinement parameters",
       "detail": "Refinement parameters (k=16, T=2) were selected via 'a small scale experiment' without specifying whether this was on a held-out set or the benchmark itself. If tuned on the test set, the refinement results are optimistically biased."
     },
     {
       "flag": "Contamination risk from public TIP source",
       "detail": "The benchmark is translated from TIP (2015 Haskell problems). While Lean 4 translations are new, the underlying logical problems and solutions are publicly available and may appear in GPT-4o's training data. This is not discussed."
     }
   ],
   "cited_papers": [
     {
       "title": "Clover: Closed-loop verifiable code generation",
       "authors": ["Chuyue Sun", "Ying Sheng", "Oded Padon", "Clark Barrett"],
       "year": 2024,
       "relevance": "LLM-based approach for automated code verification in Dafny, directly relevant to AI-driven formal verification."
     },
     {
       "title": "Evaluating large language models trained on code",
       "authors": ["Mark Chen", "Jerry Tworek"],
       "year": 2021,
       "relevance": "Foundational Codex/HumanEval paper for LLM code generation evaluation."
     },
     {
       "title": "Baldur: Whole-proof generation and repair with large language models",
       "authors": ["Emily First", "Markus N. Rabe", "Talia Ringer", "Yuriy Brun"],
       "year": 2023,
       "relevance": "LLM-based proof generation and repair for formal verification in Isabelle, closely related benchmark work."
     },
     {
       "title": "LeanDojo: Theorem proving with retrieval-augmented language models",
       "authors": ["Kaiyu Yang", "Aidan Swope", "Alex Gu"],
       "year": 2023,
       "relevance": "Retrieval-augmented theorem proving infrastructure for Lean, relevant to AI-assisted formal verification."
     },
     {
       "title": "An in-context learning agent for formal theorem-proving",
       "authors": ["Amitayush Thakur", "George Tsoukalas", "Yeming Wen", "Jimmy Xin", "Swarat Chaudhuri"],
       "year": 2024,
       "relevance": "COPRA agent for language-agnostic theorem proving, tested on code verification including CompCert."
     },
     {
       "title": "Generative language modeling for automated theorem proving",
       "authors": ["Stanislas Polu", "Ilya Sutskever"],
       "year": 2020,
       "relevance": "Foundational work on LLM-based automated theorem proving with best-first search."
     },
     {
       "title": "minictx: Neural theorem proving with (long-)contexts",
       "authors": ["Jiewen Hu", "Thomas Zhu", "Sean Welleck"],
       "year": 2024,
       "relevance": "Provides the ntp-ctx-1.3B model used as a baseline, context-aware tactic generation for theorem proving."
     },
     {
       "title": "Llemma: An open language model for mathematics",
       "authors": ["Zhangir Azerbayev", "Hailey Schoelkopf", "Keiran Paster"],
       "year": 2024,
       "relevance": "Open language model for mathematical reasoning used in theorem proving, relevant to AI capability benchmarking."
     },
     {
       "title": "Leveraging large language models for automated proof synthesis in Rust",
       "authors": ["Jianan Yao", "Ziqiao Zhou", "Weiteng Chen", "Weidong Cui"],
       "year": 2023,
       "relevance": "LLM-based proof automation for Verus/Rust verification, complementary approach to ITP-based verification."
     },
     {
       "title": "minif2f: a cross-system benchmark for formal olympiad-level mathematics",
       "authors": ["Kunhao Zheng", "Jesse Michael Han", "Stanislas Polu"],
       "year": 2022,
       "relevance": "Influential minimal benchmark for theorem proving that directly inspired miniCodeProps' design and naming."
     },
     {
       "title": "Draft, sketch, and prove: Guiding formal theorem provers with informal proofs",
       "authors": ["Albert Qiaochu Jiang", "Sean Welleck"],
       "year": 2023,
       "relevance": "Prompting strategy for theorem proving using informal proofs, relevant to AI-assisted formal verification."
     }
   ],
   "engagement_factors": {
     "practical_relevance": {
       "score": 1,
       "justification": "Primarily of interest to theorem proving researchers; not directly usable by practitioners for everyday code verification."
     },
     "surprise_contrarian": {
       "score": 1,
       "justification": "Confirms the expected finding that LLM provers struggle beyond simple cases, though the small-model-matching-GPT-4o result is mildly surprising."
     },
     "fear_safety": {
       "score": 0,
       "justification": "No AI safety or security concerns raised; the paper is about formal verification capabilities."
     },
     "drama_conflict": {
       "score": 0,
       "justification": "No controversy or conflict; straightforward benchmark contribution."
     },
     "demo_ability": {
       "score": 2,
       "justification": "Code and benchmark are publicly released on GitHub and HuggingFace, allowing researchers to run evaluations."
     },
     "brand_recognition": {
       "score": 1,
       "justification": "CMU authors have some recognition in the theorem proving community; GPT-4o is well-known but the paper itself is niche."
     }
   }
 }