The model is trained to generate candidate Sum-of-Squares (SOS) decompositions for unconstrained polynomial inequalities. In the NSPI pipeline, the model acts as a neural conjecturer: it proposes an approximate SOS structure that is subsequently checked and corrected by symbolic computation.

The intended workflow is:

Generate SOS-structure candidates with this model.
Refine numerical coefficients with Newton-style symbolic correction.
Recover exact rational SOS certificates.
Verify the recovered certificate exactly.
Generate Lean 4 proof code for machine-checkable formalization.

Please use this RL checkpoint together with the GitHub repository above rather than treating the raw model output as a final proof.

Important Limitation

This RL checkpoint is not a standalone formal prover. Its raw generations should be understood as approximate SOS structure conjectures. The generated decompositions may contain numerical errors, malformed terms, or invalid candidates.

Please use this checkpoint together with the full NSPI pipeline in the GitHub repository, including symbolic correction, rational recovery, exact verification, and Lean proof generation.

The GitHub repository also includes archived Lean proof files in lean_proof/ for successfully formalized benchmark instances.

Recommended Usage

After downloading the model, point the NSPI inference server to this checkpoint:

python python/server.py --model_name_or_path /path/to/this/checkpoint

Then run the verification and Lean-generation pipeline from the GitHub repository.

Citation

Paper: https://arxiv.org/abs/2605.15445

If you find this checkpoint or the NSPI project useful, please consider citing our paper.

bibtex

@misc{zuo2026nspi,
  title         = {{From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates}},
  author        = {Zuo, Ruobing and Zhao, Hanrui and He, Gaolei and Yang, Zhengfeng and Wang, Jianlin},
  year          = {2026},
  eprint        = {2605.15445},
  archivePrefix = {arXiv},
  primaryClass  = {cs.AI},
  doi           = {10.48550/arXiv.2605.15445},
  url           = {https://arxiv.org/abs/2605.15445}
}

NSPI RL SOS 结构猜想模型

本仓库包含随 ICML 2026 NSPI 项目发布的强化学习微调后（RL）的 SOS 结构猜想模型：

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

论文链接： https://arxiv.org/abs/2605.15445

项目代码、benchmark 文件、已生成的 Lean 证明产物，以及完整的推理、符号验证和 Lean 证明生成流程见：

GitHub： https://github.com/ruobingzuo66/NSPI

模型用途

该模型用于为无约束多项式不等式生成候选 Sum-of-Squares（SOS）分解。在 NSPI 流程中，它扮演的是神经网络猜想器的角色：模型先给出一个近似的 SOS 结构猜想，随后由符号计算模块进行检查和修正。

推荐使用流程如下：

使用该 RL 模型生成 SOS 结构候选。
通过 Newton-style symbolic correction 修正数值系数。
恢复精确的有理数 SOS certificate。
对恢复后的 certificate 做精确验证。
生成 Lean 4 证明代码，得到机器可检查的形式化证明。

请将该 RL checkpoint 与上面的 GitHub 项目代码配合使用，不要把模型的原始输出直接视为最终证明。

重要局限性

该 RL checkpoint 不是一个独立的形式化证明器。它的原始输出应该被理解为近似的 SOS 结构猜想，可能包含数值误差、格式错误或无效候选。

请将该 checkpoint 与 GitHub 仓库中的完整 NSPI pipeline 配合使用，包括符号修正、有理恢复、精确验证和 Lean 证明生成。

GitHub 仓库中也公开了成功形式化 benchmark 样例对应的 lean_proof/ 归档 Lean 证明文件。

引用

论文链接：https://arxiv.org/abs/2605.15445

如果该 checkpoint 或 NSPI 项目对你的工作有帮助，请考虑引用我们的论文。

bibtex

@misc{zuo2026nspi,
  title         = {{From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates}},
  author        = {Zuo, Ruobing and Zhao, Hanrui and He, Gaolei and Yang, Zhengfeng and Wang, Jianlin},
  year          = {2026},
  eprint        = {2605.15445},
  archivePrefix = {arXiv},
  primaryClass  = {cs.AI},
  doi           = {10.48550/arXiv.2605.15445},
  url           = {https://arxiv.org/abs/2605.15445}
}

ruobingzuo66/NSPI-SoS-Structure-Conjecturer-rl

NSPI RL SOS Structure Conjecturer

What This Model Does