Теперь на Hugging Face доступна модель AutoVerifier от InternLM, созданная на архитектуре Qwen3_5Moe. Она получает задачу, необязательное эталонное решение и пошаговое доказательство-кандидат, а затем сообщает, верно ли доказательство, указывает на ошибки и отмечает индекс первого неверного шага. Модель состоит из 40 шардов в формате safetensors общим объёмом около 68 GiB и использует InternS1Tokenizer. Она предназначена для автоматической проверки задач из набора ProverBench, входящего в AdvancedMathBench, однако разработчик отмечает, что модель всё ещё может ошибаться.
Модель можно запускать, не загружая веса: достаточно сформировать запрос с помощью шаблона proof_verifier.md, а затем передать его токенизатору в формате чата.
Почему это важно
Модель позволяет исследователям быстро и автоматически оценивать сложные математические доказательства без ручной проверки.