На GitHub проект vampire logic деградирует

Не знаю что это за хрень, но

Напиши там issue

• «Ребят, прошлый релиз у меня работал в 15 раз быстрее»
• «Вот моё железо…»
• «Вот мой системный софт, его версии, ОС и библиотеки»
• «Вот на чём я проверял…»
• «Почините пожалуйста лютые тормоза!»

P.S. Я даже загуглить конкретный проект не смог с первой попытки, второй попытки не будет.

Подозреваю, что вот это: https://vprover.github.io/

А ещё golang деградирует

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

И я деградирую!

По силе это сильнее , чем персептроны - то что сейчас называют ии, только не говорит, не рисует и не пишет симфонии.

git bisect в руки – зная «хорошую» и «плохую» версию можно очень быстро найти, когда оно «сломалось».

ТС: хоть бы пример привёл чтоли? Файл (problem.p) такой-то. Запускаю так. В версии v4.X работало столько-то. В версии v4.Y работает столько-то.

Куда привести файл проблемы, строку вызова и некороткий результат ? Это все не очень малых размеров.

Я думаю намеренное конечно, чтобы никто воспользоваться не смог результатами. А выкладывают в открытый доступ, чтобы люди (конкуренты) тратили время на изучение их работы, а не делали свою. Таким образом сразу двух зайцев убивают - и свою работу популяризуют и возможных конкурентов водят за нос. На то они и математики,я думаю.

По силе это сильнее , чем персептроны - то что сейчас называют ии, только не говорит, не рисует и не пишет симфонии

А что же оно тогда делает?

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

а, просто любопытно, вы где то обучаетесь, чтобы это понимать всё или самостоятельно?

А ещё вопрос, для чего оно всё таки нужно, я не понял? Я понял что соблюдает логику, а персептрон не соблюдает (если верно), но что с этим можно делать? Оно не говорит, не рисует, не пишет симфонии.. но что то ж оно делает?

Могу предположить что это все задачи оптимизации и пляски вокруг них. Можно почитать про SAT и нормально-коньюктивную форму задания будевых выражений. Но это неточно.

ТС, йопрст, если такие штуки приносите то хорошо бы давать краткий ликбез че она делает и зачем на пальцах. Мне вот то что Вы пишете ни о чем не говорит вообще.

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

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

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

Как и с SQL ты должен сам найти применение этому инструменту, сама эта логика ломается от глупых вопрос и полна неразрешимых ситуаций, как и SQL.

https://www.marxists.org/reference/archive/hegel/help/mean05.htm

задачи оптимизации

Добавить бы слов, я когда вижу оптимизацию, для меня это стадия в gcc.

Можно почитать про SAT и нормально-коньюктивную форму задания булевых выражений.

Там довольно абстрактно, попробую проще: сейчас задачу на выполнимость (SAT) решает любой пакетный менеджер, ему нужно найти определенный набор пакетов, в котором все зависимости будут взаимно разрешены, и не будет конфликтов. Вот примерно таким же занимается и программа из ОП-поста, только там вместо пакетов значения переменных, и у переменных есть свои ограничения в стиле X >= 5, Y != Z.

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

Здесь очевидно (раз речь зашла про булеву логику) оптимизации целочисленные. И это немножко пересекается с задачами линейного программирования и всяким таким.

задачу на выполнимость (SAT) решает любой пакетный менеджер

Не уверен что там прям вот православный SAT под капотом, но если и да, то число неизвестных очень небольшое.

В ПМ конечно другая ситуация, и там серьезные SAT-решатели не используются обычно. Пример с ПМ что бы вообще понять что это и для чего, а мало ли переменных или много, это уже не так важно.

И MOPKOBKA

Это на самом деле про верификацию кода. Но мне же интересно что ТС думает... Но ТС что то пропал..

Ну там наверное пошире чем верификация кода. Как это к верификации кода прикручивать я кстати ХЗ, не приходилось.

это про верификацию кода. пойду даже погляжу.

AntonI, MOPKOBKA

