ai-research-survey

scan.json (24882B)

---

 {
   "paper": {
     "title": "Automated Formalization via Conceptual Retrieval-Augmented LLMs",
     "authors": [
       "Wangyue Lu",
       "Lun Du",
       "Sirui Li",
       "Ke Weng",
       "Haozhe Sun",
       "Hengyu Liu",
       "Minghe Yu",
       "Tiancheng Zhang",
       "Ge Yu"
     ],
     "year": 2025,
     "venue": "arXiv preprint",
     "arxiv_id": "2508.06931"
   },
   "checklist": {
     "artifacts": {
       "code_released": {
         "applies": true,
         "answer": false,
         "justification": "No repository URL, GitHub link, or code archive is mentioned anywhere in the paper. The paper describes a framework (CRAMF) and a knowledge base but provides no link to access them."
       },
       "data_released": {
         "applies": true,
         "answer": false,
         "justification": "The paper uses public datasets miniF2F and ProofNet, but also introduces two new datasets (AdvancedMath with 173 problems and CombMath with 241 problems) without providing download links or release information for either."
       },
       "environment_specified": {
         "applies": true,
         "answer": false,
         "justification": "No requirements.txt, Dockerfile, conda environment, or detailed library version information is provided. The paper mentions specific models (MathBERT, bge-reranker-v2-m3, Faiss) but does not specify versions or environment setup details."
       },
       "reproduction_instructions": {
         "applies": true,
         "answer": false,
         "justification": "No step-by-step reproduction instructions, README, or scripts are provided. The method description covers the framework architecture but not how to run it."
       }
     },
     "statistical_methodology": {
       "confidence_intervals_or_error_bars": {
         "applies": true,
         "answer": false,
         "justification": "All results in Tables 1-6 are reported as single point estimates (e.g., '69.3%', '47.1%') with no confidence intervals, error bars, or uncertainty measures."
       },
       "significance_tests": {
         "applies": true,
         "answer": false,
         "justification": "The paper claims CRAMF 'significantly improves' and 'consistently improves' performance over baselines but provides no statistical significance tests (no p-values, no tests). All comparisons are based solely on comparing raw percentages."
       },
       "effect_sizes_reported": {
         "applies": true,
         "answer": true,
         "justification": "The paper reports relative gain (RG) percentages with baseline context throughout Tables 1 and 2 (e.g., 'from 36.9% to 47.1%, +27.6% relative improvement' for DeepSeek-V3 on MiniF2F). Both baseline and improved values are provided, allowing the reader to assess magnitude."
       },
       "sample_size_justified": {
         "applies": true,
         "answer": false,
         "justification": "The datasets have fixed sizes (miniF2F, ProofNet are standard benchmarks; AdvancedMath has 173 problems; CombMath has 241 problems) but no justification is given for why these sizes are sufficient for the claims made. No power analysis is discussed."
       },
       "variance_reported": {
         "applies": true,
         "answer": false,
         "justification": "No standard deviation, variance, or spread measures are reported. It is unclear whether results are from single runs or averaged over multiple runs. All tables show single point estimates only."
       }
     },
     "evaluation_design": {
       "baselines_included": {
         "applies": true,
         "answer": true,
         "justification": "The paper includes baselines for both autoformalization (DeepSeek-V3, GPT-4o, Herald-7B, Kimina-7B without CRAMF) and retrieval (BM25, Rewrite-Retrieve-Read, HyDE), shown in Tables 1-4."
       },
       "baselines_contemporary": {
         "applies": true,
         "answer": true,
         "justification": "Baselines include recent models: DeepSeek-V3 (2024), GPT-4o (2024), Herald-7B (2024), Kimina-7B (2025). Retrieval baselines include HyDE (2023) and R3 (2023). These are contemporary and relevant."
       },
       "ablation_study": {
         "applies": true,
         "answer": true,
         "justification": "Table 5 presents an ablation study removing individual CRAMF components (MCP, DCR, Rerank) and measuring the impact on FAR@10. Table 6 shows the effect of the rewriting mechanism on CombMath."
       },
       "multiple_metrics": {
         "applies": true,
         "answer": true,
         "justification": "The paper uses multiple evaluation metrics: Compilation Pass Rate@10 (CPR@10), Formalization Accuracy Rate@10 (FAR@10), Average Contribution Score (ACS), and HitRate@3."
       },
       "human_evaluation": {
         "applies": true,
         "answer": false,
         "justification": "All evaluation is automated. Formalization accuracy is judged by DeepSeek-V3 for semantic consistency and the Lean compiler for compilation. No human evaluation of output quality is conducted, despite the paper claiming semantic accuracy improvements where human judgment could add value."
       },
       "held_out_test_set": {
         "applies": true,
         "answer": false,
         "justification": "The paper does not discuss train/test splits or held-out sets for its knowledge base construction or retrieval pipeline. It is unclear whether any tuning decisions were made on the same data used for final evaluation."
       },
       "per_category_breakdown": {
         "applies": true,
         "answer": true,
         "justification": "Results are broken down per dataset (miniF2F, ProofNet, AdvancedMath) and per model (DeepSeek-V3, GPT-4o, Herald-7B, Kimina-7B) in Tables 1 and 2. Per-component breakdowns are in the ablation study (Table 5)."
       },
       "failure_cases_discussed": {
         "applies": true,
         "answer": true,
         "justification": "Figure 1 presents concrete failure cases illustrating model hallucination (undefined predicates) and semantic gap (conceptual polymorphism of 'neighborhood'). The introduction discusses specific failure modes in detail."
       },
       "negative_results_reported": {
         "applies": true,
         "answer": false,
         "justification": "Every experiment shows improvement with CRAMF. Even the ablation study only shows degradation when components are removed (which confirms positive contribution). No approaches that were tried and failed or configurations that did not work are reported."
       }
     },
     "claims_and_evidence": {
       "abstract_claims_supported": {
         "applies": true,
         "answer": true,
         "justification": "The abstract claims 'up to 62.1% and an average of 29.9% relative improvement.' Table 2 confirms the 62.1% figure (DeepSeek-V3 on AdvancedMath) and the overall average relative improvement across all model-dataset combinations is consistent with the 29.9% claim."
       },
       "causal_claims_justified": {
         "applies": true,
         "answer": true,
         "justification": "The paper makes causal claims about CRAMF components via ablation studies (Table 5, Table 6). The ablations systematically remove individual components (MCP, DCR, Rerank, ReWrite) and measure the effect, constituting controlled single-variable manipulation. The overall claim that CRAMF improves formalization is supported by the before/after comparison."
       },
       "generalization_bounded": {
         "applies": true,
         "answer": false,
         "justification": "The paper claims CRAMF 'effectively suppresses model hallucinations and semantic gaps' and demonstrates 'robustness and generalization capability' in the conclusion, but all experiments are on Lean 4 formalization only. The title says 'Automated Formalization' generally without bounding to Lean 4 or Mathlib specifically. The conclusion mentions extending to 'more complex mathematical domains' as future work but doesn't bound current claims."
       },
       "alternative_explanations_discussed": {
         "applies": true,
         "answer": false,
         "justification": "No alternative explanations for the improvements are discussed. For example, the improvement could partly stem from providing any additional context (not necessarily concept-level retrieval), or from the specific LLMs used for evaluation. No robustness checks or confound analysis is presented."
       }
     },
     "setup_transparency": {
       "model_versions_specified": {
         "applies": true,
         "answer": false,
         "justification": "The paper uses 'GPT-4o' and 'DeepSeek-V3' without specifying API versions or snapshot dates. 'Herald-7B' and 'Kimina-7B' are referenced by paper citation but no specific model checkpoints or versions are given. 'InternLM-Math-7B' and 'InternLM2-Math-Plus-7B' are used without version specifics. 'MathBERT' and 'bge-reranker-v2-m3' lack version details."
       },
       "prompts_provided": {
         "applies": true,
         "answer": false,
         "justification": "The paper states 'Details on prompt construction and examples are provided in the appendix' for concept extraction, and mentions prompts for ACS scoring are in the Appendix. However, the paper text available does not include the full appendix with actual prompt text. The main text describes prompts only in natural language ('we employ a query enhancement method. Using LLMs under strict prompting')."
       },
       "hyperparameters_reported": {
         "applies": true,
         "answer": false,
         "justification": "No temperature, top-p, max tokens, or other LLM API settings are reported. The paper mentions 'Top-10' and 'Top-5' and 'Top-3' for retrieval parameters but no inference hyperparameters for the LLMs."
       },
       "scaffolding_described": {
         "applies": true,
         "answer": true,
         "justification": "The CRAMF pipeline is described in detail in the Method section: knowledge base construction, concept extraction, query enhancement, dual-pathway hybrid retrieval with reranking, and integration with the autoformalizer. Figure 2 provides an overview diagram. The retrieval and reranking workflow is clearly laid out."
       },
       "data_preprocessing_documented": {
         "applies": true,
         "answer": true,
         "justification": "The knowledge base construction pipeline is documented: parsing Mathlib with doc-gen4, extracting definitions via def/class/structure, back-translation with InternLM-Math-7B, self-consistency validation, and concept extraction with DeepSeek-V3. The paper states it covers 'over 26,000 formal definitions and 1,000+ core mathematical concepts.'"
       }
     },
     "limitations_and_scope": {
       "limitations_section_present": {
         "applies": true,
         "answer": false,
         "justification": "There is no dedicated Limitations, Threats to Validity, or similar section. The conclusion briefly mentions future work ('extend to more complex mathematical domains') but does not discuss limitations of the current work."
       },
       "threats_to_validity_specific": {
         "applies": true,
         "answer": false,
         "justification": "No threats to validity are discussed anywhere in the paper. There is no consideration of potential biases in the evaluation methodology (e.g., using DeepSeek-V3 for both ACS scoring and as a baseline model)."
       },
       "scope_boundaries_stated": {
         "applies": true,
         "answer": false,
         "justification": "No explicit scope boundaries are stated. The paper does not clarify what the results do NOT show (e.g., no claim about proof generation, only formalization; limited to Lean 4; specific to Mathlib). The conclusion's mention of 'future work' is not the same as bounding current claims."
       }
     },
     "data_integrity": {
       "raw_data_available": {
         "applies": true,
         "answer": false,
         "justification": "No raw data, experimental logs, or per-example results are made available. Only aggregate results in tables are presented."
       },
       "data_collection_described": {
         "applies": true,
         "answer": true,
         "justification": "The knowledge base construction from Mathlib is described in detail. For the AdvancedMath dataset, the paper states it 'consists of 173 informalized proof problems in higher mathematics.' For CombMath, it is described as '241 combinatorics problems derived primarily from the textbook Combinatorics: The Art of Counting.' MiniF2F and ProofNet are cited standard benchmarks."
       },
       "recruitment_methods_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants are involved. The study uses automated benchmarks and datasets."
       },
       "data_pipeline_documented": {
         "applies": true,
         "answer": true,
         "justification": "The data pipeline from Mathlib parsing to knowledge base construction is documented step-by-step: doc-gen4 parsing, back-translation, self-consistency validation, concept extraction, vector encoding, and index construction. The evaluation pipeline (Lean compilation, back-translation, semantic consistency) is also described."
       }
     },
     "conflicts_of_interest": {
       "funding_disclosed": {
         "applies": true,
         "answer": false,
         "justification": "No funding information, acknowledgments, or grant numbers are mentioned anywhere in the paper."
       },
       "affiliations_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Author affiliations are clearly listed: Northeastern University, Ant Research Institute (Ant Group), and Aalborg University. The Ant Group affiliation is disclosed."
       },
       "funder_independent_of_outcome": {
         "applies": true,
         "answer": false,
         "justification": "No funding is disclosed, so independence cannot be assessed. One author is from Ant Group (Ant Research Institute), which has a potential interest in AI/LLM capabilities, but no funding relationship is disclosed."
       },
       "financial_interests_declared": {
         "applies": true,
         "answer": false,
         "justification": "No competing interests statement or financial disclosures are present in the paper."
       }
     },
     "contamination": {
       "training_cutoff_stated": {
         "applies": true,
         "answer": false,
         "justification": "The paper evaluates GPT-4o, DeepSeek-V3, Herald-7B, and Kimina-7B on miniF2F and ProofNet benchmarks but does not state any training data cutoff dates for these models."
       },
       "train_test_overlap_discussed": {
         "applies": true,
         "answer": false,
         "justification": "No discussion of whether the benchmark problems (miniF2F, ProofNet) may have appeared in the training data of the evaluated models. MiniF2F was published in 2021 and ProofNet in 2023, both potentially within training data of models released in 2024-2025."
       },
       "benchmark_contamination_addressed": {
         "applies": true,
         "answer": false,
         "justification": "MiniF2F (2021) and ProofNet (2023) are publicly available and could be in the training data of GPT-4o and DeepSeek-V3. The paper does not address this contamination risk at all. While CRAMF is compared as a relative improvement, the base model performance could be inflated by contamination."
       }
     },
     "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": "CRAMF involves multiple LLM calls (concept extraction, query enhancement, keyword generation) plus retrieval and reranking per problem, but no inference cost, latency, or token consumption is reported."
       },
       "compute_budget_stated": {
         "applies": true,
         "answer": false,
         "justification": "No computational budget, GPU hours, API costs, or hardware specifications are mentioned. Building the knowledge base from 26,000+ Mathlib definitions also involves significant compute that is not quantified."
       }
     }
   },
   "claims": [
     {
       "claim": "CRAMF achieves up to 62.1% and an average of 29.9% relative improvement in formalization accuracy across models and benchmarks.",
       "evidence": "Table 2 shows FAR@10 relative gains: DeepSeek-V3 achieves 62.1% on AdvancedMath. Average across all 12 model-dataset combinations is approximately 30%.",
       "supported": "moderate"
     },
     {
       "claim": "CRAMF significantly outperforms all retrieval baselines (BM25, R3, HyDE) in both ACS and HitRate@3.",
       "evidence": "Tables 3 and 4 show CRAMF achieves ACS of 1.93-2.14 vs. HyDE's 1.52-1.61, and HitRate@3 of 42.9-50.6% vs. HyDE's 30.7-35.5%.",
       "supported": "moderate"
     },
     {
       "claim": "Dual-channel retrieval is the most critical component, with its removal causing the largest performance degradation (average FAR drop of 15.7%).",
       "evidence": "Table 5 shows w/o DCR reduces FAR@10 from 63.1/55.1/51.4 to 48.5/36.8/37.1 across three datasets.",
       "supported": "moderate"
     },
     {
       "claim": "The problem rewriting mechanism improves FAR by 8.8% on combinatorics problems with implicit mathematical concepts.",
       "evidence": "Table 6 shows CRAMF achieves 63.1% vs. 54.3% without rewriting on CombMath.",
       "supported": "moderate"
     },
     {
       "claim": "CRAMF serves as a plug-and-play enhancement for LLM-based autoformalizers, consistently improving all tested models.",
       "evidence": "Tables 1 and 2 show improvements for all four models (DeepSeek-V3, GPT-4o, Herald-7B, Kimina-7B) on all three datasets, though gains for Kimina-7B are very small (0.4-8.5%).",
       "supported": "moderate"
     }
   ],
   "methodology_tags": [
     "benchmark-eval"
   ],
   "key_findings": "CRAMF is a retrieval-augmented framework that constructs a concept-definition knowledge base from Mathlib4 (26,000+ definitions, 1,000+ concepts) and uses dual-channel hybrid retrieval with reranking to provide contextual grounding for LLM-based mathematical autoformalization. Experiments on miniF2F, ProofNet, and AdvancedMath show consistent improvements in both compilation pass rate and formalization accuracy across four base models, with the largest gains for general-purpose models like DeepSeek-V3 (up to 62.1% relative improvement). Ablation studies confirm that dual-channel retrieval contributes the most, followed by reranking and concept parsing.",
   "red_flags": [
     {
       "flag": "No uncertainty quantification",
       "detail": "All results are single point estimates with no error bars, confidence intervals, standard deviations, or indication of multiple runs. It is unclear whether results are from single runs or averages, making it impossible to assess statistical reliability."
     },
     {
       "flag": "No significance testing",
       "detail": "The paper uses language like 'significantly outperforms' and 'significant improvement' without any statistical significance tests. All claims of superiority are based solely on comparing raw percentages."
     },
     {
       "flag": "Evaluator conflict of interest",
       "detail": "DeepSeek-V3 is used both as an evaluation judge (for semantic consistency assessment in FAR@10) and as one of the baseline models being evaluated. This creates a potential bias where the evaluator may favor its own outputs."
     },
     {
       "flag": "No limitations section",
       "detail": "The paper has no limitations, threats to validity, or discussion of potential weaknesses. This is a significant omission for a methods paper."
     },
     {
       "flag": "Benchmark contamination risk unaddressed",
       "detail": "MiniF2F (2021) and ProofNet (2023) are publicly available datasets that could appear in the training data of GPT-4o and DeepSeek-V3. The paper does not discuss this risk, though the relative comparison (with vs. without CRAMF) partially mitigates this concern for the improvement claims."
     },
     {
       "flag": "No cost analysis despite multi-step LLM pipeline",
       "detail": "CRAMF requires multiple LLM calls per problem (concept extraction, query enhancement, keyword generation, back-translation, semantic consistency checking) plus retrieval and reranking. No cost or latency analysis is provided, making practical applicability hard to assess."
     },
     {
       "flag": "New datasets not released",
       "detail": "AdvancedMath (173 problems) and CombMath (241 problems) are introduced but not released, limiting reproducibility and independent verification."
     }
   ],
   "cited_papers": [
     {
       "title": "Autoformalization with large language models",
       "authors": ["Yuhuai Wu", "Albert Qiaochu Jiang", "Wenda Li", "Markus Rabe", "Charles Staats", "Mateja Jamnik", "Christian Szegedy"],
       "year": 2022,
       "relevance": "Foundational work on using LLMs for autoformalization, directly relevant to LLM code generation capability evaluation."
     },
     {
       "title": "Retrieval-augmented generation for large language models: A survey",
       "authors": ["Yunfan Gao"],
       "year": 2023,
       "arxiv_id": "2312.10997",
       "relevance": "Comprehensive survey on RAG techniques that ground LLM outputs, relevant to understanding LLM scaffolding approaches."
     },
     {
       "title": "DeepSeek-V3 technical report",
       "authors": ["DeepSeek"],
       "year": 2024,
       "arxiv_id": "2412.19437",
       "relevance": "Technical report for a major open-source LLM used as both baseline and evaluator in this study."
     },
     {
       "title": "LeanDojo: Theorem proving with retrieval-augmented language models",
       "authors": ["Kaiyu Yang", "Aidan Swope", "Alex Gu"],
       "year": 2023,
       "relevance": "Retrieval-augmented approach to theorem proving using premise selection, relevant to LLM-based formal reasoning evaluation."
     },
     {
       "title": "Kimina-prover preview: Towards large formal reasoning models with reinforcement learning",
       "authors": ["Haiming Wang"],
       "year": 2025,
       "arxiv_id": "2504.11354",
       "relevance": "State-of-the-art formal reasoning model using RL, relevant to evaluating LLM capabilities in mathematical code generation."
     },
     {
       "title": "Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach",
       "authors": ["Qian Liu", "Xueliang Zheng"],
       "year": 2025,
       "relevance": "Proposes improved metrics and retrieval for autoformalization, directly relevant to evaluation methodology in LLM code generation."
     },
     {
       "title": "Advancing theorem proving in LLMs through large-scale synthetic data",
       "authors": ["Huajian Xin", "Daya Guo", "Zhihong Shao"],
       "year": 2024,
       "relevance": "Explores synthetic data for improving LLM theorem proving, relevant to LLM training methodology for code tasks."
     },
     {
       "title": "Lean workbook: A large-scale lean problem set formalized from natural language math problems",
       "authors": ["Huajian Ying"],
       "year": 2024,
       "relevance": "Large-scale benchmark for Lean formalization used as the evaluation pipeline in this study."
     },
     {
       "title": "Query rewriting in retrieval-augmented large language models",
       "authors": ["Xinbei Ma", "Yeyun Gong", "Pengcheng He"],
       "year": 2023,
       "relevance": "Query rewriting technique for RAG used as a retrieval baseline, relevant to LLM scaffolding methods."
     },
     {
       "title": "Precise zero-shot dense retrieval without relevance labels",
       "authors": ["Luyu Gao", "Xueguang Ma", "Jimmy Lin", "Jamie Callan"],
       "year": 2023,
       "relevance": "HyDE method used as a retrieval baseline, relevant to zero-shot retrieval approaches for LLM augmentation."
     }
   ]
 }