AI 시대의 형식적 검증

For decades, research in formal verification has been guided by a simple mental model that I recently coined the formal verification triangle. The triangle captures a trade-off between three desirable properties: - Automation – the verification tool runs largely without human guidance - Scalability – the technique works on large real systems - Precision – the method can prove interesting properties, such as functional correctness Historically, verification techniques could reliably achieve two of the three, but not all three simultaneously. | Approach | Automatic | Scalable | Precise | |---|---|---|---| | Static analysis | ✓ | ✓ | ✗ | | Model checking | ✓ | ✗ | ✓ | | Interactive theorem proving | ✗ | ✓ | ✓ | Static analysis scales to millions of lines of code but sacrifices precision. Model checking provides precise answers but struggles with large systems. Interactive theorem proving can scale and remain precise — but only through substantial human effort. The triangle was never a theorem, but it described the practical limits of verification engineering remarkably well. Until now. What the Triangle Really Measured All verification tools automate some work. The real question has always been what kind of labour can be delegated to machines. Decision procedures — SAT solving, SMT solving, abstract interpretation — allowed machines to automate certain kinds of reasoning: - constraint solving - fixpoint computation - symbolic execution - bounded state exploration But other tasks stubbornly remained human: - inventing lemmas - structuring proofs - discovering complex invariants - reorganising proof developments - repairing proofs after changes Interactive theorem proving mechanised these forms of reasoning: proofs could be constructed and checked within a proof assistant, but the reasoning itself largely remained manual. The price was labour. The landmark verification of functional correctness for the ~9k line C implementation of the seL4 verified microkernel required roughly: - ~200k lines of Isabelle/HOL proofs - completed in ~20 person-years of work The triangle therefore reflected a constraint on which kinds of reasoning could realistically be automated. A Striking Comparison Recent progress in AI-assisted theorem proving and formalisation suggests that this constraint may be shifting. An AI system recently produced a formal proof of the Fields Medal-winning sphere-packing results in dimensions 8 and 24 consisting of roughly 200k lines of proof in about two weeks. While the similarity in proof size to the seL4 result is striking, the two efforts are hardly identical. The seL4 project required building a complete system model and proof architecture for a real operating system. Mathematical formalisation builds on extensive libraries and, in the case of the sphere packing result, a large body of human-written existing theory. But the comparison is still illuminating. For decades, verification engineers implicitly assumed that a proof development of that scale implied years of human effort. Very roughly speaking, during the seL4 project we would often talk about 10,000 lines of proof being about a year’s worth of effort. That assumption may no longer hold. Recent work suggests this may be true even when proofs are written for virtually unknown proof assistants building on highly obscure proof libraries. If the cost of producing and maintaining proofs drops by even an order of magnitude, the implications for verified systems are profound. As others have noted, verification could move from heroic one-off projects to something closer to routine engineering practice. Verification as Decomposition with Feedback What seems to make recent systems effective is not simply that AI can generate proofs. Instead, they combine two ideas that verification researchers already know well: decomposition and feedback loops. Large verification problems are not solved in one step. They are recursively decomposed into smaller subproblems. For example, compositional program logics decompose the problem of reasoning about a program into reasoning over each of its procedures, each of which is decomposed into reasoning over individual program commands, and so on, recursively. Mathematical proofs are decomposed into lemmas, each of which is decomposed into subgoals, which in turn can lead to proposing and proving additional lemmas, and so on, recursively. Within this hierarchy of decomposed subproblems, reasoning proceeds inside a verification feedback loop with two key ingredients beyond recursive decomposition: - A correctness oracle - Rich feedback that enables repair Interactive theorem provers naturally embody these ideas: decomposition through lemmas and proof subgoals, a trusted proof kernel that serves as a correctness oracle, and detailed proof state (unproved goals, missing assumptions, failed tactics) that provides rich feedback. This combination of hierarchical decomposition and oracle-guided feedback might explain why AI age