Papers by Ruobing Zuo
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. |