MolLean заставляет LLM проверять химию: выигрыш в 12 из 12 задач

Химические рассуждения языковых моделей часто выглядят убедительно и при этом содержат выдуманные утверждения: модель уверенно описывает структуру, которой нет, или приписывает молекуле свойства, которых она не имеет. Авторы MolLean предлагают проверять такие утверждения программно. Они создали процессно-верифицируемый язык, в котором каждый шаг рассуждения привязан к явному состоянию молекулы и проходит через ядро на базе Lean. На 8 800 парных примерах из 12 задач с моделью Qwen3.6-27B режим уточнения всей трассы обошёл обычный chain-of-thought в каждой из задач.

Молекула как состояние, которое нельзя испортить

В обычном chain-of-thought модель пишет рассуждение текстом, и никто не проверяет, соответствует ли оно реальной молекуле. В MolLean рассуждение превращается в исполняемую трассу. Есть текущее молекулярное состояние, и каждый шаг меняет его по строгим правилам.

Ядро устроено слоями. Внизу лежат примитивные правки молекулярного графа, выше собираются составные преобразования. Поверх этого работают утверждения о молекулярных показателях. Если модель заявляет, что после правки у молекулы появилась определённая группа или изменился какой-то показатель, ядро сверяет заявление с состоянием, а не верит на слово.

Принято важное правило: отклонённое действие оставляет состояние нетронутым. Ошибочный шаг не загрязняет всё последующее рассуждение. Модель получает отказ и пробует другой ход с того же места.

Свидетели для внешних измерений

Не всё в химии можно вывести из структуры графа. Некоторые свойства приходят из внешних расчётов или измерений. Чтобы не смешивать надёжное с принятым на веру, авторы ввели протокол типизированных свидетелей. Он разделяет нативные структурные проверки, которые ядро выполняет само, и данные, поставляемые снаружи.

В результате в трассе видно, какие утверждения доказаны внутри системы, а какие опираются на внешний источник. Для аудита это существенная разница: рецензент или химик сразу видит, где проверка строгая, а где доверие делегировано.

Три режима и 8 800 примеров

Для работы с MolLean предусмотрены три режима:

• одноразовое исполнение трассы: модель пишет всё рассуждение, ядро его прогоняет;
• уточнение всей трассы: после проверки модель получает результат и переписывает рассуждение целиком;
• интерактивный режим через MolLean-MCP: модель действует шаг за шагом и получает обратную связь прямо во время генерации.

MolLean-MCP представляет собой stateful-интерфейс инструментов. Он раскрывает модели переходы между состояниями, результаты проверок и молекулярные показатели. Исходя из них модель решает, каким будет следующее действие.

Сравнение проводили с прямым chain-of-thought на 8 800 парных примерах. Они охватывают 12 задач: генерацию молекул, их редактирование, оптимизацию и реакции. Базовая модель — Qwen3.6-27B.

Ключные результаты:

• уточнение всей трассы лучше прямого chain-of-thought во всех 12 задачах;
• MolLean-MCP дополняет этот режим пошаговой обратной связью;
• в задачах на реакции интерактивный режим даёт лучший результат.

Последний пункт логичен. Реакция состоит из цепочки преобразований, где ранняя ошибка ломает всё остальное. Проверка после каждого шага ловит её сразу, а не на финальном разборе всей трассы.

Где это пригодится на практике

Модель на 27 миллиардов параметров здесь служит скорее демонстрацией: проверяющий слой не зависит от размера модели и может сопровождать другие LLM. Для команд, которые строят ассистентов по медицинской химии или планированию синтеза, подход подсказывает конкретную архитектуру. Модель должна не просто выдавать текст, а вызывать инструменты, которые хранят состояние и отвергают недопустимые шаги.

Для разработчиков агентов полезен сам паттерн. Транзакционное состояние с откатом отклонённых действий, формальное ядро проверки и разделение собственных проверок и внешних данных можно перенести в другие области, где у рассуждения есть формальный смысл. К ним относятся материаловедение, биология и проектирование схем.

Ограничения тоже понятны. Выигрыш измерен на одной модели и на заданном наборе из 12 задач. Проверка внешних измерений по-прежнему опирается на качество самих измерений. Но сдвиг в подходе заметен: химические утверждения модели из свободного текста превращаются в обязательства, которые можно проверить и пересмотреть.