1 citations · 1 across the 16 of their papers we have counts for
17 papers
Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs
Ning Zhang, Nongyu Di, Zenan Li +2
As AI-generated code proliferates, formal verification, particularly through interactive theorem provers such as Rocq and Isabelle, becomes increasingly important for ensuring soft…
Beyond Fail-to-Pass: Iterative Hardening of Co-Generated Bug Reproduction Tests and Fixes
Yuhao Tan, Zhibang Yang, Fangkai Yang +9
Large language models (LLMs) have made automated program repair (APR) increasingly practical for real-world bugs, but repairing directly from bug reports remains underconstrained.…
Full Attention Strikes Back: Transferring Full Attention into Sparse within Hundred Training Steps
Yanke Zhou, Yiduo Li, Hanlin Tang +6
Long-context inference in large language models is bottlenecked by the quadratic cost of full attention. Existing efficient alternatives often rely either on native sparse training…
Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models
Weining Cao, Guangyuan Wu, Yuan Yao +3
Distributed protocols are notoriously difficult to verify correctly. Proving safety typically requires inductive invariants that both imply the desired property and are preserved b…
Task Abstention for Large Language Models in Code Generation
Yanke Zhou, Yuhao Tan, Senrong Xu +4
Large language models (LLMs) have revolutionized automated code generation. One serious concern, however, is the so-called ``hallucination'', i.e., LLMs may generate seemingly plau…
Uncertainty Quantification for LLM-based Code Generation
Senrong Xu, Yuhao Tan, Yanke Zhou +6
Prediction sets provide a theoretically grounded framework for quantifying uncertainty in machine learning models. Adapting them to structured generation tasks, in particular, larg…
Fair Conformal Classification via Learning Representation-Based Groups
Senrong Xu, Yanke Zhou, Yuhao Tan +5
Conformal prediction methods provide statistically rigorous marginal coverage guarantees for machine learning models, but such guarantees fail to account for algorithmic biases, th…
Learning to Disprove: Formal Counterexample Generation with Large Language Models
Zenan Li, Zhaoyu Li, Kaiyu Yang +2
Mathematical reasoning demands two critical, complementary skills: constructing rigorous proofs for true statements and discovering counterexamples that disprove false ones. Howeve…
Neuro-Symbolic Proof Generation for Scaling Systems Software Verification
Baoding He, Zenan Li, Wei Sun +4
Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual a…
Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
Nongyu Di, Tianyu Chen, Shan Lu +6
Large Language Models (LLMs) are widely used for code generation. However, the correctness of code generated by LLMs remains a concern. A potential remedy to this concern is to hav…
Conformal Correction for Efficiency May be at Odds with Entropy
Senrong Xu, Tianyu Wang, Zenan Li +4
Conformal prediction (CP) provides a comprehensive framework to produce statistically rigorous uncertainty sets for black-box machine learning models. To further improve the effici…
A Theoretical Study on Bridging Internal Probability and Self-Consistency for LLM Reasoning
Zhi Zhou, Yuhao Tan, Zenan Li +4
Test-time scaling seeks to improve the reasoning performance of large language models (LLMs) by adding computational resources. A prevalent approach within the field is sampling-ba…
FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory
Xiao-Wen Yang, Zihao Zhang, Jianuo Cao +7
Large language models (LLMs) have recently demonstrated remarkable progress in formal theorem proving. Yet their ability to serve as practical assistants for mathematicians, fillin…
Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
Zenan Li, Zhaoyu Li, Wen Tang +6
Large language models (LLMs) can prove mathematical theorems formally by generating proof steps (\textit{a.k.a.} tactics) within a proof system. However, the space of possible tact…
Bridging Internal Probability and Self-Consistency for Effective and Efficient LLM Reasoning
Zhi Zhou, Tan Yuhao, Zenan Li +4
Recent advancements in large language models (LLMs) have demonstrated remarkable reasoning capabilities. However, single-shot inference often yields unreliable results for complex…
Neuro-Symbolic Data Generation for Math Reasoning
Zenan Li, Zhi Zhou, Yuan Yao +5
A critical question about Large Language Models (LLMs) is whether their apparent deficiency in mathematical reasoning is inherent, or merely a result of insufficient exposure to hi…
Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency
Zenan Li, Yifan Wu, Zhaoyu Li +4
Autoformalization, the task of automatically translating natural language descriptions into a formal language, poses a significant challenge across various domains, especially in m…