TINY STRATEGY PICKER FOR OLYMPIAD PROBLEMS WITH SYMBOLIC VERIFICATION AT SCALE

We propose a hybrid solver for Olympiad-style problems in Algebra, Number Theory, and Combinatorics that separates strategy selection from symbolic execution. The key insight is that the major difficulty in these problems lies in identifying the correct first move; once the right method is chosen, symbolic engines can reliably complete the proof.

Our system will feature a compact “strategy picker” (under 100 MB) that predicts an initial problem-solving recipe, then defers to symbolic tools for verification. The workflow includes three components:

(1) Dataset curation, collecting and annotating 1,000–3,000 Olympiad problems with lightweight labels specifying topic, method (e.g., substitution, invariant, modular arithmetic, recursion), and parameters such as candidate moduli or variable splits;

(2) Model training, using a small classifier or seq2seq model to predict a strategy recipe from problem text; and

(3) Verification, where symbolic solvers such as SymPy, modular arithmetic engines, and combinatorics search confirm the predicted solution through simplification, modular consistency, and counterexample screening.

Parallel execution on a compute cluster (Slurm/Ray) will explore multiple recipes and seeds simultaneously, caching successful paths and selecting the earliest verified proof. Performance will be evaluated by time-to-first-proof and fixed-time solve rates, with ablation studies over model size and parallelism.

Deliverables include an annotated dataset, strategy-prediction model weights, cluster execution scripts, a web demo generating concise LaTeX proofs or counterexamples, and a detailed report featuring an error taxonomy distinguishing incorrect methods, parameters, and verification failures.