10 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…
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 Bid with Unknown Private Values in Budget-Constrained First-Price Auctions
Zihao Hu, Yuxiao Wen, Yuan Yao +2
We study the operational problem of automated bidding in repeated first-price auctions under budget and return-on-spend (RoS) constraints. In this setting, an auto-bidder must tran…
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…
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…