Publications
Preprints
QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems
C. An, Q. Ye, M. Pan and J. Zhang. 2026.
[Show BibTex, Code, ICML 2026 AI4Math Workshop Spotlight, arXiv Version]@article{an2026qed, title={{QED}: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems}, author={An, Chenyang and Ye, Qihao and Pan, Minghao and Zhang, Jiayaun}, journal={arXiv preprint arXiv:2604.24021}, year={2026} }A Robust Model-Based Approach for Continuous-Time Policy Evaluation with Unknown Lévy Process Dynamics
Q. Ye, X. Tian and Y. Zhu. 2025.
[Show BibTex, arXiv Version]@article{ye2025robust, title={A Robust Model-Based Approach for Continuous-Time Policy Evaluation with Unknown {L\'evy} Process Dynamics}, author={Ye, Qihao and Tian, Xiaochuan and Zhu, Yuhua}, journal={arXiv preprint arXiv:2504.01482}, year={2025} }
Refereed Journal Papers
A Fast and Accurate Solver for the Fractional Fokker-Planck Equation with Dirac-Delta Initial Conditions
Q. Ye, X. Tian and D. Wang. 2026.
SIAM Journal on Scientific Computing
[Show BibTex, Code, Journal Version, arXiv Version]@article{ye2026fast, title={A Fast and Accurate Solver for the Fractional {F}okker--{P}lanck Equation with {D}irac-Delta Initial Conditions}, author={Ye, Qihao and Tian, Xiaochuan and Wang, Dong}, journal={SIAM Journal on Scientific Computing}, volume={48}, number={2}, pages={A1050--A1074}, year={2026}, publisher={SIAM} }Monotone Meshfree Methods for Linear Elliptic Equations in Non-Divergence Form via Nonlocal Relaxation
Q. Ye and X. Tian. 2023.
Journal of Scientific Computing
[Show BibTex, Code, Project Website, Journal Version, Correction, arXiv Version]@article{ye2023monotone, title={Monotone Meshfree Methods for Linear Elliptic Equations in Non-divergence Form via Nonlocal Relaxation}, author={Ye, Qihao and Tian, Xiaochuan}, journal={Journal of Scientific Computing}, volume={96}, number={3}, pages={85}, year={2023}, publisher={Springer} }
Accepted Conference Papers
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving
C. An, Z. Chen, Q. Ye, E. First, L. Peng, J. Zhang, Z. Wang, S. Lerner and J. Shang. 2024.
Association for Computational Linguistics 2024
[Show BibTex, Code, Dataset, Model Weights, ACL Version, arXiv Version]@inproceedings{an-etal-2024-learn, title = "Learn from Failure: Fine-tuning {LLM}s with Trial-and-Error Data for Intuitionistic Propositional Logic Proving", author = "An, Chenyang and Chen, Zhibo and Ye, Qihao and First, Emily and Peng, Letian and Zhang, Jiayun and Wang, Zihan and Lerner, Sorin and Shang, Jingbo", editor = "Ku, Lun-Wei and Martins, Andre and Srikumar, Vivek", booktitle = "Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)", month = aug, year = "2024", address = "Bangkok, Thailand", publisher = "Association for Computational Linguistics", url = "https://aclanthology.org/2024.acl-long.45", doi = "10.18653/v1/2024.acl-long.45", pages = "776--790", abstract = "Recent advances in Automated Theorem Proving have shown the effectiveness of leveraging a (large) language model that generates tactics (i.e. proof steps) to search through proof states. The current model, while trained solely on successful proof paths, faces a discrepancy at the inference stage, as it must sample and try various tactics at each proof state until finding success, unlike its training which does not incorporate learning from failed attempts. Intuitively, a tactic that leads to a failed search path would indicate that similar tactics should receive less attention during the following trials. In this paper, we demonstrate the benefit of training models that additionally learn from failed search paths. Facing the lack of such trial-and-error data in existing open-source theorem-proving datasets, we curate a dataset on intuitionistic propositional logic theorems and formalize it in Lean, such that we can reliably check the correctness of proofs. We compare our model trained on relatively short trial-and-error information (TrialMaster) with models trained only on the correct paths and discover that the former solves more unseen theorems with lower trial searches.", }