ruobingzuo66/NSPI-SoS-Structure-Conjecturer-rl
The ruobingzuo66/NSPI-SoS-Structure-Conjecturer-rl is an 8 billion parameter, RL-tuned model designed to generate candidate Sum-of-Squares (SOS) decompositions for unconstrained polynomial inequalities. Developed as part of the ICML 2026 NSPI project, this model acts as a neural conjecturer, proposing approximate SOS structures for automated polynomial inequality proving. It is specifically optimized to integrate into a larger pipeline for formalizing proofs in Lean 4, rather than functioning as a standalone prover.
Loading preview...
NSPI RL SOS Structure Conjecturer
This model, developed by ruobingzuo66 as part of the ICML 2026 NSPI project, is an RL-tuned SOS structure conjecturer with 8 billion parameters and a 32768 token context length. Its primary function is to generate candidate Sum-of-Squares (SOS) decompositions for unconstrained polynomial inequalities. It serves as a neural conjecturer within a broader pipeline, proposing approximate SOS structures that are subsequently refined and verified by symbolic computation.
Key Capabilities
- Generates approximate SOS structures: Provides initial conjectures for polynomial inequality proofs.
- Integrates with symbolic correction: Designed to work with Newton-style symbolic correction for refining numerical coefficients.
- Facilitates formalization: Part of a pipeline that recovers exact rational SOS certificates and generates Lean 4 proof code for machine-checkable formalization.
Important Limitation
This model is not a standalone formal prover. Its raw outputs are approximate conjectures and may contain numerical errors or malformed terms. It must be used in conjunction with the full NSPI pipeline, which includes symbolic correction, rational recovery, exact verification, and Lean proof generation, available at the NSPI GitHub repository.
Recommended Use Cases
- Automated polynomial inequality proving: Ideal for researchers and developers working on automated theorem proving, particularly for polynomial inequalities.
- Integration into formal verification systems: Suitable for systems that require initial conjectures for SOS decompositions to be formally verified.
- Research in AI-assisted formalization: Useful for exploring the synergy between large language models and symbolic computation in mathematical proof generation.