arXiv cs.CLPaper
NL2AGBench: Benchmarking LLM Auto-Formalization for AlphaGeometry
The real bottleneck in neuro-symbolic geometry is usability, not reasoning. AlphaGeometry already reaches near-IMO performance but requires hand-coded problem statements, which defeats the purpose. This benchmark lets you measure whether an LLM can reliably convert English geometry into formal notation. If this gets solved, the entire pipeline for automated mathematical problem-solving starts to move.