прошу прощения, перепутал с проектом viper (https://www.pm.inf.ethz.ch/research/viper.html)

Это автоматизированный теорем прувер. Немного необычный, поскольку концентрируется на логике первого порядка и не является smt солвером при этом (в классическом смысле). Похоже, делает то что делают smt солверы + какие то возможности сверху (как например печать доказательства).

Беспредметный разговор. Надо найти конкретный коммит, который так сильно деградировал скорость и писать в их issues жалобу на него. Искать методом половинного деления не так долго.

А вообще (не совсем в тему, но скажу раз вспомнил) был в восторге, когда узнал, что для языка D существует инструмент, который автоматически выискивает минимальный код воспроизводящий проблему (используется в основном при разработке компилятора, но может быть использован и для других проблем, которые могут быть определены автоматически).

Куда Вам выслать данные по теме ? Это немного больше 10 мгб.

В смысле? Разве на github не все данные? Или вы прям пример использования хотите скинуть?

Вообще-то больше 30 мгб. А про все -

https://www.amazon.com/Handbook-Automated-Reasoning-Alan-Robinson/dp/0444508120/ref=mp_s_a_1_3?adgrpid=1227055333112002&dib=eyJ2IjoiMSJ9.KpN1K0jeaYKg55LVGxyT3siCgbhUKmCRxs93eZXKuVyGVmq-uikWH1DcQcXUjRO4C4k14kmdbtgW6YvS6XmklNCtoB6oD_Bg6K-GRhzBWrI.7rrexIs9I_bNcI_tQ1qTWASnsW33ECgf0xo02pShxos&dib_tag=se&hvadid=76691126859110&hvbmt=bp&hvdev=m&hvlocphy=97428&hvnetw=s&hvqmt=e&hvtargid=kwd-76691320052755%3Aloc-190&hydadcr=3781_13323616&keywords=handbook+of+automated+reasoning&mcid=0d530360444b32439ce3067205ceb786&msclkid=6216906698361207f19ef87b0f3b39c3&qid=1746769688&sr=8-3

1-й том

Вы бы хоть пояснили что это, что с ним делать и почему том только первый.

https://scinetwork.ru/disk/file/16398

Как учебник, есть порядок чтения.

По сравнению с версией за 2024 год его скорость упала не менее чем в 15 раз. Это какое-то намеренное деяние ?

Попробую показать подход системного архитектора к подобной проблеме. Сначала делаем лаки шот методом прищуренного глаза, если не получилось тогда уже метод «в лоб» - половинное деление пулл реквестов который описали выше. Я лишь покажу что такое лаки шот.

Я не знаю TPTP-язык, но знаю человеков. Обычно, подобные деградации скорости при таком уровне пишущих код вызваны переходом на что-то более удобное в разработке, те обычно это плата скоростью за удобство.

Давайте посмотрим что там написали за последний год с момента предыдущего релиза:

git log --after="2024-07-12T00:00:00-00:00" --pretty=oneline > log.txt

тысяча с хвостиком коммитов, оставим только пулл реквесты в мастер ветку:

^((?!Merge pull reques).)*$

Итого, у нас 80 пулл рекестов. Скорее всего проблема не в реквестах обозначеных как fix, remove или refactor. Можно подумать логически, почему так, а можно просто довериться моему опыту (напомню, это просто попытка сделать быстрый лаки шот, в лоб). Удаляем из списка все подобные коммиты:

.*(fix|refactor|remove).*

Осталось около 50 коммитов:

...
https://github.com/vprover/vampire/pull/615 c0f6adbe6b36427a08bb497a2d8814587f68bc5d from vprover/poly-arith
https://github.com/vprover/vampire/pull/616 442fb90e532fa2d90da60801e41d41ce4451dc24 from vprover/martin-intent
https://github.com/vprover/vampire/pull/618 e1f554a78fe62c3cd0219371dedb5f3c880378fc from kazarmy/conf-version-cpp-build-time
https://github.com/vprover/vampire/pull/625 be4bd4ffe8f04c40af7e545d8e3479bbc2458081 from vprover/assertion-additions
https://github.com/vprover/vampire/pull/626 29343cdbddc0e521c84df726e7d1913c2c384f6c from vprover/time-tracing-focus
https://github.com/vprover/vampire/pull/627 109d6ac676dd6e1fc546d2a1238c1cfc7d764e6d from vprover/lib-additions
https://github.com/vprover/vampire/pull/628 54179430e2b43d9eee34d69186fd005831f65181 from vprover/term-additions
https://github.com/vprover/vampire/pull/629 5dbcc507aa397f709f7dca4c2e2616b34913fee4 from vprover/test-additions
https://github.com/vprover/vampire/pull/630 24f1ae3a13bb8aa2087e6987056a44ab8fa98469 from vprover/tracer-output
https://github.com/vprover/vampire/pull/631 91f48b08bb8b905baf58038cea59b22c1a2d3426 from vprover/z3-export
https://github.com/vprover/vampire/pull/632 e10d9fe903c91abbc6cff3f00a5bbf36bc9ec29f from vprover/kbo-move-semantics
https://github.com/vprover/vampire/pull/634 bbc1d2b53f378b252d485f421b204ac8f8724779 from vprover/gmp
https://github.com/vprover/vampire/pull/636 a7afcb713b5e640491d31ec581542c69e4d72330 from vprover/make-drc-encompass-default
https://github.com/vprover/vampire/pull/637 1dc0e455a302c24fb8a8c97cf8f75f5801388d97 from vprover/term-ordering-diagrams
https://github.com/vprover/vampire/pull/638 1f3a30894cd187141965dce344e38387efc12cd0 from vprover/signature-optimization
https://github.com/vprover/vampire/pull/639 e54572424c49405c6b095cb10433e58197749f22 from vprover/gmp
https://github.com/vprover/vampire/pull/641 7012b0c6a09635579cec827c47c16389e6895ac2 from vprover/martin-peak-memory-usage
https://github.com/vprover/vampire/pull/649 b6962adf53860defeeb596ceaea1e023f9af72fa from vprover/alasca
https://github.com/vprover/vampire/pull/650 b7ce420ae6c6f242038d584412e1ad49f6feb853 from vprover/michael-clause-iter
https://github.com/vprover/vampire/pull/652 b65502697fe736bd62691ccfda9c41839e974f8e from vprover/michael-proof-extra
https://github.com/vprover/vampire/pull/655 df80da95c786e20c830d39cf76109e62a3d0cb39 from vprover/clause-tracing
https://github.com/vprover/vampire/pull/657 e0a91a05f5e6764552b9b6c8f615da447262c710 from vprover/ci-ubuntu-update
https://github.com/vprover/vampire/pull/658 c34da873c7380da1daf85de2654fcffe8df7e86b from vprover/qa-auto-for-geoff
https://github.com/vprover/vampire/pull/659 549ea42ee79bc6420ec73ef99ff35cf22c623d55 from vprover/qa-auto-for-geoff
https://github.com/vprover/vampire/pull/660 94cca4198dead750412361b37c1aed2070f21e51 from vprover/cadical
https://github.com/vprover/vampire/pull/663 3118af34d7168726b0476864b5d28b6cbc0d82f2 from vprover/tod-changes
https://github.com/vprover/vampire/pull/667 130a06ac3cb518481743d01e26e1ca5280be53dc from vprover/induction-with-free-var
https://github.com/vprover/vampire/pull/668 4a06ac4184cf335c0bda1d2eb5f6c9abbfdced66 from vprover/more-paranoid-ari-checks
https://github.com/vprover/vampire/pull/669 e3d32663de49184320c2dc252e548a9fa9d89bee from vprover/conditional-redundancy
https://github.com/vprover/vampire/pull/671 ac8725f55bf3961525c3de9473358e7d3b44ed69 from vprover/michael-tptp-line-numbers
...

Ковырять каждый мне лень, давайте отсортируем их и посмотрим методом прищуренного глаза на описание каждого реквеста. В глаза сразу бросается from vprover/gmp. GMP это библиотека для работы с большими числами которая использует mpz_t структуры. Это наиболее вероятный кандидат, давайте взглянем на него подробнее:

For that we ship with mini-gmp which can be compiled from source (see mini-gmp-6.3.0/). If a system-level installation of GMP is detected we link against that one instead of using mini-gmp as the full gmp library is much faster.

А насколько же mini-gmp медленнее GMP? Открываем поисковик, вбиваем mini-gmp performance, получаем The performance target for mini-gmp is to be at most 10 times slower than the real GMP library, for numbers of size up to a few hundred bits что вполне укладывается в ваши «в 15 раз медленнее».

Попробуйте установить в систему библиотеку GMP и проверить чтобы она была доступна в PATH, после чего пересоберите вампира. Скорее всего тормоза уйдут.

P.S.: Этот пост я оформлял дольше чем применял лаки шот метод…

Вы проделали большую работу ! Я выяснил, что последняя версия с нормальной скоростью 4.5.1 Giles Reger. После этого он не изменял Vampire. Далее скорость постоянно падала и сейчас он вообще не может доказать 1 из теорем вообще за время более суток. К сожалению я не могу заменять использование библиотек, это нужно менять настройки cmake и я тут пасс.

это нужно менять настройки cmake и я тут пасс.

Попробуйте просто установить GMP, а затем пересобрать вампира не меняя ничего в cmake. Сборка должна сама определить что в системе есть полноценная GMP библиотека и использовать ее вместо gmp-mini.

libgmp-dev 2:6.2.1+dfsg1-1.1 Уже установлена

Необходима версия 6.3.0

libtool: link: ranlib .libs/libgmp.a libtool: link: rm -fr .libs/libgmp.lax libtool: link: ( cd «.libs» && rm -f «libgmp.la» && ln -s «../libgmp.la» «libgmp.la» ) make[2]: Leaving directory ‘/home/al/gmp/gmp-6.3.0’ make[1]: Leaving directory ‘/home/al/gmp/gmp-6.3.0’

Все построилось без ошибок. Перезагрузил линукс. Ускорения не произошло, пытается доказать около часа, но это вряд ли будет. На версии 4.5.1 Giles Reger на это уходит 255 сек на 4х потоках процессоров.

Похоже, что они убрали возможность подтягивать системную библиотеку в релизе 4.9. Точно подтягивается вот в этой версии: https://github.com/vprover/vampire/releases/tag/mtpa-gnn-cade2025

Она как раз перед Vampire 4.9. Проверьте чтобы при сборке было сообщение «Found system level gmp version …».

При сборке не было сообщения «Found system level gmp version» или «gmp version» .

Это странно, потому что CMakeLists.txt в этой версии содержит строки (стр 835):

################################################################
# gmp stuff
################################################################

find_package(GMP)
if (GMP_FOUND)
  message(STATUS "Found system level gmp version ${GMP_C_LIBRARIES}.")
  add_compile_definitions(VMINI_GMP=0)
  include_directories(${GMP_INCLUDE_DIRS})
  link_libraries(${GMP_LIBRARIES})
else()
  message(STATUS "Compiling mini-gmp from source. If you want faster arithmetic install gmp on your system.")
  add_compile_definitions(VMINI_GMP=1)
  include_directories(${CMAKE_CURRENT_SOURCE_DIR}/mini-gmp-6.3.0)
endif()

Те он должен сообщить либо Found system level gmp version ... либо Compiling mini-gmp from source. If you want faster arithmetic install gmp on your system..

it clone https://github.com/vprover/vampire.git cd vampire git submodule update –init –recursive mkdir ../vampire-build && cd ../vampire-build cmake ../vampire && cmake –build .

При выполнеии этих команд на экране монитора таких строк не было.

Вы пытаетесь собрать мастер ветку 4.9. В версии 4.9 MichaelRawson тупо выпилил поддержу системного GMP оставив безусловное подключение mini-gmp-6.3.0.

Вам нужно скачать исходники которые я указал выше. Продублирую тут: https://github.com/vprover/vampire/releases/tag/mtpa-gnn-cade2025

Скачиваете Source code (zip) или (tar.gz), распаковываете и собираете как обычно. В этой версии появится одна из дух строк.

– Found GMP: /usr/lib/x86_64-linux-gnu/libgmp.so
– Found system level gmp version /usr/lib/x86_64-linux-gnu/libgmp.so. CMake Error at CMakeLists.txt:852 (find_package): By not providing «FindTorch.cmake» in CMAKE_MODULE_PATH this project has asked CMake to find a package configuration file provided by «Torch», but CMake did not find one.

Could not find a package configuration file provided by «Torch» with any of the following names:

TorchConfig.cmake
torch-config.cmake

Add the installation prefix of «Torch» to CMAKE_PREFIX_PATH or set «Torch_DIR» to a directory containing one of the above files. If «Torch» provides a separate development package or SDK, be sure it has been installed.

– Configuring incomplete, errors occurred!

И давно?

Found system level gmp version /usr/lib/x86_64-linux-gnu/libgmp.so <- это то что нужно.

Ошибки дальше относятся к Pytorch. Похоже, что он у вас не установлен, а сборка требует его:

################################################################
# pytorch stuff
################################################################

find_package(Torch REQUIRED)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${TORCH_CXX_FLAGS}")
link_libraries("${TORCH_LIBRARIES}")

Доставьте pytorch в систему и попробуйте собрать.

Не помню :)

