{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,24]],"date-time":"2026-05-24T10:05:50Z","timestamp":1779617150461,"version":"3.53.1"},"publisher-location":"Singapore","reference-count":31,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819698837","type":"print"},{"value":"9789819698844","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-981-96-9884-4_16","type":"book-chapter","created":{"date-parts":[[2025,7,25]],"date-time":"2025-07-25T12:23:41Z","timestamp":1753446221000},"page":"188-200","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["FrameProver: Leveraging Formal Frameworks in Building Proofs for Enhanced Inference"],"prefix":"10.1007","author":[{"given":"Haojia","family":"Shan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Beibei","family":"Xiong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Niuniu","family":"Qi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhengfeng","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,26]]},"reference":[{"key":"16_CR1","first-page":"45","volume":"179","author":"T AlphaProof TAlphaGeometry","year":"2024","unstructured":"AlphaProof TAlphaGeometry, T.: AI achieves silver-medal standard solving international 178 mathematical olympiad problems. DeepMind blog. 179, 45 (2024)","journal-title":"DeepMind blog."},{"key":"16_CR2","unstructured":"Azerbayev, Z., et al.: Llemma: an open language model for mathematics. In: The Twelfth International Conference on Learning Representations (2023)"},{"key":"16_CR3","unstructured":"Azerbayev, Z. et al.: ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics http:\/\/arxiv.org\/abs\/2302.12433 (2023)"},{"key":"16_CR4","unstructured":"Coq, P.: The Coq Proof Assistant-reference Manual. INRIA Rocquencourt and ENS Lyon, version. 5 (1996)"},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Gu, Y., et al.: Pre-training to learn in context. In: Rogers, A. et al. (eds.) Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 4849\u20134870. Association for Computational Linguistics, Toronto, Canada (2023). https:\/\/doi.org\/10.18653\/v1\/2023.acl-long.267","DOI":"10.18653\/v1\/2023.acl-long.267"},{"key":"16_CR6","unstructured":"Hendrycks, D., et al.: Measuring Mathematical Problem Solving With the MATH Dataset. NeurIPS (2021)"},{"key":"16_CR7","unstructured":"Jiang, A.Q. et al.: Draft, sketch, and prove: guiding formal theorem provers with informal proofs. In: The Eleventh International Conference on Learning Representations (2023)"},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Kojima, T. et al.: Large Language Models are Zero-Shot Reasoners, http:\/\/arxiv.org\/abs\/2205.11916 (2023). https:\/\/doi.org\/10.48550\/arXiv.2205.11916","DOI":"10.48550\/arXiv.2205.11916"},{"key":"16_CR9","first-page":"26337","volume":"35","author":"G Lample","year":"2022","unstructured":"Lample, G., et al.: Hypertree proof search for neural theorem proving. Adv. Neural. Inf. Process. Syst. 35, 26337\u201326349 (2022)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"16_CR10","unstructured":"leanprover-community: repl (2024). https:\/\/github.com\/leanprover-community\/repl\/tree\/master"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Lin, H. et al.: Lean-STaR: Learning to Interleave Thinking and Proving (2024). http:\/\/arxiv.org\/abs\/2407.10040, https:\/\/doi.org\/10.48550\/arXiv.2407.10040","DOI":"10.48550\/arXiv.2407.10040"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Lin, Y. et al.: Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving (2025). http:\/\/arxiv.org\/abs\/2502.07640, https:\/\/doi.org\/10.48550\/arXiv.2502.07640","DOI":"10.48550\/arXiv.2502.07640"},{"key":"16_CR13","unstructured":"Liu, S. et al.: In-context vectors: making in context learning more effective and controllable through latent space steering. In: Proceedings of the 41st International Conference on Machine Learning. pp. 32287\u201332307 (2024)"},{"key":"16_CR14","unstructured":"Lu, J. et al.: FormalAlign: automated alignment evaluation for autoformalization. In: The Thirteenth International Conference on Learning Representations (2025)"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"de Moura, L. et al.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25, pp. 378\u2013388 Springer International Publishing, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Isabelle: A generic theorem prover. Springer (1994)","DOI":"10.1007\/BFb0030541"},{"key":"16_CR17","unstructured":"Polu, S. et al.: Formal mathematics statement curriculum learning. In: ICLR (2023)"},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"Polu, S., Sutskever, I.: Generative Language Modeling for Automated Theorem Proving (2020). http:\/\/arxiv.org\/abs\/2009.03393, https:\/\/doi.org\/10.48550\/arXiv.2009.03393","DOI":"10.48550\/arXiv.2009.03393"},{"key":"16_CR19","unstructured":"Shi, W. et al.: In-context pretraining: language modeling beyond document boundaries. In: The Twelfth International Conference on Learning Representations (2024)"},{"key":"16_CR20","unstructured":"Thakur, A. et al.: An In-Context Learning Agent for Formal Theorem-Proving (2024). http:\/\/arxiv.org\/abs\/2310.04353"},{"issue":"7995","key":"16_CR21","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1038\/s41586-023-06747-5","volume":"625","author":"TH Trinh","year":"2024","unstructured":"Trinh, T.H., et al.: Solving olympiad geometry without human demonstrations. Nature 625(7995), 476\u2013482 (2024). https:\/\/doi.org\/10.1038\/s41586-023-06747-5","journal-title":"Nature"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Wang, R., et al.: TheoremLlama: transforming general-purpose LLMs into Lean4 experts. In: Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pp. 11953\u201311974 (2024)","DOI":"10.18653\/v1\/2024.emnlp-main.667"},{"key":"16_CR23","first-page":"24824","volume":"35","author":"J Wei","year":"2022","unstructured":"Wei, J., et al.: Chain-of-thought prompting elicits reasoning in large language models. Adv. Neural. Inf. Process. Syst. 35, 24824\u201324837 (2022)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"16_CR24","first-page":"32353","volume":"35","author":"Y Wu","year":"2022","unstructured":"Wu, Y., et al.: Autoformalization with large language models. Adv. Neural. Inf. Process. Syst. 35, 32353\u201332368 (2022)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"Wu, Z. et al.: InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems (2024). http:\/\/arxiv.org\/abs\/2410.15700, https:\/\/doi.org\/10.48550\/arXiv.2410.15700","DOI":"10.48550\/arXiv.2410.15700"},{"key":"16_CR26","doi-asserted-by":"publisher","unstructured":"Xin, H. et al.: DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (2024). http:\/\/arxiv.org\/abs\/2408.08152, https:\/\/doi.org\/10.48550\/arXiv.2408.08152","DOI":"10.48550\/arXiv.2408.08152"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Yang, K. et al.: Formal Mathematical Reasoning: A New Frontier in AI (2024). http:\/\/arxiv.org\/abs\/2412.16075, https:\/\/doi.org\/10.48550\/arXiv.2412.16075","DOI":"10.48550\/arXiv.2412.16075"},{"key":"16_CR28","first-page":"21573","volume":"36","author":"K Yang","year":"2023","unstructured":"Yang, K., et al.: LeanDojo: theorem proving with retrieval-augmented language models. Adv. Neural. Inf. Process. Syst. 36, 21573\u201321612 (2023)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"16_CR29","unstructured":"Ying, H. et al.: Lean workbook: a large-scale lean problem set formalized from natural language math problems. In: The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track (2024)"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Zhang, Y. et al.: Active example selection for in-context learning. In: Goldberg, Y. et al. (eds.) Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, pp. 9134\u20139148. Association for Computational Linguistics, Abu Dhabi, United Arab Emirates (2022). https:\/\/doi.org\/10.18653\/v1\/2022.emnlp-main.622","DOI":"10.18653\/v1\/2022.emnlp-main.622"},{"key":"16_CR31","unstructured":"Zheng, K. et al.: MINIF2F: A Cross-system Benchmark for Formal Olympiad-level Mathematics (2022)"}],"container-title":["Lecture Notes in Computer Science","Advanced Intelligent Computing Technology and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-96-9884-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,24]],"date-time":"2026-05-24T09:46:17Z","timestamp":1779615977000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-96-9884-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9789819698837","9789819698844"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-981-96-9884-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"26 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICIC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ningbo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icic2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.ic-icc.cn\/icg\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}