Papers by Jianlin Wang
QDTSynth: Quality-Driven Formal Theorem Synthesis for Enhancing Proving Performance of LLMs (2025.acl-long)
Copied to clipboard
| Challenge: | Existing formal languages such as Lean, Coq and Metamath are proving to be useful in formal theorem proving . however, there is a scarcity of high-quality supervised fine-tuning data for formal proofs . |
| Approach: | They propose a Q**uality-**D**riven **T**heorem **S**ynthesis method in Lean4 . they propose diversity screening and the self-assessment method to select theoremas that exhibit diversity and high quality from the initial synthetic statements. |
| Outcome: | The proposed method significantly improves performance of open-source LLMs in theorem proving tasks. |
SAIR-Comb : A Structure-Aware Iterative Refinement Framework for Combinatorics Autoformalization (2026.acl-long)
Copied to clipboard
| Challenge: | Large language models (LLMs) have catalyzed advances in mathematical reasoning, propelling the development of automated theorem proving (ATP). |
| Approach: | They propose a Structure-Aware Iterative Refinement framework for Combinatorics powered by Lean 4 and LLMs. |
| Outcome: | The proposed framework achieves strong performance on the specialized CombiBench while remaining highly competitive on general-domain benchmarks. |
A Novel Cascade Binary Tagging Framework for Relational Triple Extraction (2020.acl-main)
Copied to clipboard
| Challenge: | Existing approaches to extract relational triples from unstructured text are inadequate to solve the overlapping triple problem. |
| Approach: | They propose a cascade binary tagging framework that models relations as functions that map subjects to objects in a sentence. |
| Outcome: | The proposed framework outperforms state-of-the-art methods on two datasets . it outperformed baseline methods by 17.5 and 30.2 absolute gains . |