usr/include/torch/csrc/jit/ir/ir.h:938:19: error: ‘dynamic_cast’ not permitted with ‘-fno-rtti’ 938 | auto* child = dynamic_cast<T*>(it->get());

-fno-rtti? Вы там на Arduino собираете что ли? :)

Откройте файл CMakeLists.txt в корне каталога. Найдите строку 26:

add_compile_options(-fno-rtti)

закомментируйте ее

#add_compile_options(-fno-rtti)

сохраните файл и соберите проект заново.

In file included from /home/al/logic/cade2025zip/vampire/Saturation/NeuralPassiveClauseContainers.cpp:42: /home/al/logic/cade2025zip/vampire/Saturation/NeuralPassiveClauseContainers.hpp:85:8: error: ‘optional’ in namespace ‘std’ does not name a template type 85 | std::optionaltorch::jit::Method _evalClauses;

В файле /home/al/logic/cade2025zip/vampire/Saturation/NeuralPassiveClauseContainers.hpp добавьте после строки 18:

#include "Lib/Random.hpp"

вот такую строку

#include <optional>

и попробуйте собрать.

Если не получится, тогда метод 2.

Замените #include <optional> на:

#include <experimental/optional>

и ниже в этом файле в строках 85-86 замените:

  std::optional<torch::jit::Method> _evalClauses;
  std::optional<torch::jit::Method> _journal;

