Elamur Research⌕
☰
home / authors / Jianhao Shen

Jianhao Shen

Jianhao Shen has 5 papers in our library, in 2023–2024, most of them on Reasoning; often with Haiming Wang, Zhengying Liu, Chuanyang Zheng.

5 papers in our library · 2023–2024

OpenAlex · ORCID · h-index 10 · 41 works · 672 citations OpenAlex, 2026-10-14

📄 5 works in our library · 🔗 Cited 232 times in our library · 3 more in our library without a page yet · ⭐ Paper Stars ranking: #7108

The profile is the library's match of the name; two people with one name are not always told apart.

Elsewhere: Google Scholar · Semantic Scholar · dblp · ACL Anthology

 Affiliations

🎓Shenzhen Technology UniversityShenzhen · China2023–2026 · 7 paperscurrent🎓Peking UniversityBeijing · China2018–2024 · 15 papers🎓Shenzhen UniversityShenzhen · China2017–2021 · 8 papers🏢Huawei TechnologiesShenzhen · China2023–2025 · 3 papers

From the bylines of their papers (OpenAlex, 2026-10-14), ORCID and Wikidata; institutions on papers are matched by machine.

 Fields, topics and concepts

Of its works in our library, with the number of works on each.

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 5 worksArtificial Intelligence · 5 worksComputational Theory and Mathematics · 4 worksArts and Humanities · 3 worksLanguage and Linguistics · 3 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 4 works

 Works by year

2020s

20241 paper20234 papers

 Papers

The most cited first (OpenAlex and our library).

  1. FIMO: A Challenge Formal Dataset for Automated Theorem Proving (2023 · 53 citations)
    Neural provers built on large language models still rarely solve olympiad-grade problems. Formal data is scarce and costly to produce, existing benchmarks contain few truly hard items, and most formal datasets lack natural-language counterparts. The authors address this with FIMO, a Lean benchmark drawn from the IMO…
  2. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function (2023 · 40 citations)
    Neural theorem provers usually combine a language model that proposes the next tactic with a tree search that assembles a full proof.
  3. Process-Driven Autoformalization in Lean 4 (2024 · 33 citations)
    Translating natural-language mathematics into formal code (autoformalization) has mostly been studied for languages with large online corpora, such as Lean 3. The newer and fast-changing Lean 4 lacks suitable training and evaluation data. The authors address this with two contributions.
  4. Lyra: Orchestrating Dual Correction in Automated Theorem Proving (2023 · 24 citations)
    Lyra targets automated formal theorem proving in Isabelle with large language models. It builds on the Draft, Sketch, and Prove (DSP) pipeline, where an LLM turns an informal proof into a formal sketch and an automated prover fills the remaining gaps. The authors identify two weaknesses in this setup. First, LLMs…
  5. TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models (2023 · 21 citations)
    TRIGO is a benchmark for testing whether generative language models can perform formal proof reduction that depends on numerical manipulation, such as grouping and factoring terms or substituting equivalent angle values.

All works

8 works of theirs in our library, the most cited first; 5 with a page here, the others link their original until we summarise them.

  1. Generate & Rank: A Multi-task Framework for Math Word Problems ↗Findings of the Association for Computational Linguistics: EMNLP 2021 · no summary yetJianhao Shen et al.2021 · 152 citations
  2. FIMO: A Challenge Formal Dataset for Automated Theorem ProvingarXiv:2309.04295Chengwu Liu, Jianhao Shen, Huajian Xin, et al.2023 · 53 citations
  3. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value FunctionAnnual Meeting of the Association for Computational Linguistics (ACL)Haiming Wang, Ye Yuan, Zhengying Liu, et al.2023 · 40 citations
  4. Process-Driven Autoformalization in Lean 4arXiv:2406.01940Jianqiao Lu, Yingjia Wan, Zhengying Liu, et al.2024 · 33 citations
  5. Joint Language Semantic and Structure Embedding for Knowledge Graph Completion ↗Proceedings of the 29th International Conference on Computational Linguistics · no summary yetJianhao Shen et al.2022 · 29 citations
  6. Lyra: Orchestrating Dual Correction in Automated Theorem ProvingarXiv:2309.15806Chuanyang Zheng, Haiming Wang, Enze Xie, et al.2023 · 24 citations
  7. TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language ModelsConference on Empirical Methods in Natural Language Processing (EMNLP)Jing Xiong, Jianhao Shen, Ye Yuan, et al.2023 · 21 citations
  8. PALT: Parameter-Lite Transfer of Language Models for Knowledge Graph Completion ↗Findings of the Association for Computational Linguistics: EMNLP 2022 · no summary yetJianhao Shen et al.2022 · 4 citations

 Co-authors here

12 of 26 co-authors with a page, the most papers together first.

Venues

Where their works here were published, the most works first, with the editions of those that have a page.

 Cited by

Papers of our library cite their works 232 times (of the 149,439 papers whose bibliographies we read); 81 citing papers with a page here →.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/authors/jianhao-shen/