4 papers · 1 filter
miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward
Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh
We perform a thorough analysis of the formal and informal statements in the miniF2F benchmark from the perspective of an AI system that is tasked to participate in a math Olympiad…
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh
Formal reasoning and automated theorem proving constitute a challenging subfield of machine learning, in which machines are tasked with proving mathematical theorems using formal l…
Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs
Roozbeh Yousefzadeh, Xuenan Cao
This position paper provides a critical but constructive discussion of current practices in benchmarking and evaluative practices in the field of formal reasoning and automated the…
Mathesis: Towards Formal Theorem Proving from Natural Languages
Yu Xuejun, Jianyuan Zhong, Zijin Feng +17
Recent advances in large language models show strong promise for formal reasoning. However, most LLM-based theorem provers have long been constrained by the need for expert-written…