Robocikowo>ROBOCIKOWO
Wnioskowanie

Formalna weryfikacja dowodów

2013AktywnyAktualizacja: 19 sierpnia 2026Opublikowany
Maszynowe sprawdzanie poprawności dowodów matematycznych w asystentach dowodzenia (Lean, Coq, Isabelle) na podstawie ścisłych reguł logiki — wynik jest jednoznaczny: dowód przechodzi albo nie.
Kluczowa innowacja
Maszynowe, deterministyczne sprawdzanie poprawności dowodów przez asystenty dowodzenia — dając AI weryfikowalny, bezbłędny sygnał prawdy dla rozumowania matematycznego.
Kategoria
Wnioskowanie
Poziom abstrakcji
Wzorzec
Poziom operacji
InferencjaEwaluacja (runtime)
Zastosowania
Weryfikacja dowodów matematycznych (AI-for-math)Deterministyczny sygnał nagrody dla RL w rozumowaniuWeryfikacja poprawności oprogramowania i sprzętuBudowa zaufanych bibliotek twierdzeń (mathlib)Eliminacja halucynacji w dowodach generowanych przez AI

Jak działa

Dowód wyrażony w języku formalnym asystenta (np. taktyki Lean) jest redukowany do sekwencji zastosowań aksjomatów i reguł wnioskowania. Małe, zaufane jądro (kernel) sprawdza każdy krok; jeśli którykolwiek jest niepoprawny, cały dowód jest odrzucany. W pętli z AI: model generuje/uzupełnia dowód, weryfikator zwraca sukces lub błąd, a wynik służy jako sygnał do poprawy lub jako nagroda w treningu. Poprawność opiera się na zaufaniu do (bardzo małego) jądra oraz aksjomatów.

Rozwiązany problem

Rozumowanie LLM bywa przekonujące, lecz błędne (halucynacje). Formalna weryfikacja daje obiektywne, maszynowe kryterium poprawności dowodu, dostarczając AI wiarygodnego sygnału prawdy.

Kluczowe mechanizmy

Asystent dowodzenia / interaktywny theorem prover
Małe, zaufane jądro weryfikujące (kernel)
Sprawdzanie krok po kroku względem aksjomatów i reguł
Jednoznaczny wynik: dowód przechodzi albo nie
Sygnał prawdy do pętli generuj–weryfikuj i RL

Mocne strony i ograniczenia

Mocne strony
✓Deterministyczna, niepodważalna poprawność
✓Idealny sygnał prawdy/nagrody dla AI
✓Eliminuje halucynacje w dowodach
✓Zaufanie sprowadzone do małego jądra
Ograniczenia
✗Wymaga formalnego zapisu (kosztowna formalizacja/autoformalizacja)
✗Ograniczone pokrycie bibliotek i teorii
✗Weryfikacja długich dowodów bywa kosztowna
✗Zaufanie zależy od jądra i przyjętych aksjomatów

Komponenty

Jądro weryfikująceRdzeń zaufania

Małe, zaufane jądro sprawdzające każdy krok dowodu.

Język i taktyki dowoduZapis dowodu

Formalny zapis dowodu (np. taktyki Lean) redukowany do reguł.

Oficjalna

Biblioteka twierdzeńBaza wiedzy

Zbiór zweryfikowanych definicji i twierdzeń (np. mathlib).

Oficjalna

Implementacja

Implementacje referencyjne
Lean
Lean · Lean FRO
Oficjalna
Coq
Coq/OCaml · Inria
Oficjalna
Isabelle
Isabelle/ML · Isabelle
Oficjalna
Pułapki implementacyjne
Zależność od poprawności jądra i aksjomatówŚrednia

Weryfikacja jest tak wiarygodna, jak jądro i przyjęte aksjomaty.

Rozwiązanie:Minimalne, audytowane jądro; jawne aksjomaty.
Koszt weryfikacji długich dowodówŚrednia

Złożone dowody mogą być kosztowne obliczeniowo do sprawdzenia.

Rozwiązanie:Modularizacja, lematy pomocnicze, cache.

Ewolucja

1989
Coq

Powstaje jeden z kluczowych asystentów dowodzenia.

2013
Lean

Microsoft Research inicjuje Lean; później baza mathlib.

2024
AlphaProof — AI + formalna weryfikacja
Punkt przełomowy

Weryfikacja w Lean jako sygnał prawdy dla rozumowania AI (poziom medalowy IMO).

Hiperparametry (konfigurowalne osie)

Asystent dowodzeniaWysoka
LeanPopularny w AI-for-math.
Coq / Isabelle / HOLAlternatywne systemy.
Baza zaufaniaŚrednia
małe jądroIm mniejsze jądro, tym większe zaufanie.