SubgoalXL is an advanced model for formal theorem proving, leveraging subgoal-based expert learning to enhance LLMs' formal reasoning capabilities. It addresses the challenges of scarce theorem-proving data and multi-step reasoning by optimizing data efficiency and employing subgoal-level supervision. SubgoalXL iteratively refines formal statement, proof, and subgoal generators, allowing it to extract richer information from limited proofs and generate more precise formal proofs.

Below is an example code for using SubgoalXL with its custom prompt template for generating formal proofs:

This model is intended for automated theorem proving, especially in environments that require high levels of mathematical rigor, such as Isabelle. By employing subgoal-based proof generation and expert learning, SubgoalXL is optimized for solving complex reasoning tasks in formal mathematics.

SubgoalXL sets a new state-of-the-art benchmark in formal theorem proving within the Isabelle environment, achieving an accuracy of 56.1% on the miniF2F dataset, an absolute improvement of 4.9% over previous approaches. The model has successfully solved the following problems:

For more information on the model's design and performance, please refer to the paper SubgoalXL: Subgoal-Based Expert Learning for Theorem Proving.

While SubgoalXL excels in formal theorem proving, its usage is tailored to this specific domain and may not generalize well to other tasks beyond formal logic and proof generation.

If you use SubgoalXL in your research, please cite our paper:

@article{zhao2024subgoalxl,
      title = {SubgoalXL: Subgoal-based Expert Learning for Theorem Proving},
      author = {Zhao, Xueliang and Zheng, Lin and Bo, Haige and Hu, Changran and Thakker, Urmish and Kong, Lingpeng},
      journal={arXiv preprint arXiv:2408.11172},
      url={https://arxiv.org/abs/2408.11172}, 
      year = {2024},
}

For more information, please visit the project's GitHub repository or reach out via email at xlzhao22@connect.hku.hk.