на

  std::experimental::optional<torch::jit::Method> _evalClauses;
  std::experimental::optional<torch::jit::Method> _journal; 

после чего попробуйте собрать.

метод 1

gmake[2]: *** [CMakeFiles/obj.dir/build.make:2218: CMakeFiles/obj.dir/Saturation/NeuralPassiveClauseContainers.cpp.o] Error 1 gmake[1]: *** [CMakeFiles/Makefile2:86: CMakeFiles/obj.dir/all] Error 2 gmake: *** [Makefile:91: all] Error 2

метод 2

gmake[2]: *** [CMakeFiles/obj.dir/build.make:2218: CMakeFiles/obj.dir/Saturation/NeuralPassiveClauseContainers.cpp.o] Error 1 gmake[1]: *** [CMakeFiles/Makefile2:86: CMakeFiles/obj.dir/all] Error 2 gmake: *** [Makefile:91: all] Error 2

в обоиих методах были warning: и note:

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

Обратил внимание что под капотом во всю используется Z3 Prover от MS. Не пробовали его? А то может вы зря мучаетесь с vampire? Он собирается без проблем, как по скорости не знаю - сравнить не с чем.

z3 - очень слабый логический прувер, его используют для получения приемлемых результатов при использовании арифметических выражений в экономике и др областях, где нужно получить приемkемый рнезультат. vampire с некоторого времени расширили для этих целей. Это все логика 2го порядка, где можно искать результат, грубо говоря. как угодно с таким же результатом. В логике 1-го порядка даже рядом с vampire нет никого.