Baiyu Huang

FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

Autoformalization—translating mathematical problems from natural language into formal proof assistant code—is essential for rigorous machine reasoning. However, existing evaluation frameworks provide only opaque binary verdicts or scalar scores, offering no interpretable insight into where or why tr…