Сможет ли ИИ решить физику?

Вы когда-нибудь смотрели на формулу и пытались понять, что там написано? Для меня, как для программиста, физическая формула - это полный набор антипаттернов.

• Односимвольные имена - есть.

• Юникод символы в названии переменных - есть.

• Отсутствие тестов - есть.

• Неявные типы (физические размерности) - есть.

Даже просто прочитать формулу про себя - непростая задача, так как я не всегда знаю, как произносится та или иная греческая закорючка.

Физические законы как Python код

Так появилась идея проекта Symplyphysics - описание физических законов на Python. Python выбран неспроста - в нём присутствует библиотека символьных вычислений SymPy. SymPy позволил мне решить проблему комбинаторного взрыва - например простая формула потребовала бы трёх функций:

• F(m, a)

• m(F, a)

• a(F, m)

Вместо этого SymPy позволяет записать отношение между физическими величинами одним равенством и  автоматически получать "перевернутые" отношения:

acceleration = symbols.acceleration
force = symbols.force
mass = symbols.mass

law = Eq(acceleration, force / mass)

(Пример закона из acceleration_is_force_over_mass.py)

Из этого равенства можно получить и функцию вычисления силы, причём с автоматической проверкой размерностей:

@validate_input(mass_=mass, acceleration_=acceleration)
@validate_output(force)
def calculate_force(mass_: Quantity, acceleration_: Quantity) -> Quantity:
    result_force_expr = solve(law, force, dict=True)[0][force]
    result_expr = result_force_expr.subs({mass: mass_, acceleration: acceleration_})
    return Quantity(result_expr)

(Создание конкретной функции для получения силы с автоматической валидацией размерности и автоматическим “переворачиванием” исходной формулы)

Теперь физик, студент или любой другой любитель физики может увидеть закон в понятном виде. Вместо таинственного F - объект "force", с явно заданной физической размерностью и коротким описанием. Вместо - валидируемое, тестируемое и исполняемое выражение.
Под валидацией я имею в виду автоматическую проверку входных и выходных размерностей. Под тестируемостью - покрытие тестами на основе реальных данных. Исполняемость означает, что в выражение можно подставить нужные параметры в любых удобных единицах измерения и получить ответ или построить график.

Так выглядит простой тест закона:

@fixture(name="test_args")
def test_args_fixture() -> Args:
    m = Quantity(1  units.kilogram)
    a = Quantity(3  units.meter / units.second**2)
    return Args(m=m, a=a)

def test_basic_force(test_args: Args) -> None:
    result = newton_second_law.calculate_force(test_args.m, test_args.a)
    assert_equal(result, 3 * units.newton)

(Тестируем закон на референсных значениях)

В проекте есть и графики. Например, цикл Карно. Да, он выглядит не так красиво, как нам показывали на лекциях.

От формул к доказательствам

Следующим логическим шагом стало добавление доказательств.

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

• Циклы проверяются системой импортов в Python. Если два закона ссылаются друг на друга, то проект не соберётся.

• SymPy берёт на себя большую часть работы при преобразованиях и математических операциях. Это не полностью доказанная корректность вывода, как в Lean, но в целом, SymPy можно верить.

• Все неявные допущения нужно прописывать явно. Оказывается, школьные доказательства были не совсем верными и работают только при определенных условиях.

Так мы добавляли всё больше законов и всё больше доказательств, пока не появился ИИ.

Первые опыты. Как ИИ пытается жульничать

Конечно, первым делом я попробовал дать задачу ChatGPT, чтобы он написал мне очередное доказательство. Казалось бы, задача очевидная: посмотреть как устроены уже готовые доказательства в проекте, найти известный вывод, переписать доказательство на имеющихся примитивах проекта.

Но ИИ в такой простой задаче облажался по полной:

• Вместо существующих базовых законов вставлял новые соотношения прямо в вывод формулы.

• Брал закон, который требовалось доказать, преобразовывал его туда и обратно (round-trip) и считал, что задача выполнена.

• Добавлял неоправданные предположения - например смена минуса на плюс без обоснования.

Поэтому я считал, что эта задача - камень преткновения для ИИ. Так было до тех пор, пока не появился Fable.

Fable. Первые удачные доказательства

Когда вышел Fable, то я закинул ему задачу на добавление доказательств просто на удачу. Написал что-то вроде: "Посмотри как сделаны доказательства в проекте. Найди 3 наилучших кандидата для добавления доказательства и напиши их".

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

Чтобы не быть голословным - оцените качество решения: https://github.com/blackyblack/symplyphysics/pull/1188

Агент добавил вывод сразу трёх критических параметров газа Ван-дер-Ваальса - давления, температуры и молярного объёма.

Например, для критического давления, он использует уже существующее уравнение состояния и два условия критической точки (стационарной точки перегиба изотермы):

Затем решает систему уравнений для критического молярного объёма и температуры и подставляет результат обратно, чтобы получить критическое давление.

_critical_point_solved = solve(
    (_inflection_point_eqn, flattangent_eqn),
    (critical_point.volume, waals_law.temperature),
    dict=True,
)[0]

criticalpressure_derived = isothermpressure.subs(_critical_point_solved)

assert expr_equals(_critical_pressure_derived, law.rhs)

(Фрагмент доказательства из critical_van_der_waals_pressure.py)

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

На момент этого эксперимента GPT-6 Astra ещё не вышла, но подозреваю, что Astra тоже достаточно "интеллектуальна", чтобы повторить это достижение.

Получилось ли у AI доказывать физику?

Не совсем.

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

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

В коде это специально поясняется комментарием, а заключительная проверка выглядит так:

assert expr_equals_abs(_voltage_derived, law.rhs)

(Пример из voltage_is_electric_field_times_distance.py)

И главное: мы пока не знаем, что будет делать агент, когда нужной формулы или вывода просто-напросто не окажется в доступных источниках.

Что дальше?

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

Сможет ли ИИ написать новое доказательство известного закона, которого нет в доступных источниках? Сможет ли ИИ написать новый закон, который потом можно будет проверить экспериментально?

Чтобы ответить на эти вопросы я планирую добавлять новые доказательства, сделать визуализацию графа законов и MCP сервер.

Если вам интересна формализация физики или опыт использования агентов для научных задач, буду рад обсудить это в комментариях.

Похожие проекты:

• Physics Derivation Graph с графом физических выводов

• Physlib с гораздо более строгой формализацией физики на Lean.