Learning to Disprove: Formal Counterexample Generation with Large Language Models
The research fine-tunes large language models to generate formal counterexamples for mathematical statements, moving beyond simple proof construction. The method uses a symbolic mutation strategy to create training data and a multi-reward framework to guide the model. This approach significantly improves the model's ability to find disproofs, enhancing its self-corrective reasoning capabilities.